#15707: More liberally kinded coercions for newtypes -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by mniip: Old description:

Consider the infinite data family (possible thanks to #12369):

{{{#!hs data family I :: k -> k newtype instance I a = I0 (a) newtype instance I a x = I1 (a x) newtype instance I a x y = I2 (a x y) newtype instance I a x y z = I3 (a x y z) ... }}}

We end up with a family of eta-contracted coercions: {{{#!hs forall (a :: *). a ~R I a forall (a :: k -> *). a ~R I a forall (a :: k -> l -> *). a ~R I a forall (a :: k -> l -> m -> *). a ~R I a ... }}}

What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`

Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I` data constructor and pattern would still only use the *-kinded restriction of it.

We could then recover other constructors with: {{{#!hs i1 :: a x -> I a x i1 = coerce ... }}}

New description: Consider the infinite data family (possible thanks to #12369): {{{#!hs data family I :: k -> k newtype instance I a = I0 (a) newtype instance I a x = I1 (a x) newtype instance I a x y = I2 (a x y) newtype instance I a x y z = I3 (a x y z) ... }}} We end up with a family of eta-contracted coercions: {{{#!hs forall (a :: *). a ~R I a forall (a :: k -> *). a ~R I a forall (a :: k -> l -> *). a ~R I a forall (a :: k -> l -> m -> *). a ~R I a ... }}} What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a` Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the *-kinded restriction of it. We could then recover other constructors with: {{{#!hs i1 :: a x -> I a x i1 = coerce ... }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15707#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15707: More liberally kinded coercions for newtypes -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15707#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15707: More liberally kinded coercions for newtypes -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But do you have a concrete program (invent syntax if necessary) that uses this feature? It's much easier to understand the implications of it all with an example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15707#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler