TestEquality dangerous for value equality (e.g. MapF)

[Ericson2314]

From the docs, http://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Equality.html#t:TestEquality:

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

This doesn't specify whether the terms themselves should be equal. (Or "deemed equal", if there is no forall a. (Eq (f a)). This can lead to MapF behaving surprisingly to the user. Either changing the docs in base or making a new class (as we conservatively have done with our http://hackage.haskell.org/package/dependent-sum-0.6.2.0/docs/Data-GADT-Compare.html#t:GEq) solve the problem. I'm not sure which is better.

[joehendrix]

Thanks for the bug report. MapF functions are all constrained on OrdF rather than TestEquality, and so the TestEquality instance only comes from the superclass.
I think the simplest fix is just to expand the documentation of OrdF to further constrain testEquality assumptions to indicate it should be a test for value equality. We currently don't describe any constraints on OrdF whereas for the MapF operations to be sound, it should be a total order.

[Ericson2314]

That works, thanks.

[georgefst]

Just chiming in to say that this thread is the only place I've found confirmation of the contracts here (e.g. for use in MapF). It would be great if the docs mentioned that:

• TestEquality should check value equality
• OrdF should define a total order across values of all types

[joehendrix]

I'm going to close this issue because I documented our requirements in OrdF. This includes some properties required of TestEquality but should address questions about OrdF and TestEquality requirements for MapF at least.

[Ericson2314]

Please check out haskell/core-libraries-committee#21 where the CLC is learning towards an interpretation of TestEquality that doesn't mesh with laws relating it to OrdF added in #90.

Note it would be easy to just modify the laws from OrdF, such that no OrdF instances need to be changed, but I still wanted to give you all heads up.

[Ericson2314]

See also #62. If you want to use the classes from https://hackage.haskell.org/package/some instead, this would de-duplicate the ecosystem and also side-step the issue.