Let's rework Data.Type.Equality.==

[David Feuer]

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 <david.feuer at gmail.com> wrote:
> 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.