Zulip Chat Archive
Stream: mathlib4
Topic: weird type class synthesis error
Jireh Loreaux (Feb 09 2024 at 20:55):
I'm hoping that somehow I've just been really stupid (either now or in my development of docs#Unitization), and the answer to this is obvious, but right now I find this to be a real head scratcher:
The problem is type class synthesis can't find Unitization.instNormedRing?
Anatole Dedecker (Feb 09 2024 at 23:04):
It looks like the error doesn't come from unital/nonunital but from the second variable line stating the "normed algebra" condition. That is, this also fails:
variable {A : Type*} -- A is a unital C⋆-algebra.
variable [NormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A]
variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
example (x : Unitization ℂ A) (hx : IsSelfAdjoint x) : spectralRadius ℂ x = 0 := by
rw [hx.spectralRadius_eq_nnnorm] -- fails
sorry
Anatole Dedecker (Feb 09 2024 at 23:08):
Ah, this is actually not a type class synthesis error, the indication was in the second error message
failed to synthesize instance
NormedRing (Unitization ℂ A)
Anatole Dedecker (Feb 09 2024 at 23:10):
Adding [RegularNormedAlgebra ℂ A] to the variables solves it, but it shouldn't be needed right ?
Jireh Loreaux (Feb 09 2024 at 23:11):
(deleted)
Anatole Dedecker (Feb 09 2024 at 23:12):
And just adding let _ : RegularNormedAlgebra ℂ A := inferInstance just before also works ?!?!?
Jireh Loreaux (Feb 09 2024 at 23:13):
Yeah, Lean should be able to find that instance I think.
Jireh Loreaux (Feb 09 2024 at 23:14):
We have docs#CstarRing.instRegularNormedAlgebra
Anatole Dedecker (Feb 09 2024 at 23:14):
It's very weird that it finds it when asked but otherwise doesn't
Jireh Loreaux (Feb 09 2024 at 23:15):
I know. I need to test if this broke with the latest release candidate or not, but I'm busy right now.
Matthew Ballard (Feb 09 2024 at 23:28):
This seems to end on a stuck meta variable ?m.41224 : StarRing (Unitization \C A)
Matthew Ballard (Feb 09 2024 at 23:31):
[] ✅ Star (Unitization ℂ A) =?= Star (Unitization ℂ A)
[] ❌ star =?= fun ra => (star (Unitization.fst ra), star (Unitization.snd ra)) ▼
[] ❌ fun ra => (star (Unitization.fst ra), star (Unitization.snd ra)) =?= fun a => star a ▼
[] ✅ Unitization ℂ A =?= Unitization ℂ A
[] ❌ (star (Unitization.fst ra), star (Unitization.snd ra)) =?= star ra ▼
[] ❌ (star (Unitization.fst ra), star (Unitization.snd ra)) =?= StarAddMonoid.toInvolutiveStar.1.1 ra ▼
[] ✅ Unitization ℂ A =?= ℂ × A ▶
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= star (Unitization.fst ra) ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= star (Unitization.fst ra) ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= InvolutiveStar.toStar.1 (Unitization.fst ra) ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= { re := (Unitization.fst ra).re, im := -(Unitization.fst ra).im } ▼
[] ✅ ℂ =?= ℂ
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1.re =?= (Unitization.fst ra).re ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= Unitization.fst ra ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= ra.1 ▼
[] ❌ (StarAddMonoid.toInvolutiveStar.1.1 ra).1 =?= ra.1 ▼
[] ❌ StarAddMonoid.toInvolutiveStar.1.1 ra =?= ra ▼
[onFailure] ❌ StarAddMonoid.toInvolutiveStar.1.1 ra =?= ra ▼
[stuckMVar] found stuck MVar ?m.41224 : StarRing (Unitization ℂ A)
Anatole Dedecker (Feb 10 2024 at 00:14):
It’s weird that it gets stuck on StarRing since this part doesn’t depend on RegularNormedAlgebra
Kevin Buzzard (Feb 10 2024 at 09:54):
I posted another example due to Amelia recently where typeclass inference randomly fails to find an instance on a finsupp. They are so hard to minimise though :-(
Eric Wieser (Feb 10 2024 at 10:40):
Is the problem this line? https://github.com/leanprover-community/mathlib4/blob/b1a09514e5543efb07e5748b55bcbf1d9bd32655/Mathlib/Algebra/Algebra/Unitization.lean#L600
Eric Wieser (Feb 10 2024 at 10:41):
I think @Matthew Ballard concluded we're not supposed to use RingHoms to build Algebras, because RingHom.comp isn't reducible
Eric Wieser (Feb 10 2024 at 10:41):
If that's the case, adding a toFun field would fix it
Jireh Loreaux (Feb 10 2024 at 16:05):
I just tested that, no success. Note: It's easy to test changes to Unitization because there's only two files you need to build.
Jireh Loreaux (Feb 11 2024 at 01:03):
This line really concerns me. Lean should not be asking about ℂ × A at all.
[] ✅ Unitization ℂ A =?= ℂ × A ▶
It makes me suspect that something is causing Lean to see through the (default transparency) def. I'm going to try upgrading the barrier between the two to see if that helps.
Eric Wieser (Feb 11 2024 at 07:53):
It would be nice to understand why the current approach is leaking; though indeed upgrading to a structure would fix it
Jireh Loreaux (Feb 12 2024 at 16:06):
Well, this is somewhat depressing: I went through the annoying work of turning docs#Unitization into a structure, but the error persists, albeit in this case it just fails to find an occurrence of the pattern in the expression.
Jireh Loreaux (Feb 12 2024 at 16:06):
The trick of supplying the RegularNormedAlgebra instance manually still fixes it.
Jireh Loreaux (Feb 12 2024 at 16:06):
You can play for yourself at branch#j-loreaux/Unitization-structure
Jireh Loreaux (Feb 12 2024 at 16:07):
Even if the full cache isn't there yet, it only takes about a minute to build the imports for the example file given at the top of the thread.
Jireh Loreaux (Feb 12 2024 at 16:11):
How about this line as the problem (at this point, I'm just flailing)?
instance [Zero R] : CoeTC A (Unitization R A) where
coe := inr
Should we not be using CoeTC? (EDIT: still fails with CoeTail; although I'm still wondering whether or not we should be using CoeTC here.)
Jireh Loreaux (Feb 12 2024 at 16:18):
One more thing to note: I did try this on master prior to the 4.6.0 bump and the error exists there too. I didn't go further back than that.
Anne Baanen (Feb 12 2024 at 18:06):
I agree that CoeTC is suspicious. These were introduced in the port because we aligned coe_out to it, but it's not supposed to be instantiated in mathlib code. I didn't have enough time today to check this out, hopefully I can get to it tomorrow.
Anne Baanen (Feb 13 2024 at 10:39):
Jireh Loreaux said:
This line really concerns me. Lean should not be asking about
ℂ × Aat all.[] ✅ Unitization ℂ A =?= ℂ × A ▶It makes me suspect that something is causing Lean to see through the (default transparency)
def. I'm going to try upgrading the barrier between the two to see if that helps.
This seems to happen because docs#Unitization.instStar is unfolded (at default transparency, so it doesn't matter whether this is an instance or a def) when elaborating hx.spectralRadius_eq_nnnorm. It doesn't matter whether Unitiziation is a def or a structure, we can't block unfolding instStar. And it needs to be reducible to make the rest of the file where it's defined work.
So it's not the rw tactic but just elaborating a term. For example, the following code also reproduces the issue:
import Mathlib.Analysis.NormedSpace.Star.Spectrum
import Mathlib.Analysis.NormedSpace.Star.Unitization
variable {A : Type*} -- A is a unital C⋆-algebra.
variable [NormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A]
variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
example (x : Unitization ℂ A) (hx : IsSelfAdjoint x) : spectralRadius ℂ x = 0 := by
-- let _ : RegularNormedAlgebra ℂ A := inferInstance -- Uncomment to make everything work.
have := hx.spectralRadius_eq_nnnorm
sorry
As part of this defeq check the NormedRing (Unitization ℂ A) instance needs to be synthesized, which causes all the downstream issues.
Anne Baanen (Feb 13 2024 at 10:46):
Specifically the defeq check goes up to [stuckMVar] found stuck MVar ?m.41224 : StarRing (Unitization ℂ A) as Matt described can be made unstuck by instance synthesis, and then we get to the mysterious failing search that works by itself.
Anne Baanen (Feb 13 2024 at 10:47):
If we look at the synthesis goal StarRing (Unitization ℂ A) then it turns out it actually has a metavariable of its own: @StarRing (Unitization ℂ A) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring (... (@NormedRing.toRing (Unitization ℂ A) ?m.22212)))
Anne Baanen (Feb 13 2024 at 10:49):
By itself StarRing (Unitization ℂ A) gets the instance Unitization.instNonAssocRing in place of the NormedRing metavariable.
Anne Baanen (Feb 13 2024 at 10:53):
Some more trace output:
[] ❌ apply @Unitization.instStarRing to StarRing (Unitization ℂ A) ▼
[tryResolve] ❌ StarRing (Unitization ℂ A) ≟ StarRing (Unitization ?m.30771 ?m.30772) ▼
[isDefEq] ❌ StarRing (Unitization ℂ A) =?= StarRing (Unitization ?m.30771 ?m.30772) ▼
[] ✅ Unitization ℂ A =?= Unitization ?m.30771 ?m.30772 ▶
[] ❌ NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring =?= NonAssocSemiring.toNonUnitalNonAssocSemiring ▼
...
[] ❌ (NonUnitalNonAssocSemiring.toAddCommMonoid.1.1.1.1 p q).1 =?= AddSemigroup.toAdd.1 p.1 q.1 ▼
[onFailure] ❌ (NonUnitalNonAssocSemiring.toAddCommMonoid.1.1.1.1 p q).1 =?= AddSemigroup.toAdd.1 p.1 q.1 ▼
[stuckMVar] found stuck MVar ?m.30750 : NormedRing (Unitization ℂ A)
[synthInstance] ❌ NormedRing (Unitization ℂ A) ▶
Anne Baanen (Feb 13 2024 at 11:05):
So now we get into the root cause:
[] new goal NormedRing (Unitization ℂ A) ▶
[] ✅ apply @Unitization.instNormedRing to NormedRing (Unitization ℂ A) ▶
...
[] ❌ apply CstarRing.instRegularNormedAlgebra to RegularNormedAlgebra ℂ A ▼
[tryResolve] ❌ RegularNormedAlgebra ℂ A ≟ RegularNormedAlgebra ?m.30893 ?m.30894 ▼
[isDefEq] ❌ RegularNormedAlgebra ℂ A =?= RegularNormedAlgebra ?m.30893 ?m.30894 ▼
[] ✅ ℂ =?= ?m.30893 ▶
[] ✅ A =?= ?m.30894 ▶
[] ❌ inst✝³ =?= ?m.30899 ▼
[] inst✝³ [nonassignable] =?= ?m.30899 [assignable]
[] ❌ NormedSpace ℂ A =?= NormedSpace ℂ A ▼
[] ✅ ℂ =?= ℂ
[] ✅ A =?= A
[] ❌ DenselyNormedField.toNormedField =?= Complex.instNormedFieldComplex ▼
[] ❌ DenselyNormedField.toNormedField =?= NormedField.mk Complex.instNormedFieldComplex.proof_1
Complex.instNormedFieldComplex.proof_2 ▼
[] ❌ ?m.30895.1 =?= NormedField.mk Complex.instNormedFieldComplex.proof_1 Complex.instNormedFieldComplex.proof_2 ▼
[] ✅ NormedField ℂ =?= NormedField ℂ ▶
[] ❌ NormedField.toNorm =?= Complex.instNormComplex ▼
[] ❌ NormedField.toNorm =?= { norm := ⇑Complex.abs } ▼
[] ❌ ?m.30895.1.1 =?= { norm := ⇑Complex.abs } ▼
[] ✅ Norm ℂ =?= Norm ℂ ▶
[] ❌ norm =?= ⇑Complex.abs ▼
[] ❌ ?m.30895.1.1.1 =?= AbsoluteValue.funLike.1 Complex.abs ▼
[] ❌ ?m.30895.1.1.1 =?= Complex.abs.toFun ▼
[] ❌ ?m.30895.1.1.1 =?= Complex.abs.toMulHom.1 ▼
[] ❌ ?m.30895.1.1.1 =?= fun x => Real.sqrt (Complex.normSq x) ▼
[] ❌ fun x => Real.sqrt (Complex.normSq x) =?= fun a => ?m.30895.1.1.1 a ▼
[] ✅ ℂ =?= ℂ
[] ❌ Real.sqrt (Complex.normSq x) =?= ?m.30895.1.1.1 x ▼
[] ❌ ↑(NNReal.sqrt (Real.toNNReal (Complex.normSq x))) =?= ?m.30895.1.1.1 x ▼
[] ❌ ↑(NNReal.sqrt (Real.toNNReal (Complex.normSq x))) =?= ?m.30895.1.1.1 x ▼
[] ❌ (NNReal.sqrt (Real.toNNReal (Complex.normSq x))).1 =?= ?m.30895.1.1.1 x ▼
[onFailure] ❌ (NNReal.sqrt (Real.toNNReal (Complex.normSq x))).1 =?= ?m.30895.1.1.1 x ▼
[stuckMVar] found stuck MVar ?m.30895 : DenselyNormedField ℂ
Anne Baanen (Feb 13 2024 at 11:06):
It tuns out the ultimate problem is a stuck MVar ?m.30895 : DenselyNormedField ℂ which doesn't get unstuck!
Anne Baanen (Feb 13 2024 at 11:22):
Is this maybe the return of leanprover/lean4#2522?
Anne Baanen (Feb 13 2024 at 11:27):
Ah no, this is just a consequence of the code here: with set_option trace.Meta.synthPending we get [synthPending] too many nested synthPending invocations
Anne Baanen (Feb 13 2024 at 11:30):
So I suppose the question is: should we increase the limit of nested invocations of synthPending? Or can we work around the issue in another way?
Anne Baanen (Feb 13 2024 at 11:32):
This is as much as I can do today, hopefully this helps getting the issue unstuck!
Jireh Loreaux (Feb 13 2024 at 13:40):
Thanks for your help debugging this @Anne Baanen !
Jireh Loreaux (Jul 09 2024 at 16:20):
@Anne Baanen : I was asked by @Frédéric Dupuis here to revisit this issue now that we have new tools, like seal and unseal. But, if I understand correctly, neither of those will fix this issue since (a) Unitization.instStar still has to be unfolded, and (b) the issue is really about extra metavariables that don't get solved resulting in the extra synthPending depth.
Basically, it would be great if we can fix this now, but I still don't see a path towards that. Do you have some insight that I may be missing?
Anne Baanen (Jul 10 2024 at 10:06):
So the naïve idea doesn't seem to work:
import Mathlib.Analysis.NormedSpace.Star.Spectrum
import Mathlib.Analysis.NormedSpace.Star.Unitization
variable {A : Type*} -- A is a unital C⋆-algebra.
variable [NormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A]
variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
seal Unitization.instStar
example (x : Unitization ℂ A) (hx : IsSelfAdjoint x) : spectralRadius ℂ x = 0 := by
have := hx.spectralRadius_eq_nnnorm -- fails like before
sorry
example (x : Unitization ℂ A) (hx : IsSelfAdjoint x) : spectralRadius ℂ x = 0 := by
let _ : RegularNormedAlgebra ℂ A := inferInstance
have := hx.spectralRadius_eq_nnnorm -- works like before
sorry
Anne Baanen (Jul 10 2024 at 10:06):
I kind of forgot the details of what is going wrong, so let me check again...
Anne Baanen (Jul 10 2024 at 10:25):
Okay, I can reproduce the issue like before, and with seal Unitization.instStar Unitization.instAddCommMonoid the unfolding to ℂ × A doesn't happen. So I don't think seal is going to help.
Anne Baanen (Jul 10 2024 at 11:04):
Here's a re-explanation of the issue. When trying to apply spectralRadius_eq_nnorm to hx, Lean needs to check the type of hx : IsSelfAdjoint x. docs#IsSelfAdjoint depends on an instance of Star (Unitization ℂ A). We have multiple instances: docs#Unitization.instStar (inferred for hx) and a path that goes from NormedRing to Star (inferred for spectralRadius_eq_nnorm.
The thing is, at this point spectralRadius_eq_nnorm has no idea which normed ring it's being called on: its instances are postponed. So we try to unify the two Star (Unitization ℂ A) instances, until we hit a dead end: on the left we have Unitization.instStar and on the right we have InvolutiveStar.toStar (StarAddMonoid.toInvolutiveStar (StarRing.toStarAddMonoid ?m.57268)). These are all projections of some unknown value, which can't reduce further.
Thankfully, Lean has a procedure to escape the dead end. Finding a StarRing instance might supply an actual structure in the place of ?m.57268 which we can then unfold and project to check for equality. So the search for a StarRing (Unitization ℂ A) instance starts, and almost instantly we can apply docs#Unitization.instStarRing.
But now the same issue happens! Because the class StarRing (Unitization ℂ A) depends on the ring structure on Unitization ℂ A. And Unitization.instStarRing uses docs#Unitization.instNonAssocSemiring while the instance goal is still assuming we have some NormedRing instance to project away. So we get stuck again trying to prove that Unitization.instNonAssocSemiring.toNonUnitalNonAssocSemiring is defeq to NonAssocSemiring.toNonUnitalNonAssocSemiring (Semiring.toNonUnitalSemiring (Ring.toSemiring (NormedRing.toRing ?m.57265)))).
We can escape the dead end again by finding a value for ?m.57265, this time of type NormedRing (Unitization ℂ A). And soon we can apply docs#Unitization.instNormedRing. This has a bunch of instances we need to search for, and they all go well until we hit the last one: RegularNormedAlgebra ℂ A. We should be able to apply docs#CstarRing.instRegularNormedAlgebra.
Now here's where the magic happens. We try to unify the RegularNormedAlgebra ℂ A instance goal with the type of CstarRing.instRegularNormedAlgebra. RegularNormedAlgebra depends on a bunch of instances itself, but these are all filled in by the previous steps. In particular a NormedSpace ℂ A instance has been found (which is inst³ in the context). The type of CstarRing.instRegularNormedAlgebra doesn't have these instances filled in yet. So let's see if we can't assign a few through unification. Namely, the NormedSpace ℂ A one. Only thing we need to do is check the type: is the instance inst³ : NormedSpace ℂ A we found in the context of the right type to fill in the metavariable ?m.57392 : NormedSpace ℂ A? Only if the arguments to NormedSpace are equal. Apart from the explicit ℂ and A we also need a NormedField ℂ instance.
The NormedField ℂ instance used in inst³ : NormedSpace ℂ A is docs#Complex.instNormedField. But CstarRing.instRegularNormedAlgebra depends on a docs#DenselyNormedField instance. And recall that we haven't assigned any instances yet! So we have to check that Complex.instNormedField equals DenselyNormedField.toNormedField ?m.57388. Oops, we have yet again a projection applied to a metavariable and we're stuck.
We can get unstuck again by looking for a DenselyNormedField ℂ instance. But at this point Lean sees it's three levels deep in the same unify → stuck → find instance → unify → ... loop and decides to fail outright. The NormedSpace unification fails, which means CstarRing.instRegularNormedAlgebra isn't applied, which means Unitization.instNormedRing isn't applied, which means Unitization.instStarRing isn't applied, which means the unification fails right at the start.
Anne Baanen (Jul 10 2024 at 11:08):
So we can't avoid this failure by making things irreducible. It's to do with the structure of classes and instances.
Anne Baanen (Jul 10 2024 at 11:18):
Haven't figured out how to minimize this, but the crucial part is we have a class C whose type depends on an instance of another class D, and we have instances of C that instead depend on a subclass of D. And if D in turn does the same thing, we get into this mess.
Kevin Buzzard (Jul 10 2024 at 18:53):
You can fix this sort of problem by increasing maxSynthPendingDepth. Sorry if this is known to everyone already, I just didn't see it mentioned yet in this thread:
import Mathlib.Analysis.NormedSpace.Star.Spectrum
import Mathlib.Analysis.NormedSpace.Star.Unitization
variable {A : Type*} -- A is a unital C⋆-algebra.
variable [NormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A]
variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
set_option maxSynthPendingDepth 2 in
example (x : Unitization ℂ A) (hx : IsSelfAdjoint x) : spectralRadius ℂ x = 0 := by
have := hx.spectralRadius_eq_nnnorm -- now works
sorry
This option is already being used several times in mathlib, e.g. in NumberTheory.NumberField.Units.Regulator this option is set globally near the top of the file. I only understood that this was a possible solution after Anne's careful explanation of the problem above. Edit: oh now I see where this solution is mentioned -- it's in the PR. Sorry for the noise!
Jireh Loreaux (Jul 10 2024 at 21:30):
Thanks for the very detailed explanation Anne!
Jireh Loreaux (Jul 10 2024 at 21:34):
Do we have a way to clearly tell that Lean hit the max synthPending depth? It will be very frustrating to run into this example repeatedly in various contexts.
I suspect one way to avoid it going forward is to create some actual classes for C*-algebras (i.e., bundle all the bits together), to minimize type class searches. But I don't think that would fix this particular issue.
Anne Baanen (Jul 11 2024 at 08:14):
The only diagnostics I know are to scroll down in the trace until you find a [stuckMVar] found stuck MVar ?m.30895 : DenselyNormedField ℂ without a following [synthInstance] DenselyNormedField ℂ line
Last updated: May 02 2025 at 03:31 UTC