[GHC] #9097: Change GHC.Exts.Any to a type family
GHC
ghc-devs at haskell.org
Sun May 11 02:58:04 UTC 2014
#9097: Change GHC.Exts.Any to a type family
------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: task | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Keywords: | Operating System: Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: None/Unknown
Difficulty: Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: |
------------------------------------+-------------------------------------
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.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9097>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list