Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#9097 closed task (fixed)

Change GHC.Exts.Any to a type family

Reported by: goldfire Owned by: goldfire
Priority: high Milestone: 7.10.1
Component: Compiler Version: 7.8.2
Keywords: Cc: jan.stolarek@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_fail/T9097
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.

Change History (8)

comment:1 Changed 3 years ago by simonpj

Milestone: 7.10.1
Owner: set to goldfire
Priority: normalhigh

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.


comment:2 Changed 3 years ago by goldfire

Test Case: indexed-types/should_fail/T9097

Patch on the way...

comment:3 Changed 3 years ago by jstolarek

Cc: jan.stolarek@… added

comment:4 Changed 3 years ago by Richard Eisenberg <eir@…>

In 051d694fc978ad28ac3043d296cafddd3c2a7050/ghc:

Fix #9097.

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

comment:5 Changed 3 years ago by Richard Eisenberg <eir@…>

comment:6 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed

comment:7 Changed 3 years ago by 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.



comment:8 Changed 3 years ago by 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.

Note: See TracTickets for help on using tickets.