fix: key visited expressions by structural equality

Export.lean

@@ -32,10 +32,28 @@ def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
 structure Context where
   env : Environment
 
+/--
+A wrapper around `Expr` whose `BEq` uses structural equality. This keeps
+expressions that differ only in binder names or binder info distinct in
+`visitedExprs`, so an export does not depend on which declarations were
+exported before it.
+-/
+structure ExprKey where
+  expr : Expr
+  deriving Inhabited
+
+instance : BEq ExprKey where
+  beq a b := a.expr.equal b.expr
+
+instance : Hashable ExprKey where
+  -- `Expr.hash` ignores binder names, so it is compatible with the finer
+  -- `Expr.equal` relation used by `BEq`.
+  hash a := hash a.expr
+
 structure State where
   visitedNames : HashMap Name Nat := HashMap.emptyWithCapacity 200000 |>.insert .anonymous 0
   visitedLevels : HashMap Level Nat := HashMap.emptyWithCapacity 1000 |>.insert .zero 0
-  visitedExprs : HashMap Expr Nat := HashMap.emptyWithCapacity 10000000
+  visitedExprs : HashMap ExprKey Nat := HashMap.emptyWithCapacity 10000000
   visitedConstants : NameHashSet := {}
   noMDataExprs : HashMap Expr Expr := HashMap.emptyWithCapacity 100000
   exportMData : Bool := false
@@ -155,7 +173,7 @@ def removeMData (e : Expr) : M Expr := do
 mutual
 
 partial def dumpExprAux (e : Expr) : M Nat := do
-  getIdx e "ie" (·.visitedExprs) ({ · with visitedExprs := · }) do
+  getIdx (ExprKey.mk e) "ie" (·.visitedExprs) ({ · with visitedExprs := · }) do
     match e with
     | .fvar .. | .mvar .. => panic! "cannot export free variables or metavariables"
     | .mdata a e' =>

Test.lean

@@ -70,6 +70,22 @@ info: {"in":1,"str":{"pre":0,"str":"Prod"}}
 #guard_msgs in
 #eval run <| dumpExpr (.proj `Prod 1 (.bvar 0))
 
+/--
+info:
+{"in":1,"str":{"pre":0,"str":"x"}}
+{"ie":0,"sort":0}
+{"bvar":0,"ie":1}
+{"ie":2,"lam":{"binderInfo":"default","body":1,"name":1,"type":0}}
+{"in":2,"str":{"pre":0,"str":"y"}}
+{"ie":3,"lam":{"binderInfo":"implicit","body":1,"name":2,"type":0}}
+-/
+#guard_msgs in
+#eval runEmpty <| do
+  let e1 := .lam `x (.sort .zero) (.bvar 0) .default
+  let e2 := .lam `y (.sort .zero) (.bvar 0) .implicit
+  let _ ← dumpExpr e1
+  let _ ← dumpExpr e2
+
 /-- info: {"ie":0,"natVal":"100000000000000023456789"}
 -/
 #guard_msgs in