@@ -45,7 +45,7 @@ import qualified Data.Set as S
4545import qualified Data.Text as T
4646import Debug.Trace
4747
48−data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
48+data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
4949 deriving Eq
5050
5151
@@ -143,7 +143,7 @@ build ist info emode opts fn tm
143143 if log /= ""
144144 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
145145 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
146− where pattern = emode == ELHS
146+ where pattern = emode == ELHS || emode == EImpossible
147147 tydecl = emode == ETyDecl
148148
149149 mkPat = do hs <- get_holes
@@ -189,7 +189,7 @@ buildTC ist info emode opts fn ns tm
189189 if (log /= "")
190190 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
191191 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
192− where pattern = emode == ELHS
192+ where pattern = emode == ELHS || emode == EImpossible
193193
194194-- | return whether arguments of the given constructor name can be
195195-- matched on. If they're polymorphic, no, unless the type has beed
@@ -259,9 +259,11 @@ elab ist info emode opts fn tm
259259 mkPat
260260 update_term liftPats)
261261 where
262− pattern = emode == ELHS
262+ pattern = emode == ELHS || emode == EImpossible
263+ eimpossible = emode == EImpossible
263264 intransform = emode == ETransLHS
264265 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
266+ || emode == EImpossible
265267 autoimpls = opt_autoimpls (idris_options ist)
266268
267269 get_delayed_elab est =
@@ -332,13 +334,13 @@ elab ist info emode opts fn tm
332334 pexp ct]))
333335
334336 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
335− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
337+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
336338 ht == txt "Delayed" = notDelay orig
337339 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
338− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
340+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t'),
339341 ht == txt "Delayed" = notDelay orig
340342 forceErr orig env (InfiniteUnify _ t _)
341− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
343+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
342344 ht == txt "Delayed" = notDelay orig
343345 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
344346 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
@@ -498,13 +500,13 @@ elab ist info emode opts fn tm
498500 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
499501
500502 doPrune as =
501− do compute -- to get 'Delayed' if it's there
503+ do whnf_compute -- to get 'Delayed' if it's there
502504 ty <- goal
503505 ctxt <- get_context
504506 env <- get_env
505− let ty' = normalise ctxt env (unDelay ty)
507+ let ty' = whnf ctxt env (unDelay ty)
506508 let (tc, _) = unApply ty'
507− return $ pruneByType env tc ty' ist as
509+ return $ pruneByType eimpossible env tc ty' ist as
508510
509511 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
510512 l == txt "Delayed" = unDelay arg
@@ -566,7 +568,7 @@ elab ist info emode opts fn tm
566568 recoverableErr _ = True
567569
568570 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
569− = case unApply (normalise (tt_ctxt ist) env inc) of
571+ = case unApply (whnf (tt_ctxt ist) env inc) of
570572 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts
571573 (Constant _, _) -> alts
572574 _ -> filter isLend alts -- special case hack for 'Borrowed'
@@ -842,7 +844,7 @@ elab ist info emode opts fn tm
842844 let dataCon = isDConName f ctxt
843845 annot <- findHighlight f
844846 mapM_ checkKnownImplicit args_in
845− let args = insertScopedImps fc (normalise ctxt env fty) args_in
847+ let args = insertScopedImps fc (whnfArgs ctxt env fty) args_in
846848 let unmatchableArgs = if pattern
847849 then getUnmatchable (tt_ctxt ist) f
848850 else []
@@ -904,7 +906,7 @@ elab ist info emode opts fn tm
904906 return []
905907 Just rguess -> do
906908 gty <- get_type rguess
907− let ty_n = normalise ctxt env gty
909+ let ty_n = whnf ctxt env gty
908910 return $ getReqImps ty_n
909911 else return []
910912 -- Now we find out how many implicits we needed at the
@@ -961,7 +963,7 @@ elab ist info emode opts fn tm
961963 case lookup n env of
962964 Nothing -> return ()
963965 Just b ->
964− case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
966+ case unApply (whnf (tt_ctxt ist) env (binderTy b)) of
965967 (P _ c _, args) ->
966968 case lookupCtxtExact c (idris_interfaces ist) of
967969 Nothing -> return ()
@@ -1627,11 +1629,11 @@ pruneAlt xs = map prune xs
16271629
16281630-- Rule out alternatives that don't return the same type as the head of the goal
16291631-- (If there are none left as a result, do nothing)
1630−pruneByType :: Env -> Term -> -- head of the goal
1632+pruneByType :: Bool -> Env -> Term -> -- head of the goal
16311633 Type -> -- goal
16321634 IState -> [PTerm] -> [PTerm]
16331635-- if an alternative has a locally bound name at the head, take it
1634−pruneByType env t goalty c as
1636+pruneByType imp env t goalty c as
16351637 | Just a <- locallyBound as = [a]
16361638 where
16371639 locallyBound [] = Nothing
@@ -1647,7 +1649,7 @@ pruneByType env t goalty c as
16471649 getName _ = Nothing
16481650
16491651-- 'n' is the name at the head of the goal type
1650−pruneByType env (P _ n _) goalty ist as
1652+pruneByType imp env (P _ n _) goalty ist as
16511653-- if the goal type is polymorphic, keep everything
16521654 | Nothing <- lookupTyExact n ctxt = as
16531655-- if the goal type is a ?metavariable, keep everything
@@ -1679,12 +1681,13 @@ pruneByType env (P _ n _) goalty ist as
16791681 Just ty -> case unApply (getRetTy ty) of
16801682 (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
16811683 -> False
1682− _ -> let ty' = normalise ctxt [] ty in
1683−-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $
1684+ _ -> let ty' = whnf ctxt [] ty in
1685+-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
1686+-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
16841687 case unApply (getRetTy ty') of
16851688 (V _, _) ->
16861689 isPlausible ist var env n ty
1687− _ -> matching (getRetTy ty') goalty
1690+ _ -> matchingTypes imp (getRetTy ty') goalty
16881691 || isCoercion (getRetTy ty') goalty
16891692-- May be useful to keep for debugging purposes for a bit:
16901693-- let res = matching (getRetTy ty') goalty in
@@ -1692,9 +1695,12 @@ pruneByType env (P _ n _) goalty ist as
16921695-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
16931696 _ -> False
16941697
1698+ matchingTypes True = matchingHead
1699+ matchingTypes False = matching
1700+
16951701 -- If the goal is a constructor, it must match the suggested function type
16961702 matching (P _ ctyn _) (P _ n' _)
1697− | isTConName n' ctxt = ctyn == n'
1703+ | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
16981704 | otherwise = True
16991705 -- Variables match anything
17001706 matching (V _) _ = True
@@ -1705,14 +1711,28 @@ pruneByType env (P _ n _) goalty ist as
17051711 matching (Bind n _ sc) _ = True
17061712 matching _ (Bind n _ sc) = True
17071713 -- If we hit a function name, it's a plausible match
1708− matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True
1709− matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True
1710− -- Otherwise, match the rest of the structure
1711− matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1714+ matching apl@(App _ _ _) apr@(App _ _ _)
1715+ | (P _ fl _, argsl) <- unApply apl,
1716+ (P _ fr _, argsr) <- unApply apr
1717+ = fl == fr && and (zipWith matching argsl argsr)
1718+ || (not (isConName fl ctxt && isConName fr ctxt))
1719+ -- If the application structures aren't easily comparable, it's a
1720+ -- plausible match
1721+ matching (App _ f a) (App _ f' a') = True
17121722 matching (TType _) (TType _) = True
17131723 matching (UType _) (UType _) = True
17141724 matching l r = l == r
17151725
1726+ -- In impossible-case mode, only look at the heads (this is to account for
1727+ -- the non type-directed case with 'impossible' - we'd be ruling out
1728+ -- too much and wouldn't find the mismatch we're looking for)
1729+ matchingHead apl@(App _ _ _) apr@(App _ _ _)
1730+ | (P _ fl _, argsl) <- unApply apl,
1731+ (P _ fr _, argsr) <- unApply apr,
1732+ isConName fl ctxt && isConName fr ctxt
1733+ = fl == fr
1734+ matchingHead _ _ = True
1735+
17161736 -- Return whether there is a possible coercion between the return type
17171737 -- of an alternative and the goal type
17181738 isCoercion rty gty | (P _ r _, _) <- unApply rty
@@ -1737,7 +1757,7 @@ pruneByType env (P _ n _) goalty ist as
17371757 _ -> False
17381758
17391759
1740−pruneByType _ t _ _ as = as
1760+pruneByType _ _ t _ _ as = as
17411761
17421762-- Could the name feasibly be the return type?
17431763-- If there is an interface constraint on the return type, and no implementation
@@ -2882,8 +2902,8 @@ processTacticDecls info steps =
28822902 let lhs = addImplPat ist lhs_in
28832903 let fc = fileFC "elab_reflected_totality"
28842904 case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
2885− (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
2886− (infTerm lhs))) of
2905+ (erun fc (buildTC ist info EImpossible [] fname (allNamesIn lhs_in)
2906+ (infTerm lhs))) of
28872907 OK (ElabResult lhs' _ _ _ _ _ name', _) ->
28882908 do -- not recursively calling here, because we don't
28892909 -- want to run infinitely many times