chore: fix canonicalizer handling over forall/lambda

[kim-em]

This PR changes how the canonicalizer handles forall and lambda, replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth on zulip.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 22:23:15)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-14 23:47:59)

[JLimperg]

To squeeze some more performance out of this, you could copy the instantiation strategy from ForEachExpr. The instantiateRevs there effectively batch multiple instantiate1s, which should be faster.

[leodemoura]

@kim-em I finally had time to review this PR. The unexpected bounded variable errors are caused by the getFunInfo application. We use this primitive to retrieve information about the function, which is then used to skip propositions and implicit arguments.

You mentioned concerns about performance issues related to withLocalDecl and withLetDecl. I agree that this could be a problem. We can address it by first checking whether f contains loose bounded variables. This check is constant time. If f contains bounded variables, we can simply consider all arguments. Here is the suggested modification:

modified   src/Lean/Meta/Canonicalizer.lean
@@ -91,7 +91,12 @@ 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.
+          pure {}
+        else
+          getFunInfo f
         let mut k ← mkKey f
         for i in [:e.getAppNumArgs] do
           if h : i < info.paramInfo.size then