From 00296f4d1093957d579b0515575e79bf620febb8 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 7 Feb 2026 11:02:51 -0800
Subject: [PATCH] Allow local names to override imports

---
 src/Lib/ProcessDecl.newt | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt
index ea0a4a1..aaa21b7 100644
--- a/src/Lib/ProcessDecl.newt
+++ b/src/Lib/ProcessDecl.newt
@@ -94,7 +94,7 @@ impTele tele = map foo tele
 checkAlreadyDef : FC → Name → M Unit
 checkAlreadyDef fc nm = do
   top <- getTop
-  case lookupRaw nm top of
+  case lookup (QN top.ns nm) top of
     Nothing => pure MkUnit
     Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
 
@@ -104,14 +104,9 @@ processDecl : List String -> Decl -> M Unit
 processTypeSig : List String → FC → List Name → Raw → M Unit
 processTypeSig ns fc names tm = do
   log 1 $ \ _ => "-----"
-
   top <- getTop
-  let mc = top.metaCtx
-  -- let mstart = length' mc.metas
   traverse (checkAlreadyDef fc) names
   ty <- check (mkCtx fc) tm (VU fc)
-  -- this is not needed
-  -- ty <- zonk top 0 Nil ty
   log 1 $ \ _ => "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
   ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
 
@@ -163,7 +158,7 @@ processDef ns fc nm clauses = do
   log 1 $ \ _ => "Def \{show nm}"
   top <- getTop
   let mc = top.metaCtx
-  let (Just entry) = lookupRaw nm top
+  let (Just entry) = lookup (QN ns nm) top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
   let (MkEntry fc name ty Axiom _) = entry
     | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"
@@ -284,7 +279,7 @@ processInstance ns instfc ty decls = do
   -- This needs to be declared before processing the defs, but the defs need to be
   -- declared before this - side effect is that a duplicate def is noted at the first
   -- member
-  case lookupRaw instname top of
+  case lookup (QN ns instname) top of
     Just _ => pure MkUnit -- TODO check that the types match
     Nothing => do
       -- only add once
@@ -442,7 +437,7 @@ processData ns fc nm ty cons = do
   top <- getTop
   let mc = top.metaCtx
   tyty <- check (mkCtx fc) ty (VU fc)
-  case lookupRaw nm top of
+  case lookup (QN ns nm) top of
     Just (MkEntry _ name type Axiom _) => do
       tyty' <- eval Nil tyty
       type' <- eval Nil type