termination IR check failed unexpected type

Stream: lean4

[Michael Jam]

Here is a mwe where it fails to show termination. Feels a lot like a bug:

def Family (α : Type _) (n : Nat) := Inhabited (Fin n → α)

def all_but_last {α} {n} (f : Family α (n + 1)) : Family α n :=
Inhabited.mk λ k => f.default ⟨k.val, Nat.lt_trans k.isLt n.lt_succ_self⟩

def all : {n : Nat} → Family Prop n → Prop
| 0, _ => True
| n + 1, f => all (all_but_last f)

def th : (n : Nat) → (f : Family Prop n) → Decidable (all f)
| 0, f => isTrue ⟨⟩
| n + 1, f => th n (all_but_last f)

The error message is:

fail to show termination for
  th
with errors
IR check failed at 'th', error: unexpected type '◾'

Surprisingly the termination check is repaired if I do any of the following:

• Remove the useless Inhabited wrapper in Family's def, that is make Family a synonym of Fin n → α
• Replace α with Prop in all_but_last to specialize a little bit.
• Remove Decidable and isTrue in th
• Make th a theorem instead of a def

I am using Lean (version 4.0.0-nightly-2022-02-13, commit 340c331da908, Release)

Thanks for taking a look!

[Leonardo de Moura]

Pushed a fix for this.
https://github.com/leanprover/lean4/commit/dedb6ee01bfca70481f615f79ff06d8bcf187de0
The error message is a bit misleading. It was a bug in the code generator.