`instance_wanted` doesn't work after a chained `instance_wanted`

[riccardobrasca]

When one instance_wanted depends on an earlier one (its class takes the earlier class as an instance argument), every instance_wanted registered after the chained one can no longer be found by typeclass inference.

Minimal example:

import Batteries.Util.ProofWanted

class Pointed (a : Type) where point : a
class DoublePointed (a : Type) [Pointed a] where second : a
class Stupid (a : Type) [Pointed a] : Prop where stupid : True

def_wanted W : Type

instance_wanted : Pointed (❰W❱)
instance_wanted : DoublePointed (❰W❱)
instance_wanted : Stupid (❰W❱)

theorem_wanted foo : True := by
  have : Stupid (❰W❱) := by infer_instance --error
  trivial

Here is an analysis made by Claude (feel free to ignore it, I am not competent enough to judge it).

The auto-include loop in elabWanted gives instStupid a binder for instDoublePointed that
re-quantifies the Pointed dependency from scratch (#print with pp.explicit):

private def instStupid : {d_W : @DefWanted.Val Type W} →
  [d_instPointed : {d_W : @DefWanted.Val Type W} → @DefWanted.Val (Pointed d_W) (@instPointed d_W)] →
    [{d_W : @DefWanted.Val Type W} →
          [d_instPointed : {d_W : @DefWanted.Val Type W} → @DefWanted.Val (Pointed d_W) (@instPointed d_W)] →
            @DefWanted.Val (@DoublePointed d_W (@d_instPointed d_W)) (@instDoublePointed d_W d_instPointed)] →
      DefWanted (@Stupid d_W (@d_instPointed d_W))

In foo, synthesizing Stupid d_W✝ applies the local instance d_instStupid✝, whose chained
premise becomes the subgoal

{d_W : W.Val} → [d_instPointed : {d_W : W.Val} → instPointed.Val] → instDoublePointed.Val

The only candidate is foo's own d_instDoublePointed✝ binder — syntactically of the very same
type — yet tryResolve fails (set_option trace.Meta.synthInstance true):

[Meta.synthInstance.apply] ❌️ apply d_instDoublePointed✝ to {d_W : W.Val} →
      [d_instPointed : {d_W : W.Val} → instPointed.Val] → instDoublePointed.Val
  [Meta.synthInstance.tryResolve] ❌️ instDoublePointed.Val ≟ DoublePointed ?m.18
    [Meta.synthInstance] ✅️ {d_W : W.Val} →
          [d_instPointed : {d_W : W.Val} → instPointed.Val] → {d_W : W.Val} → instPointed.Val
      ...
      [Meta.synthInstance] result fun {d_W} [{d_W : W.Val} → instPointed.Val] => d_instPointed✝

The reason: the subgoal's conclusion is
DefWanted.Val (@DoublePointed d_W (@d_instPointed d_W)) (…), where d_instPointed is the
subgoal's own Π-bound instance binder. Matching the candidate requires unifying
@DoublePointed d_W (@d_instPointed d_W) with @DoublePointed ?w (@?ip ?w), and when isDefEq
reaches the instance-implicit ?ip, synthPending fires and resolves it against the ambient
local instances, committing ?ip := d_instPointed✝ (the theorem-level binder) — a different fvar
from the subgoal's Π-bound one. The two sides then fail to unify, the premise is unsolvable, and
since every later wanted's d_instStupid✝/d_instSimple✝ binder carries this premise, those
instances can never be applied.

The problem is the Π-re-quantification encoding itself, not DefWanted. Batteries-free
distillation of the generated binder structure, failing identically:

class Pointed (a : Type) where point : a
class DoublePointed (a : Type) [Pointed a] where second : a
class Stupid (a : Type) [Pointed a] : Prop where stupid : True

example (V : Type)
    [d_iP : {w : Type} → Pointed w]
    [d_iDP : {w : Type} → [ip : {x : Type} → Pointed x] → @DoublePointed w (@ip w)]
    [d_iS : {w : Type} → [ip : {x : Type} → Pointed x] →
            [idp : {w' : Type} → [ip' : {x : Type} → Pointed x] → @DoublePointed w' (@ip' w')] →
            @Stupid w (@ip w)] : True := by
  have : @Stupid V (@d_iP V) := by infer_instance  -- fails
  trivial

Possible fix

Instead of Π-quantifying an auto-included binder over all of the referenced wanted's own binders
(classifyWantedRef/mkBinderSyn), saturate the binders that correspond to wanteds already bound
in the enclosing signature with those enclosing binders. nameToHypRef already tracks that
correspondence, and registration order guarantees dependencies are bound first. For instStupid
the chained binder would become

[{w : W.Val} → DefWanted.Val (@instDoublePointed w d_instPointed)]

referring to the sibling d_instPointed binder. The saturated encoding synthesizes fine:

example (V : Type)
    [d_iP : {w : Type} → Pointed w]
    [d_iDP : {w : Type} → @DoublePointed w (@d_iP w)]
    [d_iS : {w : Type} → @Stupid w (@d_iP w)] : True := by
  have : @Stupid V (@d_iP V) := by infer_instance        -- ok
  have : @DoublePointed V (@d_iP V) := by infer_instance -- ok
  trivial

[Chessing234]

Fixing in a PR with #1911.

[Chessing234]

PR #1914.

[Chessing234]

Opened a PR that saturates already-bound wanteds instead of re-quantifying them.