The discussion has been going for nearly a month, but I've only really gotten feedback from Richard and Ryan Scott
I guess not so many use type equality in Haskell and, consequently, have no opinion formed. On 08.09.2017 01:35, David Feuer wrote:
The discussion has been going for nearly a month, but I've only really gotten feedback from Richard and Ryan Scott (which was both positive and useful). Based on that feedback, I'd like to make this an official proposal and get some votes. Be it proposed that Data.Type.Equality shall be redefined as follows:
type family (a :: k) == (b :: k) :: Bool where f a == g b = f == g && a == b a == a = 'True _ == _ = 'False
Unlike the previous definition:
1. (==) is a *closed* type family. 2. It works out of the box for types of all kinds, in a completely uniform manner. 3. It is now safe to conclude in all cases that (a == b) ~ 'True entails a ~ b, although GHC will not give us direct evidence of that.
Since all the ad hoc instances and special cases are gone, there will be cases in which the previous definition will reduce and this one will not, and vice versa. But there was no particular rhyme or reason to the way it used to be, and I think that making everything simple and uniform is worth the (likely minor) breakage.
David Feuer _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www.cse.chalmers.se/~abela/