chore: fix canonicalizer handling over forall/lambda (#6082)

This PR changes how the canonicalizer handles `forall` and `lambda`,
replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth
on
[zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Quantifiers.20in.20CanonM/near/482483448).

src/Lean/Meta/Canonicalizer.lean

@@ -91,7 +91,15 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do
           let eNew ← instantiateMVars e
           unless eNew == e do
             return (← mkKey eNew)
-        let info ← getFunInfo f
+        let info ← if f.hasLooseBVars then
+          -- If `f` has loose bound variables, `getFunInfo` will fail.
+          -- This can only happen if `f` contains local variables.
+          -- Instead we use an empty `FunInfo`, which results in the
+          -- `i < info.paramInfo.size` check below failing for all indices,
+          -- and hence mixing in the hash for all arguments.
+          pure {}
+        else
+          getFunInfo f
         let mut k ← mkKey f
         for i in [:e.getAppNumArgs] do
           if h : i < info.paramInfo.size then
@@ -101,10 +109,13 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do
           else
               k := mixHash k (← mkKey (e.getArg! i))
         return k
-      | .lam _ t b _
-      | .forallE _ t b _ =>
+      | .lam n t b bi
+      | .forallE n t b bi =>
+        -- Note that we do not use `withLocalDecl` here, for performance reasons.
+        -- Instead we have a guard for loose bound variables in the `.app` case above.
         return mixHash (← mkKey t) (← mkKey b)
-      | .letE _ _ v b _ =>
+      | .letE n t v b _ =>
+        -- Similarly, we do not use `withLetDecl` here.
         return mixHash (← mkKey v) (← mkKey b)
       | .proj _ i s =>
         return mixHash i.toUInt64 (← mkKey s)
@@ -124,11 +135,11 @@ def canon (e : Expr) : CanonM Expr := do
         if (← isDefEq e e') then
           return e'
       -- `e` is not definitionally equal to any expression in `es'`. We claim this should be rare.
-      unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k (e :: es') }
+      modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k (e :: es') }
       return e
   else
     -- `e` is the first expression we found with key `k`.
-    unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k [e] }
+    modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k [e] }
     return e
 
 end Canonicalizer

tests/lean/run/canonM_exists_fun.lean

@@ -0,0 +1,22 @@
+import Lean.Meta.Canonicalizer
+import Lean.Elab.Tactic
+
+elab "foo" t:term : tactic => do
+  let e ← Lean.Elab.Tactic.elabTerm t none
+  trace[debug] "canonicalizing {e}"
+  let e' ← (Lean.Meta.canon e).run'
+  trace[debug] "canonicalized it to {e'}"
+
+/-- info: ∃ f, ∀ (x : Nat), f x = 0 : Prop -/
+#guard_msgs in
+#check (∃ f : Nat → Nat, ∀ x, f x = 0) -- works fine
+
+/--
+info: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0
+[debug] canonicalized it to ∃ f, ∀ (x : Nat), f x = 0
+-/
+#guard_msgs in
+set_option trace.debug true in
+example : True := by
+  foo (∃ f : Nat → Nat, ∀ x, f x = 0) -- used to fail with "unexpected bound variable #1"
+  trivial