@@ -138,12 +138,37 @@ buildTC ist info emode opts fn tm
138138 else return (tm, ds, is)
139139 where pattern = emode == ELHS
140140
141+-- return whether arguments of the given constructor name can be
142+-- matched on. If they're polymorphic and the type doesn't appear in the
143+-- return type, then no, otherwise yes.
144+getUnmatchable :: Context -> Name -> [Bool]
145+getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
146+ = case lookupTyExact n ctxt of
147+ Nothing -> []
148+ Just ty -> checkArgs [] [] ty
149+ where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
150+ checkArgs env ns (Bind n (Pi t _) sc)
151+ = let env' = case t of
152+ TType _ -> n : env
153+ _ -> env in
154+ checkArgs env' (intersect env (refsIn t) : ns)
155+ (instantiate (P Bound n t) sc)
156+ checkArgs env ns t
157+ = map (anyMissing (intersect env (refsIn t))) (reverse ns)
158+
159+ anyMissing tns [] = False
160+ anyMissing tns (x : xs) = not (x `elem` tns) || anyMissing tns xs
161+
162+getUnmatchable ctxt n = []
163+
141164data ElabCtxt = ElabCtxt { e_inarg :: Bool,
142165 e_guarded :: Bool,
143166 e_intype :: Bool,
144− e_qq :: Bool }
167+ e_qq :: Bool,
168+ e_nomatching :: Bool -- ^ can't pattern match
169+ }
145170
146−initElabCtxt = ElabCtxt False False False False
171+initElabCtxt = ElabCtxt False False False False False
147172
148173-- Returns the set of declarations we need to add to complete the definition
149174-- (most likely case blocks to elaborate)
@@ -268,6 +293,8 @@ elab ist info emode opts fn tm
268293 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
269294 && isTypeConst c
270295 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
296+ | pattern && e_nomatching ina
297+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
271298 | otherwise = do apply (RConstant c) []; solve
272299 elab' ina fc (PQuote r) = do fill r; solve
273300 elab' ina _ (PTrue fc _) =
@@ -365,10 +392,12 @@ elab ist info emode opts fn tm
365392-- elab' (_, _, inty) (PRef fc f)
366393-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
367394-- = lift $ tfail (Msg "Typecase is not allowed")
368− elab' ec _ (PRef fc n)
395+ elab' ec _ tm@(PRef fc n)
369396 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
370397 && isTConName n (tt_ctxt ist)
371398 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
399+ | pattern && e_nomatching ec
400+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
372401 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
373402 = do let ina = e_inarg ec
374403 guarded = e_guarded ec
@@ -395,6 +424,8 @@ elab ist info emode opts fn tm
395424 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
396425 && isTConName n (tt_ctxt ist)
397426 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
427+ | pattern && e_nomatching ina
428+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
398429 | otherwise = erun fc $ do apply (Var n) []; solve
399430 elab' ina fc (PLam n Placeholder sc)
400431 = do -- if n is a type constructor name, this makes no sense...
@@ -551,8 +582,14 @@ elab ist info emode opts fn tm
551582-- = lift $ tfail (Msg "Typecase is not allowed")
552583 -- if f is local, just do a simple_app
553584 elab' ina _ tm@(PApp fc (PRef _ f) args)
585+ | pattern && e_nomatching ina
586+ = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
587+ | otherwise
554588 = do env <- get_env
555589 ty <- goal
590+ let unmatchableArgs = if pattern
591+ then getUnmatchable (tt_ctxt ist) f
592+ else []
556593 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
557594 && isTConName f (tt_ctxt ist)) $
558595 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
@@ -589,7 +626,8 @@ elab ist info emode opts fn tm
589626 sortBy cmpArg (zip ns args)
590627 ulog <- getUnifyLog
591628 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
592− [] fc False f ns'
629+ [] fc False f
630+ (zip ns' (unmatchableArgs ++ repeat False))
593631 (f == sUN "Force")
594632 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
595633 solve
@@ -1004,21 +1042,21 @@ elab ist info emode opts fn tm
10041042 -> FC -- ^ Source location
10051043 -> Bool
10061044 -> Name -- ^ Name of the function being applied
1007− -> [(Name, Name)] -- ^ (Argument Name, Hole Name)
1045+ -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)
10081046 -> Bool -- ^ under a 'force'
1009− -> [PTerm] -- ^ (Laziness, argument)
1047+ -> [PTerm] -- ^ argument
10101048 -> ElabD ()
10111049 elabArgs ist ina failed fc retry f [] force _ = return ()
1012− elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)
1050+ elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)
10131051 = do hs <- get_holes
10141052 if holeName `elem` hs then
10151053 do focus holeName
10161054 case t of
10171055 Placeholder -> do movelast holeName
10181056 elabArgs ist ina failed fc r f ns force args
1019− _ -> elabArg argName holeName t
1057+ _ -> elabArg t
10201058 else elabArgs ist ina failed fc r f ns force args
1021− where elabArg argName holeName t =
1059+ where elabArg t =
10221060 do -- solveAutos ist fn False
10231061 now_elaborating fc f argName
10241062 wrapErr f argName $ do
@@ -1033,7 +1071,8 @@ elab ist info emode opts fn tm
10331071 g <- goal
10341072 ulog <- getUnifyLog
10351073 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1036− elab ina (Just fc) t; return failed
1074+ elab (ina { e_nomatching = unm }) (Just fc) t
1075+ return failed
10371076 done_elaborating_arg f argName
10381077 elabArgs ist ina failed fc r f ns force args
10391078 wrapErr f argName action =