(kernel) function expected .noConfusion

Stream: lean4

[Sébastien Michelland]

This behavior seems to be a bug in the dependent matcher - MyBool.noConfusion gets passed both an argument for b = .MyTrue and an extra one for u = ().

inductive MyBool :=
  | MyTrue
  | MyFalse

inductive T :=
  | mk (b: MyBool) (u: Unit)

inductive isTrue: T → Type :=
  | intro: isTrue (.mk .MyTrue ())

example {τ: T} (h: isTrue τ): Unit :=
  match τ, h with
  | .mk .MyTrue (), .intro => ()
-- (kernel) function expected
--   MyBool.noConfusion (_ : b✝ = MyBool.MyTrue) (_ : u✝ = ())

I there is a way to write such a function without first refining τ then h, I'd also like to know.

[Leonardo de Moura]

Thanks for reporting this issue. I pushed a fix for it: https://github.com/leanprover/lean4/commit/32db3161666325b704ef9d4876f9ee9718e03bb2