PSA: `Expr.abstract` is unsafe

Stream: lean4

[Gabriel Ebner]

I'm sure this is well-known by now, but did you know that Expr.abstract is unsafe and should probably never be used (if the expression could contain a metavariable)? This has to do with the way metavariables and free variables interact: let's say you have a term ?m + y and you want to abstract the free variable y. In Lean 3 you would want the result ?m[#0] + #0 (containing the beloved delayed abstraction macro). In Lean 4, this is done differently: a new metavariable ?n is created, and the result should be ?n #0 + #0 (adding the assignment ?m := ?n y).

However, Expr.abstract completely ignores this situation and you get ?m + #0 as the result. This is bad because the instantiated expression can still contain the free variable y even though you thought that you abstracted it away! (Side note: the expr.abstract_locals function in Lean 3 has exactly the same issue. This explains many mysterious "failed to add declaration to environment, it contains local constants" errors...)

The correct replacement is called Lean.MetavarContext.MkBinding.abstractRange, and it's of course private. If you want to create a lambda or a forall, you can use the higher-level functions mkLambdaFVars and mkForallFVars, resp. But please be aware that these functions will not always create lambdas or foralls, despite their name. Sometimes they will also create lets, and sometimes they will also do nothing.

[Daniel Fabian]

I suggest creating an mwe and a github issue for how this be solved best in lean 4. It is possible that abstract should handle the case. If abstractRange is private, then it's quite possible that this is a bug.

[Gabriel Ebner]

Expr.abstract can't handle that case since it needs to create a new metavariable. For that it needs access to the metavariable context.

[Mario Carneiro]

Probably worth clarifying what "unsafe" means here. I guess you mean "will produce incorrect results in tactics using it, which will later be caught by the kernel", not "memory unsafe" or "allows you to prove false"