PSA: `Expr.abstract` does not do what you think it does

Stream: lean4

[Gabriel Ebner]

I'm happy about suggestions for a better term than unsafe. "Considered harmful" was my other choice, but I think this would come across even worse.

[Mario Carneiro]

"incorrect" seems the most accurate

[Mario Carneiro]

although as you point out it's not clear that a correct function with the same signature can exist

[Gabriel Ebner]

Daniel Fabian said:

I suggest creating an mwe and a github issue for how this be solved best in lean 4.

I am very reserved with suggesting library changes in Lean 4 these days. This is the function that I would have expected:

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index cd6a7fc920..fcbaa584be 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -434,6 +434,14 @@ def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl := do
     setNGen newS.ngen;
     throwError "failed to create binder due to failure when reverting variable dependencies"

+/-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
+def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
+  liftMkBindingM <| fun lctx => MetavarContext.MkBinding.abstractRange xs n e false
+
+/-- Replace free variables `xs` with loose bound variables. -/
+def abstract (e : Expr) (xs : Array Expr) : MetaM Expr :=
+  abstractRange e xs.size xs
+
 def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) : MetaM Expr :=
   if xs.isEmpty then pure e else liftMkBindingM <| MetavarContext.mkForall xs e usedOnly usedLetOnly

diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index f69a69c62a..61be8edf1f 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -948,7 +948,7 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
   contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.

   `elimMVarDeps` is defined later in this file. -/
-@[inline] private def abstractRange (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do
+@[inline] def abstractRange (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do
   let e ← elimMVarDeps xs e
   pure (e.abstractRange i xs)

[Daniel Fabian]

@Gabriel Ebner I was not proposing a PR, rather a bug. You can clearly add your change as a description of the problem. My point was about making sure we can have a good solution in lean4. And as I mentioned, there's probably a good reason for the function to be private.

It is difficult for me to judge if the behaviour you are experiencing is expected, e.g. because it's a perf trade off or something, or an oversight. Hence the issue.

[Mario Carneiro]

there's probably a good reason for the function to be private

I find it more likely that the developers just make things private by habit and make them public only when needed. That's certainly a habit I get into when writing in languages with pervasive module privacy like java or rust.

[Mario Carneiro]

I think it is possible to justify Expr.abstract as written if it has a precondition that the expr in question has no metavariables, for example because it is already fully elaborated and pulled from an earlier definition

[Daniel Fabian]

and my first guess from reading the delta is that there may be a perf issue latent in the other version.