Failed to infer structural recursion: .brecOn mismatch

Stream: new members

[aron]

I get this error on the below code:

failed to infer structural recursion:
Cannot use parameter uh:
  application type mismatch
    @IsValidUniVarKey.brecOn ↑uniVarsMap fun uv uh => (nextTypeVar : TypeVar) → funType uv nextTypeVar uh
  argument
    fun uv uh => (nextTypeVar : TypeVar) → funType uv nextTypeVar uh
  has type
    (uv : UniVar) → IsValidUniVarKey (↑uniVarsMap) uv → Type : Type 1
  but is expected to have type
    (a : UniVar) → IsValidUniVarKey (↑uniVarsMap) a → Prop : Type

I don't really understand this error. Is it saying that my inductive type is a Type instead of a Prop? Or vice versa?

The code:

import Std.Data.HashMap
import Mathlib
open Std



inductive Primitive where
  | unit
  | string
  | int
  | bool
  | nat
  deriving DecidableEq



structure TypeVar where
  index : Nat
  deriving DecidableEq

structure UnificationVar where
  index : Nat
  deriving Hashable, DecidableEq


instance : Min UnificationVar where
  min a b := min a.index b.index |> UnificationVar.mk

instance : Max UnificationVar where
  max a b := max a.index b.index |> UnificationVar.mk


def UnificationVar.toString (uv : UnificationVar) : String :=
    "?" ++ uv.index.repr

abbrev UniVar := UnificationVar










/-- A type that does away with the frills, and is purpose built from the ground up for how we do inference: namely it only represents primitives, type constructors, and anything beyond that is a univar that references an `Option SimpleType`. in the UniVarsMap. -/
inductive SimpleType where
  | primitive : Primitive → SimpleType
  /-- A type name with the type variables -/
  | typeCtor : String → List UniVar → SimpleType





instance instMembershipUniVarSimpleType : Membership UniVar SimpleType where
  mem container item :=
    match container with
    | .primitive _ => False
    | .typeCtor _ uniVars => uniVars.contains item


instance instMembershipUniVarOptionSimpleType : Membership UniVar (Option SimpleType) where
  mem container item :=
    match container with
    | .some t => item ∈ t
    | .none => False


instance instMembershipUniVarPrimitive : Membership UniVar Primitive where
  mem _ _ := False


instance {a} : Membership UniVar (HashMap UniVar a) where
  mem container item :=
    container.contains item






@[simp] theorem SimpleType.mem_leaf_eq (x : Primitive) (k : UniVar) : (k ∈ SimpleType.primitive x) = False := rfl

@[simp] theorem SimpleType.mem_typeCtor_eq {ctor : String} (uniVars : List UniVar) (k : UniVar) : (k ∈ SimpleType.typeCtor ctor uniVars) = (k ∈ uniVars) := by
  simp [instMembershipUniVarSimpleType]






abbrev SimpleTypeMap' :=
  HashMap UniVar (Option SimpleType)









/-- The inductive predicate that a uniVar is a valid key in a `SimpleTypeMap'`, that every univar at a value in the map is also a valid key in the map, and that there are no cycles of univars looping round to point to each other! -/
inductive IsValidUniVarKey (m : SimpleTypeMap') : UniVar → Prop where
  | mk (uniVar : UniVar)
       (hmem : uniVar ∈ m)
       (h : ∀ uv ∈ m[uniVar]'hmem, IsValidUniVarKey m uv) : IsValidUniVarKey m uniVar



/-- The predicate that a type is in the map and that all univars in that type are also in the map -/
inductive ContainsValidUniVars (m : SimpleTypeMap') : SimpleType → Prop where
  | mk (t : SimpleType)
       (h : ∀ uv ∈ t, IsValidUniVarKey m uv) : ContainsValidUniVars m t







def ContainsValidUniVars.mkFromPrimitive (m : SimpleTypeMap') (p : Primitive) : ContainsValidUniVars m (SimpleType.primitive p) := by
  refine .mk (SimpleType.primitive p) ?_
  intro uv huv
  simp only [instMembershipUniVarSimpleType] at huv


def ContainsValidUniVars.mkFromKnownPrimitive (m : SimpleTypeMap') {t : SimpleType} (p : Primitive) (h : t = SimpleType.primitive p) : ContainsValidUniVars m t := by
  rw [h]
  exact .mkFromPrimitive m p



def ContainsValidUniVars.mkFromEmptyCtor (ctor : String) {t : SimpleType} (m : SimpleTypeMap') (h : t = SimpleType.typeCtor ctor []) : ContainsValidUniVars m t := by
  rw [h]
  refine .mk (SimpleType.typeCtor ctor []) ?_
  intro uv huv
  simp [instMembershipUniVarSimpleType] at huv







@[simp] theorem SimpleType.uniVar_nin_primitive {uv : UniVar} {p : Primitive} : (uv ∈ SimpleType.primitive p) = False := by
  simp [instMembershipUniVarSimpleType]


@[simp] theorem SimpleType.uniVar_in_typeCtor {uv : UniVar} {ctor : String} {uniVars : List UniVar} : (uv ∈ SimpleType.typeCtor ctor uniVars) = (uv ∈ uniVars) := by
  simp [instMembershipUniVarSimpleType]




def makePrfUniVarInPrimitive {p : Primitive} (uv : UniVar) (t : SimpleType) (h : t = SimpleType.primitive p) (hh : uv ∈ t) : False := by
  simp [instMembershipUniVarSimpleType] at hh
  rw [h] at hh
  simp at hh








def SimpleTypeMap := { map : SimpleTypeMap' // ∀ uv ∈ map, IsValidUniVarKey map uv }














inductive SimpleZonkedType where
  | primitive : Primitive → SimpleZonkedType
  /-- A type variable. Might be slightly tricky to make sure we keep typevars that should be the same skolem the same, whilst ensuring that typevars that can be different are different.
  But what I'm thinking rn is that at every zonking step we return the next available typevar index, and when we learn that we can generalise a univar, we replace that with this next available typevar index. At which point we create the next typevar by incrementing the index of the last one, and bubble that one up the callers.
   -/
  | typeVar : TypeVar → SimpleZonkedType
  | typeCtor : String → List SimpleZonkedType → SimpleZonkedType



abbrev SimpleZonkedTypeMap := HashMap UniVar SimpleZonkedType






def HashMap.attach {k v : Type u} [DecidableEq k] [Hashable k] (map : HashMap k v) : List {key : k // key ∈ map} :=
  map.keys.attach.map fun ⟨key, hkey⟩ => ⟨key, HashMap.mem_keys.mp hkey⟩



/-- We go through the map one univar key at a time, and zonk it until it can no longer be zonked. At which point by the end we should have a map of fully zonked types, which should be trivially convertible to a `SimpleZonkedTypeMap` I believe. -/
def zonkSimpleTypeMap (uniVarsMap : SimpleTypeMap) : SimpleZonkedTypeMap :=
  let firstTypeVar : TypeVar := .mk 0

  let allUniVars := uniVarsMap.1 |> HashMap.attach
  let map :=
    allUniVars.foldl (init := (HashMap.empty, firstTypeVar)) (fun (acc, accTypeVar) ⟨uv, uvInMap⟩ =>
      let isValidUniVarKey := uniVarsMap.2 uv uvInMap
      let zonked := zonkSingleUv uv accTypeVar isValidUniVarKey

      (acc.insert uv zonked.1, zonked.2)
    )
  map.1

where
  -- ok so i don't think this will really work because just focusing on one univar at a time will probably not let us generalise the univars to typevars consistently across the thing, but I think let's try this just for one univar at a time and see how we go from there.
  -- @TODO: need to prove termination on `zonkSimpleType`, and need to do so by feeding in an inductive as an argument, somehow. Should probably be able to derive this from an `IsValidUniVarKey` somehow
  zonkSingleUv (uv : UniVar) (nextTypeVar : TypeVar) (uh : IsValidUniVarKey uniVarsMap.1 uv) : SimpleZonkedType × TypeVar :=
    let hmem :=
      match uh with
      | IsValidUniVarKey.mk _ hmem _ => hmem

    match hh : uniVarsMap.1[uv]'hmem with
    | none =>
      (SimpleZonkedType.typeVar nextTypeVar, { nextTypeVar with index := nextTypeVar.index + 1 })

    | some someVal =>
      let h : ContainsValidUniVars uniVarsMap.1 someVal :=
        by
        cases hhh : someVal with
        | primitive p =>
          refine .mkFromKnownPrimitive uniVarsMap.1 p ?_
          rfl


        | typeCtor tag uniVars =>
          cases univarsPrf : uniVars with
          | nil =>
            refine .mkFromEmptyCtor tag uniVarsMap.1 ?_
            rewrite [univarsPrf] at hhh
            rfl

          | cons hd tl =>
            have tt : ∀ uv_1 ∈ uniVarsMap.1[uv], IsValidUniVarKey uniVarsMap.1 uv_1 :=
              match uh with
              | IsValidUniVarKey.mk _ _ tt => tt

            rw [← univarsPrf, ← hhh]
            constructor
            intro thisUv huv
            simp [instMembershipUniVarOptionSimpleType] at huv
            rw [hh] at tt
            have := tt thisUv huv
            exact this


      match hh : someVal with
      | .primitive p => (SimpleZonkedType.primitive p, nextTypeVar)
      | .typeCtor ctor uniVars =>
        let zonkedArgs :=
          uniVars.attach.foldl (init := ([], nextTypeVar))
            fun (acc, accTypeVar) ⟨thisUv, thisUvInUniVars⟩ =>
            by
            let zonked := zonkSingleUv thisUv accTypeVar ?_
            refine (zonked.1 :: acc, zonked.2)
            have huv :=
              match h with
              | .mk _ huv => huv
            rw [hh] at huv
            have : thisUv ∈ SimpleType.typeCtor ctor uniVars → IsValidUniVarKey uniVarsMap.1 thisUv := huv thisUv
            simp [SimpleType.uniVar_in_typeCtor] at this
            exact this thisUvInUniVars

        (SimpleZonkedType.typeCtor ctor zonkedArgs.1, zonkedArgs.2)

  termination_by structural uh

[Aaron Liu]

It says that when doing structural recursion on IsValidUniVarKey, you can only eliminate into Prop.

[aron]

what does that mean? that I can't recurse on IsValidUniVarKey inside a function unless that function returns a Prop? why?

[Aaron Liu]

It means you can't recurse on IsValidUniVarKey unless you're proving a theorem. This is because IsValidUniVarKey is a Prop, and so is subject to proof irrelevance.

[Aaron Liu]

Now that I'm looking at IsValidUniVarKey, you may be able to modify its definition a little to make this work.

[aron]

when I change the two proofs to return Types instead, Lean seems to go into an infinite loop and doesn't show me any errors even when I write some nonsense code :thinking:
Screenshot 2025-03-15 at 23.06.19.png