instance in both directions

Stream: mathlib4

[Artie Khovanov]

All formally real rings are semireal. A semireal field is formally real. Do I have to choose one of these to register as an instance, and manually pass the other in whenever I need to use it? Or is there some way around this?

[Sébastien Gouëzel]

You can register both as instances.

[Anne Baanen]

The rule is that instance loops are allowed, as long as it loops back to an exactly syntactically equal goal. So IsFormallyReal R -> Semireal R -> IsFormallyReal R is allowed, but something like Finite a -> Finite (Sum a b) -> Finite (Sum (Sum a b) b) -> ... would loop forever.

[Floris van Doorn]

Perhaps not directly related to your question: For performance reasons it might not be a good idea to have all of these "upgrading" instances as global instances in Mathlib. With an upgrading instance I mean an instance where a stronger class is inferred from a weaker class in special cases.

An example of this is docs#littleWedderburn. Suppose I write x * y, where x and y are in some type A without multiplication. Before Lean raises can raise an error, it has to navigate all instances that involve multiplication, including littleWedderburn. I'm not quite sure about the instantiation order for that instance, but unless we're very careful (and in general, we're not careful at all), type class inference will now try to infer Finite A to find out whether A has a multiplication. When I investigated some very slow type-class inference failures a year ago, to figure out whether some type was a subsingleton, it would basically navigate all algebraic, topological, order-theoretic and some categorical classes before it could conclude whether the type was a subsingleton.

I think scoping some well-chosen instances in Mathlib could lead to significant speed-ups, at the cost of requiring users to open namespaces more often (and unfortunately getting unhelpful error messages if they don't).