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