synthPendingDepth breaks TC caching

[Kha]

Description

It is possible to break TC caching, i.e. to create an unexpected interaction between supposedly independent elaboration steps doing the same TC query, if they occur at different depths. This is because the depth can influence the result but is not currently included in the caching logic.

Context

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20search.20is.20affected.20by.20other.20subexpressions. More data on impact should be collected, but the indirectness of the issue may make it hard for users to notice they are affected by this specific issue.

Steps to Reproduce

From Eric. Needs to be MWE'd, which should be more feasible now that we know what we need to look for (a sufficiently deep dependent TC hierarchy).

import Mathlib.Analysis.NormedSpace.OperatorNorm

variable (𝕜 : Type) [NontriviallyNormedField 𝕜]
variable (E : Type) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

abbrev Dual : Type _ := E →L[𝕜] 𝕜

def inclusionInDoubleDual : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := sorry

example : ‖inclusionInDoubleDual 𝕜 E‖ = 0 := by
  -- this `rw` is needed to make the `have` below work
  -- rw [inclusionInDoubleDual]
  haveI : Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) := inferInstance
  sorry

Here we first encounter (at inclusionInDoubleDual 𝕜 E) SeminormedAddCommGroup (Dual 𝕜 E) as a nested TC problem, which fails because of the depth restriction. Then at inferInstance we encounter it as a non-nested problem, which nevertheless uses the cached failure. Inserting the rewrite resets the cache and make the second problem succeed.
Trace paths to the two problems without the rewrite:

[Meta.synthInstance] ✅ Norm (E →L[𝕜] Dual 𝕜 (Dual 𝕜 E))
  [Meta.synthInstance] ✅ apply @ContinuousLinearMap.hasOpNorm to Norm (E →L[𝕜] Dual 𝕜 (Dual 𝕜 E))
    [Meta.synthInstance.tryResolve] ✅ Norm (E →L[𝕜] Dual 𝕜 (Dual 𝕜 E)) ≟ Norm (E →L[𝕜] Dual 𝕜 (Dual 𝕜 E))
      [Meta.synthInstance] ✅ SeminormedAddCommGroup (Dual 𝕜 (Dual 𝕜 E))
        [Meta.synthInstance] ✅ apply @ContinuousLinearMap.toSeminormedAddCommGroup to SeminormedAddCommGroup
              (Dual 𝕜 (Dual 𝕜 E))
          [Meta.synthInstance.tryResolve] ✅ SeminormedAddCommGroup
                (Dual 𝕜 (Dual 𝕜 E)) ≟ SeminormedAddCommGroup (Dual 𝕜 E →L[𝕜] 𝕜)
            [Meta.synthInstance] ❌ SeminormedAddCommGroup (Dual 𝕜 E)
              [Meta.synthInstance] ❌ apply @ContinuousLinearMap.toSeminormedAddCommGroup to SeminormedAddCommGroup
                    (Dual 𝕜 E)
                [Meta.synthInstance.tryResolve] ❌ SeminormedAddCommGroup
                      (Dual 𝕜 E) ≟ SeminormedAddCommGroup (?m.4617 →SL[?m.4625] ?m.4618)
                  [Meta.synthPending] too many nested synthPending invocations
...
[Meta.synthInstance] ❌ Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E)
  [Meta.synthInstance] ❌ apply @ContinuousLinearMap.hasOpNorm to Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E)
    [Meta.synthInstance.tryResolve] ❌ Norm (Dual 𝕜 E →L[𝕜] Dual 𝕜 E) ≟ Norm (?m.8118 →SL[?m.8126] ?m.8119)
      [Meta.synthInstance] ❌ SeminormedAddCommGroup (Dual 𝕜 E)
        [Meta.synthInstance] result <not-available> (cached)

Expected behavior: The rewrite should not affect the unrelated TC query.

Actual behavior: It does.

Versions

g63d2bdd490

[eric-wieser]

Based on the following, it looks like "sufficiently nested" is "nested more than once":

lean4/src/Lean/Meta/SynthInstance.lean

Lines 762 to 765 in 13ca443

	/- TODO: use a configuration option instead of the hard-coded limit `1`. -/
	if (← read).synthPendingDepth > 1 then
	trace[Meta.synthPending] "too many nested synthPending invocations"
	return false

[kbuzzard]

Here is a mathlib-free version of the above example:

class Norm' (E : Type) where
  norm : E → Nat

export Norm' (norm)

class TopologicalSpace' (α : Type) where
  random : α -- need something here for some reason

class SeminormedAddCommGroup' (α : Type) extends Norm' α, TopologicalSpace' α where

-- need to extend Norm' again for some reason; note that this doesn't seem to cause a diamond
class NonUnitalSeminormedRing' (α : Type) extends Norm' α, SeminormedAddCommGroup' α where

variable (𝕜 : Type) [NonUnitalSeminormedRing' 𝕜]
variable (E : Type) [SeminormedAddCommGroup' E]

structure ContinuousLinearMap' (M : Type) [TopologicalSpace' M] (M₂ : Type) [TopologicalSpace' M₂] where

notation:25 M " →z " M₂ => ContinuousLinearMap' M M₂

abbrev Dual : Type := E →z 𝕜

instance ContinuousLinearMap'.toSeminormedAddCommGroup' {E : Type} {F : Type}
    [SeminormedAddCommGroup' E] [SeminormedAddCommGroup' F] :
  SeminormedAddCommGroup' (E →z F) := sorry

def foo : E →z Dual 𝕜 (Dual 𝕜 E) := sorry

#synth SeminormedAddCommGroup' (Dual 𝕜 E) -- works fine

set_option trace.Meta.synthInstance true
example : norm (foo 𝕜 E) = 0 := by
  -- this `rw` is needed to make the `have` below work
  --rw [foo]
  have : SeminormedAddCommGroup' (Dual 𝕜 E) := inferInstance -- fails
  sorry

The relevant traces are:

1) On `norm (foo 𝕜 E)`: 

[Meta.synthInstance] ✅ Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
  [] new goal Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @NonUnitalSeminormedRing'.toNorm' to Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ❌ apply inst✝¹ to NonUnitalSeminormedRing' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @SeminormedAddCommGroup'.toNorm' to Norm' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ❌ apply inst✝ to SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▶
  [] ✅ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
    [tryResolve] ✅ SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ≟ SeminormedAddCommGroup' (E →z Dual 𝕜 (Dual 𝕜 E)) ▼
      [] ✅ SeminormedAddCommGroup' E ▶
      [] ✅ SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▼
        [] new goal SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▶
        [] ❌ apply inst✝ to SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▶
        [] ✅ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ▼
          [tryResolve] ✅ SeminormedAddCommGroup' (Dual 𝕜 (Dual 𝕜 E)) ≟ SeminormedAddCommGroup' (Dual 𝕜 E →z 𝕜) ▼
            [] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ▼
              [] new goal SeminormedAddCommGroup' (Dual 𝕜 E) ▶
              [] ❌ apply inst✝ to SeminormedAddCommGroup' (Dual 𝕜 E) ▶
              [] ❌ apply @ContinuousLinearMap'.toSeminormedAddCommGroup' to SeminormedAddCommGroup' (Dual 𝕜 E) ▼
                [tryResolve] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ≟ SeminormedAddCommGroup' (?m.8308 →z ?m.8309) 

2) Later, on `inferInstance`

[Meta.synthInstance] ❌ SeminormedAddCommGroup' (Dual 𝕜 E) ▼
  [] result <not-available> (cached) 

[kbuzzard]

Re: "More data on impact should be collected."

It was a common issue during the port that a big simp only [A,B,C,D,E,...] block which worked in Lean 3 would fail in Lean 4. Nobody ever understood why. Often it was a case that one random simp lemma was not firing for reasons nobody could understand, and the proof could be fixed (after a lot of debugging) by changing it to simp only [A,D]; rw [B]; simp only [C,E,...].

Scott attempted to start collecting examples in leanprover-community/mathlib4#5026 but only very late on during the porting process. I also made a more haphazard collection of some examples where simp only [X] failed but rw [X] succeeded at this Zulip thread. The example here started off as such an issue: see here (this example was coming from porting the sphere eversion project). A week later Patrick had entirely taken the simp call apart and it was an instance of the standard phenomenon: simp only [X] would fail but rw [X] would work. Then Eric took over and we ended up with the example which starts this thread. So perhaps some subset of the failing simp only calls are due to this phenomenon. However #2461 also started off as another example of the "simp only [X] fails, rw [X] works" phenomenon and it wouldn't surprise me if it were unrelated. Hence it's difficult for me to know how much disruption this particular issue is causing.