tracking down apparent de Bruijn indexing bugs?

Stream: lean4

[Jason Gross]

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)
argument
  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)