typeclass loops

Stream: mathlib4

[Kevin Buzzard]

I was experimenting with making OrderDual a structure, to see if it helped with the issue reported here and noted here. In doing so I noticed that the declaration in question, namely def liftSemilatticeInf [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α :=, actually has some proofs being proofs of the fields for SemilatticeInf αᵒᵈᵒᵈ, and we make it home because of defeq abuse. This made me wonder whether we should instead be defining def liftSemilatticeInf [SemilatticeInf βᵒᵈ] (gi : GaloisCoinsertion l u) : SemilatticeInf αᵒᵈ := so we can avoid this defeq abuse. However the problem with this approach is that whilst Mathlib4 can infer PartialOrder αᵒᵈ from PartialOrder α, right now it can't currently infer PartialOrder α from PartialOrder αᵒᵈ. In Lean 3 I think this would be a bad instance because it would loop. Is this instance OK in Lean 4 though? I vaguely remember promises that loops would be fine.

[Eric Wieser]

This might work for partial_order, but once you get to typeclasses with Sup and Inf, the resultant loop will not be defeq

[Eric Wieser]

So I don't think this is a pattern we should encourage in general

[Eric Wieser]

And if we're not going to use it generally, you can just use a def for the one place you actually need it; inside the liftSemilatticeInf lemma