idris-lang
Case splitting - not covering
The following code typechecks
fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
fnc 0 0 prf = ?fnc_rhs_2
fnc 0 (S k) prf = ?fnc_rhs_3
fnc (S k) b prf = ?fnc_rhs_1
When case splitting on prf in line 2 and 3 I get the following code:
fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
fnc 0 0 Refl impossible
fnc 0 (S _) Refl impossible
fnc (S k) b prf = ?fnc_rhs_1
Typechecking the code, I get following error about not covering:
"c.idr" 4L, 136C written
Error: fnc is not covering.
c:1:1--1:55
1 | fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Missing cases:
fnc 0 _ _
Try using absurd prf on the RHS instead of impossible on the LHS.
This will keep the pattern-matches in the case tree and help the coverage checker see that everything is alright.
The issue here is that we silently ignore impossible clauses with fromInteger on the left side. So essentially, you can't have numbers in impossible clauses and Idris doesn't tell you that. If you put Z instead of 0, it would work.
I have now made a PR that emits a warning when an impossible clause is not accepted.
