@@ -18,7 +18,7 @@ import Idris.Core.ProofTerm (getProofTerm)
1818import Idris.Core.TT
1919import Idris.Core.Typecheck (check, converts, isType, recheck)
2020import Idris.Core.Unify
21−import Idris.Core.WHNF (whnf)
21+import Idris.Core.WHNF (whnf,whnfArgs)
2222import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
2323import Idris.Delaborate
2424import Idris.DSL
@@ -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
@@ -201,7 +201,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
201201 Nothing -> []
202202 Just ty -> checkArgs [] [] ty
203203 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
204− checkArgs env ns (Bind n (Pi _ t _) sc)
204+ checkArgs env ns (Bind n (Pi _ _ t _) sc)
205205 = let env' = case t of
206206 TType _ -> n : env
207207 _ -> env in
@@ -227,7 +227,7 @@ goal_polymorphic =
227227 do ty <- goal
228228 case ty of
229229 P _ n _ -> do env <- get_env
230− case lookup n env of
230+ case lookupBinder n env of
231231 Nothing -> return False
232232 _ -> return True
233233 _ -> return False
@@ -245,23 +245,30 @@ elab :: IState
245245elab ist info emode opts fn tm
246246 = do let loglvl = opt_logLevel (idris_options ist)
247247 when (loglvl > 5) $ unifyLog True
248− compute -- expand type synonyms, etc
248+ whnf_compute_args -- expand type synonyms, etc
249249 let fc = maybe "(unknown)"
250250 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
251251 est <- getAux
252252 sequence_ (get_delayed_elab est)
253253 end_unify
254+ when (pattern || intransform) $
255+ -- convert remaining holes to pattern vars
256+ do unify_all
257+ matchProblems False -- only the ones we matched earlier
258+ unifyProblems
259+ mkPat
260+ update_term liftPats
254261 ptm <- get_term
255− when (pattern || intransform) -- convert remaining holes to pattern vars
256− (do unify_all
257− matchProblems False -- only the ones we matched earlier
258− unifyProblems
259− mkPat
260− update_term liftPats)
262+ when pattern $
263+ -- Look for Rig1 (linear) pattern bindings
264+ do let pnms = findLinear ist [] ptm
265+ update_term (setLinear pnms)
261266 where
262− pattern = emode == ELHS
267+ pattern = emode == ELHS || emode == EImpossible
268+ eimpossible = emode == EImpossible
263269 intransform = emode == ETransLHS
264270 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
271+ || emode == EImpossible
265272 autoimpls = opt_autoimpls (idris_options ist)
266273
267274 get_delayed_elab est =
@@ -293,7 +300,7 @@ elab ist info emode opts fn tm
293300
294301 -- | elabE elaborates an expression, possibly wrapping implicit coercions
295302 -- and forces/delays. If you make a recursive call in elab', it is
296− -- normally correct to call elabE - the ones that don't are desugarings
303+ -- normally correct to call elabE - the ones that don't are `desugarings
297304 -- typically
298305 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
299306 elabE ina fc' t =
@@ -332,13 +339,13 @@ elab ist info emode opts fn tm
332339 pexp ct]))
333340
334341 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
335− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
342+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
336343 ht == txt "Delayed" = notDelay orig
337344 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
338− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
345+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t'),
339346 ht == txt "Delayed" = notDelay orig
340347 forceErr orig env (InfiniteUnify _ t _)
341− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
348+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
342349 ht == txt "Delayed" = notDelay orig
343350 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
344351 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
@@ -349,7 +356,7 @@ elab ist info emode opts fn tm
349356 notDelay _ = True
350357
351358 local f = do e <- get_env
352− return (f `elem` map fst e)
359+ return (f `elem` map fstEnv e)
353360
354361 -- | Is a constant a type?
355362 constType :: Const -> Bool
@@ -370,7 +377,10 @@ elab ist info emode opts fn tm
370377 solve
371378 highlightSource fc' (AnnType "Type" "The type of types")
372379 elab' ina fc (PUniverse fc' u) =
373− do apply (RUType u) []
380+ do unless (UniquenessTypes `elem` idris_language_extensions ist
381+ || e_qq ina) $
382+ lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")
383+ apply (RUType u) []
374384 solve
375385 highlightSource fc' (AnnType (show u) "The type of unique types")
376386-- elab' (_,_,inty) (PConstant c)
@@ -387,7 +397,7 @@ elab ist info emode opts fn tm
387397 highlightSource fc' (AnnConst c)
388398 elab' ina fc (PQuote r) = do fill r; solve
389399 elab' ina _ (PTrue fc _) =
390− do compute
400+ do whnf_compute
391401 g <- goal
392402 case g of
393403 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
@@ -421,7 +431,7 @@ elab ist info emode opts fn tm
421431 pexp l, pexp r]))
422432
423433 elab' ina _ (PPair fc hls _ l r)
424− = do compute
434+ = do whnf_compute
425435 g <- goal
426436 let (tc, _) = unApply g
427437 case g of
@@ -444,7 +454,7 @@ elab ist info emode opts fn tm
444454 IsType -> asType
445455 IsTerm -> asValue
446456 TypeOrTerm ->
447− do compute
457+ do whnf_compute
448458 g <- goal
449459 case g of
450460 TType _ -> asType
@@ -498,11 +508,13 @@ elab ist info emode opts fn tm
498508 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
499509
500510 doPrune as =
501− do compute
511+ do compute -- to get 'Delayed' if it's there
502512 ty <- goal
503− let (tc, _) = unApply (unDelay ty)
513+ ctxt <- get_context
504514 env <- get_env
505− return $ pruneByType env tc (unDelay ty) ist as
515+ let ty' = unDelay ty
516+ let (tc, _) = unApply ty'
517+ return $ pruneByType eimpossible env tc ty' ist as
506518
507519 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
508520 l == txt "Delayed" = unDelay arg
@@ -532,7 +544,7 @@ elab ist info emode opts fn tm
532544 (trySeq' deferr xs) True
533545 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
534546 env <- get_env
535− compute
547+ whnf_compute
536548 ty <- goal
537549 let doelab = elab' ina fc orig
538550 tryCatch doelab
@@ -564,7 +576,7 @@ elab ist info emode opts fn tm
564576 recoverableErr _ = True
565577
566578 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
567− = case unApply (normalise (tt_ctxt ist) env inc) of
579+ = case unApply (whnf (tt_ctxt ist) env inc) of
568580 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts
569581 (Constant _, _) -> alts
570582 _ -> filter isLend alts -- special case hack for 'Borrowed'
@@ -656,7 +668,7 @@ elab ist info emode opts fn tm
656668 do fty <- get_type (Var n) -- check for implicits
657669 ctxt <- get_context
658670 env <- get_env
659− let a' = insertScopedImps fc (normalise ctxt env fty) []
671+ let a' = insertScopedImps fc (whnfArgs ctxt env fty) []
660672 if null a'
661673 then erun fc $
662674 do apply (Var n) []
@@ -698,19 +710,30 @@ elab ist info emode opts fn tm
698710 solve
699711 highlightSource nfc (AnnBoundName n False)
700712 elab' ina fc (PPi p n nfc Placeholder sc)
701− = do attack; arg n (is_scoped p) (sMN 0 "ty")
713+ = do attack;
714+ case pcount p of
715+ RigW -> return ()
716+ _ -> unless (LinearTypes `elem` idris_language_extensions ist
717+ || e_qq ina) $
718+ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a count")
719+ arg n (pcount p) (is_scoped p) (sMN 0 "phTy")
702720 addAutoBind p n
703721 addPSname n -- okay for proof search
704722 elabE (ina { e_inarg = True, e_intype = True }) fc sc
705723 solve
706724 highlightSource nfc (AnnBoundName n False)
707725 elab' ina fc (PPi p n nfc ty sc)
708− = do attack; tyn <- getNameFrom (sMN 0 "ty")
726+ = do attack; tyn <- getNameFrom (sMN 0 "piTy")
709727 claim tyn RType
710728 n' <- case n of
711729 MN _ _ -> unique_hole n
712730 _ -> return n
713− forall n' (is_scoped p) (Var tyn)
731+ case pcount p of
732+ RigW -> return ()
733+ _ -> unless (LinearTypes `elem` idris_language_extensions ist
734+ || e_qq ina) $
735+ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")
736+ forall n' (pcount p) (is_scoped p) (Var tyn)
714737 addAutoBind p n'
715738 addPSname n' -- okay for proof search
716739 focus tyn
@@ -753,7 +776,7 @@ elab ist info emode opts fn tm
753776 (ivs' \\ ivs)
754777 -- HACK: If the name leaks into its type, it may leak out of
755778 -- scope outside, so substitute in the outer scope.
756− expandLet n (case lookup n env of
779+ expandLet n (case lookupBinder n env of
757780 Just (Let t v) -> v
758781 other -> error ("Value not a let binding: " ++ show other))
759782 solve
@@ -803,10 +826,10 @@ elab ist info emode opts fn tm
803826 ans <- claimArgTys env xs
804827 return ((aval, (True, (Var an))) : ans)
805828 fnTy [] ret = forget ret
806− fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)
829+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi RigW Nothing xt RType) (fnTy xs ret)
807830
808831 localVar env (PRef _ _ x)
809− = case lookup x env of
832+ = case lookupBinder x env of
810833 Just _ -> Just x
811834 _ -> Nothing
812835 localVar env _ = Nothing
@@ -840,7 +863,7 @@ elab ist info emode opts fn tm
840863 let dataCon = isDConName f ctxt
841864 annot <- findHighlight f
842865 mapM_ checkKnownImplicit args_in
843− let args = insertScopedImps fc (normalise ctxt env fty) args_in
866+ let args = insertScopedImps fc (whnfArgs ctxt env fty) args_in
844867 let unmatchableArgs = if pattern
845868 then getUnmatchable (tt_ctxt ist) f
846869 else []
@@ -849,7 +872,7 @@ elab ist info emode opts fn tm
849872 && isTConName f (tt_ctxt ist)) $
850873 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
851874-- trace (show (f, args_in, args)) $
852− if (f `elem` map fst env && length args == 1 && length args_in == 1)
875+ if (f `elem` map fstEnv env && length args == 1 && length args_in == 1)
853876 then -- simple app, as below
854877 do simple_app False
855878 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
@@ -897,12 +920,12 @@ elab ist info emode opts fn tm
897920 imp <- if (e_isfn ina) then
898921 do guess <- get_guess
899922 env <- get_env
900− case safeForgetEnv (map fst env) guess of
923+ case safeForgetEnv (map fstEnv env) guess of
901924 Nothing ->
902925 return []
903926 Just rguess -> do
904927 gty <- get_type rguess
905− let ty_n = normalise ctxt env gty
928+ let ty_n = whnf ctxt env gty
906929 return $ getReqImps ty_n
907930 else return []
908931 -- Now we find out how many implicits we needed at the
@@ -950,16 +973,16 @@ elab ist info emode opts fn tm
950973 = lift $ tfail $ UnknownImplicit (pname imp) f
951974 checkKnownImplicit _ = return ()
952975
953− getReqImps (Bind x (Pi (Just i) ty _) sc)
976+ getReqImps (Bind x (Pi _ (Just i) ty _) sc)
954977 = i : getReqImps sc
955978 getReqImps _ = []
956979
957980 checkIfInjective n = do
958981 env <- get_env
959− case lookup n env of
982+ case lookupBinder n env of
960983 Nothing -> return ()
961984 Just b ->
962− case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
985+ case unApply (whnf (tt_ctxt ist) env (binderTy b)) of
963986 (P _ c _, args) ->
964987 case lookupCtxtExact c (idris_interfaces ist) of
965988 Nothing -> return ()
@@ -1032,6 +1055,9 @@ elab ist info emode opts fn tm
10321055 elab' ina fc (PElabError e) = lift $ tfail e
10331056 elab' ina mfc (PRewrite fc substfn rule sc newg)
10341057 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
1058+ -- A common error case if trying to typecheck an autogenerated case block
1059+ elab' ina _ c@(PCase fc Placeholder opts)
1060+ = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")
10351061 elab' ina _ c@(PCase fc scr opts)
10361062 = do attack
10371063
@@ -1069,13 +1095,13 @@ elab ist info emode opts fn tm
10691095 -- unnecessarily (can only do this for unique things, since we
10701096 -- assume they don't appear implicitly in types)
10711097 ptm <- get_term
1072− let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
1098+ let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
10731099
10741100 let argsDropped = filter (isUnique envU)
10751101 (nub $ allNamesIn scr ++ inApp ptm ++
10761102 inOpts)
10771103
1078− let args' = filter (\(n, _) -> n `notElem` argsDropped) args
1104+ let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args
10791105
10801106 attack
10811107 cname' <- defer argsDropped (mkN (mkCaseName fc fn))
@@ -1126,8 +1152,8 @@ elab ist info emode opts fn tm
11261152 Just u -> u
11271153 _ -> False
11281154
1129− getKind env (n, _)
1130− = case lookup n env of
1155+ getKind env (n, _, _)
1156+ = case lookupBinder n env of
11311157 Nothing -> return (n, False) -- can't happen, actually...
11321158 Just b ->
11331159 do ty <- get_type (forget (binderTy b))
@@ -1210,13 +1236,13 @@ elab ist info emode opts fn tm
12101236 loadState
12111237 updateAux (\aux -> aux { highlighting = hs })
12121238
1213− let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
1239+ let quoted = fmap (explicitNames . binderVal) $ lookupBinder nTm env
12141240 isRaw = case unApply (normaliseAll ctxt env finalTy) of
12151241 (P _ n _, []) | n == reflm "Raw" -> True
12161242 _ -> False
12171243 case quoted of
12181244 Just q -> do ctxt <- get_context
1219− (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
1245+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, RigW, Lam RigW Erased) | uq <- unquoteNames] (forget q) q
12201246 if pattern
12211247 then if isRaw
12221248 then reflectRawQuotePattern unquoteNames (forget q')
@@ -1245,7 +1271,7 @@ elab ist info emode opts fn tm
12451271 elab' ina fc (PQuoteName n True nfc) =
12461272 do ctxt <- get_context
12471273 env <- get_env
1248− case lookup n env of
1274+ case lookupBinder n env of
12491275 Just _ -> do fill $ reflectName n
12501276 solve
12511277 highlightSource nfc (AnnBoundName n False)
@@ -1274,7 +1300,9 @@ elab ist info emode opts fn tm
12741300 dotterm
12751301 elab' ina fc t
12761302 elab' ina fc (PRunElab fc' tm ns) =
1277− do attack
1303+ do unless (ElabReflection `elem` idris_language_extensions ist) $
1304+ lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
1305+ attack
12781306 n <- getNameFrom (sMN 0 "tacticScript")
12791307 let scriptTy = RApp (Var (sNS (sUN "Elab")
12801308 ["Elab", "Reflection", "Language"]))
@@ -1312,7 +1340,7 @@ elab ist info emode opts fn tm
13121340 env <- get_env
13131341 ctxt <- get_context
13141342 let v = fmap (normaliseAll ctxt env . finalise . binderVal)
1315− (lookup n env)
1343+ (lookupBinder n env)
13161344 loadState -- we have the highlighting - re-elaborate the value
13171345 elab' ina fc tm
13181346 case v of
@@ -1335,9 +1363,9 @@ elab ist info emode opts fn tm
13351363 delayElab pri t
13361364 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
13371365
1338− isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1339− isScr (PRef _ _ n) (n', b) = (n', (n == n', b))
1340− isScr _ (n', b) = (n', (False, b))
1366+ isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))
1367+ isScr (PRef _ _ n) (n', _, b) = (n', (n == n', b))
1368+ isScr _ (n', _, b) = (n', (False, b))
13411369
13421370 caseBlock :: FC -> Name
13431371 -> PTerm -- original scrutinee
@@ -1437,8 +1465,8 @@ elab ist info emode opts fn tm
14371465 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)
14381466 mkDelay env t
14391467 = let fc = fileFC "Delay" in
1440− addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))
1441− [pexp t])
1468+ addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] (sUN "Delay"))
1469+ [pexp t])
14421470
14431471
14441472 -- Don't put implicit coercions around applications which are marked
@@ -1463,7 +1491,7 @@ elab ist info emode opts fn tm
14631491 case fullApp tm of
14641492 -- if f is global, leave it alone because we've already
14651493 -- expanded it to the right arity
1466− PApp fc ftm@(PRef _ _ f) args | Just aty <- lookup f env ->
1494+ PApp fc ftm@(PRef _ _ f) args | Just aty <- lookupBinder f env ->
14671495 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))
14681496 return (mkPApp fc a ftm args)
14691497 _ -> return tm
@@ -1472,12 +1500,12 @@ elab ist info emode opts fn tm
14721500 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
14731501 fullApp x = x
14741502
1475− insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1503+ insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs
14761504 | tcimplementation i && not (toplevel_imp i)
14771505 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
14781506 | not (toplevel_imp i)
14791507 = pimp n Placeholder True : insertScopedImps fc sc xs
1480− insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
1508+ insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)
14811509 = x : insertScopedImps fc sc xs
14821510 insertScopedImps _ _ xs = xs
14831511
@@ -1488,7 +1516,7 @@ elab ist info emode opts fn tm
14881516 addLam ty' t
14891517 where
14901518 -- just one level at a time
1491− addLam (Bind n (Pi (Just _) _ _) sc) t =
1519+ addLam (Bind n (Pi _ (Just _) _ _) sc) t =
14921520 do impn <- unique_hole n -- (sMN 0 "scoped_imp")
14931521 if e_isfn ina -- apply to an implicit immediately
14941522 then return (PApp emptyFC
@@ -1516,7 +1544,7 @@ elab ist info emode opts fn tm
15161544 mkCoerce env (PAlternative ms aty tms) n
15171545 = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
15181546 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
1519− addImplBound ist (map fst env)
1547+ addImplBound ist (map fstEnv env)
15201548 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
15211549
15221550 -- | Elaborate the arguments to a function
@@ -1575,7 +1603,7 @@ elab ist info emode opts fn tm
15751603 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
15761604
15771605 addAutoBind :: Plicity -> Name -> ElabD ()
1578− addAutoBind (Imp _ _ _ _ False) n
1606+ addAutoBind (Imp _ _ _ _ False _) n
15791607 = updateAux (\est -> est { auto_binds = n : auto_binds est })
15801608 addAutoBind _ _ = return ()
15811609
@@ -1625,17 +1653,17 @@ pruneAlt xs = map prune xs
16251653
16261654-- Rule out alternatives that don't return the same type as the head of the goal
16271655-- (If there are none left as a result, do nothing)
1628−pruneByType :: Env -> Term -> -- head of the goal
1656+pruneByType :: Bool -> Env -> Term -> -- head of the goal
16291657 Type -> -- goal
16301658 IState -> [PTerm] -> [PTerm]
16311659-- if an alternative has a locally bound name at the head, take it
1632−pruneByType env t goalty c as
1660+pruneByType imp env t goalty c as
16331661 | Just a <- locallyBound as = [a]
16341662 where
16351663 locallyBound [] = Nothing
16361664 locallyBound (t:ts)
16371665 | Just n <- getName t,
1638− n `elem` map fst env = Just t
1666+ n `elem` map fstEnv env = Just t
16391667 | otherwise = locallyBound ts
16401668 getName (PRef _ _ n) = Just n
16411669 getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
@@ -1645,7 +1673,7 @@ pruneByType env t goalty c as
16451673 getName _ = Nothing
16461674
16471675-- 'n' is the name at the head of the goal type
1648−pruneByType env (P _ n _) goalty ist as
1676+pruneByType imp env (P _ n _) goalty ist as
16491677-- if the goal type is polymorphic, keep everything
16501678 | Nothing <- lookupTyExact n ctxt = as
16511679-- if the goal type is a ?metavariable, keep everything
@@ -1677,12 +1705,13 @@ pruneByType env (P _ n _) goalty ist as
16771705 Just ty -> case unApply (getRetTy ty) of
16781706 (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
16791707 -> False
1680− _ -> let ty' = normalise ctxt [] ty in
1681−-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $
1708+ _ -> let ty' = whnf ctxt [] ty in
1709+-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
1710+-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
16821711 case unApply (getRetTy ty') of
16831712 (V _, _) ->
16841713 isPlausible ist var env n ty
1685− _ -> matching (getRetTy ty') goalty
1714+ _ -> matchingTypes imp (getRetTy ty') goalty
16861715 || isCoercion (getRetTy ty') goalty
16871716-- May be useful to keep for debugging purposes for a bit:
16881717-- let res = matching (getRetTy ty') goalty in
@@ -1690,9 +1719,12 @@ pruneByType env (P _ n _) goalty ist as
16901719-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
16911720 _ -> False
16921721
1722+ matchingTypes True = matchingHead
1723+ matchingTypes False = matching
1724+
16931725 -- If the goal is a constructor, it must match the suggested function type
16941726 matching (P _ ctyn _) (P _ n' _)
1695− | isTConName n' ctxt = ctyn == n'
1727+ | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
16961728 | otherwise = True
16971729 -- Variables match anything
16981730 matching (V _) _ = True
@@ -1703,14 +1735,28 @@ pruneByType env (P _ n _) goalty ist as
17031735 matching (Bind n _ sc) _ = True
17041736 matching _ (Bind n _ sc) = True
17051737 -- If we hit a function name, it's a plausible match
1706− matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True
1707− matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True
1708− -- Otherwise, match the rest of the structure
1709− matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1738+ matching apl@(App _ _ _) apr@(App _ _ _)
1739+ | (P _ fl _, argsl) <- unApply apl,
1740+ (P _ fr _, argsr) <- unApply apr
1741+ = fl == fr && and (zipWith matching argsl argsr)
1742+ || (not (isConName fl ctxt && isConName fr ctxt))
1743+ -- If the application structures aren't easily comparable, it's a
1744+ -- plausible match
1745+ matching (App _ f a) (App _ f' a') = True
17101746 matching (TType _) (TType _) = True
17111747 matching (UType _) (UType _) = True
17121748 matching l r = l == r
17131749
1750+ -- In impossible-case mode, only look at the heads (this is to account for
1751+ -- the non type-directed case with 'impossible' - we'd be ruling out
1752+ -- too much and wouldn't find the mismatch we're looking for)
1753+ matchingHead apl@(App _ _ _) apr@(App _ _ _)
1754+ | (P _ fl _, argsl) <- unApply apl,
1755+ (P _ fr _, argsr) <- unApply apr,
1756+ isConName fl ctxt && isConName fr ctxt
1757+ = fl == fr
1758+ matchingHead _ _ = True
1759+
17141760 -- Return whether there is a possible coercion between the return type
17151761 -- of an alternative and the goal type
17161762 isCoercion rty gty | (P _ r _, _) <- unApply rty
@@ -1735,7 +1781,7 @@ pruneByType env (P _ n _) goalty ist as
17351781 _ -> False
17361782
17371783
1738−pruneByType _ t _ _ as = as
1784+pruneByType _ _ t _ _ as = as
17391785
17401786-- Could the name feasibly be the return type?
17411787-- If there is an interface constraint on the return type, and no implementation
@@ -1752,7 +1798,7 @@ isPlausible ist var env n ty
17521798 where
17531799 collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
17541800 (Maybe Name, [(Term, [Name])])
1755− collectConstraints env tcs (Bind n (Pi _ ty _) sc)
1801+ collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)
17561802 = let tcs' = case unApply ty of
17571803 (P _ c _, _) ->
17581804 case lookupCtxtExact c (idris_interfaces ist) of
@@ -1770,7 +1816,7 @@ isPlausible ist var env n ty
17701816findHighlight :: Name -> ElabD OutputAnnotation
17711817findHighlight n = do ctxt <- get_context
17721818 env <- get_env
1773− case lookup n env of
1819+ case lookupBinder n env of
17741820 Just _ -> return $ AnnBoundName n False
17751821 Nothing -> case lookupTyExact n ctxt of
17761822 Just _ -> return $ AnnName n Nothing Nothing Nothing
@@ -1790,7 +1836,7 @@ solveAuto ist fn ambigok (n, failc)
17901836 when (not isg) $
17911837 proofSearch' ist True ambigok 100 True Nothing fn [] [])
17921838 (lift $ Error (addLoc failc
1793− (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
1839+ (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env))))
17941840 return ()
17951841 where addLoc (FailContext fc f x : prev) err
17961842 = At fc (ElaboratingArg f x
@@ -1863,7 +1909,7 @@ case_ ind autoSolve ist fn tm = do
18631909 focus valn
18641910 elab ist toplevel ERHS [] (sMN 0 "tac") tm
18651911 env <- get_env
1866− let (Just binding) = lookup letn env
1912+ let (Just binding) = lookupBinder letn env
18671913 let val = binderVal binding
18681914 if ind then induction (forget val)
18691915 else casetac (forget val)
@@ -1886,7 +1932,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
18861932 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
18871933
18881934 patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
1889− patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
1935+ patvars ns (Bind n (PVar _ t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
18901936 patvars ns tm = (ns, tm)
18911937
18921938 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
@@ -1955,7 +2001,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
19552001
19562002 -- | Add another argument to a Pi
19572003 mkPi :: RFunArg -> Raw -> Raw
1958− mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy
2004+ mkPi arg rTy = RBind (argName arg) (Pi RigW Nothing (argTy arg) (RUType AllTypes)) rTy
19592005
19602006 mustBeType ctxt tm ty =
19612007 case normaliseAll ctxt [] (finalise ty) of
@@ -2012,7 +2058,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20122058 _ -> n
20132059
20142060 getRetTy :: Type -> Type
2015− getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
2061+ getRetTy (Bind _ (Pi _ _ _ _) sc) = getRetTy sc
20162062 getRetTy ty = ty
20172063
20182064 elabScriptStuck :: Term -> ElabD a
@@ -2220,7 +2266,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22202266 = do ~[n, ty] <- tacTmArgs 2 tac args
22212267 n' <- reifyTTName n
22222268 ty' <- reifyRaw ty
2223− forall n' Nothing ty'
2269+ forall n' RigW Nothing ty'
22242270 returnUnit
22252271 | n == tacN "Prim__PatVar"
22262272 = do ~[n] <- tacTmArgs 1 tac args
@@ -2230,7 +2276,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22302276 | n == tacN "Prim__PatBind"
22312277 = do ~[n] <- tacTmArgs 1 tac args
22322278 n' <- reifyTTName n
2233− patbind n'
2279+ patbind n' RigW
22342280 returnUnit
22352281 | n == tacN "Prim__LetBind"
22362282 = do ~[n, ty, tm] <- tacTmArgs 3 tac args
@@ -2252,7 +2298,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22522298 = do ~[tm] <- tacTmArgs 1 tac args
22532299 tm' <- reifyTT tm
22542300 ctxt <- get_context
2255− fmap fst . checkClosed . reflect $ whnf ctxt tm'
2301+ fmap fst . checkClosed . reflect $ whnf ctxt [] tm'
22562302 | n == tacN "Prim__Converts"
22572303 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
22582304 env' <- reifyEnv env
@@ -2426,11 +2472,11 @@ runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
24262472runTac autoSolve ist perhapsFC fn tac
24272473 = do env <- get_env
24282474 g <- goal
2429− let tac' = fmap (addImplBound ist (map fst env)) tac
2475+ let tac' = fmap (addImplBound ist (map fstEnv env)) tac
24302476 if autoSolve
24312477 then runT tac'
24322478 else no_errors (runT tac')
2433− (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
2479+ (Just (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env)))
24342480 where
24352481 runT (Intro []) = do g <- goal
24362482 attack; intro (bname g)
@@ -2460,7 +2506,7 @@ runTac autoSolve ist perhapsFC fn tac
24602506 tryAll tacs
24612507 when autoSolve solveAll
24622508 where envArgs n = do e <- get_env
2463− case lookup n e of
2509+ case lookupBinder n e of
24642510 Just t -> return $ map (const False)
24652511 (getArgTys (binderTy t))
24662512 _ -> return []
@@ -2478,7 +2524,7 @@ runTac autoSolve ist perhapsFC fn tac
24782524 where isImp (PImp _ _ _ _ _) = True
24792525 isImp _ = False
24802526 envArgs n = do e <- get_env
2481− case lookup n e of
2527+ case lookupBinder n e of
24822528 Just t -> return $ map (const False)
24832529 (getArgTys (binderTy t))
24842530 _ -> return []
@@ -2587,9 +2633,9 @@ runTac autoSolve ist perhapsFC fn tac
25872633 where tacticTy = Var (reflm "Tactic")
25882634 listTy = Var (sNS (sUN "List") ["List", "Prelude"])
25892635 scriptTy = (RBind (sMN 0 "__pi_arg")
2590− (Pi Nothing (RApp listTy envTupleType) RType)
2636+ (Pi RigW Nothing (RApp listTy envTupleType) RType)
25912637 (RBind (sMN 1 "__pi_arg")
2592− (Pi Nothing (Var $ reflm "TT") RType) tacticTy))
2638+ (Pi RigW Nothing (Var $ reflm "TT") RType) tacticTy))
25932639 runT (ByReflection tm) -- run the reflection function 'tm' on the
25942640 -- goal, then apply the resulting reflected Tactic
25952641 = do tgoal <- goal
@@ -2785,7 +2831,7 @@ processTacticDecls info steps =
27852831 mapM_ (addIBC . IBCDef . cn) ctors
27862832 ctxt <- getContext
27872833 let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)
2788− let typeInfo = TI (map cn ctors) False [] params []
2834+ let typeInfo = TI (map cn ctors) False [] params [] False
27892835 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
27902836 -- otherwise writing the IBC just fails silently!
27912837 updateIState $ \i -> i { idris_datatypes =
@@ -2826,15 +2872,16 @@ processTacticDecls info steps =
28262872 RClausesInstrs n cs ->
28272873 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
28282874 solveDeferred emptyFC n
2829− let lhss = map (\(_, lhs, _) -> lhs) cs
2875+ let lhss = map (\(ns, lhs, _) -> (map fst ns, lhs)) cs
28302876 let fc = fileFC "elab_reflected"
28312877 pmissing <-
28322878 do ist <- getIState
28332879 possible <- genClauses fc n lhss
2834− (map (\lhs ->
2880+ (map (\ (ns, lhs) ->
28352881 delab' ist lhs True True) lhss)
28362882 missing <- filterM (checkPossible n) possible
2837− return (filter (noMatch ist lhss) missing)
2883+ let undef = filter (noMatch ist (map snd lhss)) missing
2884+ return undef
28382885 let tot = if null pmissing
28392886 then Unchecked -- still need to check recursive calls
28402887 else Partial NotCovering -- missing cases implies not total
@@ -2871,16 +2918,16 @@ processTacticDecls info steps =
28712918 where
28722919 -- TODO: see if the code duplication with Idris.Elab.Clause can be
28732920 -- reduced or eliminated.
2921+ -- These are always cases generated by genClauses
28742922 checkPossible :: Name -> PTerm -> Idris Bool
28752923 checkPossible fname lhs_in =
28762924 do ctxt <- getContext
28772925 ist <- getIState
28782926 let lhs = addImplPat ist lhs_in
28792927 let fc = fileFC "elab_reflected_totality"
2880− let tcgen = False -- TODO: later we may support dictionary generation
28812928 case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
2882− (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
2883− (infTerm lhs))) of
2929+ (erun fc (buildTC ist info EImpossible [] fname (allNamesIn lhs_in)
2930+ (infTerm lhs))) of
28842931 OK (ElabResult lhs' _ _ _ _ _ name', _) ->
28852932 do -- not recursively calling here, because we don't
28862933 -- want to run infinitely many times
@@ -2890,9 +2937,7 @@ processTacticDecls info steps =
28902937 OK _ -> return True
28912938 err -> return False
28922939 -- if it's a recoverable error, the case may become possible
2893− Error err -> if tcgen then return (recoverableCoverage ctxt err)
2894− else return (validCoverageCase ctxt err ||
2895− recoverableCoverage ctxt err)
2940+ Error err -> return (recoverableCoverage ctxt err)
28962941
28972942
28982943 -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause