[GHC] #9097: Change GHC.Exts.Any to a type family
#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
#9097: Change GHC.Exts.Any to a type family -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: task | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * owner: => goldfire * priority: normal => high * milestone: => 7.10.1 Comment: 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9097: Change GHC.Exts.Any to a type family -------------------------------------------------+------------------------- Reporter: goldfire | Owner: Type: task | goldfire Priority: high | Status: new Component: Compiler | Milestone: Resolution: | 7.10.1 Operating System: Unknown/Multiple | Version: 7.8.2 Type of failure: None/Unknown | Keywords: Test Case: indexed- | Architecture: types/should_fail/T9097 | Unknown/Multiple Blocking: | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by goldfire): * testcase: => indexed-types/should_fail/T9097 Comment: Patch on the way... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9097: Change GHC.Exts.Any to a type family -------------------------------------------------+------------------------- Reporter: goldfire | Owner: Type: task | goldfire Priority: high | Status: new Component: Compiler | Milestone: Resolution: | 7.10.1 Operating System: Unknown/Multiple | Version: 7.8.2 Type of failure: None/Unknown | Keywords: Test Case: indexed- | Architecture: types/should_fail/T9097 | Unknown/Multiple Blocking: | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9097: Change GHC.Exts.Any to a type family
-------------------------------------------------+-------------------------
Reporter: goldfire | Owner:
Type: task | goldfire
Priority: high | Status: new
Component: Compiler | Milestone:
Resolution: | 7.10.1
Operating System: Unknown/Multiple | Version: 7.8.2
Type of failure: None/Unknown | Keywords:
Test Case: indexed- | Architecture:
types/should_fail/T9097 | Unknown/Multiple
Blocking: | Difficulty:
| Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Richard Eisenberg
#9097: Change GHC.Exts.Any to a type family
-------------------------------------------------+-------------------------
Reporter: goldfire | Owner:
Type: task | goldfire
Priority: high | Status: new
Component: Compiler | Milestone:
Resolution: | 7.10.1
Operating System: Unknown/Multiple | Version: 7.8.2
Type of failure: None/Unknown | Keywords:
Test Case: indexed- | Architecture:
types/should_fail/T9097 | Unknown/Multiple
Blocking: | Difficulty:
| Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Richard Eisenberg
#9097: Change GHC.Exts.Any to a type family -------------------------------------------------+------------------------- Reporter: goldfire | Owner: Type: task | goldfire Priority: high | Status: Component: Compiler | closed Resolution: fixed | Milestone: Operating System: Unknown/Multiple | 7.10.1 Type of failure: None/Unknown | Version: 7.8.2 Test Case: indexed- | Keywords: types/should_fail/T9097 | Architecture: Blocking: | Unknown/Multiple | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9097: Change GHC.Exts.Any to a type family -------------------------------------------------+------------------------- Reporter: goldfire | Owner: Type: task | goldfire Priority: high | Status: Component: Compiler | closed Resolution: fixed | Milestone: Operating System: Unknown/Multiple | 7.10.1 Type of failure: None/Unknown | Version: 7.8.2 Test Case: indexed- | Keywords: types/should_fail/T9097 | Architecture: Blocking: | Unknown/Multiple | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (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. thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9097: Change GHC.Exts.Any to a type family -------------------------------------------------+------------------------- Reporter: goldfire | Owner: Type: task | goldfire Priority: high | Status: Component: Compiler | closed Resolution: fixed | Milestone: Operating System: Unknown/Multiple | 7.10.1 Type of failure: None/Unknown | Version: 7.8.2 Test Case: indexed- | Keywords: types/should_fail/T9097 | Architecture: Blocking: | Unknown/Multiple | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9097#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC