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