expected type sorry?

Stream: lean4

[Jason Gross]

Should I be seeing "but is expected to have type sorry" in cases where I don't use sorry?

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

#check fun (Γ : Type)
(A : Ty)
(Actx : Γ = A.ctx)
(x : Tm)
(xTy : x.ty = A)
=> Eq.rec (motive := fun ty _ => ∀ {Γ}, ty.ty Γ) (fun {Γ:x.ty.ctx} => x.tm (Γ:=Γ)) xTy
/-
13:71: type mismatch
  Tm.tm x
has type
  Ty.ty x.ty Γ
but is expected to have type
  sorry
-/

[Leonardo de Moura]

Pushed a fix for this one: https://github.com/leanprover/lean4/commit/7a79ef62d1ee7ff34ac3141eacbecb537ec62e28

[Jason Gross]

Great, thanks!