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

…and #3276 (#3396)

* [ fix ] impossible confuses constructors between types

* Handle IAlternative when making an impossible term

* Check types in impossible clauses

src/Core/Coverage.idr

@@ -148,7 +148,7 @@ isEmpty defs env _ = pure False
 altMatch : CaseAlt vars -> CaseAlt vars -> Bool
 altMatch _ (DefaultCase _) = True
 altMatch (DelayCase _ _ t) (DelayCase _ _ t') = True
-altMatch (ConCase _ t _ _) (ConCase _ t' _ _) = t == t'
+altMatch (ConCase n t _ _) (ConCase n' t' _ _) = t == t'
 altMatch (ConstCase c _) (ConstCase c' _) = c == c'
 altMatch _ _ = False
 

src/TTImp/Impossible.idr

@@ -45,7 +45,6 @@ match nty (n, i, rty)
 dropNoMatch : {auto c : Ref Ctxt Defs} ->
               Maybe (NF []) -> List (Name, Int, GlobalDef) ->
               Core (List (Name, Int, GlobalDef))
-dropNoMatch _ [t] = pure [t]
 dropNoMatch Nothing ts = pure ts
 dropNoMatch (Just nty) ts
     = -- if the return type of a thing in ts doesn't match nty, drop it
@@ -168,6 +167,8 @@ mutual
   mkTerm (INamedApp fc fn nm arg) mty exps autos named
      = mkTerm fn mty exps autos ((nm, arg) :: named)
   mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
+  mkTerm (IAlternative _ (UniqueDefault tm) _) mty exps autos named
+     = mkTerm tm mty exps autos named
   mkTerm tm _ _ _ _ = nextVar (getFC tm)
 
 -- Given an LHS that is declared 'impossible', build a term to match from,

src/TTImp/ProcessDef.idr

@@ -221,6 +221,8 @@ recoverableErr defs (CantSolveEq fc gam env l r)
                         !(nf defs env r)
 recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True
 recoverableErr defs (CyclicMeta _ _ _ _) = pure False
+-- Don't mark a case as impossible because we can't see the constructor.
+recoverableErr defs (InvisibleName _ _ _) = pure True
 recoverableErr defs (AllFailed errs)
     = anyM (recoverableErr defs) (map snd errs)
 recoverableErr defs (WhenUnifying _ _ _ _ _ err)

tests/idris2/coverage/coverage021/Head.idr

@@ -0,0 +1,9 @@
+total
+head : List a -> a
+head (x :: xs) = x
+head () impossible
+
+total
+head' : List a -> a
+head' (x :: xs) = x
+head' Z impossible

tests/idris2/coverage/coverage021/Issue2250a.idr

@@ -0,0 +1,19 @@
+View : Type -> Type
+View a = a -> Type
+
+-- Pre-image view
+data (.inv) : (f : a -> b) -> View b where
+  Choose : (x : a) -> f.inv (f x)
+
+LessThanOrEqualTo : Nat -> Nat -> Type
+LessThanOrEqualTo n k = (+n).inv k
+
+Ex1 : 3 `LessThanOrEqualTo` 5
+Ex1 = Choose 2
+
+Bug : Not (3 `LessThanOrEqualTo` 5)
+Bug Refl impossible
+
+Yikes : Void
+Yikes = Bug Ex1
+

tests/idris2/coverage/coverage021/Issue2250b.idr

@@ -0,0 +1,11 @@
+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}
+

tests/idris2/coverage/coverage021/Issue2250c.idr

@@ -0,0 +1,7 @@
+%default total
+
+g : Not Bool
+g () impossible
+
+f : Void
+f = g True

tests/idris2/coverage/coverage021/Issue3276.idr

@@ -0,0 +1,21 @@
+%default total
+
+namespace Bits8
+  export
+  data LessThan : Bits8 -> Bits8 -> Type where
+    MkLessThan : (a < b) === True -> LessThan a b
+
+  export
+  %hint
+  mkLessThan : (a < b) === True -> LessThan a b
+  mkLessThan = MkLessThan
+
+data Digit : Bits8 -> Type where
+  MkDigit : (x : Bits8) -> {auto prf1 : LessThan 47 x} -> {auto prf2 : LessThan x 58} -> Digit x
+
+prf1 : Digit 51
+prf1 = MkDigit 51
+
+dis0 : Digit 51 -> Void
+dis0 (MkDigit _ {prf1=Refl}) impossible
+

tests/idris2/coverage/coverage021/Visibility.idr

@@ -0,0 +1,8 @@
+%default total
+namespace Blah
+    export
+    data Foo : Type where
+        MkFoo : Foo
+
+boom : Foo -> Void
+boom Z impossible

tests/idris2/coverage/coverage021/expected

@@ -0,0 +1,120 @@
+1/1: Building Issue2250a (Issue2250a.idr)
+Error: Bug is not covering.
+
+Issue2250a:14:1--14:36
+ 10 | 
+ 11 | Ex1 : 3 `LessThanOrEqualTo` 5
+ 12 | Ex1 = Choose 2
+ 13 | 
+ 14 | Bug : Not (3 `LessThanOrEqualTo` 5)
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    Bug _
+
+Error: Yikes is not covering.
+
+Issue2250a:17:1--17:13
+ 13 | 
+ 14 | Bug : Not (3 `LessThanOrEqualTo` 5)
+ 15 | Bug Refl impossible
+ 16 | 
+ 17 | Yikes : Void
+      ^^^^^^^^^^^^
+
+Calls non covering function Main.Bug
+1/1: Building Issue2250b (Issue2250b.idr)
+Error: f is not covering.
+
+Issue2250b:5:1--5:22
+ 1 | import Data.Nat
+ 2 | 
+ 3 | %default total
+ 4 | 
+ 5 | f : n `LTE` m -> Void
+     ^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    f LTEZero
+
+Error: x is not covering.
+
+Issue2250b:9:1--9:9
+ 5 | f : n `LTE` m -> Void
+ 6 | f Z impossible
+ 7 | f (LTESucc x) = f x
+ 8 | 
+ 9 | x : Void
+     ^^^^^^^^
+
+Calls non covering function Main.f
+1/1: Building Issue2250c (Issue2250c.idr)
+Error: f is not covering.
+
+Issue2250c:6:1--6:9
+ 2 | 
+ 3 | g : Not Bool
+ 4 | g () impossible
+ 5 | 
+ 6 | f : Void
+     ^^^^^^^^
+
+Calls non covering function Main.g
+Error: g is not covering.
+
+Issue2250c:3:1--3:13
+ 1 | %default total
+ 2 | 
+ 3 | g : Not Bool
+     ^^^^^^^^^^^^
+
+Missing cases:
+    g _
+
+1/1: Building Issue3276 (Issue3276.idr)
+Error: dis0 is not covering.
+
+Issue3276:19:1--19:24
+ 15 | 
+ 16 | prf1 : Digit 51
+ 17 | prf1 = MkDigit 51
+ 18 | 
+ 19 | dis0 : Digit 51 -> Void
+      ^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    dis0 _
+
+1/1: Building Visibility (Visibility.idr)
+Error: boom is not covering.
+
+Visibility:7:1--7:19
+ 3 |     export
+ 4 |     data Foo : Type where
+ 5 |         MkFoo : Foo
+ 6 | 
+ 7 | boom : Foo -> Void
+     ^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    boom _
+
+1/1: Building Head (Head.idr)
+Error: head is not covering.
+
+Head:1:1--2:19
+ 1 | total
+ 2 | head : List a -> a
+
+Missing cases:
+    head []
+
+Error: head' is not covering.
+
+Head:6:1--7:20
+ 6 | total
+ 7 | head' : List a -> a
+
+Missing cases:
+    head' []
+

tests/idris2/coverage/coverage021/run

@@ -0,0 +1,8 @@
+. ../../../testutils.sh
+
+check Issue2250a.idr
+check Issue2250b.idr
+check Issue2250c.idr
+check Issue3276.idr
+check Visibility.idr
+check Head.idr