fix: loose bound variables at ACLt

closes #3705

test: for issue

src/Lean/Meta/ACLt.lean

@@ -84,6 +84,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 +109,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 +147,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

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