[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:  7.12.1
             Component:  Compiler    |          Version:  7.8.2
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Project (more
       Type of failure:              |  than a week)
  None/Unknown                       |       Blocked By:
             Test Case:              |  Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I've recently realized that an alternate, much more tantalizing fix to
 this problem is to allow quantifying over implication constraints (#2256).

 To be concrete, consider

 {{{#!hs
 class Monad m where
   join :: m (m a) -> m a

 data StateT s m a = StateT (s -> m (a, s))   -- could be a newtype, but
 that doesn't change my argument
 type role StateT nominal representational nominal   -- as inferred
 instance Monad m => Monad (StateT s m) where ...

 newtype IntStateT m a = IntStateT (StateT Int m a)
   deriving Monad
 }}}

 This induces the following instance:

 {{{
 instance (...) => Monad (IntStateT m) where
   join = coerce (join :: StateT Int m (StateT Int m a) -> StateT Int m a)
            :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
 }}}

 GHC needs to infer the `(...)`. It starts with `Monad m` along with

 {{{
 Coercible (StateT Int m (StateT Int m a) -> StateT Int m a) (IntStateT m
 (IntStateT m a) -> IntStateT m a)
 }}}

 This gets reduced to

 {{{
 Coercible (StateT Int m (StateT Int m a)) (StateT Int m (IntStateT m a))
 }}}

 and is then stuck, unable to unwrap the newtype in a nominal context. The
 problem, at this point is that `a` is out of scope in the instance context
 `(...)`, and so GHC gives up. If we had implication constraints, we could
 just quantify! The instance context would be complex, but everything would
 work out in practice.

 As a separate case, imagine I had declared `StateT` as a newtype (so that
 we can look through to its definition) and we wanted to prove, say,
 `Coercible (StateT Int) (StateT Age)`. Right now, we're stuck, but, I
 conjecture that the following would work:

 {{{
 data Coercion a b where Coercion :: Coercible a b => Coercion a b
 pf :: forall m c. (forall a b. Coercible a b => Coercible (m a) (m b)) =>
 Coercion (StateT Int m c) (StateT Age m c)
 pf = Coercion
 }}}

 (The `c` parameter is necessary to allow GHC to unwrap the newtype, as it
 won't unwrap a partially-applied newtype.)

 To prove, GHC unwraps the newtypes to get

 {{{
 [W] Coercible (Int -> m (c, Int)) (Age -> m (c, Age))
 }}}

 and then

 {{{
 [W] Coercible (m (c, Int)) (m (c, Age))
 }}}

 GHC will then look for an appropriate instance, finding

 {{{
 [G] forall a b. Coercible a b => Coercible (m a) (m b)
 }}}

 which matches nicely. (This last step is beyond the current algorithm for
 the treatment of givens, but it's exactly what the instance-lookup
 algorithm does! So we just adapt that to a new scenario.) Thus, we now
 have

 {{{
 [W] Coercible (c, Int) (c, Age)
 }}}

 which is solved handily.

 More comments on the solving algorithm on #2256, shortly.

 I think this solution, of using implication constraints, is '''much'''
 better than the ad-hoc idea in [wiki:Roles2]. It's more powerful, simpler
 to explain, simpler to implement, and it goes "all the way".

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