Failure to synthesize instance

Stream: mathlib4

[Chris Hughes]

This instance failure came up when porting Order.Hom.Basic . PR It seems pretty difficult to fix and in earlier versions of Lean4 (2022-20-10), the class OrderIsoClass gives an error to do with LE \a depending on an outParam but not being an outParam. This seems to not have a solution within my Lean4 expertise.

class EquivLike (E : Sort _) (α β : outParam (Sort _)) where
/-- `OrderIsoClass F α β` states that `F` is a type of order isomorphisms.


You should extend this class when you extend `OrderIso`. -/
class OrderIsoClass (F : Type _) (α β : outParam (Type _)) [LE α] [LE β] extends
  EquivLike F α β where


example (F α β : Type _) [LE α] [LE β] [OrderIsoClass F α β] : EquivLike F α β := by infer_instance

[Sebastien Gouezel]

Is this the same issue as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instance.20loop.3F/near/313151621?

[Scott Morrison]

We should probably just wait on porting any files involving EquivLike for now.

[Scott Morrison]

Until https://github.com/leanprover/lean4/issues/1901 is fixed, EquivLike is going to cause lots of problems.

[Scott Morrison]

Sorry, even FunLike.

[Chris Hughes]

There are not very many files that don't depend on these things.

[Scott Morrison]

Yes, it's a difficult situation. Hopefully we have a fix soon.

[Scott Morrison]

If someone reviews/merges my category theory PR, most of category theory is independent of FunLike.

[Scott Morrison]

And if someone finishes my Heyting PR, getting up to Data.Set.Basic should be open.

[Chris Hughes]

I'm working on your Heyting PR right now. There's a difficult Type Class issue there as well. It's hard to minimize

[Chris Hughes]

Chris Hughes said:

I'm working on your Heyting PR right now. There's a difficult Type Class issue there as well. It's hard to minimize

Type class problem fixed and this PR should be Ready To Merge