Oh, one more thing, Richard. You say that this doesn't need
TypeInType, but I wasn't able to make the polykinded recursion work
without it. Could you show how that might be done? Maybe I missed
something.
On Thu, Aug 10, 2017 at 12:29 AM, David Feuer
The (==) type family in Data.Type.Equality was designed largely to calculate structural equality of types. However, limitations of GHC's type system at the type prevented this from being fully realized. Today, with TypeInType, we can actually do it, replacing the boatload of ad hoc instances like so:
type (a :: k) == (b :: k) = Equal k a b infix 4 ==
type family Equal (k :: Type) (a :: k) (b :: k) where Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) = Equal (j -> k) f g && Equal j a b Equal k a a = 'True Equal k a b = 'False
This == behaves in a much more uniform way than the current one. I see two potential causes for complaint:
1. For types of kind *, the new version will sometimes fail to reduce when the old one succeeded (and vice versa). For example, GHC currently accepts
eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True eqeq _ = Refl
while the proposed version does not.
2. Some users may want non-structural equality on their types for some reason. The only example in base is
type instance (a :: ()) == (b :: ()) = 'True
which consists two types of kind () the same even if they're stuck types. But perhaps someone wants to implement a non-trivial type-level data structure with a special notion of equality.
I don't think (1) is really worth worrying too much about. For (2), if users want to have control, we could at least use a mechanism similar to the above to make the obvious instances easier to write.