54dd588fc2
the code stumbled over recursive functions whose type doesn’t have enough manifest foralls, like: ``` 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 ``` This can be fixed by using `whnf` in appropriate places, to expose the `.forall` constructor. Fixes #2925, comes with test case.
15 lines
302 B
Text
15 lines
302 B
Text
def FunType := Nat → Nat
|
|
def Fun2Type := Nat → Nat → Nat
|
|
|
|
mutual
|
|
def foo : FunType
|
|
| .zero => 0
|
|
| .succ n => bar n
|
|
def bar : Nat → Nat
|
|
| .zero => 0
|
|
| .succ n => baz n 0
|
|
def baz : Fun2Type
|
|
| .zero, m => 0
|
|
| .succ n, m => foo n
|
|
end
|
|
termination_by foo n => n; bar n => n; baz n _ => n
|