grind canonicalizer creates closed term with proof lacking `nestedProof`

[datokrat]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In my understanding, propagateForallPropUp relies on the invariant that closed terms have been preprocessed and, in particular, every proof term is wrapped into nestedProof. However, when the canonicalizer re-synthesizes instances, it can make terms closed that had loose bvars before, and it seemingly does not re-preprocess these terms. As a consequence, the e-graph can contain two nodes that are only different in that one contains a proof wrapped into nestedProof and the other contains the unwrapped proof, and this obstructs closing the goal.

Context

This occurred when I tested grind against the GetElemV redesign. Many GetElemV applications use Nonempty _ proofs that depend on some external hypothesis or value, and these instances get canonicalized when possible.

Steps to Reproduce

MWE:

public section

namespace Mwe

opaque P {α : Type} (a : α) : Prop

/--
`f` carries a `Nonempty α` instance-implicit argument.
The canonicalizer re-synthesizes it if possible.
-/
opaque f {α : Type} [_n : Nonempty α] (a : α) : α := sorry

opaque aux {α : Type} (a : α) (_h : P a) : α := sorry

inductive Mem {α : Type} : α → List α → Prop where
  | head {a : α} {as : List α} : Mem a (a :: as)
  | tail {a b : α} {as : List α} : Mem a as → Mem a (b :: as)

@[simp] theorem mem_f_dep {α : Type} (a : α) (_h : P a) :
    haveI : Nonempty α := ⟨aux a _h⟩
    Mem (f a) [a] := sorry

grind_pattern mem_f_dep => Mem (@f α ⟨aux a _h⟩ a) [a]

@[simp] theorem mem_f_indep [n : Nonempty α] (a : α) (_h : P a) :
    Mem (f a) [a] := sorry

grind_pattern mem_f_indep => Mem (f a) [a]

end Mwe
open Mwe

/--
Fails (bug):

`mem_f_dep`'s body captures `_h` via `aux a _h`. During preprocessing of the body,
`markNestedSubsingletons` sees that the `Nonempty α` proof has a loose bvar (capturing `_h`) and skips.
The canonicalizer then re-synthesizes the
`Nonempty α` from the example's `[Nonempty α]`, getting a closed term, but unwrapped.

Later, `P a` is propagated into `mem_f_dep` using `propagateForallPropUp`.
Because the body is already a closed term, it is not reprocessed again.
Therefore, the `Nonempty α` proof term stays unwrapped in `f x`.

The `f x` from `hc`, however, contains a correctly wrapped `Nonempty α` instance.
So the wrapped `f x` from `hc` and the unwrapped `f x` (from `mem_f_dep`'s body)
end up as two distinct enodes, so
`Mem c [x] = False ∧ Mem (f x [unwrapped Nonempty]) [x] = True ∧ c = f x [wrapped Nonempty]`
is not detected as a contradiction.

The problem is a violated invariant that `propagateForallPropUp` relies on:
If a term has no loose bvars, it must be preprocessed correctly.
In particular, proof terms must be wrapped into `nestedProof`.
-/
example {α : Type} [Nonempty α] (x c : α)
    (hc : (f x) = c)
    (this : P x)
    (notMem : ¬ Mem c [x]) : False := by
  fail_if_success
    grind only [usr mem_f_dep]
  sorry

/--
Passes (expected):

`mem_f_dep`'s body still captues `_h` via `aux a _h`.
However, the canonicalizer does cannot synthesize a new `Nonempty α` instance,
so the captured bvar stays in the body of `mem_f_dep`.
Therefore, `propagateForallPropUp` does not take the fast path. It makes the body
closed and then correctly preprocesses it, wrapping the `Nonempty α` instance into
`nestedProof`.
-/
example {α : Type} (x c : α)
    (hc : (haveI : Nonempty α := sorry; f x) = c)
    (this : P x)
    (notMem : ¬ Mem c [x]) : False := by
  grind only [usr mem_f_dep]

/--
Passes (expected):

`mem_f_indep`'s body has no loose bvar in the Nonempty arg, so
`markNestedSubsingletons` recurses and wraps the `Nonempty α` instance into `nestedProof`.
We get a contradiction:
`Mem c [x] = False ∧ Mem (f x [wrapped Nonempty]) [x] = True ∧ c = f x [wrapped Nonempty]`
-/
example [Nonempty α] (x c : α)
    (hc : (f x) = c)
    (this : P x)
    (notMem : ¬ Mem c [x]) : False := by
  grind only [usr mem_f_indep]

Expected behavior:

All of these examples should succeed. In particular, there's no observable difference in behavior between mem_f_dep and mem_f_indep.

Actual behavior:

The first example fails as explained in the docstring.

Versions

Lean 4.31.0-nightly-2026-05-05
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.