'unreachable' code was reached by termination check

Stream: lean4

[Alex Keizer]

The following MWE triggers unreachable code in the latest nightly (nightly-2022-05-04):

universe u

/-- A curried function of exactly `n` arguments; `α → ... → α → β` -/
abbrev CurriedFun (α β : Type u) : Nat → Type u
  | 0   => β
  | n+1 => α → CurriedFun α β n

/-- A curried type function of `n` arguments, i.e., `Type u → Type u → ... → Type u` -/
abbrev CurriedTypeFun : Nat → Type (u+1)
  := CurriedFun (Type u) (Type u)

/-- In my actual code, `GenTypeFun` is distinct from `CurriedTypeFun`, and `m` is used -/
abbrev GenTypeFun (n m : Nat) : Type _
  := CurriedFun (Type u) (Type u) n


def asCurried {n m : Nat} (F : GenTypeFun n m) : CurriedTypeFun (m + n)
  := match n, m with
      | 0,   _    => by sorry
      | _,   0    => by sorry
      | n+1, _    => fun τ => asCurried (F τ)

The error is

fail to show termination for
  asCurried
with errors
'unreachable' code was reached

'unreachable' code was reached

Note that my code triggers the same error without sorry's, those are not the issue.

Termination should be easy to prove, it just recurses on n, but adding the termination hint does not fix the issue.

[Alex Keizer]

The issue seems to be with the simultaneous match on n and m, the following code works as expected:

def asCurried {n m : Nat} (F : GenTypeFun n m) : CurriedTypeFun (m + n)
  := match n with
      | 0     => by sorry
      | n+1   => match m with
                | 0 => by sorry
                | _ => fun τ => asCurried (F τ)

[Leonardo de Moura]

Pushed a fix for this https://github.com/leanprover/lean4/commit/16ed5a321366b08b9dadcc59d6f35da281c8b8cb