[ re #1632 ] (->) does not unify with any of TCon/Type/PrimVal

Author: gallais

src/TTImp/ProcessDef.idr

@@ -75,23 +75,36 @@ impossibleOK : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Defs -> NF vars -> NF vars -> Core Bool
 impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
-    = if xn == yn
-         then anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
-         else pure False
+    = if xn /= yn
+         then pure True
+         else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
 -- If it's a data constructor, any mismatch will do
 impossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
     = if xt /= yt
          then pure True
          else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
 impossibleOK defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)
-impossibleOK defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
+
+-- NPrimVal is apart from NDCon, NTCon, NBind, and NType
 impossibleOK defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
-impossibleOK defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure True
+impossibleOK defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
+impossibleOK defs (NPrimVal _ _) (NBind _ _ _ _) = pure True
+impossibleOK defs (NBind _ _ _ _) (NPrimVal _ _) = pure True
 impossibleOK defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure True
-impossibleOK defs (NTCon _ _ _ _ _) (NType _) = pure True
-impossibleOK defs (NType _) (NTCon _ _ _ _ _) = pure True
+impossibleOK defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure True
 impossibleOK defs (NPrimVal _ _) (NType _) = pure True
 impossibleOK defs (NType _) (NPrimVal _ _) = pure True
+
+-- NTCon is apart from NBind, and NType
+impossibleOK defs (NTCon _ _ _ _ _) (NBind _ _ _ _) = pure True
+impossibleOK defs (NBind _ _ _ _) (NTCon _ _ _ _ _) = pure True
+impossibleOK defs (NTCon _ _ _ _ _) (NType _) = pure True
+impossibleOK defs (NType _) (NTCon _ _ _ _ _) = pure True
+
+-- NBind is apart from NType
+impossibleOK defs (NBind _ _ _ _) (NType _) = pure True
+impossibleOK defs (NType _) (NBind _ _ _ _) = pure True
+
 impossibleOK defs x y = pure False
 
 export
@@ -133,6 +146,9 @@ recoverable defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure False
 -- Type constructor vs. type
 recoverable defs (NTCon _ _ _ _ _) (NType _) = pure False
 recoverable defs (NType _) (NTCon _ _ _ _ _) = pure False
+-- Type constructor vs. binder
+recoverable defs (NTCon _ _ _ _ _) (NBind _ _ _ _) = pure False
+recoverable defs (NBind _ _ _ _) (NTCon _ _ _ _ _) = pure False
 
 recoverable defs (NTCon _ _ _ _ _) _ = pure True
 recoverable defs _ (NTCon _ _ _ _ _) = pure True
@@ -155,6 +171,9 @@ recoverable defs (NApp _ (NRef _ f) fargs) (NApp _ (NRef _ g) gargs)
 
 -- PRIMITIVES
 recoverable defs (NPrimVal _ x) (NPrimVal _ y) = pure (x == y)
+-- primitive vs. binder
+recoverable defs (NPrimVal _ _) (NBind _ _ _ _) = pure False
+recoverable defs (NBind _ _ _ _) (NPrimVal _ _) = pure False
 
 -- OTHERWISE: no
 recoverable defs x y = pure False

tests/Main.idr

@@ -51,7 +51,7 @@ idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
        "coverage005", "coverage006", "coverage007", "coverage008",
        "coverage009", "coverage010", "coverage011", "coverage012",
        "coverage013", "coverage014", "coverage015", "coverage016",
-       "coverage017", "coverage018"]
+       "coverage017", "coverage018", "coverage019"]
 
 idrisTestsCasetree : TestPool
 idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing

tests/idris2/coverage001/expected

@@ -15,15 +15,3 @@ Vect2:8:1--8:21
      ^^^^^^^^^^^^^^^^^^^^
 
 1/1: Building Vect3 (Vect3.idr)
-Error: Impossible pattern gives an error:
-When unifying Nat and Vect ?n ?b.
-Mismatch between: Nat and Vect ?n ?b.
-
-Vect3:9:8--9:9
- 5 |      Nil  : Vect Z a
- 6 |      (::) : a -> Vect k a -> Vect (S k) a
- 7 | 
- 8 | zip : Vect n a -> Vect n b -> Vect n (a, b)
- 9 | zip [] Z impossible
-            ^
-

tests/idris2/coverage019/Issue1632.idr

@@ -0,0 +1,14 @@
+%default total
+
+data Command : Type -> Type where
+    Empty : Command ()
+    Pure : t -> Command t
+
+test : Command (List a) -> ()
+test (Pure x) = ()
+
+test2 : Command (a -> b) -> ()
+test2 (Pure x) = ()
+
+test3 : Command Type -> ()
+test3 (Pure x) = ()

tests/idris2/coverage019/expected

@@ -0,0 +1 @@
+1/1: Building Issue1632 (Issue1632.idr)

tests/idris2/coverage019/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --no-banner --console-width 0 --check Issue1632.idr