[GHC] #9123: Need for higher kinded roles

[GHC]

#9123: Need for higher kinded roles
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |             Keywords:  Roles,
      Resolution:                    |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I have discovered something interesting.  The new quantified-constraints
 machinery is enough
 to accept the example in comment:42 (because of the super-duper handling
 of superclasses):
 {{{
 type role Wrap representational nominal
 newtype Wrap m a = Wrap (m a)

 class Monad' m where
   join' :: forall a. m (m a) -> m a

 instance ( forall p q. Coercible p q => Coercible (m p) (m q)
          , Monad' m)
       => Monad' (Wrap m) where
   join' :: forall a. Wrap m (Wrap m a) -> Wrap m a
   join' = coerce @(m (m a) -> m a)
                  @(Wrap m (Wrap m a) -> Wrap m a)
                  join'
 }}}
 But alas it is NOT enough to accept the example in comment:29! Here is how
 it goes wrong.
 {{{
 class MyMonad m where
   join :: m (m a) -> m a

 type role StateT nominal representational nominal   -- as inferred
 data StateT s m a = StateT (s -> m (a, s))

 instance MyMonad m => Monad (StateT s m) where ...

 type role IntStateT representational nominal   -- as inferred
 newtype IntStateT m a = IntStateT (StateT Int m a)
 }}}
 and suppose we use quantified constraints to do this:
 {{{
 instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q))
                => MyMonad (IntStateT m) where
   join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
   join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a)
                 @(IntStateT  m (IntStateT  m a) -> IntStateT  m a)
                 join
 }}}
 You would think this should work. But it doesn't.
 {{{
 T9123a.hs:27:10: error:
     • Couldn't match type ‘IntStateT m a’ with ‘StateT Int m a’
         arising from a use of ‘coerce’
 }}}
 The reason is that from the `coerce` we gert
 {{{
     [W] Coercible (StateT Int m (StateT Int m a) -> StateT Int m a)
                   (IntStateT  m (IntStateT  m a) -> IntStateT  m a)

 --> (built in rule)
     [W] (StateT Int m (StateT Int m a) -> StateT Int m a)
         ~R#
         (IntStateT  m (IntStateT  m a) -> IntStateT  m a)

 --> (decompose arrow)
     [W] (StateT Int m (StateT Int m a))
         ~R#
         (IntStateT  m (IntStateT  m a))

     [W] StateT Int m a ~ IntStateT m a    -- This one is easily solved


 --> (unwrap IntStateT newtype)
     [W] (StateT Int m (StateT Int m a))
         ~R#
         (StateT Int m (IntStateT  m a))

 --> (decompose StateT)   YIKES
     [W] (StateT Int m a)
         ~N#
         (IntStateT  m a)
 }}}
 This last step is the mistake. Instead we should use the "given"
 {{{
      forall p q. Coercible p q => Coercible (m p) (m q)
 }}}
 Then we'd have
 {{{
     [W] (StateT Int m (StateT Int m a))
         ~R#
         (StateT Int m (IntStateT  m a))

 --> (use given: forall p q. Coercible p q => Coercible (m p) (m q))
     [W] (StateT Int m a)
         ~R#
         (IntStateT  m a)
 }}}
 which of course we can solve.

 Now we have a very unsettling overlap between the `(decompose `StateT)`
 rule and the `(use given)` rule, in which the former can lead us into a
 dead end.

 Moreover, in the [https://www.microsoft.com/en-us/research/publication
 /safe-coercions/ Safe Coercions paper], Section 2.2.4, we suggest (but do
 not really work out) that we can only decompose `T a1 .. an ~R# T b1 ..
 bn` if the nominal-role parameters are equal --- whereas in the
 implementation we decompose eagerly and emit a nominal equality, which is
 wrong on this occasion.  I wonder what would happen if we refrained from
 decomposing when the nominal parameters differed?

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