Re: [GHC] #9123: Need for higher kinded roles

31 Jan 2018

      #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):

 Now that we have [wiki:QuantifiedContexts quantified constraints]
 (currently just on `wip/T2983`) we want to take advantage of them to do
 roles, along the lines of comment:29.  But alas this does not work
 {{{
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module T2893b where

 import Data.Coerce

 newtype Wrap m a = Wrap (m a)

 class Monad' m where
   join' :: 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'
 }}}
 We get
 {{{
 T2893b.hs:16:10: error:
     • Couldn't match representation of type ‘m (m a)’
                                with that of ‘m (Wrap m a)’
       NB: We cannot know what roles the parameters to ‘m’ have;
         we must assume that the role is nominal
     • In the ambiguity check for an instance declaration
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the instance declaration for ‘Monad' (Wrap m)’
 }}}
 And I can see why. We have
 {{{
    [W] Coercible (m (m a) -> m a)
                  (Wrap m (Wrap m a) -> Wrap m a)
 }}}
 That doesn't match the local instance declaration for `Coercible`, so we
 reduce it to
 {{{
    [W] (~R#) (m (m a) -> m a)
              (Wrap m (Wrap m a) -> Wrap m a)
 }}}
 Now we can decompose on the arrow,  to get
 {{{
    [W] (~R#) (m (m a)) (Wrap m (Wrap m a))
    [W] (~R#) (m a) (Wrap m a)
 }}}
 The latter can be solved by newtype unwrapping, but if we do newtype
 unwrappign
 on the former we get
 {{{
    [W] (~R#) (m (m a)) (m (Wrap m a)
 }}}
 and now we are stuck.  If only we were looking for
 {{{
    [W] Coercible (m (m a)) (m (Wrap m a))
 }}}
 we could use the local instance; but alas we "gone down" to `~R#` from
 `Coercible`.

 I guess the same would happen for equality `(~)`; again, the constraint
 solver works
 over the primitive equality `(~N#)`, so local instances for `(~)` may not
 help.

 Why doesn't this happen when we have a non-quantified constraint
 `Coercible s t` a given?  Because in that case we proactively spit out its
 superclasses and hence can solve `s ~R# t`.

 A vaguely similar situation could be
 {{{
 f :: forall f.  (Ord b, forall a. Ord a => Ord (f a)) => b -> b
 f = ....[W] Eq (f b)....
 }}}
 Here we have `Eq (f b)`, which ''could'' be solved (via superclass) from
 `Ord (f a)`;
 which we could get via the local instance and the `Ord b` constraint.
 Similar
 because it involves a superclass.

 We could make an ad hoc solution for `(~R#)` and `(~N#)`.  But I don't see
 a general solution.

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