Better typecase check

Only allow matching on polymorphic arguments if they have been refined
to something concrete due to some other argument by the time they're
elaborated.

src/Idris/Delaborate.hs

@@ -263,7 +263,7 @@ pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
 pprintErr' i (WithFnType ty) =
   text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))
 pprintErr' i (CantMatch t) =
-  text "Can't match on " <+> annTm t (pprintTerm i (delab i t))
+  text "Can't match on" <+> annTm t (pprintTerm i (delab i t))
 pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
 pprintErr' i UniverseError = text "Universe inconsistency"
 pprintErr' i (UniqueError NullType n)

src/Idris/ElabTerm.hs

@@ -144,8 +144,8 @@ buildTC ist info emode opts fn tm
   where pattern = emode == ELHS
 
 -- return whether arguments of the given constructor name can be 
--- matched on. If they're polymorphic and the type doesn't appear in the
--- return type, then no, otherwise yes.
+-- matched on. If they're polymorphic, no, unless the type has beed made
+-- concrete by the time we get around to elaborating the argument.
 getUnmatchable :: Context -> Name -> [Bool]
 getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
    = case lookupTyExact n ctxt of
@@ -159,10 +159,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
                   checkArgs env' (intersect env (refsIn t) : ns) 
                             (instantiate (P Bound n t) sc)
         checkArgs env ns t
-            = map (anyMissing (intersect env (refsIn t))) (reverse ns)
-
-        anyMissing tns [] = False
-        anyMissing tns (x : xs) = not (x `elem` tns) || anyMissing tns xs
+            = map (not . null) (reverse ns)
 
 getUnmatchable ctxt n = []
 
@@ -175,6 +172,16 @@ data ElabCtxt = ElabCtxt { e_inarg :: Bool,
 
 initElabCtxt = ElabCtxt False False False False False
 
+goal_polymorphic :: ElabD Bool
+goal_polymorphic =
+   do ty <- goal
+      case ty of
+           P _ n _ -> do env <- get_env
+                         case lookup n env of
+                              Nothing -> return False
+                              _ -> return True
+           _ -> return False
+
 -- Returns the set of declarations we need to add to complete the definition
 -- (most likely case blocks to elaborate)
 
@@ -1098,9 +1105,11 @@ elab ist info emode opts fn tm
                               -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
                               do focus holeName;
                                  g <- goal
+                                 -- Can't pattern match on polymorphic goals
+                                 poly <- goal_polymorphic
                                  ulog <- getUnifyLog
                                  traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
-                                  elab (ina { e_nomatching = unm }) (Just fc) t
+                                  elab (ina { e_nomatching = unm && poly }) (Just fc) t
                                  return failed
                    done_elaborating_arg f argName
                    elabArgs ist ina failed fc r f ns force args

test/reg010/expected

@@ -1,2 +1,2 @@
 reg010.idr:5:15:When elaborating left hand side of with block in usubst.unsafeSubst:
-Can't match on  with block in usubst.unsafeSubst warg a P x x px
+Can't match on with block in usubst.unsafeSubst warg a P x x px

test/reg034/expected

@@ -1,4 +1,4 @@
 reg034.idr:6:5:When elaborating left hand side of bar:
-Can't match on  bar xs xs Refl
+Can't match on bar xs xs Refl
 reg034.idr:9:5:When elaborating left hand side of foo:
-Can't match on  foo f x x Refl
+Can't match on foo f x x Refl

test/reg055/expected

@@ -1,6 +1,9 @@
 reg055.idr:5:3:When elaborating left hand side of g:
-Can't match on  g (f 0)
+Can't match on g (f 0)
 reg055.idr:8:3:When elaborating left hand side of h:
-Can't match on  h x x
-reg055a.idr:10:7:When elaborating left hand side of Foo.apply:
-Can't match on  apply (\x => \y => x) a
+Can't match on h x x
+reg055a.idr:8:5:When elaborating left hand side of foo:
+When elaborating an application of constructor Foo.CAny:
+        Attempting concrete match on polymorphic argument: Nothing
+reg055a.idr:13:7:When elaborating left hand side of Foo.apply:
+Can't match on apply (\x => \y => x) a

test/reg055/reg055a.idr

@@ -1,10 +1,13 @@
 module Foo
 
--- data CrappySet : (a : Type) -> Ord a -> Type where
---   Empty : (inst : Ord a) -> CrappySet a inst
---   Item  : (inst : Ord a) -> a -> CrappySet a inst -> CrappySet a inst
--- 
--- empty : (inst : Ord a) => CrappySet a inst
+data Cheat : Type -> Type where
+     CAny : a -> Cheat a
+     CInt : Cheat Int
+
+foo : Cheat a -> Int
+foo (CAny Nothing) = 42 
+foo (CAny (Just x)) = 43 
+foo CInt = 0 
 
 apply : (a -> a -> b) -> a -> a
 apply (\x => \y => x) a = a