[error] Add message for ambiguous symbol error

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -1140,6 +1140,9 @@ entryOverName f = snd . entryPrism f
 entryName :: SymbolEntry -> S.Name' ()
 entryName = fst . entryPrism id
 
+instance HasLoc SymbolEntry where
+  getLoc = S._nameDefined . entryName
+
 overModuleRef'' :: forall s s'. (forall t. ModuleRef'' s t -> ModuleRef'' s' t) -> ModuleRef' s -> ModuleRef' s'
 overModuleRef'' f = over unModuleRef' (\(t :&: m'') -> t :&: f m'')
 

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Ansi.hs

@@ -2,6 +2,8 @@ module MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Ansi where
 
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Scoped.Error.Pretty.Base
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as S
+
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 
@@ -11,3 +13,4 @@ renderAnsi = renderStrict . reAnnotateS stylize
 stylize :: Eann -> AnsiStyle
 stylize a = case a of
   Highlight -> colorDull Red
+  ScopedAnn s -> S.stylize s

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Pretty/Base.hs

@@ -13,6 +13,7 @@ import Prettyprinter
 import Text.EditDistance
 
 data Eann = Highlight
+  | ScopedAnn P.Ann
 
 highlight :: Doc Eann -> Doc Eann
 highlight = annotate Highlight
@@ -21,7 +22,7 @@ ppSymbolT :: Text -> Doc Eann
 ppSymbolT = highlight . pretty
 
 ppCode :: P.PrettyCode c => c -> Doc Eann
-ppCode = unAnnotate . P.runPrettyCode P.defaultOptions
+ppCode = reAnnotate ScopedAnn . P.runPrettyCode P.defaultOptions
 
 indent' :: Doc ann -> Doc ann
 indent' = indent 2
@@ -156,9 +157,9 @@ instance PrettyError UnusedOperatorDef where
 instance PrettyError AmbiguousSym where
   ppError AmbiguousSym {..} =
     "The symbol" <+> ppCode _ambiguousSymName <+> "at" <+> pretty (getLoc _ambiguousSymName) <+> "is ambiguous." <> line
-      <> "It could be either of"
+      <> "It could be any of:"
       <> line
-      <> undefined
+      <> indent' (vsep (map ppCode _ambiguousSymEntires))
 
 instance PrettyError AmbiguousModuleSym where
   ppError AmbiguousModuleSym {} =

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -798,7 +798,8 @@ ppExpression = case sing :: SStage s of
   SParsed -> ppCode
 
 instance PrettyCode SymbolEntry where
-  ppCode ent = return (kindTag <+> pretty (entryName ent ^. S.nameVerbatim))
+  ppCode ent = return (kindTag <+> pretty (entryName ent ^. S.nameVerbatim)
+    <+> "at" <+> pretty (getLoc ent))
     where
     pretty' :: Text -> Doc a
     pretty' = pretty

tests/negative/AmbiguousSymbol.mjuvix

@@ -1,10 +1,18 @@
 module AmbiguousSymbol;
 
   axiom A : Type;
+
+  module O;
+    inductive T {
+      A : T;
+    };
+  end;
+  open O;
+
   module M;
     axiom A : Type;
   end;
   open M;
 
   axiom B : A;
-end;
+end;