d6a3eae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Careful with shadowing when abstracting with

Specifically, need to lookup exact (i.e. fully qualified) names rather than unqualified names to make sure we don't accidentally think local names are global. Fixes #1147

commitd6a3eae5eb3a3095ee78f7afb6a7eec608411963 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 May 2014, 15:13 (12 years ago) parentf9827ac

2 files changed+6−4

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/ElabDecls.hs+4−2

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1620,8 +1620,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

16201620 where -- TODO THINK added niTacImp, but is it right?

16211621 ni env (PRef _ n)

16221622 | n `elem` vars && not (n `elem` env)

1623− = case lookupTy n (tt_ctxt ist) of

1624− [] -> [n]

1623+ = case lookupDefExact n (tt_ctxt ist) of

1624+ Nothing -> [n]

16251625 _ -> []

16261626 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

16271627 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

src/Idris/ElabDecls.hs+4−2

@@ -86,13 +86,14 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

8686 ctxt <- getContext

8787 i <- getIState

8888

89− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

89+ logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'

9090 ty' <- addUsingConstraints syn fc ty'

9191 ty' <- implicit info syn n ty'

9292

9393 let ty = addImpl i ty'

9494 inacc = inaccessibleArgs 0 ty

95− logLvl 3 $ show n ++ " type " ++ showTmImpls ty

95+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

96+ logLvl 5 $ show n ++ " type " ++ showTmImpls ty

9697 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

9798

9899 ((tyT, defer, is), log) <-

@@ -1671,6 +1672,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16711672 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

16721673 addDeferred def''

16731674 mapM_ (elabCaseBlock info opts) is

1675+ logLvl 5 ("Checked wval " ++ show wval')

16741676 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

16751677 let cwvaltyN = explicitNames cwvalty

16761678 let cwvalN = explicitNames cwval