[GHC] #9123: Need for higher kinded roles

[GHC]

#9123: Need for higher kinded roles
-------------------------------------+------------------------------------
        Reporter:  simonpj           |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------
Description changed by simonpj:

Old description:

> This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html
> thread] on ghc-devs identifies a real shortcoming of the new roles
> system.  Here's a compact example, from the thread
> {{{
> class C m where
>   ret :: a -> m a
>   bind :: m a -> (a -> m b) -> m b
>   join :: m (m a) -> m a
>
> newtype T m a = MkT (m a) deriving( C )
> }}}
> The `deriving(C)` is accepted without `join` in the class, but rejected
> when `join` is added.  And the AMP proposal adds `join` to class `Monad`!
>
> In one way it is rightly rejected: it really would be unsound to derive
> an instance for `C (T K)` where `K`'s argument had nominal (but not
> representational) role.  But we have no way to limit the type
> constructors at which `T` can be used.
>
> This deficiency is noted in the [http://research.microsoft.com/en-
> us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems
> to be the first occasion on which it has bitten us badly.
>
> Edward [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html
> made a suggestion] on the thread.

New description:

 This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html
 thread] on ghc-devs identifies a real shortcoming of the new roles system.
 Here's a compact example, from the thread
 {{{
 class C m where
   ret :: a -> m a
   bind :: m a -> (a -> m b) -> m b
   join :: m (m a) -> m a

 newtype T m a = MkT (m a) deriving( C )
 }}}
 The `deriving(C)` is accepted without `join` in the class, but rejected
 when `join` is added.
 {{{
 T9123.hs:10:37:
     Could not coerce from `m (m a)' to `m (T m a)'
       because `m (m a)'
           and `m (T m a)'
           are different types.
       arising from the coercion of the method `join'
                    from type `forall a. m (m a) -> m a'
                      to type `forall a. T m (T m a) -> T m a'
 }}}
 Note that the AMP proposal adds `join` to class `Monad`!

 In one way it is rightly rejected: it really would be unsound to derive an
 instance for `C (T K)` where `K`'s argument had nominal (but not
 representational) role.  But we have no way to limit the type constructors
 at which `T` can be used.

 This deficiency is noted in the [http://research.microsoft.com/en-
 us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems
 to be the first occasion on which it has bitten us badly.

 Edward [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html
 made a suggestion] on the thread.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9123#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler