Mutual wf recursion: unexpected bound variable #0

[nomeata]

Description

This causes an unexpected bound variable #0:

def FunType := Nat → Nat

mutual
def foo : FunType
  | .zero => 0
  | .succ n => bar n
def bar : FunType
  | .zero => 0
  | .succ n => foo n
end
termination_by foo n => n; bar n => n

It still happens when FunType is an abbrev.

It works if foo and bar simply have function types, or if it isn’t mutual recursion.

Versions

4.3.0-rc2

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.