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

@@ -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...

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

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)