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

[David Feuer]

To be more specific about the ad hoc equality option, I'm thinking about
something like this (if it doesn't compile, I'm sure something similar
will):

type family (a :: k) == (b :: k) :: Bool
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 && (a == b)
  Equal k a a = 'True
  Equal k a b = 'False

type instance (a :: Type) == b = Equal Type a b
type instance (a :: Maybe k) == b = Equal Type a b
....

So for example, we'd get

'Just (x :: k) == 'Just y
=
Equal (k -> Maybe k) 'Just && x == y
=
x == y

On Aug 10, 2017 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170810/beb170c8/attachment.html>