From 2c609ae2c1b2ffced953e6526ac1a12c556abfa0 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 18 May 2015 21:43:17 +0100 Subject: [PATCH] Environment fix in prepare_apply One for the "How did this ever work" files. When claiming a metavariable for a function argument, we need to take the current environment before called 'forget' so that names are correct. Fixes #2211 (Okay, I know how this worked before really: essentially it used an assumption which is violated by scoped implicits, so now no longer make that assumption.) --- src/Idris/Core/Elaborate.hs | 7 ++++--- src/Idris/Core/TT.hs | 2 +- src/Idris/Elab/Term.hs | 12 ++++++++---- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs index 970d94cf70..b574125878 100644 --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -501,7 +501,8 @@ prepare_apply fn imps = env <- get_env -- let claims = getArgs ty imps -- claims <- mkClaims (normalise ctxt env ty) imps [] - claims <- mkClaims (finalise ty) + claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $ + mkClaims (finalise ty) (normalise ctxt env (finalise ty)) imps [] (map fst env) ES (p, a) s prev <- get @@ -522,8 +523,8 @@ prepare_apply fn imps = n <- getNameFrom (mkMN n') -- when (null claims) (start_unify n) let sc' = instantiate (P Bound n t) sc --- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $ - claim n (forget t) + env <- get_env + claim n (forgetEnv (map fst env) t) when i (movelast n) mkClaims sc' scn is ((n', n) : claims) hs -- if we run out of arguments, we need the normalised version... diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs index d46c317961..b06dad7756 100644 --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -1258,7 +1258,7 @@ safeForget tm = safeForgetEnv [] tm forgetEnv :: [Name] -> TT Name -> Raw forgetEnv env tm = case safeForgetEnv env tm of Just t' -> t' - Nothing -> error $ "Scope error in " ++ show tm + Nothing -> error $ "Scope error in " ++ show tm ++ show env safeForgetEnv :: [Name] -> TT Name -> Maybe Raw diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs index b7c6aabc60..5ae5bace60 100644 --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -757,10 +757,14 @@ elab ist info emode opts fn tm (map (\x -> getTm x) args) -- TODO: remove this False arg imp <- if (e_isfn ina) then do guess <- get_guess - gty <- get_type (forget guess) env <- get_env - let ty_n = normalise ctxt env gty - return $ getReqImps ty_n + case safeForgetEnv (map fst env) guess of + Nothing -> + return [] + Just rguess -> do + gty <- get_type rguess + let ty_n = normalise ctxt env gty + return $ getReqImps ty_n else return [] -- Now we find out how many implicits we needed at the -- end of the application by looking at the goal again @@ -1250,7 +1254,7 @@ elab ist info emode opts fn tm where -- just one level at a time addLam (Bind n (Pi (Just _) _ _) sc) t = - do impn <- unique_hole (sMN 0 "imp") + do impn <- unique_hole n -- (sMN 0 "scoped_imp") if e_isfn ina -- apply to an implicit immediately then return (PApp emptyFC (PLam emptyFC impn NoFC Placeholder t)