Change GHC.Exts.Any to a type family

[goldfire]

I just had this slightly alarming interchange with GHCi:

Prelude> import Data.Type.Equality
Prelude Data.Type.Equality> import GHC.Exts
Prelude Data.Type.Equality GHC.Exts> :kind! ((Any :: Bool) == (Any :: Bool))
((Any :: Bool) == (Any :: Bool)) :: Bool
= 'False

After staring at the result in disbelief, I figured out why. The instance for == at kind Bool looks like this:

type family EqBool a b where
  EqBool False False = True
  EqBool True  True  = True
  EqBool a     b     = False
type instance (a :: Bool) == (b :: Bool) = EqBool a b

Well, Any isn't False, Any isn't True, so Any == Any must be False!

The solution to this, of course, is to make Any a type family, not a datatype. Then, it wouldn't be apart from the equations in EqBool. I believe this idea has been floated previously but was not implemented as it would have disturbed TypeLits and/or singletons. These libraries have been updated, and it's time.

I'm happy to do this myself in due course.

[simonpj]

Absolutely. Go for it.

Please add a Note that mentions this ticket, or at least gives this example; it's a useful one, and we totally didn't think about before.

Simon

[goldfire]

Patch on the way...

[Richard Eisenberg <eir@…>]

In 051d694fc978ad28ac3043d296cafddd3c2a7050/ghc:

Fix #9097.

`Any` is now an abstract (that is, no equations) closed type family.

[Richard Eisenberg <eir@…>]

In 7b10d013a50a9fe4f100a2cb8b02a28e8d398357/ghc:

Test #9097.

[simonpj]

Richard: excellent, thank you. But could you add some comments with the defn of Any that explain the subtleties. There is a very good reason why Any should be a type family, and this should be noted (with a pointer to this ticket). And there was a very good reason that it initially was a data type, and this too might be worth noting. The diffs don't seem to cover these points unless I'm mis-reading.

thanks

Simon

[goldfire]

You're absolutely right that the diffs don't cover this -- that's because the explanation was already there:

Note [Any types]
~~~~~~~~~~~~~~~~
The type constructor Any of kind forall k. k has these properties:
...
  * It is a *closed* type family, with no instances.  This means that
    if   ty :: '(k1, k2)  we add a given coercion
             g :: ty ~ (Fst ty, Snd ty)
    If Any was a *data* type, then we'd get inconsistency because 'ty'
    could be (Any '(k1,k2)) and then we'd have an equality with Any on
    one side and '(,) on the other. See also #9097.
...

It seems that this comment was left when you reverted the last time you made this change. Well, it's now correct again.