fix: deterministic fvar alias printing

src/Lean/Elab/InfoTree/Main.lean

@@ -145,7 +145,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.id.name} -> {info.baseId.name}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"

src/Lean/Elab/InfoTree/Types.lean

@@ -109,10 +109,13 @@ structure UserWidgetInfo where
   deriving Inhabited
 
 /--
-Specifies that the given free variables should be considered semantically identical in the current local context.
+Specifies that the given free variables should be considered semantically identical.
+The free variable `baseId` might not be in the current local context
+because it has been cleared.
 Used for e.g. connecting variables before and after `match` generalization.
 -/
 structure FVarAliasInfo where
+  userName : Name
   id     : FVarId
   baseId : FVarId
 

src/Lean/Elab/Match.lean

@@ -785,7 +785,7 @@ private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchT
             -- connect match-generalized pattern fvars, which are a suffix of `latLHS.fvarDecls`,
             -- to their original fvars (independently of whether they were cleared successfully) in the info tree
             for (fvar, baseId) in altLHS.fvarDecls.toArray.reverse.zip toClear.reverse do
-              pushInfoLeaf <| .ofFVarAliasInfo { id := fvar.fvarId, baseId }
+              pushInfoLeaf <| .ofFVarAliasInfo { id := fvar.fvarId, baseId, userName := fvar.userName }
             let matchType ← instantiateMVars matchType
             -- If `matchType` is of the form `@m ...`, we create a new metavariable with the current scope.
             -- This improves the effectiveness of the `isDefEq` default approximations

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -59,8 +59,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias _uniq.634 -> _uniq.299
-        • FVarAlias _uniq.633 -> _uniq.297
+        • FVarAlias a
+        • FVarAlias α
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -74,8 +74,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias _uniq.665 -> _uniq.299
-        • FVarAlias _uniq.664 -> _uniq.297
+        • FVarAlias a
+        • FVarAlias n
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩