nested linear map norm failure

Stream: mathlib4

[Matthew Ballard]

This is strange

import Mathlib.Analysis.NormedSpace.OperatorNorm

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

#synth Norm ((𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜) -- ContinuousLinearMap.hasOpNorm
#synth Norm (𝕜 →L[𝕜] (𝕜 →L[𝕜] 𝕜)) -- ContinuousLinearMap.hasOpNorm
#synth Norm (𝕜 →L[𝕜] (𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜) -- failed

[Patrick Massot]

I’ve seen this many times, it’s the curse of the operator norm.

[Matthew Ballard]

Each time it pulls off a k except the last time we get

[synthInstance] ✅ SeminormedAddCommGroup k ▼
            [] result NonUnitalSeminormedRing.toSeminormedAddCommGroup (cached)

On the last one it, it doesn’t try to synthesize this and just puts in a metavariable. It then gets stuck of course

[Matthew Ballard]

First

[isDefEq] ❌ SeminormedAddCommGroup (k →L[k] k →L[k] k) =?= SeminormedAddCommGroup (?m.7403 →SL[?m.7411] ?m.7404) ▼
                  [] ❌ k →L[k] k →L[k] k =?= ?m.7403 →SL[?m.7411] ?m.7404 ▼
                    [] ✅ k =?= ?m.7401 ▶
                    [] ✅ k =?= ?m.7402 ▶
                    [] ✅ RingHom.id k =?= ?m.7411 ▶
                    [] ✅ k =?= ?m.7403 ▶
                    [] ✅ k →L[k] k =?= ?m.7404 ▶
                    [] ✅ DivisionSemiring.toSemiring =?= DivisionSemiring.toSemiring ▶
                    [] ✅ DivisionSemiring.toSemiring =?= DivisionSemiring.toSemiring
                    [synthInstance] ✅ SeminormedAddCommGroup k ▼
                      [] result NonUnitalSeminormedRing.toSeminormedAddCommGroup (cached)
                      [isDefEq] ✅ SeminormedAddCommGroup k =?= SeminormedAddCommGroup k
                    [] ✅ UniformSpace.toTopologicalSpace =?= UniformSpace.toTopologicalSpace ▶
                    [] ✅ NonUnitalNonAssocSemiring.toAddCommMonoid =?= AddCommGroup.toAddCommMonoid ▶
                    [synthInstance] ❌ SeminormedAddCommGroup (k →L[k] k) ▼

and then finally

[isDefEq] ❌ SeminormedAddCommGroup (k →L[k] k) =?= SeminormedAddCommGroup (?m.7426 →SL[?m.7434] ?m.7427) ▼
                            [] ❌ k →L[k] k =?= ?m.7426 →SL[?m.7434] ?m.7427 ▼
                              [] ✅ k =?= ?m.7424 ▶
                              [] ✅ k =?= ?m.7425 ▶
                              [] ✅ RingHom.id k =?= ?m.7434 ▶
                              [] ✅ k =?= ?m.7426 ▶
                              [] ✅ k =?= ?m.7427 ▶
                              [] ✅ DivisionSemiring.toSemiring =?= DivisionSemiring.toSemiring ▶
                              [] ✅ DivisionSemiring.toSemiring =?= DivisionSemiring.toSemiring
                              [] ❌ UniformSpace.toTopologicalSpace =?= UniformSpace.toTopologicalSpace ▶

[Matthew Ballard]

Replace k with distinct modules won’t fix it. That is where I came from

[Matthew Ballard]

Aha! trace.Meta.synthPending reports:

[Meta.synthPending] too many nested synthPending invocations

Thank goodness this one was plugged in lol

[Matthew Ballard]

From docs#Lean.Meta.Context

Remark: in the current implementation, synthPending fails if synthPendingDepth > 0.
We will add a configuration option if necessary. -/

[Matthew Ballard]

I am not sure why we get depth > 0 after 4 copies of k and not less (or more?)

[Matthew Ballard]

It hits that because for k →L[k] k →L[k] k →L[k] k it needs to synth SeminormedAddCommGroup for the last k →L[k] k →L[k] k and then needs to do it again for k →L[k] k which trips the wire.

For k →L[k] k →L[k] k it does it once for k →L[k] k and then can figure out the SeminormedAddCommGroup k for the source and target

[Jireh Loreaux]

Note: this issue came up for me recently too. Search RegularNormedAlgebra

[Matthew Ballard]

Oh. I guess I missed something or I should have suspecting synthPending immediately.

[Matthew Ballard]

Going to test changes to the default synthPendingDepth. Anyone have any good numbers besides 0?

[Sébastien Gouëzel]

1? 100?

[Matthew Ballard]

$\infty$ :smiling_devil:

[Ruben Van de Velde]

37

[Michael Stoll]

5077

[Matthew Ballard]

I quickly learned this is the only thing keeping synthInstance from looping

[Mario Carneiro]

this discussion reminds me of https://www.youtube.com/watch?v=0obMRztklqU