PR !4#21344: chore: attempt to avoid diamond in OreLocali...

Stream: triage

[Random Issue Bot]

Today I chose PR #21344 for discussion!

chore: attempt to avoid diamond in OreLocalization
Created by @Kevin Buzzard (@kbuzzard) on 2025-02-02
Labels: please-adopt, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

This was my attempt to solve a problem which I later realised was beyond my understanding. @Andrew Yang what should I do with this? Just close it? IIRC you've thought about this issue since the PR.

[Yaël Dillies]

I have also thought about this, and my current belief is that it is unsolvable :frown:

[Andrew Yang]

I still come back and think about this from time to time and now that the LocalizedModule refactor is in we might be able to experiment more freely on options that could make the situation better.

[Eric Wieser]

Is this the thing that Andrew and I were discussing at Big Proof, where we made conflicting PRs and then ran out of time to review either?

[Andrew Yang]

Yes. I don’t plan on changing any definitions now so you could try again if your idea is still working and whether it does improve on the situation if you have time.

[Eric Wieser]

Ah, so your work got merged or deliberately abandoned?

[Andrew Yang]

It is merged now.