What is an outParam?

Stream: mathlib4

[Kevin Buzzard]

I have always ignored how type class inference works in the past, dismissing it as "too CS for me". My current level of understanding is that I'm dimly aware that it might be a "prolog-like search" but I don't really know what that means. Of course I know in practice what type class inference does in mathlib, and that understanding of the "basic idea" has been all I've needed.

In the past I have been able to remain ignorant about the details of type class inference very effectively because type class inference issues never really affected me in Lean 3. There were plenty of experts here who had mastered them, and my experience with Lean 3 was that they "just worked".

With Lean 4 the situation is different. There are type class inference issues coming up all the time, when porting files I care about, and in stark contrast to Lean 3 right now there are more questions than answers. Just in the last two days we've had this question and this question, and there are issues lean4#1852 (which I don't understand properly) and of course lean4#2003 fixing my issue lean4#1986 but still not merged so we're still having to work around it, as well as my new issue lean4#2055. I'm hence minded to actually try and understand properly how type class inference works, not least because I suspect that it will not be too hard for me to get my head around it given that I have a pretty good working knowledge of what it's doing in practice.

In the past when I have not understood things I have attempted to write documents explaining them: for example I wrote the first version of this page on simp many years ago, when I was getting the hang of simp, and the write-up was so bad that it forced other people to write a better one ;-) I now understand simp so well that I can teach it. I would like to get to the same situation with type class inference.

A lot of discussion recently has been about outParams, as out_params are called in Lean 4. One marked improvement of Lean 4 over Lean 3 is that documentation of the source code is much better, so I can read the docstring for outParam, which I quote here:

Gadget for marking output parameters in type classes.

For example, the `Membership` class is defined as:
```
class Membership (α : outParam (Type u)) (γ : Type v)
```
This means that whenever a typeclass goal of the form `Membership ?α ?γ` comes
up, lean will wait to solve it until `?γ` is known, but then it will run
typeclass inference, and take the first solution it finds, for any value of `?α`,
which thereby determines what `?α` should be.

This expresses that in a term like `a ∈ s`, `s` might be a `Set α` or
`List α` or some other type with a membership operation, and in each case
the "member" type `α` is determined by looking at the container type.

I am already a little lost with this, and it's a pretty simple example. I can write my own Membership' without the outParam and it seems to work fine:

import Mathlib

variables (X : Type) (a : X) (S : Set X)

#check a ∈ S -- works fine

-- no outParam
class Membership' (α : Type u) (γ : Type v) where
  /-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. -/
  mem : α → γ → Prop

instance {α : Type} : Membership' α (Set α) where
  mem := Set.Mem

#check Membership'.mem a S -- works fine

So clearly the outParam is needed to cover some other use case. But I don't understand what that use case is: I'm missing something completely fundamental. The docs say "This means that whenever a typeclass goal of the form Membership ?α ?γ comes
up...". When does such a goal ever come up? I never write _ ∈ _ in my code, I write a ∈ S, and I would not expect _ ∈ _ to ever be useful. What am I missing?

I think my problem is that my model of what type class inference does is "it solves monoid X given normed_field X", but that this model is too simplistic. What is the next simplest case? What is the simplest case of type class inference which actually happens in practice and needs outParams? I had a vague idea that it showed up in Module R M but I've looked at the source code and I can't see any outParams there.

[Johan Commelin]

Non-mathlib example: remember that we has class module (R : out_param Type) (M : Type)?
That way, if you passed around some x : M, Lean would be able to figure out R from that info.

[Johan Commelin]

But we decided (rightly), that we want multiple Rs for one M. So in that case out_param was a bad design choice.

[Floris van Doorn]

The goal of outParam is that type class inference search will fire if that argument is unknown. So the fact that αis an out-param of Membership means that Lean can understand what a ∈ S means even though it doesn't know the type of a (if it knows the type of S). Here is how the difference shows in your example. Note that I'm not specifying the type of a.

import Mathlib.Data.Set.Basic

variable (X : Type) (S : Set X)

example := fun a => a ∈ S -- works fine

-- no outParam
class Membership' (α : Type u) (γ : Type v) where
  /-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. -/
  mem : α → γ → Prop

instance {α : Type} : Membership' α (Set α) where
  mem := Set.Mem

example := fun a => Membership'.mem a S -- cannot figure out the type of `a`.

[Kevin Buzzard]

OK so this I understand. What I don't understand is why typeclass inference ever needs to solve such a problem. Maybe I should now go back and look at the issues which had come up recently.

[Kevin Buzzard]

So let's take a look at this example from one of the threads:

import Mathlib.Order.Hom.Basic

class SupHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] extends
  FunLike F α fun _ => β where
  map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b

class LatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β] extends
  SupHomClass F α β where
  map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b

class BoundedLatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β]
  [BoundedOrder α] [BoundedOrder β] extends LatticeHomClass F α β where
  map_top (f : F) : f ⊤ = ⊤
  map_bot (f : F) : f ⊥ = ⊥

instance (priority := 100) SupHomClass.toOrderHomClass [SemilatticeSup α] [SemilatticeSup β]
    [SupHomClass F α β] : OrderHomClass F α β :=
  { ‹SupHomClass F α β› with
    map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }

example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    OrderHomClass F α β :=
SupHomClass.toOrderHomClass -- works

set_option synthInstance.maxHeartbeats 400 in -- to stop huge outputs crashing VS code
set_option trace.Meta.synthInstance true in
example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    OrderHomClass F α β :=
inferInstance -- loops

My completely deficient mental model of this situation is: the typeclass inference system is asked "I'll give you instances of Lattice α, Lattice β etc -- now you go and find me an instance of OrderHomClass F α β. My answer to that (I am "being the type class inference system") is "[pause while I shuffle through this big list of instances I have...] sure: SupHomClass.toOrderHomClass is an instance so I'll use that -- I guess I need to now find instances of SemilatticeSup α, SemilatticeSup β and SupHomClass F α β but these are equally easily solved using other instances in my database". Job done! What am I missing? Why are people going on about outParams in that thread?

[Kevin Buzzard]

example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    SemilatticeSup α :=
inferInstance

example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    SupHomClass F α β :=
inferInstance

etc

[Anne Baanen]

The important part about out params is that they allow Lean to solve goals of the form OrderHomClass F ?_ ?_, where the values for α and β are not yet known. This is useful because it allows you to write something like ∀ x y, f x ≤ f y without having to hint that x : α and f x : β: those are the output of searching for the instance (hence out-param).

[Anne Baanen]

Due to dependent types, we could (and did, in the case of has_coe_to_fun before it was backported from Lean 4) instead turn α and β into fields in the class, so something like:

class CoeFun (F : Type) where
  (α β : Type)
  (toFun : F → α → β)

This should give you exactly the same mental image of the class as the current outParam based implementation.

(I'm omitting universe parameters, which would make this slightly more awkward.)

[Sebastian Ullrich]

Note also that the behavior of outParams and "in params" (all other params) is in fact disjoint: If you ask Lean to infer OrderHomClass F α β, it will actually start with the goal OrderHomClass F ?α ?β -- it will actively forget that it already knew something about the outParam values, which is important to make elaboration less dependent on the exact elaboration ordering. So as the next step it will try to infer [Lattice ?α], which is usually a bad idea.

[Anne Baanen]

However, we get a problem when we want to talk about the order on α and β. We would have to add these orderings as fields:

class OrderHomClass (F : Type) where
  (α β : Type)
  [leα : LE α] [leβ : LE β]
  (toFun : α → β)
  (map_le : ∀ f x y, x ≤ y → toFun f x ≤ toFun f y)

Now trying to apply OrderHomClass.map_le f doesn't give you any guarantee that f's idea of ≤ coincides with yours. So we somehow have to put the LE instances into the type of map_le. And we can only do this when α β are also in the type, which we can only do by making them outParams.

[Sebastian Ullrich]

Sebastian Ullrich said:

it will actively forget that it already knew something about the outParam values

Note however that this only applies to the initial TC goal; as soon as typeclass inference is running, outParam is irrelevant

[Kevin Buzzard]

Wait a minute!

If you ask Lean to infer OrderHomClass F α β, it will actually start with the goal OrderHomClass F ?α ?β

Why? Isn't that a crazy idea?

which is important to make elaboration less dependent on the exact elaboration ordering

I don't understand what this means.

[Sebastian Ullrich]

Strictly speaking it's in the name: it is (purely) an output of TC inference. Everything that is not an output is an input, the two are never mixed.

[Anne Baanen]

Is there a technical reason why we have to turn them into metavariables? Or is it (I suppose) just for ease of implementation?

[Anne Baanen]

I came across some cases where Lean 3 would accept an out-param where it wouldn't an in-param: https://github.com/leanprover-community/mathlib/pull/18291/commits/fa1a311b0fdf0784bc0e7830e4e8f9f4985a91b0 but that seems to be more of a case of the resulting out-params being checked at semireducible transparency vs. in-params being checked at the point the instance is applied, with instance-reducible transparency.

[Kevin Buzzard]

So right now TCI (if I can call it that) when faced with

example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    OrderHomClass F α β :=
inferInstance

says "Ok I want to solve OrderHomClass F α β and because the definition of OrderHomClass is

abbrev OrderHomClass (F : Type _) (α β : outParam (Type _)) [LE α] [LE β] :=
  RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)

which mentions outParams I will instead try and solve OrderHomClass F ?1 ?2 even though I know what ?1 and ?2 are. I will now look in my big list of instances -- oh look, here's SupHomClass.toOrderHomClass, so now I need to solve SemilatticeSup ?1 and SemilatticeSup ?2 and SupHomClass F ?1 ?2", and the point is that it's trying to solve SemilatticeSup ?1 next even though it knows what ?1 is but somehow has now forgotten?

[Sebastian Ullrich]

The most important property for elaboration robustness is what I and maybe no-one else is calling monotonicity: assigning a metavariable should not change the output of a subsequent elaboration step other than to change it from failure to success. But if we allowed mixed in/out TC parameters, [OrderHomClass F ?α ?β] and OrderHomClass F α ?β] could certainly both succeed with different answers.

[Kevin Buzzard]

Wait -- isn't there supposed to be precisely one answer to that typeclass problem?

[Sebastian Ullrich]

No, Lean TC problems can have many solutions. The second one is more constrained, so it may skip the first's solution and find a different one.

[Sebastian Ullrich]

Replace α with some constant in the second problem to maybe make it more realistic

[Anne Baanen]

Certainly it seems possible and useful to have a local instance that differs from a global default one, which would violate the one-answer rule.

[Sebastian Ullrich]

In other words, this property is important to guarantee that it doesn't matter in which order we solve TC problems, as long as we can solve them at all

[Kevin Buzzard]

Why doesn't the typeclass inference system immediately abort when faced with the goal SemilatticeSup ?α? It's a manifestly dumb question. The point is that right now there is no way of telling the system this, other than just by letting it time out?

With regards to OrderHomClass, isn't F is supposed to be some proxy for α -> β? I don't understand why OrderHomClass F ?α ?β doesn't have a unique solution (I mean one solution for ?alpha, one for ?beta and one for the term of type OrderHomClass F alpha beta.

[Anne Baanen]

On the other hand I have been considering writing a linter that enforces all of these overlapping instances (to use Haskell terminology) are definitionally equal, and I am rather sure this would save a lot of headaches in mathlib while not majorly breaking any existing patterns.

[Sebastian Ullrich]

Also, I'm not saying that Lean elaboration is perfectly monotonic everywhere, but since TC resolution is deferred by default it's a good property to have here

[Anne Baanen]

So my answer would be: the meaning of "supposed" is "library maintainers should check this", not "the compiler enforces this".

[Kevin Buzzard]

I thought the whole point of type class inference was that it was supposed to be running under the assumption that there was only one solution to every question it was asked, and it was up to maintainers to ensure that this is the case? And yet you're now suggesting that it's been designed to allow the possibility that this is false?

[Kevin Buzzard]

I thought that we remove diamonds from mathlib because they were breaking proofs because they were contradicting assumptions which the typeclass inference system was designed to assume.

[Sebastian Ullrich]

That's not really on the TC system, it could happen even without any inference. If you have two ways to state something, and you use, or have inferred, both of them in two different contexts and then try to combine these parts, you're in trouble unless they are defeq.

[Sebastian Ullrich]

For what it's worth, I believe proper use and propagation of outParams would be far easier to systematically enforce (as in Kevin's

Why doesn't the typeclass inference system immediately abort when faced with the goal SemilatticeSup ?α

) than uniqueness of TC solutions, but this is probably not the time to revise the design of TC inference in such a way...

[Kevin Buzzard]

Right! And for module ?a M we definitely want more than one solution (which is why R is not an outParam). But for OrderHomClass F ?a ?b I am claiming that mathlib is set up so that there is only one solution to that up to defeq, i.e. one choice for ?a, one for ?b, and one for the term of type OrderHomClass F (the right answer) (the right answer), and the outParam is supposed to be telling the system this.

Going back to the example I posted above, the trace looks like this:

[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
  [] new goal RelHomClass F _tc.2 _tc.3 ▶
  [] ✅ apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ▼
    [tryResolve] ✅ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1 ≟ RelHomClass F (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1
    [] new goal SemilatticeSup _tc.0 ▼
      [instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]

and I now understand why the goal has changed from RelHomClass F alpha beta to RelHomClass F _? _? but now it seems that if we want to use SupHomClass.toOrderHomClass (and we do) then there are three typeclass problems to solve, and typeclass inference is solving them in the wrong order (you can see it trying to solve SemilatticeSup _? which is a disaster). What is determining the order in which these things are being solved?

[Kevin Buzzard]

Sebastian Ullrich said:

For what it's worth, I believe proper use and propagation of outParams would be far easier to systematically enforce (as in Kevin's

Why doesn't the typeclass inference system immediately abort when faced with the goal SemilatticeSup ?α

) than uniqueness of TC solutions, but this is probably not the time to revise the design of TC inference in such a way...

Aren't things like lean4#2003 precisely redesigning TC inference? And aren't issues like lean4#1901 indicating that they need to be redesigned some more?

[Sebastian Ullrich]

The first one is not really TC, while the second one is important enough with immediate impact to consider

[Sebastian Ullrich]

If for example we enforced the handling of outParams and metavariables at the start of TC resolution throughout it as well, that would be a far greater change with unclear repercussions

[Sebastian Ullrich]

Kevin Buzzard said:

What is determining the order in which these things are being solved?

Right now it's simply left-to-right. The second issue you linked considers changing that.

[Sebastian Ullrich]

Sebastian Ullrich said:

If for example we enforced the handling of outParams and metavariables at the start of TC resolution throughout it as well, that would be a far greater change with unclear repercussions

Well now I see that 1901 does go in that direction, though not the metavariables part that may be the bigger change and give your "immediate abort" semantics

[Kevin Buzzard]

Sebastian Ullrich said:

Right now it's simply left-to-right. The second issue you linked considers changing that.

Aargh! And we can't change the order and write

SupHomClass.toOrderHomClass [SupHomClass F α β] [SemilatticeSup α] [SemilatticeSup β]

because SupHomClass F α β needs the Sup on alpha from SemilatticeSup α!

[Anne Baanen]

I found an example showing sometimes sensible-looking instances* mean you actually have to search for an instance with metavariables: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Instance.20diamonds.20depending.20on.20.60outParam.60s

[Anne Baanen]

(* Sensible here means: it was the logical consequence of the FunLike pattern in the circumstances and it took a lot of thinking to figure out why it wouldn't work.)

[Sebastian Ullrich]

Kevin Buzzard said:

Sebastian Ullrich said:

Right now it's simply left-to-right. The second issue you linked considers changing that.

Aargh! And we can't change the order and write

SupHomClass.toOrderHomClass [SupHomClass F α β] [SemilatticeSup α] [SemilatticeSup β]

because SupHomClass F α β needs the Sup on alpha from SemilatticeSup α!

Yes, which is where you would apply the workaround the issue mentioned

SupHomClass.toOrderHomClass {_ : SemilatticeSup α} {_ : SemilatticeSup β} [SupHomClass F α β]

(untested), which is effectively doing a manual reordering/delaying of subgoals

[Kevin Buzzard]

Aah I now see where these {}s are coming from! Many thanks to all, I've learnt a lot from this. I realised that conversations were happening which I could not be a part of because I hadn't understood the basics, and now I'm in much better shape. Anne yes I rememember that post and I remember at the time just ignoring it because I didn't understand it (because it mentioned outParams).

[Gabriel Ebner]

Sebastian Ullrich said:

For what it's worth, I believe proper use and propagation of outParams would be far easier to systematically enforce (as in Kevin's

We do have a linter for that. And if you follow its advice you should never get a SemilatticeSup ?L subgoal.

[Kevin Buzzard]

Ha yes I had just independently discovered this and came back to post here! I think that yesterday's thread might be another instance of autoported code failing to lint.

[Kevin Buzzard]

Yeah it is. That's funny, not only has this conversation taught me a great deal but it's also exposed a bug in my workflow. When I'm porting a file I first try to get everything compiling, and then and only then do I lint (in the sense that I push and then CI lints for me). I should be linting earlier: a whole bunch of these early instances in Order.Hom.Lattice are dangerous in Lean 4 (before the problems start).

Dare I ask why they weren't dangerous in Lean 3?

[Eric Wieser]

Sebastian Ullrich said:

Yes, which is where you would apply the workaround the issue mentioned

SupHomClass.toOrderHomClass {_ : SemilatticeSup α} {_ : SemilatticeSup β} [SupHomClass F α β]

(untested), which is effectively doing a manual reordering/delaying of subgoals

This pattern presumably doesn't work if our lemma requires something stronger than SemilatticeSup α, and the stronger something participates in a defeq diamond such that it can no longer be found by unification

[Gabriel Ebner]

Unification can call TC synthesis in that case. It's not ideal because it doesn't participate in the tabled resolution mechanism, etc., but it should work for this.

[Eric Wieser]

So for instance, if it requires docs4#CoFrame but the actual application is looking for docs4#CompleteDistribLattice; the term we have might look like (CompleteDistribLattice.toFrame I).toCompleteLattice.toSemilatticeSup but the one we have available might look like (Coframe.toCompleteLattice _).toSemilatticeSup.

[Eric Wieser]

So unification uses TC synthesis to produce _ = (CompleteDistribLattice.toCoframe I) there?

[Kevin Buzzard]

This is related to why Gabriel uses the term "bandaid" in lean4#1901, presumably?

[Eric Wieser]

(the picture in my example is that CompleteDistribLattice is at the top of the diamond, Frame and Coframe are at the sides, and CompleteLattice is at the bottom; with arrows going top to bottom)

[Gabriel Ebner]

Yes, if you unify (Coframe.toCompleteLattice ?inst).toSemilatticeSup with another instance side of the diamond, then Lean will try to fill in ?inst using TC synthesis.

[Sebastien Gouezel]

Would the following have any drawback?

• First solve from left to right all TC that have outparams
• Then solve from left to right the other ones

[Sebastien Gouezel]

This would avoid the workarounds with {...}that are bound to trip many users.

[Kevin Buzzard]

Here's another question: if right now the dangerous instance linter is supposed to flag instances which can yield goals of the form SemilatticeSup _? then why does it not complain about

instance (priority := 100) SupHomClass.toOrderHomClass [SemilatticeSup α] [SemilatticeSup β]
    [SupHomClass F α β] : OrderHomClass F α β :=
  { ‹SupHomClass F α β› with
    map_rel := fun f a b h => by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h] }

(the instance which caused all the problems yesterday)?

[Gabriel Ebner]

Yes, that is the next step here. (Although you can skip the second step IIUYC, those are already filled in via unification)

[Gabriel Ebner]

@Kevin Buzzard Is the α/β in OrderHomClass tagged with outParam?

[Gabriel Ebner]

If you have a repro, I can investigate more.

[Kevin Buzzard]

abbrev OrderHomClass (F : Type _) (α β : outParam (Type _)) [LE α] [LE β] :=
  RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)

(and RelHomClass also has outParams on everything). But as we saw yesterday, this instance was still causing goals of the form SemilatticeSup _?.

[Kevin Buzzard]

By a repro, do you mean a mathlib-free one?

Youch, what does one do here? The linter isn't complaining about the class, but one of the projections.

import Mathlib.Order.Hom.Basic

class SupHomClass (F : Type _) (α β : Type _) [HasSup α] [HasSup β] extends
  FunLike F α fun _ => β where
  map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check @SupHomClass.toFunLike /- generates subgoals with metavariables: argument 4 inst✝¹ : HasSup
  ?α, argument 5 inst✝ : HasSup ?β -/

Here

@SupHomClass.toFunLike : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : HasSup α] → [inst_1 : HasSup β] → [self : SupHomClass F α β] → FunLike F α fun x => β

[Kevin Buzzard]

Oh this is precisely lean4#1901 -- I had not read this issue in the past because the outParam always intimidated me.

[Kevin Buzzard]

Aah, I see; alpha and beta need to be outParams here.

[Kevin Buzzard]

@Sebastian Ullrich suggested @[infer_tc_goals_rl] but the dangerousInstance linter still complains. Is this instance really still dangerous with this attribute @Gabriel Ebner ?

import Mathlib.Order.Hom.Basic

class SupHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] extends
  FunLike F α fun _ => β where
  map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b

class SupBotHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] [Bot α]
  [Bot β] extends SupHomClass F α β where
  map_bot (f : F) : f ⊥ = ⊥

@[infer_tc_goals_rl]
instance (priority := 100) OrderIsoClass.toSupBotHomClass [SemilatticeSup α] [OrderBot α]
    [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] : SupBotHomClass F α β :=
sorry

@[infer_tc_goals_rl]
instance (priority := 100) OrderIsoClass.toSupBotHomClass' {_ : SemilatticeSup α} {_ : OrderBot α}
    {_ : SemilatticeSup β} {_ : OrderBot β} [OrderIsoClass F α β] : SupBotHomClass F α β :=
sorry


#lint only dangerousInstance
/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check @OrderIsoClass.toSupBotHomClass /- generates subgoals with metavariables: argument 4 inst✝⁴ : SemilatticeSup
  ?α, argument 6 inst✝² : SemilatticeSup ?β -/
#check @OrderIsoClass.toSupBotHomClass' /- unassigned metavariable in out-param: SupBotHomClass F α β -/

I had guessed that both instances should be fine and that the first is preferable because it's less confusing for the user with the square brackets.

[Gabriel Ebner]

The linter doesn't know about the attribute. As far as I'm concerned the attribute is only there for testing purposes, and should not be used in production.

[Kevin Buzzard]

Possibly relevant definitions:

/-- The class `EquivLike E α β` expresses that terms of type `E` have an
injective coercion to bijections between `α` and `β`.

This typeclass is used in the definition of the homomorphism typeclasses,
such as `ZeroEquivClass`, `MulEquivClass`, `MonoidEquivClass`, ....
-/
class EquivLike (E : Sort _) (α β : outParam (Sort _)) where
  /-- The coercion to a function in the forward direction. -/
  coe : E → α → β
  /-- The coercion to a function in the backwards direction. -/
  inv : E → β → α
  /-- The coercions are left inverses. -/
  left_inv : ∀ e, Function.LeftInverse (inv e) (coe e)
  /-- The coercions are right inverses. -/
  right_inv : ∀ e, Function.RightInverse (inv e) (coe e)
  /-- If two coercions to functions are jointly injective. -/
  coe_injective' : ∀ e g, coe e = coe g → inv e = inv g → e = g
  -- This is mathematically equivalent to either of the coercions to functions being injective, but
  -- the `inv` hypothesis makes this easier to prove with `congr'`

and

class OrderIsoClass (F : Type _) (α β : outParam (Type _)) [LE α] [LE β] extends
  EquivLike F α β where
  /-- An order isomorphism respects `≤`. -/
  map_le_map_iff (f : F) {a b : α} : f a ≤ f b ↔ a ≤ b

Edit: :racecar: