Look deeper when coverage checking

If there is a pattern variable with an obviously empty type, because all
of the constructors are in a different part of the family due to
disjoint indices, then reject the clause as impossible.

src/Idris/Coverage.hs

@@ -280,30 +280,30 @@ genAll i (addPH, args)
     nc' o = o
 
     otherPats :: PTerm -> [PTerm]
-    otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
-    otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o
-    otherPats o@(PPair fc hls _ l r)
+    otherPats (PRef fc hl n) = ph $ ops fc n []
+    otherPats (PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs
+    otherPats (PPair fc hls _ l r)
         = ph $ ops fc pairCon
                 ([pimp (sUN "A") Placeholder True,
                   pimp (sUN "B") Placeholder True] ++
-                 [pexp l, pexp r]) o
-    otherPats o@(PDPair fc hls p t _ v)
+                 [pexp l, pexp r])
+    otherPats (PDPair fc hls p t _ v)
         = ph $ ops fc sigmaCon
                 ([pimp (sUN "a") Placeholder True,
                   pimp (sUN "P") Placeholder True] ++
-                 [pexp t,pexp v]) o
+                 [pexp t,pexp v])
     otherPats o@(PConstant _ c) = ph [o, nextConst o]
     otherPats arg = return Placeholder
 
-    ops fc n xs o
+    ops fc n xs 
         | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
             = do xs' <- mapM otherPats (map getExpTm xs)
                  let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
                  let tyn = getTy n (tt_ctxt i)
                  case lookupCtxt tyn (idris_datatypes i) of
                          (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
                          _ -> [p]
-    ops fc n arg o = return Placeholder
+    ops fc n arg = return Placeholder
 
     getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
     getExpTm t = getTm t

src/Idris/Elab/Clause.hs

@@ -566,7 +566,7 @@ checkPossible info fc tcgen fname lhs_in
    = do ctxt <- getContext
         i <- getIState
         let lhs = addImplPat i lhs_in
-        logLvl 10 $ "Trying missing case: " ++ showTmImpls lhs
+        logElab 10 $ "Trying missing case: " ++ showTmImpls lhs
         -- if the LHS type checks, it is possible
         case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
                             (erun fc (buildTC i info ELHS [] fname
@@ -577,10 +577,17 @@ checkPossible info fc tcgen fname lhs_in
                   processTacticDecls info newDecls
                   sendHighlighting highlights
                   updateIState $ \i -> i { idris_name = newGName }
-                  let lhs_tm = orderPats (getInferTerm lhs')
-                  case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of
-                       OK _ -> return True
-                       err -> return False
+                  let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))
+                  let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm
+                  if emptyPat then 
+                     do logElab 10 $ "Empty type in pattern "
+                        return False
+                    else
+                      case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of
+                           OK _ -> do logElab 10 $ "Valid"
+                                      return True
+                           err -> do logElab 10 $ "Conversion failure"
+                                     return False
             -- if it's a recoverable error, the case may become possible
             Error err -> do logLvl 10 $ "Impossible case " ++ show err
                             if tcgen then return (recoverableCoverage ctxt err)

src/Idris/Elab/Utils.hs

@@ -542,4 +542,32 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in
                              return (App s f' a')
     getPats t = return t
 
-
+isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
+isEmpty ctxt tyctxt ty
+    | (P _ tyname _, args) <- unApply (getRetTy ty),
+      Just tyinfo <- lookupCtxtExact tyname tyctxt
+      -- Compare all the constructor types against the type we need
+      -- If they *all* have an argument position where some constructor
+      -- clases with the needed type, then the type we're looking for must
+      -- be empty
+         = let neededty = getRetTy ty
+               contys = mapMaybe getConType (con_names tyinfo) in
+                 all (findClash neededty) contys
+  where
+    getConType n = do t <- lookupTyExact n ctxt
+                      return (getRetTy (normalise ctxt [] t))
+
+    findClash l r
+       | (P _ n _, _) <- unApply l,
+         (P _ n' _, _) <- unApply r,
+         isConName n ctxt && isConName n' ctxt, n /= n' 
+           = True
+    findClash (App _ f a) (App _ f' a') = findClash f f' || findClash a a'
+    findClash l r = False
+
+isEmpty ctxt tyinfo ty = False
+
+hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool
+hasEmptyPat ctxt tyctxt (Bind n (PVar ty) sc)
+    = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc
+hasEmptyPat ctxt tyctxt _ = False

test/TestData.hs

@@ -274,7 +274,8 @@ testFamiliesData = [
       ( 14, ANY  ),
       ( 15, ANY  ),
       ( 16, ANY  ),
-      ( 17, ANY  )]),
+      ( 17, ANY  ),
+      ( 18, ANY  )]),
   ("tutorial",        "Tutorial examples",
     [ (  1, ANY  ),
       (  2, ANY  ),

test/interfaces002/interfaces002.idr

@@ -1,5 +1,7 @@
 import Data.Vect
 
+%default total
+
 interface ArrayM where
   Array : (n : Nat) -> (a : Type) -> Type
 

test/totality018/expected

@@ -0,0 +1 @@
+totality018.idr:12:1:Main.bar is not total as there are missing cases

test/totality018/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ totality018.idr --check
+rm -f *.ibc

test/totality018/totality018.idr

@@ -0,0 +1,15 @@
+import Data.Fin
+
+%default total
+
+foo : Fin 3 -> Nat
+foo FZ = 0
+foo (FS FZ) = 1
+foo (FS (FS FZ)) = 2
+-- testing that there is no need for an extra 'impossible'
+
+bar : Fin 4 -> Nat
+bar FZ = 0
+bar (FS FZ) = 1
+bar (FS (FS FZ)) = 2
+-- should be non-total