git.iko.soy/Idris-dev
on master help sign in
Lookup exact names in Typecheck

Fixes #2271. If there's ambiguities between names x and A.x, then 'x' can't be resolved directly, so if the typechecker encounters such an ambiguous name it should use assume the name is fully qualified. Normally names are expanded before calling the checker.

commitdcdfd8565eabbae0754f0d7e1dcfb43d4e4ddc9c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 May 2015, 14:44 (11 years ago) parent1b7359c
2 files changed+13−5
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+9−4 src/Idris/Core/Typecheck.hs+4−1
src/Idris/Core/Evaluate.hs+9−4
@@ -1007,11 +1007,11 @@ isTCDict n ctxt
10071007 _ -> False
10081008
10091009lookupP :: Name -> Context -> [Term]
1010−lookupP = lookupP_all False
1010+lookupP = lookupP_all False False
10111011
1012−lookupP_all :: Bool -> Name -> Context -> [Term]
1013−lookupP_all all n ctxt
1014− = do (n', def) <- lookupCtxtName n (definitions ctxt)
1012+lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
1013+lookupP_all all exact n ctxt
1014+ = do (n', def) <- names
10151015 p <- case def of
10161016 (Function ty tm, a, _, _) -> return (P Ref n' ty, a)
10171017 (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)
@@ -1020,6 +1020,11 @@ lookupP_all all n ctxt
10201020 case snd p of
10211021 Hidden -> if all then return (fst p) else []
10221022 _ -> return (fst p)
1023+ where
1024+ names = let ns = lookupCtxtName n (definitions ctxt) in
1025+ if exact
1026+ then filter (\ (n', d) -> n' == n) ns
1027+ else ns
10231028
10241029lookupDefExact :: Name -> Context -> Maybe Def
10251030lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
src/Idris/Core/Typecheck.hs+4−1
@@ -86,7 +86,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
8686 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
8787 -- If we're elaborating, we don't want the private names; if we're
8888 -- checking an already elaborated term, we do
89− | [P nt n' ty] <- lookupP_all (not holes) n ctxt
89+ | [P nt n' ty] <- lookupP_all (not holes) False n ctxt
90+ = return (P nt n' ty, ty)
91+ -- If the names are ambiguous, require it to be fully qualified
92+ | [P nt n' ty] <- lookupP_all (not holes) True n ctxt
9093 = return (P nt n' ty, ty)
9194 | otherwise = do lift $ tfail $ NoSuchVariable n
9295 chk u env ap@(RApp f RType) | not holes