Proposal: Rework Data.Type.Equality.==

[Andreas Abel]

 > 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 at 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 at gu.se
http://www.cse.chalmers.se/~abela/