[ fix ] Address some proofs of void via impossible from issues #2250 and #3276

[dunhamsteve]

Description

This PR addresses a few issues in #2250 and issue #3276. They are caused by an issue with IAlternative in impossible clauses, a type confusion issue in impossible clauses, and treatment of out of hidden constructors as impossible. An additional issue was brought up in #2250 that is not addressed here. I'll first discuss the issues and how I resolved them and then discuss a frex issue that should be patched before merging.

Issues fixed

The IAlternative issue is illustrated at the top of #2550:

%default total

g : Not Bool
g () impossible

f : Void
f = g True

Here the impossible clause is accepted because the type doesn't match at all, but when it is converted by mkTerm to a term for coverage checking, the ambiguous () is converted to a pattern variable which is then considered to cover everything. I addressed this by choosing the default alternative. I didn't see a way to determine the appropriate alternative at that point in the code. A user will have to explicitly say Unit or Pair to get the other option in an impossible clause.

The type confusion issue is illustrated in #2250 by:

import Data.Nat
%default total

f : n `LTE` m -> Void
f Z impossible
f (LTESucc x) = f x

x : Void
x = f $ LTEZero {right=Z}

Here Z is impossible because it has the wrong type, but during coverage checking only the constructor tag is looked at and Z is confused with LTEZero. I addressed this by also checking that the name matches. I coerce the names to resolved names in getCons because some constructor names were resolved in the context and others were not.

Finally, in #3276 there was a false impossible because a constructor was not visible. I adjusted recoverableError to not consider InvisibleName to be evidence of impossible.

The issues fixed in #2250 and #3276 are included as test cases.

Frex

Frex is relying on the ambiguity bug with Pair/MkPair in one location. The function is indeed covering, but Idris cannot capable of determining that if MkPair is used instead of (,). The current code is only working because of the above bug. This can be addressed with the following patch to frex, which pushes the impossible match down to a separate case tree:

diff --git a/src/Frexlet/Monoid/Frex/Structure.idr b/src/Frexlet/Monoid/Frex/Structure.idr
index 8ccc22e..0164d67 100644
--- a/src/Frexlet/Monoid/Frex/Structure.idr
+++ b/src/Frexlet/Monoid/Frex/Structure.idr
@@ -159,8 +159,10 @@ MultHomomorphism a s (i, ConsUlt i1 x is) (j,ConsUlt j1 y js)
   = ( a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
     , x_eq_y
     ) :: is_eq_js
-MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) (MkAnd _ _) impossible
-MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) (MkAnd _ _) impossible
+MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) x with (x)
+  _ | MkAnd _ _ impossible
+MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) x with (x)
+  _ | MkAnd _ _ impossible
 
 public export
 AppendHomomorphismProperty : (a : Monoid) -> (x : Setoid) ->

[mjustus]

I'd be happy for it to be merged but I am still in two minds about this change in the coverage checker.

It is clearly correct and fixes an existing bug but I was under the impression that coverage checking implicitly assumes that all patterns passed to it are already well-typed. So I'd prefer if ill-typed patterns like

Bug : Not (3 `LessThanOrEqualTo` 5)
Bug Refl impossible

are rejected before the coverage checker is called. On the other hand, that would require a much more involved change and it may be a while before somebody finds the time to work on it.