[ fix ] recoverability criteria

If the "can't convert" error arises from a mismatch between a type
constructor and a primitive value, it is not recoverable.

src/TTImp/ProcessDef.idr

@@ -107,20 +107,32 @@ recoverable : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF vars -> Core Bool
 -- Unlike the above, any mismatch will do
+
+-- TYPE CONSTRUCTORS
 recoverable defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
     = if xn /= yn
          then pure False
          else pure $ not !(anyM (mismatch defs) (zip xargs yargs))
+-- Type constructor vs. primitive type
+recoverable defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure False
+recoverable defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure False
+recoverable defs (NTCon _ _ _ _ _) _ = pure True
+
+-- DATA CONSTRUCTORS
 recoverable defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
     = if xt /= yt
          then pure False
          else pure $ not !(anyM (mismatch defs) (zip xargs yargs))
+recoverable defs (NDCon _ _ _ _ _) _ = pure True
+
+-- FUNCTION CALLS
 recoverable defs (NApp _ (NRef _ f) fargs) (NApp _ (NRef _ g) gargs)
     = pure True -- both functions; recoverable
-recoverable defs (NTCon _ _ _ _ _) _ = pure True
-recoverable defs (NDCon _ _ _ _ _) _ = pure True
+
+-- PRIMITIVES
 recoverable defs (NPrimVal _ x) (NPrimVal _ y) = pure (x == y)
-recoverable defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure False
+
+-- OTHERWISE: no
 recoverable defs x y = pure False
 
 export

tests/Main.idr

@@ -48,7 +48,7 @@ idrisTests = MkTestPool []
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
-       "coverage009", "coverage010",
+       "coverage009", "coverage010", "coverage011",
        -- Documentation strings
        "docs001", "docs002",
        -- Evaluator

tests/idris2/coverage011/Sing.idr

@@ -0,0 +1,13 @@
+module Sing
+
+%default total
+
+data Fing : Type -> Type where
+  StringFing : String -> Fing String
+  BoolFing : Bool -> Fing Bool
+
+stringFing : Fing String -> String
+stringFing (StringFing s) = s
+
+boolFing : Fing Bool -> Bool
+boolFing (BoolFing b) = b

tests/idris2/coverage011/expected

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

tests/idris2/coverage011/run

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