No DecidableEq instance for Except?

Stream: lean4

[David Mazarro]

Is there any particular reason why this is the case? Especially considering it can be easily derived

[Eric Wieser]

@loogle DecidableEq, Except

[loogle]

:shrug: nothing found

[Eric Wieser]

I'm particularly surprised that Batteries and Mathlib also didn't add the instance

[David Mazarro]

I'd be willing to take on this, would this be a desirable addition? Can I simply open a PR with a proposal, or does it need to be approved beforehand? (I've never contributed to Lean)

[Yury G. Kudryashov]

One way to avoid, e.g., compiling Lean, is to open a PR to Batteries or Mathlib, then wait until someone from the FRO upstreams the change.

[David Mazarro]

I thought development for Lean was mostly independent from that of Batteries and Mathlib

[Jakub Nowak]

I think Batteries/Mathlib gets stuff that would be considered too experimental for upstream, or when there are multiple competing solutions. Things get upstreamed once community/FRO makes sure it's a good and complete approach.

[Yury G. Kudryashov]

Batteries/Mathlib have lower contribution barriers (e.g., you don't have to recompile Lean and there are more reviewers). Instances and theorems about types from core get upstreamed to the core repository from time to time.

[Eric Wieser]

Also a contribution to Lean core will not be available in a release candidate for at least a month, whereas a contribution to batteries is available to mathlib users in a day or so.

[David Mazarro]

Opened a small PR in Batteries: https://github.com/leanprover-community/batteries/pull/1692

[François G. Dorais]

I'm happy to merge this with a low priority instance. But let me speculate why there is no such instance...

I think the majority of uses of = for Except ε α are misguided. It requires the error type ε to have decidable equality, which may happen, but does it make sense to compare errors that way? For example, if ε is String.Slice then = means that the errors are the same slice of the same string not that the two slices have the same text.

Anyway, I will merge since it does make sense if ε is a kind of enumeration type (à la ERRNO in C).

[Eric Wieser]

What's the point of making it low priority? Any other higher priority instance would be equal to it anyway

[François G. Dorais]

Diamonds?

[François G. Dorais]

I want a core instance to override systematically, should there ever be one.

[Eric Wieser]

I don't think that's particularly worth worrying about, any cure instance would surely be derived anyway

[François G. Dorais]

Sometimes, core adds instances and downstream Batteries and Mathlib get no notification. It takes forever for someone to discover the redundant instances via an unexpected diamond. I'm looking into ways to stop that. Reducing priority is a quick way to fix that but I've just come up with germs of other alternatives after this short discussion (thanks!). Other solutions are welcome.

[Yury G. Kudryashov]

Add a #guard_msgs trying to synthesize the instance just before deriving it?

[David Mazarro]

@François G. Dorais I think for most use cases, checking for equality on the error type makes sense, at least for testing applications (even if it doesn't make much sense for some types like you said)

[David Mazarro]

@Yury G. Kudryashov want me to add that check to my PR?

[Yury G. Kudryashov]

I think that it's for @François G. Dorais to decide what's to do about it.

[François G. Dorais]

My preferred solution at this time is to add a test for Batteries instances that may/should become redundant if a corresponding instance is added to core. When that test fails, Batteries should remove the redundant Batteries instance. So, @David Mazarro, just ad a test file with the test Yury suggested and I will fine-tune the idea later...

[David Mazarro]

@François G. Dorais done :)
https://github.com/leanprover-community/batteries/pull/1692/changes/96a5bf5997c300caf3c5f72a268f8089fca8807d
Does this look good?