[ fix ] False positives checking for conflicts in coverage checking (#3478)

* [ fix ] expand functions when checking for impossibility

* [ fix ] don't compare incompatible spines

* [ fix ] Krivine was relying on false positive for impossible

* improve code clarity

Author: dunhamsteve

libs/papers/Language/IntrinsicTyping/Krivine.idr

@@ -522,13 +522,15 @@ namespace Machine
   public export
   vlam0 : (eq : ctx = []) -> (tr : Trace (Lam sc) env ctx) -> tr ~=~ Machine.Done {sc, env}
   vlam0 eq Done = Refl
+  vlam0 eq (Beta {arg = Element _ _, ctx = Element _ _} _) impossible
 
   public export
   vlamS : {0 env : ValidEnv g} -> {0 arg : ValidClosed a} ->
           {0 sc : Term (a :: g) b} -> {0 ctx' : ValidEvalContext b c} ->
           (eq : ctx = ValidEvalContext.(::) arg ctx') ->
           (tr : Trace (Lam sc) env ctx) ->
           (tr' : Trace sc (arg :: env) ctx' ** tr ~=~ Machine.Beta {sc, arg, env} tr')
+  vlamS {arg = (Element _ _)} {ctx' = (Element _ _)} eq Done impossible
   vlamS eq (Beta tr) with 0 (fst (biinjective @{CONS} eq))
     _ | Refl with 0 (snd (biinjective @{CONS} eq))
       _ | Refl = (tr ** Refl)

src/Core/Coverage.idr

@@ -24,20 +24,21 @@ conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool
 conflictMatch [] = False
 conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
   where
-    clash : Term vars -> Term vars -> Bool
+    data ClashResult = Distinct | Same | Incomparable
+
+    clash : Term vars -> Term vars -> ClashResult
     clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
-        = t /= t'
+        = if t /= t' then Distinct else Same
     clash (Ref _ (TyCon t _) _) (Ref _ (TyCon t' _) _)
-        = t /= t'
-    clash (PrimVal _ c) (PrimVal _ c')
-      = c /= c'
-    clash (Ref _ t _) (PrimVal _ _) = isJust (isCon t)
-    clash (PrimVal _ _) (Ref _ t _) = isJust (isCon t)
-    clash (Ref _ t _) (TType _ _) = isJust (isCon t)
-    clash (TType _ _) (Ref _ t _) = isJust (isCon t)
-    clash (TType _ _) (PrimVal _ _) = True
-    clash (PrimVal _ _) (TType _ _) = True
-    clash _ _ = False
+        = if t /= t' then Distinct else Same
+    clash (PrimVal _ c) (PrimVal _ c') = if  c /= c' then Distinct else Same
+    clash (Ref _ t _) (PrimVal _ _) = if isJust (isCon t) then Distinct else Incomparable
+    clash (PrimVal _ _) (Ref _ t _) = if isJust (isCon t) then Distinct else Incomparable
+    clash (Ref _ t _) (TType _ _)   = if isJust (isCon t) then Distinct else Incomparable
+    clash (TType _ _) (Ref _ t _)   = if isJust (isCon t) then Distinct else Incomparable
+    clash (TType _ _) (PrimVal _ _) = Distinct
+    clash (PrimVal _ _) (TType _ _) = Distinct
+    clash _ _ = Incomparable
 
     findN : Nat -> Term vars -> Bool
     findN i (Local _ _ i' _) = i == i'
@@ -60,7 +61,10 @@ conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
     conflictTm tm tm'
         = let (f, args) = getFnArgs tm
               (f', args') = getFnArgs tm' in
-          clash f f' || any (uncurry conflictTm) (zip args args')
+          case clash f f' of
+            Distinct => True
+            Incomparable => False
+            Same => (any (uncurry conflictTm) (zip args args'))
 
     conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
     conflictArgs n tm [] = False
@@ -107,13 +111,12 @@ conflict defs env nfty n
       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
+          -- put possible
           = 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))])
+          = pure (Just [(n, !(quote defs env nf))])
       conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
           = if t == t'
                then conflictArgs i (map snd args) (map snd args')

src/TTImp/ProcessDef.idr

@@ -1118,7 +1118,9 @@ processDef opts nest env fc n_in cs_in
                               pure (Just rtm))
                (\err => do defs <- get Ctxt
                            if not !(recoverableErr defs err)
-                              then pure Nothing
+                              then do
+                                log "declare.def.impossible" 5 "impossible because \{show err}"
+                                pure Nothing
                               else pure (Just tm))
       where
         closeEnv : Defs -> NF [] -> Core ClosedTerm

tests/idris2/coverage/coverage022/Issue3477.idr

@@ -0,0 +1,2 @@
+test : (xs : List Int) ->  2 = length xs -> (Int, Int)
+test (x1 :: x2 :: x3 :: []) pf = (x1, x2)

tests/idris2/coverage/coverage022/expected

@@ -0,0 +1,10 @@
+1/1: Building Issue3477 (Issue3477.idr)
+Error: test is not covering.
+
+Issue3477:1:1--1:55
+ 1 | test : (xs : List Int) ->  2 = length xs -> (Int, Int)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    test [_, _] _
+

tests/idris2/coverage/coverage022/run

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