[GHC] #14420: Data families should not instantiate to non-Type kinds
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs data family Any :: k -- allowable now due to fix for #12369 type family F (a :: Bool) :: Nat where F True = 0 F False = 1 F Any = 2 }}} {{{ ghci> :kind! F True F True :: Nat = 0 ghci> :kind! F False F False :: Nat = 1 ghci> :kind! F Any F Any :: Nat = 2 }}} Oh dear. We should require that any instantiation of a data family be to a kind that ends in `Type`. Inspired by comment:31:ticket:9429 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) Comment: Hope this won't affect #12369, interestingly your [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs Constrained Type Families] paper doesn't mention constraining data families.. But if we require all data families to be associated {{{#!hs class CAny k where data Any :: k }}} then using `Any :: Bool` as a case in the type family `F` will create a `CAny Bool` constraint, we are already barred from actually defining `data instance Any :: Bool`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, that paper silently ignored data families, but I've thought all along (well, at least since I started thinking about constrained type families) that they should be associated, too. They're simpler because there are no closed data families. Chalk this up as yet another problem the constrained type families approach would solve... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: TypeInType => Comment: This is not related to `TypeInType`. I suppose I won't argue if you want to make a new keyword `RichardsBailiwick`, but this truly isn't `TypeInType`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeFamilies Comment: OK. What keyword should we give it? Otherwise, with 14,000+ tickets, it just gets lost in the sea. Let's try `TypeFamilies`, [wiki:TypeFunctions summarised here] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ekmett): * cc: ekmett (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by kcsongor): * cc: kcsongor (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): According to Adam, this bug somehow imperils #7259. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by oerjan): * cc: oerjan (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I've got lost about what the actual problem is here. The Description says "Oh dear" but fails to elaborate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): The definition `data Bool = False | True` defines a closed type: the only values of type `Bool` are `False` and `True`, pattern matching on both of them defines a total function. A function `Bool -> A` is equivalent to a tuple `(A,A)`. It's natural to expect the same behavior on the kind level: the promoted kind `Bool` should have only two inhabitants, type `False` and `True`. Currently, this doesn't hold. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14420: Data families should not instantiate to non-Type kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by glaebhoerl): * cc: glaebhoerl (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14420#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC