Change GHC.Exts.Any to a type family
|Reported by:||goldfire||Owned by:||goldfire|
|Type of failure:||None/Unknown||Test Case:||indexed-types/should_fail/T9097|
|Related Tickets:||Differential Rev(s):|
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 2 years ago by simonpj
- Milestone set to 7.10.1
- Owner set to goldfire
- Priority changed from normal to high
comment:6 Changed 23 months ago by goldfire
- Resolution set to fixed
- Status changed from new to closed