2c609ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commit2c609ae2c1b2ffced953e6526ac1a12c556abfa0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 May 2015, 21:43 (11 years ago) parentcfb1016

3 files changed+13−8

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+4−3 src/Idris/Core/TT.hs+1−1 src/Idris/Elab/Term.hs+8−4

src/Idris/Core/Elaborate.hs+4−3

@@ -501,7 +501,8 @@ prepare_apply fn imps =

501501 env <- get_env

502502 -- let claims = getArgs ty imps

503503 -- claims <- mkClaims (normalise ctxt env ty) imps []

504− claims <- mkClaims (finalise ty)

504+ claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

505+ mkClaims (finalise ty)

505506 (normalise ctxt env (finalise ty))

506507 imps [] (map fst env)

507508 ES (p, a) s prev <- get

@@ -522,8 +523,8 @@ prepare_apply fn imps =

522523 n <- getNameFrom (mkMN n')

523524-- when (null claims) (start_unify n)

524525 let sc' = instantiate (P Bound n t) sc

525−-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

526− claim n (forget t)

526+ env <- get_env

527+ claim n (forgetEnv (map fst env) t)

527528 when i (movelast n)

528529 mkClaims sc' scn is ((n', n) : claims) hs

529530 -- if we run out of arguments, we need the normalised version...

src/Idris/Core/TT.hs+1−1

@@ -1258,7 +1258,7 @@ safeForget tm = safeForgetEnv [] tm

12581258forgetEnv :: [Name] -> TT Name -> Raw

12591259forgetEnv env tm = case safeForgetEnv env tm of

12601260 Just t' -> t'

1261− Nothing -> error $ "Scope error in " ++ show tm

1261+ Nothing -> error $ "Scope error in " ++ show tm ++ show env

12621262

12631263

12641264safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

src/Idris/Elab/Term.hs+8−4

@@ -757,10 +757,14 @@ elab ist info emode opts fn tm

757757 (map (\x -> getTm x) args) -- TODO: remove this False arg

758758 imp <- if (e_isfn ina) then

759759 do guess <- get_guess

760− gty <- get_type (forget guess)

761760 env <- get_env

762− let ty_n = normalise ctxt env gty

763− return $ getReqImps ty_n

761+ case safeForgetEnv (map fst env) guess of

762+ Nothing ->

763+ return []

764+ Just rguess -> do

765+ gty <- get_type rguess

766+ let ty_n = normalise ctxt env gty

767+ return $ getReqImps ty_n

764768 else return []

765769 -- Now we find out how many implicits we needed at the

766770 -- end of the application by looking at the goal again

@@ -1250,7 +1254,7 @@ elab ist info emode opts fn tm

12501254 where

12511255 -- just one level at a time

12521256 addLam (Bind n (Pi (Just _) _ _) sc) t =

1253− do impn <- unique_hole (sMN 0 "imp")

1257+ do impn <- unique_hole n -- (sMN 0 "scoped_imp")

12541258 if e_isfn ina -- apply to an implicit immediately

12551259 then return (PApp emptyFC

12561260 (PLam emptyFC impn NoFC Placeholder t)