decidable_lt_of_decidable_le

Stream: general

[Yaël Dillies]

Why is docs#decidable_lt_of_decidable_le still an instance? This messes up with the decidability coming from docs#linear_order.

[Eric Rodriguez]

I mean, if this is an instance then why can't we just yeet the decidable_le from linear_order? It doesn't even need decidable_eq

[Yaël Dillies]

Because deriving decidability instances is bad.

[Eric Rodriguez]

why? the argument is that it causes diamonds, but if we exclusively use this one then I don't see the real problem

[Eric Rodriguez]

urgh, I guess it still causes diamonds

[Eric Rodriguez]

i pray for typeclass inference to look at subsingleton issues or at least give special support for subsingleton instances <3

[Reid Barton]

FWIW linear_order used to not contain decidability instances

[Yaël Dillies]

You mean that decidable_lt_of_decidable_le should have been made an instance when linear_order was refactored?

[Eric Rodriguez]

that's what I meant, yes, but I'm not so sure that's sufficient

[Eric Rodriguez]

I think you'd still get issues with classical etc