git.iko.soy/Idris-dev
on master help sign in
Lookup exact names in Typecheck
dcdfd85Edwin Brady
src/Idris/Core/Evaluate.hs+9−4
compare with master
unifiedsplit
@@ -1007,11 +1007,11 @@ isTCDict n ctxt
1007 _ -> False
1007 _ -> False
1008
1008
1009lookupP :: Name -> Context -> [Term]
1009lookupP :: Name -> Context -> [Term]
1010−lookupP = lookupP_all False
1010+lookupP = lookupP_all False False
1011
1011
1012−lookupP_all :: Bool -> Name -> Context -> [Term]
1012+lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
1013−lookupP_all all n ctxt
1013+lookupP_all all exact n ctxt
1014− = do (n', def) <- lookupCtxtName n (definitions ctxt)
1014+ = do (n', def) <- names
1015 p <- case def of
1015 p <- case def of
1016 (Function ty tm, a, _, _) -> return (P Ref n' ty, a)
1016 (Function ty tm, a, _, _) -> return (P Ref n' ty, a)
1017 (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)
1017 (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)
@@ -1020,6 +1020,11 @@ lookupP_all all n ctxt
1020 case snd p of
1020 case snd p of
1021 Hidden -> if all then return (fst p) else []
1021 Hidden -> if all then return (fst p) else []
1022 _ -> return (fst p)
1022 _ -> 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
1023
1028
1024lookupDefExact :: Name -> Context -> Maybe Def
1029lookupDefExact :: Name -> Context -> Maybe Def
1025lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
1030lookupDefExact 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
86 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
86 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
87 -- If we're elaborating, we don't want the private names; if we're
87 -- If we're elaborating, we don't want the private names; if we're
88 -- checking an already elaborated term, we do
88 -- 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
90 = return (P nt n' ty, ty)
93 = return (P nt n' ty, ty)
91 | otherwise = do lift $ tfail $ NoSuchVariable n
94 | otherwise = do lift $ tfail $ NoSuchVariable n
92 chk u env ap@(RApp f RType) | not holes
95 chk u env ap@(RApp f RType) | not holes