Zulip Chat Archive

Stream: lean4

Topic: tracking down apparent de Bruijn indexing bugs?

view this post on Zulip Jason Gross (Mar 05 2021 at 21:38):

set_option trace.Elab.definition true doesn't seem to do anything here, is there a better option?

structure Ty where
  ctx : Type
  ty : ctx  Type
structure Tm where
  ty : Ty
  tm :  {Γ}, ty.ty Γ

def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t
set_option trace.Elab.definition true
def foo (x' : Type) (f : Tm) (fTy : f.ty = Ty.mk x' (fun _ => Unit)) (xTy : Unit)
  := Tm.inj _ (cast (congrFun fTy _) _)
12:16: application type mismatch
  cast (congrFun ?m.529 xTy)
  congrFun ?m.529 xTy
has type
  @Eq Type (?m.581 x' f fTy xTy) (?m.580 x' f fTy xTy)
but is expected to have type
  @Eq Type (?m.581 x' f fTy xTy) (?m.580 x' f fTy xTy)


(reported as https://github.com/leanprover/lean4/issues/333, btw)

Last updated: May 18 2021 at 23:14 UTC