Better checking for empty types

This improves coverage checking, because it can now see that things like
(Z = S x) and (x = S x) are empty. Previously, it only checked that all
possible constructors had a disjoint index. Now, it looks for matches
and checks for disjointness in the matches, which catches a lot more
things especially with equality.

src/Core/Coverage.idr

@@ -7,59 +7,132 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
+import Data.Bool.Extra
 import Data.List
 import Data.NameMap
 
 %default covering
 
+-- Return whether any of the name matches conflict
+conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool
+conflictMatch [] = False
+conflictMatch ((x, tm) :: ms)
+    = if conflictArgs x tm ms
+         then True
+         else conflictMatch ms
+  where
+    clash : Term vars -> Term vars -> Bool
+    clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
+        = t /= t'
+    clash _ _ = False
+
+    findN : Nat -> Term vars -> Bool
+    findN i (Local _ _ i' _) = i == i'
+    findN i tm
+        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
+                   | _ => False in
+              anyTrue (map (findN i) args)
+
+    -- Assuming in normal form. Look for: mismatched constructors, or
+    -- a name appearing strong rigid in the other term
+    conflictTm : Term vars -> Term vars -> Bool
+    conflictTm (Local _ _ i _) tm
+        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
+                   | _ => False in
+              anyTrue (map (findN i) args)
+    conflictTm tm (Local _ _ i _)
+        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
+                   | _ => False in
+              anyTrue (map (findN i) args)
+    conflictTm tm tm'
+        = let (f, args) = getFnArgs tm
+              (f', args') = getFnArgs tm' in
+              if clash f f'
+                 then True
+                 else anyTrue (zipWith conflictTm args args') 
+
+    conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
+    conflictArgs n tm [] = False
+    conflictArgs n tm ((x, tm') :: ms)
+        = if n == x && conflictTm tm tm'
+             then True
+             else conflictArgs n tm ms
+
 -- Return whether any part of the type conflicts in such a way that they
 -- can't possibly be equal (i.e. mismatched constructor)
 conflict : {vars : _} ->
-           Defs -> NF vars -> Name -> Core Bool
-conflict defs nfty n
+           {auto c : Ref Ctxt Defs} ->
+           Defs -> Env Term vars -> NF vars -> Name -> Core Bool
+conflict defs env nfty n
     = do Just gdef <- lookupCtxtExact n (gamma defs)
               | Nothing => pure False
          case (definition gdef, type gdef) of
               (DCon t arity _, dty)
-                  => conflictNF nfty !(nf defs [] dty)
+                  => do Nothing <- conflictNF 0 nfty !(nf defs [] dty)
+                            | Just ms => pure $ conflictMatch ms
+                        pure True
               _ => pure False
   where
     mutual
-      conflictArgs : List (Closure vars) -> List (Closure []) -> Core Bool
-      conflictArgs [] [] = pure False
-      conflictArgs (c :: cs) (c' :: cs')
+      conflictArgs : Int -> List (Closure vars) -> List (Closure []) ->
+                     Core (Maybe (List (Name, Term vars)))
+      conflictArgs _ [] [] = pure (Just [])
+      conflictArgs i (c :: cs) (c' :: cs')
           = do cnf <- evalClosure defs c
                cnf' <- evalClosure defs c'
-               pure $ !(conflictNF cnf cnf') || !(conflictArgs cs cs')
-      conflictArgs _ _ = pure False
+               Just ms <- conflictNF i cnf cnf'
+                    | Nothing => pure Nothing
+               Just ms' <- conflictArgs i cs cs'
+                    | Nothing => pure Nothing
+               pure (Just (ms ++ ms'))
+      conflictArgs _ _ _ = pure (Just [])
 
-      conflictNF : NF vars -> NF [] -> Core Bool
-      conflictNF t (NBind fc x b sc)
-          = conflictNF t !(sc defs (toClosure defaultOpts [] (Erased fc False)))
-      conflictNF (NDCon _ n t a args) (NDCon _ n' t' a' args')
+      -- If the constructor type (the NF []) matches the variable type,
+      -- then there may be a way to construct it, so return the matches in
+      -- the indices.
+      -- If any of those matches clash, the constructor is not valid
+      -- e.g, Eq x x matches Eq Z (S Z), with x = Z and x = S Z
+      -- conflictNF returns the list of matches, for checking
+      conflictNF : Int -> NF vars -> NF [] -> 
+                   Core (Maybe (List (Name, Term vars)))
+      conflictNF i t (NBind fc x b sc)
+          -- invent a fresh name, in case a user has bound the same name
+          -- twice somehow both references appear in the result  it's unlikely
+          -- put posslbe
+          = let x' = MN (show x) i in
+                conflictNF (i + 1) t 
+                       !(sc defs (toClosure defaultOpts [] (Ref fc Bound x')))
+      conflictNF i nf (NApp _ (NRef Bound n) [])
+          = do empty <- clearDefs defs
+               pure (Just [(n, !(quote empty env nf))])
+      conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
           = if t == t'
-               then conflictArgs args args'
-               else pure True
-      conflictNF (NTCon _ n t a args) (NTCon _ n' t' a' args')
+               then conflictArgs i args args'
+               else pure Nothing
+      conflictNF i (NTCon _ n t a args) (NTCon _ n' t' a' args')
           = if n == n'
-               then conflictArgs args args'
-               else pure True
-      conflictNF (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c')
-      conflictNF _ _ = pure False
+               then conflictArgs i args args'
+               else pure Nothing
+      conflictNF i (NPrimVal _ c) (NPrimVal _ c')
+          = if c == c'
+               then pure (Just [])
+               else pure Nothing
+      conflictNF _ _ _ = pure (Just [])
 
 -- Return whether the given type is definitely empty (due to there being
 -- no constructors which can possibly match it.)
 export
 isEmpty : {vars : _} ->
-          Defs -> NF vars -> Core Bool
-isEmpty defs (NTCon fc n t a args)
+          {auto c : Ref Ctxt Defs} ->
+          Defs -> Env Term vars -> NF vars -> Core Bool
+isEmpty defs env (NTCon fc n t a args)
      = case !(lookupDefExact n (gamma defs)) of
             Just (TCon _ _ _ _ flags _ cons _)
                  => if not (external flags)
-                       then allM (conflict defs (NTCon fc n t a args)) cons
+                       then allM (conflict defs env (NTCon fc n t a args)) cons
                        else pure False
             _ => pure False
-isEmpty defs _ = pure False
+isEmpty defs env _ = pure False
 
 -- Need this to get a NF from a Term; the names are free in any case
 freeEnv : FC -> (vs : List Name) -> Env Term vs

src/TTImp/ProcessDef.idr

@@ -329,9 +329,10 @@ bindReq fc (b :: env) (DropCons p) ns tm
 --  * Every constructor of the family has a return type which conflicts with
 --    the given constructor's type
 hasEmptyPat : {vars : _} ->
+              {auto c : Ref Ctxt Defs} ->
               Defs -> Env Term vars -> Term vars -> Core Bool
 hasEmptyPat defs env (Bind fc x (PVar c p ty) sc)
-   = pure $ !(isEmpty defs !(nf defs env ty))
+   = pure $ !(isEmpty defs env !(nf defs env ty))
             || !(hasEmptyPat defs (PVar c p ty :: env) sc)
 hasEmptyPat defs env _ = pure False
 

tests/Main.idr

@@ -41,7 +41,7 @@ idrisTests
        "basic036", "basic037", "basic038", "basic039", "basic040",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
-       "coverage005", "coverage006",
+       "coverage005", "coverage006", "coverage007",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",

tests/idris2/coverage005/expected

@@ -1,7 +1,6 @@
 1/1: Building Cover (Cover.idr)
 Main> Main.zsym is total
-Main> Main.zsym':
-zsym' (NS _) _
+Main> Main.zsym': All cases covered
 Main> Main.foo is total
 Main> Main.bar is total
 Main> Bye for now!

tests/idris2/coverage006/Cover.idr

@@ -1,20 +0,0 @@
-import Data.Fin
-
-data NNat = NZ | NS NNat
-
-zsym : (x : NNat) -> x = NZ -> NZ = x
-zsym NZ Refl = Refl
-zsym (NS _) Refl impossible
-
-zsym' : (x : NNat) -> x = NZ -> NZ = x
-zsym' NZ Refl = Refl
-
-foo : Nat -> String
-foo 0 = "zero"
-foo 1 = "one"
-foo x = "something else"
-
-bar : Fin (S (S (S Z))) -> String
-bar 0 = "a"
-bar 1 = "b"
-bar 2 = "c"

tests/idris2/coverage007/eq.idr

@@ -0,0 +1,30 @@
+
+eq1 : (x : Nat) -> (x = S x) -> Nat
+eq1 x p impossible
+  
+eq2 : (x : Nat) -> (S x = Z) -> Nat
+eq2 x p impossible
+  
+eq3 : (x : Nat) -> (S (S x) = (S x)) -> Nat
+eq3 x p impossible
+  
+eq4 : (x : Nat) -> (S x = x) -> Nat
+eq4 x p impossible
+  
+eq5 : (x : Nat) -> (Z = S x) -> Nat
+eq5 x p impossible
+  
+eq6 : (x : Nat) -> (S x = (S (S x))) -> Nat
+eq6 x p impossible
+
+eqL1 : (xs : List a) -> (x :: xs = []) -> Nat
+eqL1 xs p impossible
+
+eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
+eqL2 xs p impossible
+
+badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
+badeq x y p impossible
+
+badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
+badeql xs ys p impossible

tests/idris2/coverage007/expected

@@ -0,0 +1,3 @@
+1/1: Building eq (eq.idr)
+eq.idr:27:1--29:1:badeq x y p is not a valid impossible case
+eq.idr:30:1--31:1:No type declaration for Main.badeql

tests/idris2/coverage007/run

@@ -0,0 +1,3 @@
+$1 --no-banner eq.idr --check
+
+rm -rf build