@@ -615,7 +615,7 @@ elab ist info emode opts fn tm
615615-- elab' (_, _, inty) (PRef fc f)
616616-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
617617-- = lift $ tfail (Msg "Typecase is not allowed")
618− elab' ec _ tm@(PRef fc hl n)
618+ elab' ec fc' tm@(PRef fc hls n)
619619 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
620620 && isTConName n (tt_ctxt ist)
621621 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
@@ -628,22 +628,24 @@ elab ist info emode opts fn tm
628628 guarded = e_guarded ec
629629 inty = e_intype ec
630630 ctxt <- get_context
631+ env <- get_env
631632
633+ -- If the name is defined, globally or locally, elaborate it
634+ -- as a reference, otherwise it might end up as a pattern var.
632635 let defined = case lookupTy n ctxt of
633− [] -> False
636+ [] -> case lookupTyEnv n env of
637+ Just _ -> True
638+ _ -> False
634639 _ -> True
635− -- this is to stop us resolve interfaces recursively
636− -- trace (show (n, guarded)) $
640+
641+ -- this is to stop us resolving interfaces recursively
637642 if (tcname n && ina && not intransform)
638643 then erun fc $
639644 do patvar n
640645 update_term liftPats
641646 highlightSource fc (AnnBoundName n False)
642− else if defined
643− then do apply (Var n) []
644− annot <- findHighlight n
645− solve
646− highlightSource fc annot
647+ else if defined -- finally, ordinary PRef elaboration
648+ then elabRef ec fc' fc hls n tm
647649 else try (do apply (Var n) []
648650 annot <- findHighlight n
649651 solve
@@ -664,19 +666,7 @@ elab ist info emode opts fn tm
664666 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
665667 | pattern && not reflection && not (e_qq ina) && e_nomatching ina
666668 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
667− | otherwise =
668− do fty <- get_type (Var n) -- check for implicits
669− ctxt <- get_context
670− env <- get_env
671− let a' = insertScopedImps fc (normalise ctxt env fty) []
672− if null a'
673− then erun fc $
674− do apply (Var n) []
675− hilite <- findHighlight n
676− solve
677− mapM_ (uncurry highlightSource) $
678− (fc, hilite) : map (\f -> (f, hilite)) hls
679− else elab' ina fc' (PApp fc tm [])
669+ | otherwise = elabRef ina fc' fc hls n tm
680670 elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
681671 elab' ina _ (PLam fc n nfc Placeholder sc)
682672 = do -- if n is a type constructor name, this makes no sense...
@@ -1512,14 +1502,14 @@ elab ist info emode opts fn tm
15121502 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
15131503 fullApp x = x
15141504
1515− insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs
1505+ insertScopedImps fc ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs
15161506 | tcimplementation i && not (toplevel_imp i)
15171507 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
15181508 | not (toplevel_imp i)
15191509 = pimp n Placeholder True : insertScopedImps fc sc xs
15201510 insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)
15211511 = x : insertScopedImps fc sc xs
1522− insertScopedImps _ _ xs = xs
1512+ insertScopedImps _ ty xs = xs
15231513
15241514 insertImpLam ina t =
15251515 do ty <- goal
@@ -1528,13 +1518,9 @@ elab ist info emode opts fn tm
15281518 addLam ty' t
15291519 where
15301520 -- just one level at a time
1531− addLam (Bind n (Pi _ (Just _) _ _) sc) t =
1521+ addLam goal@(Bind n (Pi _ (Just _) _ _) sc) t =
15321522 do impn <- unique_hole n -- (sMN 0 "scoped_imp")
1533− if e_isfn ina -- apply to an implicit immediately
1534− then return (PApp emptyFC
1535− (PLam emptyFC impn NoFC Placeholder t)
1536− [pexp Placeholder])
1537− else return (PLam emptyFC impn NoFC Placeholder t)
1523+ return (PLam emptyFC impn NoFC Placeholder t)
15381524 addLam _ t = return t
15391525
15401526 insertCoerce ina t@(PCase _ _ _) = return t
@@ -1559,6 +1545,21 @@ elab ist info emode opts fn tm
15591545 addImplBound ist (map fstEnv env)
15601546 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
15611547
1548+ elabRef :: ElabCtxt -> Maybe FC -> FC -> [FC] -> Name -> PTerm -> ElabD ()
1549+ elabRef ina fc' fc hls n tm =
1550+ do fty <- get_type (Var n) -- check for implicits
1551+ ctxt <- get_context
1552+ env <- get_env
1553+ let a' = insertScopedImps fc (normalise ctxt env fty) []
1554+ if null a'
1555+ then erun fc $
1556+ do apply (Var n) []
1557+ hilite <- findHighlight n
1558+ solve
1559+ mapM_ (uncurry highlightSource) $
1560+ (fc, hilite) : map (\f -> (f, hilite)) hls
1561+ else elab' ina fc' (PApp fc tm [])
1562+
15621563 -- | Elaborate the arguments to a function
15631564 elabArgs :: IState -- ^ The current Idris state
15641565 -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)