Getting `(kernel) application type mismatch` in theorems

Stream: new members

[aron]

Bit of a long #mwe because I have no idea what's causing this so I don't know how to reproduce it other than in the code I actually have here.

But there are two theorems in the OccursCheck section that have (kernel) application type mismatch errors and I don't really get what's causing it. Could this be a bug in Lean?

section Vec

inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

@[reducible] def Vec.get (vec : Vec α n) (index : Fin n) : α :=
  match vec, index with
  | .cons head tail, ⟨ 0, _ ⟩ => head
  | .cons head tail, ⟨ n+1, _ ⟩ => by
    refine tail.get ⟨ n, ?_ ⟩
    expose_names
    exact Nat.succ_lt_succ_iff.mp isLt

instance : GetElem (Vec α n) (Fin n) α (valid := fun _ _ => True) where
  getElem as i _ := as.get i

end Vec


section Ty

inductive PrimTy
  | unit
  | int
  | nat
  | bool
  | str
  deriving DecidableEq

mutual

/-- The type index tells us the size of the ctx we're in, so that we know what the max de Bruijn index for a uniVar to point to is -/
inductive TyInner : (ctxLen : Nat) → Type u where
  | prim : PrimTy → TyInner ctxLen
  | pair : (fst : Ty ctxLen) → (snd : Ty ctxLen) → TyInner ctxLen
  | arrow : (from_ : Ty ctxLen) → (to_ : Ty ctxLen) → TyInner ctxLen

/-- The type index is for how many levels of binders this type is used inside of – so that we know what the `.uniVar` is allowed to reference -/
inductive Ty : (ctxLen : Nat) → Type u where
  | uniVar : (deBruijnLevel : Fin ctxLen) → Ty ctxLen
  | shape : TyInner ctxLen → Ty ctxLen

end

/-- The type index here is the index that this `TyMaybe` has in the ctx – which should always be fine because `TyMaybe`s don't really make sense outside a list -/
inductive TyMaybe : (ctxLen : Nat) → Type u where
  /-- Concrete type -/
  | conc : (ty : Ty ctxLen) → TyMaybe ctxLen
  -- | conc : (indexInCtx : Fin ctxLen) → (ty : Ty ctxLen) → TyMaybe indexInCtx
  /-- As of yet unspecified type. This is to be swapped out for a concrete one when we close off the lambda.
  `indexInCtx` denotes at what index in the ctx list this particular `.unspec` resides. -/
  | unspec : (indexInCtx : Fin ctxLen) → TyMaybe ctxLen

end Ty


mutual
@[simp] def Ty.mem_uniVar {ctxLen} (ty : Ty ctxLen) (index : Fin ctxLen) : Prop :=
  match ty with
  | .uniVar i => i = index
  | .shape shape => TyInner.mem_uniVar shape index

@[simp] def TyInner.mem_uniVar {ctxLen} (ty : TyInner ctxLen) (index : Fin ctxLen) : Prop :=
  match ty with
  | .prim _ => False
  | .pair a b
  | .arrow a b => Ty.mem_uniVar a index ∨ Ty.mem_uniVar b index
end



@[simp] instance {ctxLen} : Membership (Fin ctxLen) (TyInner ctxLen) where
  mem := TyInner.mem_uniVar

@[simp] instance {ctxLen} : Membership (Fin ctxLen) (Ty ctxLen) where
  mem := Ty.mem_uniVar

@[simp] instance {ctxLen} : Membership (Fin ctxLen) (TyMaybe ctxLen) where
  mem := fun ty index =>
    match ty with
    | .conc ty => index ∈ ty
    | .unspec _ => False


section OccursCheck

mutual
inductive NotInTyInnerRef {ctxLen} (ctx : Vec (TyMaybe ctxLen) ctxLen) : (index : Fin ctxLen) → TyInner ctxLen → Prop where
  | prim : NotInTyInnerRef ctx index (.prim p)
  | pair : NotInTyRef ctx index t1 → NotInTyRef ctx index t2 → NotInTyInnerRef ctx index (.pair t1 t2)
  | arrow : NotInTyRef ctx index t1 → NotInTyRef ctx index t2 → NotInTyInnerRef ctx index (.arrow t1 t2)

inductive NotInTyRef {ctxLen} (ctx : Vec (TyMaybe ctxLen) ctxLen) : (index : Fin ctxLen) → Ty ctxLen → Prop where
  | uniVar_unspec :
    otherIndex ≠ index →
    ctx[otherIndex] = .unspec otherIndex →
    NotInTyRef ctx index (.uniVar otherIndex)

  | uniVar_conc :
    otherIndex ≠ index →
    ctx[otherIndex] = .conc t →
    NotInTyRef ctx index t →
    NotInTyRef ctx index (.uniVar otherIndex)

  | shape :
    NotInTyInnerRef ctx index t →
    NotInTyRef ctx index (.shape t)
end


inductive NotInTyMaybeRef {ctxLen} (ctx : Vec (TyMaybe ctxLen) ctxLen) : (index : Fin ctxLen) → TyMaybe ctxLen → Prop where
  | unspec : NotInTyMaybeRef ctx index (.unspec unspecIndex)
  | conc : NotInTyRef ctx index t → NotInTyMaybeRef ctx index (.conc t)



theorem NotInTyRef.not_inside {ctxLen} {ctx : Vec (TyMaybe ctxLen) ctxLen} (index : Fin ctxLen) (t : Ty ctxLen) (h : NotInTyRef ctx index t) : index ∉ t := by
  cases h with
  | uniVar_unspec =>
    intro h
    simp at h
    contradiction
  | uniVar_conc =>
    intro h
    simp at h
    contradiction
  | shape h =>
    cases h with
    | prim => simp
    | pair ha hb
    | arrow ha hb =>
      expose_names
      have aa := not_inside index t1 ha
      have bb := not_inside index t2 hb
      simp at aa bb ⊢
      constructor
      exact aa
      exact bb


theorem NotInTyRef.uniVar_not_mem_self {ctxLen} {ctx : Vec (TyMaybe ctxLen) ctxLen} (index : Fin ctxLen) (t : Ty ctxLen) (h : NotInTyRef ctx index t) : ∀ uv ∈ t, uv ≠ index := by
  intro uv mem
  cases h with
  | uniVar_unspec a b =>
    simp at mem
    rw [mem] at a
    exact a
  | uniVar_conc a b c =>
    simp at mem
    rw [mem] at a
    exact a
  | shape hh =>
    cases hh with
    | prim => simp at mem
    | pair ha hb
    | arrow ha hb =>
      expose_names
      have aa := NotInTyRef.uniVar_not_mem_self index t1 ha
      have bb := NotInTyRef.uniVar_not_mem_self index t2 hb
      simp at mem aa bb ⊢
      cases mem with
      | inl h => exact aa uv h
      | inr h => exact bb uv h

end OccursCheck

[Aaron Liu]

This is a bug in Lean, but I can't tell if it's a bug in cases or a bug in the recursion compiler

[aron]

Hm ok. Should I report this bug somewhere?

[Aaron Liu]

This is a good place to report it

[aron]

as in should I consider this post sufficient as a bug report? is my work here done?

[Aaron Liu]

You should probably try to get a shorter #mwe

[aron]

any idea what lean is getting tripped up on here? not really sure where to start cutting things down otherwise

[Aaron Liu]

You can start replacing definitions by sorry and see if the bug is still there

[aron]

definitions? or proofs?

[Aaron Liu]

Both