[GHC] #15707: More liberally kinded coercions for newtypes

[GHC]

#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