d3660ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't pass used unique variables to metavars

We can't use them anyway, and the resulting application won't typecheck if we're not careful to remove them.

commitd3660ed9f6949975db44134be648e4407d433b9e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 26 Aug 2014, 11:45 (12 years ago) parentb591600

2 files changed+42−2

compare with master

unifiedsplit

src/Idris/Elab/Utils.hs+31 src/Idris/ElabTerm.hs+11−2

src/Idris/Elab/Utils.hs+31

@@ -13,6 +13,7 @@ import Idris.Core.Evaluate

1313import Idris.Core.Typecheck

1414

1515import Control.Applicative hiding (Const)

16+import Control.Monad.State

1617import Control.Monad

1718import Data.List

1819

@@ -205,3 +206,33 @@ paramNames args env (p : ps)

205206 else paramNames args env ps

206207 _ -> paramNames args env ps

207208 | otherwise = paramNames args env ps

209+

210+getUniqueUsed :: Context -> Term -> [Name]

211+getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

212+ where

213+ getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

214+ getUniq env us (Bind n b sc)

215+ = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

216+ OK (_, UType UniqueType) -> True

217+ OK (_, UType NullType) -> True

218+ OK (_, UType AllTypes) -> True

219+ _ -> False in

220+ do getUniqB env us b

221+ getUniq ((n,b):env) ((n, uniq):us) sc

222+ getUniq env us (App f a) = do getUniq env us f; getUniq env us a

223+ getUniq env us (V i)

224+ | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

225+ getUniq env us (P _ n _)

226+ | Just u <- lookup n us = if u then use n else return ()

227+ getUniq env us _ = return ()

228+

229+ use n = do ns <- get; put (n : ns)

230+

231+ getUniqB env us (Let t v) = do getUniq env us t; getUniq env us v

232+ getUniqB env us (Guess t v) = do getUniq env us t; getUniq env us v

233+ getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

234+ getUniqB env us (NLet t v) = do getUniq env us t; getUniq env us v

235+ getUniqB env us b = getUniq env us (binderTy b)

236+

237+

238+

src/Idris/ElabTerm.hs+11−2

@@ -17,6 +17,7 @@ import Idris.Core.Unify

1717import Idris.Core.Typecheck (check, recheck)

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

20+import Idris.Elab.Utils

2021import qualified Util.Pretty as U

2122

2223import Control.Applicative ((<$>))

@@ -629,8 +630,16 @@ elab ist info emode opts fn tm

629630 solve

630631 elab' ina Placeholder = do (h : hs) <- get_holes

631632 movelast h

632− elab' ina (PMetavar n) = let n' = mkN n in

633− do attack; defer [] n'; solve

633+ elab' ina (PMetavar n) =

634+ do ptm <- get_term

635+ -- When building the metavar application, leave out the unique

636+ -- names which have been used elsewhere in the term, since we

637+ -- won't be able to use them in the resulting application.

638+ let unique_used = getUniqueUsed (tt_ctxt ist) ptm

639+ let n' = mkN n

640+ attack

641+ defer unique_used n'

642+ solve

634643 where mkN n@(NS _ _) = n

635644 mkN n = case namespace info of

636645 Just xs@(_:_) -> sNS n xs