@@ -442,6 +442,7 @@ elab ist info emode opts fn tm
442442-- trace (show (map showHd as')) $
443443 ty <- goal
444444 case as' of
445+ [] -> lift $ tfail $ NoValidAlts (map showHd as)
445446 [x] -> elab' ina fc x
446447 -- If there's options, try now, and if that fails, postpone
447448 -- to later.
@@ -458,18 +459,24 @@ elab ist info emode opts fn tm
458459 [x] -> elab' ina fc x
459460 _ -> tryAll (zip (map (elab' ina fc) as'')
460461 (map showHd as'')))
461− where showHd (PApp _ (PRef _ _ n) _) = n
462+ where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
463+ | l == txt "Delay" = showHd (getTm arg)
464+ showHd (PApp _ (PRef _ _ n) _) = n
462465 showHd (PRef _ _ n) = n
463466 showHd (PApp _ h _) = showHd h
464467 showHd x = NErased -- We probably should do something better than this here
465468
466469 doPrune as =
467− do hnf_compute
470+ do compute
468471 ty <- goal
469− let (tc, _) = unApply ty
472+ let (tc, _) = unApply (unDelay ty)
470473 env <- get_env
471474 return $ pruneByType env tc ist as
472475
476+ unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
477+ l == txt "Lazy'" = unDelay arg
478+ | otherwise = t
479+
473480
474481 isAmbiguous (CantResolveAlts _) = delayok
475482 isAmbiguous (Elaborating _ _ e) = isAmbiguous e
@@ -492,20 +499,21 @@ elab ist info emode opts fn tm
492499 solveAutos ist fn False) (trySeq' deferr xs) True
493500 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
494501 env <- get_env
502+ compute
495503 ty <- goal
496504 let doelab = elab' ina fc orig
497505 tryCatch doelab
498506 (\err ->
499507 if recoverableErr err
500508 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
501− -- show alts ++ "\n" ++
502− -- showQuick err) $
509+ -- show alts ++ "\n" ++
510+ -- showQuick err) $
503511 -- Prune the coercions so that only the ones
504512 -- with the right type to fix the error will be tried!
505513 case pruneAlts err alts env of
506514 [] -> lift $ tfail err
507− alts' ->
508− try' (elab' ina fc (PAlternative [] (ExactlyOne False) alts'))
515+ alts' -> do
516+ try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))
509517 (lift $ tfail err) -- take error from original if all fail
510518 True
511519 else lift $ tfail err)
@@ -529,8 +537,8 @@ elab ist info emode opts fn tm
529537 _ -> filter isLend alts -- special case hack for 'Borrowed'
530538 pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env
531539 pruneAlts (At _ e) alts env = pruneAlts e alts env
532− pruneAlts (NoValidAlts _) alts env = alts
533− pruneAlts _ alts _ = filter isLend alts
540+ pruneAlts (NoValidAlts as) alts env = alts
541+ pruneAlts err alts _ = filter isLend alts
534542
535543 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'
536544 hasArg n env (PApp _ (PRef _ _ a) _)
@@ -538,7 +546,8 @@ elab ist info emode opts fn tm
538546 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
539547 any (fnIs n) args
540548 Nothing -> False
541− hasArg n _ _ = False
549+ hasArg n env (PAlternative _ _ as) = any (hasArg n env) as
550+ hasArg n _ tm = False
542551
543552 isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]
544553 isLend _ = False
@@ -1376,7 +1385,7 @@ elab ist info emode opts fn tm
13761385 notImplicitable (PRef _ _ n)
13771386 | [opts] <- lookupCtxt n (idris_flags ist)
13781387 = NoImplicit `elem` opts
1379− notImplicitable (PAlternative _ (ExactlyOne _) as) = any notImplicitable as
1388+ notImplicitable (PAlternative _ _ as) = any notImplicitable as
13801389 -- case is tricky enough without implicit coercions! If they are needed,
13811390 -- they can go in the branches separately.
13821391 notImplicitable (PCase _ _ _) = True
@@ -1420,9 +1429,11 @@ elab ist info emode opts fn tm
14201429 (PCoerced tm, _) -> tm
14211430 (_, []) -> t
14221431 (_, cs) -> PAlternative [] TryImplicit
1423− (t : map (mkCoerce env t) cs)
1432+ (t : map (mkCoerce env t) cs)
14241433 return t'
14251434 where
1435+ mkCoerce env (PAlternative ms aty tms) n
1436+ = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
14261437 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
14271438 addImplBound ist (map fst env)
14281439 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
@@ -1520,6 +1531,8 @@ pruneByType env t c as
15201531 n `elem` map fst env = Just t
15211532 | otherwise = locallyBound ts
15221533 getName (PRef _ _ n) = Just n
1534+ getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
1535+ | l == txt "Delay" = getName (getTm arg)
15231536 getName (PApp _ f _) = getName f
15241537 getName (PHidden t) = getName t
15251538 getName _ = Nothing
@@ -1528,18 +1541,20 @@ pruneByType env t c as
15281541pruneByType env (P _ n _) ist as
15291542-- if the goal type is polymorphic, keep everything
15301543 | Nothing <- lookupTyExact n ctxt = as
1544+-- if the goal type is a ?metavariable, keep everything
1545+ | Just _ <- lookup n (idris_metavars ist) = as
15311546 | otherwise
15321547 = let asV = filter (headIs True n) as
15331548 as' = filter (headIs False n) as in
15341549 case as' of
1535− [] -> case asV of
1536− [] -> as
1537− _ -> asV
1550+ [] -> asV
15381551 _ -> as'
15391552 where
15401553 ctxt = tt_ctxt ist
15411554
15421555 headIs var f (PRef _ _ f') = typeHead var f f'
1556+ headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1557+ | l == txt "Delay" = headIs var f (getTm arg)
15431558 headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'
15441559 headIs var f (PApp _ f' _) = headIs var f f'
15451560 headIs var f (PPi _ _ _ _ sc) = headIs var f sc