perf: use structural equality at ACLt

closes #3705

test: for issue

src/Lean/Meta/ACLt.lean

@@ -50,7 +50,7 @@ mutual
    - We ignore metadata.
    - We ignore universe parameterst at constants.
 -/
-unsafe def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool :=
+partial def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool := do
   lt a b
 where
   reduce (e : Expr) : MetaM Expr := do
@@ -66,7 +66,9 @@ where
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do
-    if ptrAddrUnsafe a == ptrAddrUnsafe b then
+    if a == b then
+      -- We used to have an "optimization" using only pointer equality.
+      -- This was a bad idea, `==` is often much cheaper than `acLt`.
       return false
     -- We ignore metadata
     else if a.isMData then
@@ -84,6 +86,16 @@ where
     else
       lt a₂ b₂
 
+  getParamsInfo (f : Expr) (numArgs : Nat) : MetaM (Array ParamInfo) := do
+    -- Ensure `f` does not have loose bound variables. This may happen in
+    -- since we go inside binders without extending the local context.
+    -- See `lexSameCtor` and `allChildrenLt`
+    -- See issue #3705.
+    if f.hasLooseBVars then
+      return #[]
+    else
+      return (← getFunInfoNArgs f numArgs).paramInfo
+
   ltApp (a b : Expr) : MetaM Bool := do
     let aFn := a.getAppFn
     let bFn := b.getAppFn
@@ -99,7 +111,7 @@ where
       else if aArgs.size > bArgs.size then
         return false
       else
-        let infos := (← getFunInfoNArgs aFn aArgs.size).paramInfo
+        let infos ← getParamsInfo aFn aArgs.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -137,7 +149,7 @@ where
     | .proj _ _ e ..    => lt e b
     | .app ..           =>
       a.withApp fun f args => do
-        let infos := (← getFunInfoNArgs f args.size).paramInfo
+        let infos ← getParamsInfo f args.size
         for i in [:infos.size] do
           -- We ignore instance implicit arguments during comparison
           if !infos[i]!.isInstImplicit then
@@ -176,7 +188,8 @@ end
 
 end ACLt
 
-@[implemented_by ACLt.main, inherit_doc ACLt.main]
-opaque Expr.acLt : Expr → Expr → (mode : ACLt.ReduceMode := .none) → MetaM Bool
+@[inherit_doc ACLt.main]
+def acLt (a b : Expr) (mode : ACLt.ReduceMode := .none) : MetaM Bool :=
+  ACLt.main a b mode
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -128,7 +128,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
         We use `.reduceSimpleOnly` because this is how we indexed the discrimination tree.
         See issue #1815
         -/
-        if !(← Expr.acLt rhs e .reduceSimpleOnly) then
+        if !(← acLt rhs e .reduceSimpleOnly) then
           trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {e} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, {e} ==> {rhs}"

tests/lean/run/3705.lean

@@ -0,0 +1,34 @@
+structure MonoidHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
+  toFun : M → N
+  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y
+
+class CommMagma (G : Type _) extends Mul G where
+  mul_comm : ∀ a b : G, a * b = b * a
+
+set_option quotPrecheck false
+infixr:25 " →*' " => MonoidHom
+
+instance [Mul M] [Mul N] : CoeFun (M →*' N) (fun _ => M → N) where
+  coe := MonoidHom.toFun
+
+open CommMagma
+
+-- -- this instance needed
+instance MonoidHom.commMonoid [Mul M] [Mul N] :
+    CommMagma (M →*' N) where
+  mul := fun f g => { toFun := fun x => f x * g x, map_mul' := sorry }
+  mul_comm := sorry
+
+
+example {M} [Mul M] [Mul G] [Pow G Int] :
+    let zpow : Int → (M →*' G) → (M →*' G) := fun n f => { toFun := fun x => f x ^ n, map_mul' := sorry }
+    ∀ (n : Nat) (a : M →*' G), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a := by
+  simp only [Int.ofNat_eq_coe] -- commenting out this line makes simp loop
+  simp (config := { failIfUnchanged := false }) only [mul_comm] -- should not produce: unexpected bound variable 2
+  sorry
+
+theorem ex₂ {M} [Mul M] [Mul G] [Pow G Int] :
+    let zpow : Int → (M →*' G) → (M →*' G) := fun n f => { toFun := fun x => f x ^ n, map_mul' := sorry }
+    ∀ (n : Nat) (a : M →*' G), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a := by
+  simp only [mul_comm]
+  sorry