Incorrect error message

[leodemoura]

Given the definition

def foo : Nat -> Nat -> Nat -> List Nat
| _, _, 0   => [1]
| 0, _, _   => [2]
| n, d, k+1 => foo n d k

the equation compiler produces the incorrect error message.

-- error: equation compiler error, equation #2 has not been used in the compilation (possible solution: delete equation)

The bug is that the equation compiler has multiple steps. In this example, it first applies structural_rec to eliminate the recursion. The third parameter is selected to justify why the recursion terminates, and the second equation is split into two because the third argument is variable here, but a pattern in other equations.

def foo : Nat → Nat → Π (a : Nat), Nat.below a → List Nat
| _x, _x_1, 0, _F := 1::List.nil
| 0, _x, 0, _F := 2::List.nil
| 0, _x, Nat.succ n, _F := 2::List.nil
| n, d, k+1,  _F := (_F.fst).fst n d

The split is not communicated to the next step elim_match that performs pattern matching.
The new second equation is not used and elim_match incorrectly reports the error.

This bug will be fixed in the new equation compiler that we will implement in Lean.
In the meantime, we can avoid this issue by writing the definition as.

def foo : Nat -> Nat -> Nat -> List Nat
| _, _, 0   => [1]
| 0, _, Nat.succ _   => [2]
| n, d, k+1 => foo n d k