Proposal: Rework Data.Type.Equality.==

[David Feuer]

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