improve already defined error messages

aoc2024/Day17.newt

@@ -80,10 +80,6 @@ step mach@(M a b c mem ip out) =
     combo 6 = c
     combo n = itobi n
 
-find : ∀ a. (a → Bool) → List a → Maybe a
-find f Nil = Nothing
-find f (x :: xs) = if f x then Just x else find f xs
-
 Cand : U
 Cand = BigInt ×  SnocList Int ×  List Int
 

src/Lib/ProcessDecl.idr

@@ -207,7 +207,7 @@ processDecl (TypeSig fc names tm) = do
   let mstart = length mc.metas
   for_ names $ \nm => do
     let Nothing := lookup nm top
-      | _ => error fc "\{show nm} is already defined"
+      | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
     pure ()
   ty <- check (mkCtx fc) tm (VU fc)
   ty <- zonk top 0 [] ty
@@ -241,7 +241,7 @@ processDecl (Def fc nm clauses) = do
   let Just entry = lookup nm top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
   let (MkEntry fc name ty Axiom) := entry
-    | _ => throwError $ E fc "\{nm} already defined"
+    | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"
 
   putStrLn "check \{nm} at \{pprint [] ty}"
   vty <- eval empty CBN ty

src/Lib/TopContext.idr

@@ -45,8 +45,8 @@ setDef name fc ty def = do
   where
     go : List TopEntry -> M (List TopEntry)
     go [] = pure $ [MkEntry fc name ty def]
-    go (x@(MkEntry _ nm ty' def') :: defs) = if nm == name
+    go (x@(MkEntry fc' nm ty' def') :: defs) = if nm == name
-      then error fc "\{name} is already defined"
+      then error fc "\{name} is already defined at \{show fc'}"
       else (x ::) <$> go defs
 
 public export