PR !4#13124: chore: remove `CovariantClass` and `Contrava...

Stream: triage

[Random Issue Bot]

Today I chose PR #13124 for discussion!

chore: remove CovariantClass and ContravariantClass
Created by @Zhao Yuyang 赵雨扬 (@astrainfinita) on 2024-05-22
Labels: WIP, merge-conflict

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

[Violeta Hernández]

I agree that these typeclasses are ineffective and non-idiomatic. But what's the proposed alternative? The PR is quite large and messy.

[Yaël Dillies]

I think removing them is a bit much, but using MulLeftMono, etc... instead of them is a good move

[Yaël Dillies]

As in, in an ideal world, they would only be used for non-standard relations/operations

[Yury G. Kudryashov]

Some lemmas about filters (limsup etc) use them to avoid duplicating lemmas for le and ge.

[Yaël Dillies]

Yeah I think that should be allowed, but it's currently a minority use