d6a3eae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Careful with shadowing when abstracting with

d6a3eaeEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+2−2

compare with master

unifiedsplit

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

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

1621 ni env (PRef _ n)

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

1623− = case lookupTy n (tt_ctxt ist) of

1623+ = case lookupDefExact n (tt_ctxt ist) of

1624− [] -> [n]

1624+ Nothing -> [n]

1625 _ -> []

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

1627 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

86 ctxt <- getContext

87 i <- getIState

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

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

90 ty' <- addUsingConstraints syn fc ty'

91 ty' <- implicit info syn n ty'

93 let ty = addImpl i ty'

94 inacc = inaccessibleArgs 0 ty

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

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

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

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

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

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

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

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

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

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

1672 addDeferred def''

1673 addDeferred def''

1673 mapM_ (elabCaseBlock info opts) is

1674 mapM_ (elabCaseBlock info opts) is

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

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

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

1675 let cwvaltyN = explicitNames cwvalty

1677 let cwvaltyN = explicitNames cwvalty

1676 let cwvalN = explicitNames cwval

1678 let cwvalN = explicitNames cwval