[ fix ] Accept not fully applied impossible clauses

Author: spcfox

src/TTImp/Impossible.idr

@@ -66,58 +66,67 @@ mutual
   processArgs : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto q : Ref QVar Int} ->
+                Bool -> -- should be fully applied
                 ClosedTerm -> ClosedNF ->
                 (expargs : List RawImp) ->
                 (autoargs : List RawImp) ->
                 (namedargs : List (Name, RawImp)) ->
                 Core ClosedTerm
   -- unnamed takes priority
-  processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
+  processArgs con fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
      = do e' <- mkTerm e (Just ty) [] [] []
           defs <- get Ctxt
-          processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
+          processArgs con (App fc fn e')
+                      !(sc defs (toClosure defaultOpts Env.empty e'))
                       exps autos named
-  processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) [] autos named
+  processArgs con fn (NBind fc x (Pi _ _ Explicit ty) sc) [] autos named
      = do defs <- get Ctxt
           case findNamed x named of
             Just ((_, e), named') =>
                do e' <- mkTerm e (Just ty) [] [] []
-                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
+                  processArgs con (App fc fn e')
+                              !(sc defs (toClosure defaultOpts Env.empty e'))
                               [] autos named'
-            Nothing => badClause fn [] autos named
-  processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exps autos named
+            Nothing => -- Expected an explicit argument, but only implicits left
+                       if not con && null autos && null named
+                          then pure fn
+                          else badClause fn [] autos named
+  processArgs con fn (NBind fc x (Pi _ _ Implicit ty) sc) exps autos named
      = do defs <- get Ctxt
           case findNamed x named of
             Nothing => do e' <- nextVar fc
-                          processArgs (App fc fn e')
+                          processArgs con (App fc fn e')
                                       !(sc defs (toClosure defaultOpts Env.empty e'))
                                       exps autos named
             Just ((_, e), named') =>
                do e' <- mkTerm e (Just ty) [] [] []
-                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
+                  processArgs con (App fc fn e')
+                              !(sc defs (toClosure defaultOpts Env.empty e'))
                               exps autos named'
-  processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exps autos named
+  processArgs con fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exps autos named
      = do defs <- get Ctxt
           case autos of
                (e :: autos') => -- unnamed takes priority
                    do e' <- mkTerm e (Just ty) [] [] []
-                      processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
+                      processArgs con (App fc fn e')
+                                  !(sc defs (toClosure defaultOpts Env.empty e'))
                                   exps autos' named
                [] =>
                   case findNamed x named of
                      Nothing =>
                         do e' <- nextVar fc
-                           processArgs (App fc fn e')
+                           processArgs con (App fc fn e')
                                        !(sc defs (toClosure defaultOpts Env.empty e'))
                                        exps [] named
                      Just ((_, e), named') =>
                         do e' <- mkTerm e (Just ty) [] [] []
-                           processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
+                           processArgs con (App fc fn e')
+                                       !(sc defs (toClosure defaultOpts Env.empty e'))
                                        exps [] named'
-  processArgs fn ty [] [] [] = pure fn
-  processArgs fn ty (x :: _) autos named
+  processArgs _ fn _ [] [] [] = pure fn
+  processArgs _ fn _ (x :: _) autos named
      = throw $ GenericMsg (getFC x) "Too many arguments"
-  processArgs fn ty exps autos named
+  processArgs _ fn _ exps autos named
      = badClause fn exps autos named
 
   buildApp : {auto c : Ref Ctxt Defs} ->
@@ -148,7 +157,10 @@ mutual
            -- When `head` is `Func`, the pattern will be marked as forced and
            -- the coverage checker will considers that all the cases have been
            -- covered!
-           processArgs (Ref fc (getDefNameType gdef) (Resolved i)) tynf exps autos named
+           let nameType = getDefNameType gdef
+           processArgs (isJust $ isCon nameType)
+                       (Ref fc nameType (Resolved i))
+                       tynf exps autos named
 
   mkTerm : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->

tests/idris2/coverage/impossible002/Issue3679.idr

@@ -0,0 +1,6 @@
+interface Cogen a where
+  constructor MkCogen
+  perturb : a -> Nat -> Nat
+
+Cogen Void where
+  perturb _ impossible

tests/idris2/coverage/impossible002/Main.idr

@@ -0,0 +1,2 @@
+foo : Void -> Nat -> Nat
+foo _ impossible

tests/idris2/coverage/impossible002/expected

@@ -0,0 +1,2 @@
+1/1: Building Main (Main.idr)
+1/1: Building Issue3679 (Issue3679.idr)

tests/idris2/coverage/impossible002/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check Main.idr
+check Issue3679.idr

tests/idris2/coverage/impossible003/Main.idr

@@ -0,0 +1,3 @@
+foo : Nat -> Nat
+foo S impossible
+foo Z = Z

tests/idris2/coverage/impossible003/expected

@@ -0,0 +1,17 @@
+1/1: Building Main (Main.idr)
+Warning: Main:2:5--2:6:Badly formed impossible clause (Prelude.Types.S, ([], ([], [])))
+
+Main:2:5--2:6
+ 1 | foo : Nat -> Nat
+ 2 | foo S impossible
+         ^
+
+Error: foo is not covering.
+
+Main:1:1--1:17
+ 1 | foo : Nat -> Nat
+     ^^^^^^^^^^^^^^^^
+
+Missing cases:
+    foo (S _)
+

tests/idris2/coverage/impossible003/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+# expect a coverage error
+check Main.idr