git.iko.soy/Idris-dev
on master help sign in
Ignore accessibility when rechecking
9546bd4Edwin Brady
src/Idris/Core/Evaluate.hs+6−3
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
12− lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
12+ lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 mapDefCtxt,
13 mapDefCtxt,
14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
@@ -1007,7 +1007,10 @@ isTCDict n ctxt
1007 _ -> False
1007 _ -> False
1008
1008
1009lookupP :: Name -> Context -> [Term]
1009lookupP :: Name -> Context -> [Term]
1010−lookupP n ctxt
1010+lookupP = lookupP_all False
1011+
1012+lookupP_all :: Bool -> Name -> Context -> [Term]
1013+lookupP_all all n ctxt
1011 = do def <- lookupCtxt n (definitions ctxt)
1014 = do def <- lookupCtxt n (definitions ctxt)
1012 p <- case def of
1015 p <- case def of
1013 (Function ty tm, a, _, _) -> return (P Ref n ty, a)
1016 (Function ty tm, a, _, _) -> return (P Ref n ty, a)
@@ -1015,7 +1018,7 @@ lookupP n ctxt
1015 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)
1018 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)
1016 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)
1019 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)
1017 case snd p of
1020 case snd p of
1018− Hidden -> []
1021+ Hidden -> if all then return (fst p) else []
1019 _ -> return (fst p)
1022 _ -> return (fst p)
1020
1023
1021lookupDefExact :: Name -> Context -> Maybe Def
1024lookupDefExact :: Name -> Context -> Maybe Def
src/Idris/Core/Typecheck.hs+4−1
@@ -81,7 +81,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
81 Env -> Raw -> StateT UCs TC (Term, Type)
81 Env -> Raw -> StateT UCs TC (Term, Type)
82 chk u env (Var n)
82 chk u env (Var n)
83 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
83 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
84+ -- If we're elaborating, we don't want the private names; if we're
85+ -- checking an already elaborated term, we do
86+ | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt
84− | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)
87+ = return (P nt n' ty, ty)
85 | otherwise = do lift $ tfail $ NoSuchVariable n
88 | otherwise = do lift $ tfail $ NoSuchVariable n
86 chk u env ap@(RApp f a)
89 chk u env ap@(RApp f a)
87 = do (fv, fty) <- chk u env f
90 = do (fv, fty) <- chk u env f