#13179: Levity-polymorphic data types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12708 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm afraid your definitions may not be what you think they are. In particular, the way you've written your GADT constructors forces `TYPE rep ~ Type`, so in effect they're not much different from `Product`, `Sum`, and `Compose` and they exist today in `base`. If you tried to write truly levity polymorphic definitions for, say, `Product`, it'll actually be rejected! {{{#!hs data Product :: forall rep. (k -> TYPE rep) -> (k -> TYPE rep) -> (k -> Type) where Pair :: forall rep k (f :: k -> TYPE rep) (g :: k -> TYPE rep) (a :: k). f a -> g a -> (Product f g) a }}} {{{ <interactive>:9:85: error: • A levity-polymorphic type is not allowed here: Type: f a Kind: TYPE rep • In the definition of data constructor ‘Pair’ In the data type declaration for ‘Product’ <interactive>:9:85: error: • A levity-polymorphic type is not allowed here: Type: g a Kind: TYPE rep • In the definition of data constructor ‘Pair’ In the data type declaration for ‘Product’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13179#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler