feat: hide macro scopes encoding when displaying errors

src/Init/Lean/Elab/Term.lean

@@ -769,10 +769,9 @@ match result? with
 | none =>
   let process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do {
     when candidates.isEmpty $ do {
-      -- TODO: improve pretty printing
-      -- let extractionResult := extractMacroScopes n;
-      -- env ← getEnv;
-      throwError ref ("unknown identifier '" ++ toString n ++ "'")
+      mainModule ← getMainModule;
+      let view := extractMacroScopes n;
+      throwError ref ("unknown identifier '" ++ view.format mainModule ++ "'")
     };
     mkConsts ref candidates explicitLevels
   };

src/Init/Lean/Elab/Util.lean

@@ -14,6 +14,14 @@ match stx.truncateTrailing.reprint with -- TODO use syntax pretty printer
 | some str => format str.toFormat
 | none     => format stx
 
+def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format :=
+format $
+  if view.scopes.isEmpty then view.name
+  else if view.mainModule == mainModule then
+   view.scopes.foldl mkNameNum (view.name ++ view.imported)
+  else
+   view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
+
 namespace Elab
 
 structure MacroStackElem :=