[GHC] #14883: QuantifiedConstraints don't kick in when used in TypeApplications

[GHC]

#14883: QuantifiedConstraints don't kick in when used in TypeApplications
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints, wipT2893    |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 module Bug where

 import Data.Coerce
 import Data.Kind

 type Representational1 m = (forall a b. Coercible a b => Coercible (m a)
 (m b) :: Constraint)

 class Representational1 f => Functor' f where
   fmap' :: (a -> b) -> f a -> f b

 class Functor' f => Applicative' f where
   pure'  :: a -> f a
   (<*>@) :: f (a -> b) -> f a -> f b

 class Functor' t => Traversable' t where
   traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)

 -- Typechecks
 newtype T1 m a = MkT1 (m a) deriving Functor'
 instance Traversable' m => Traversable' (T1 m) where
   traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f
 (T1 m b)
   traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                      @((a -> f b) -> T1 m a -> f (T1 m b))
                      traverse'

 -- Doesn't typecheck
 newtype T2 m a = MkT2 (m a) deriving Functor'
 instance Traversable' m => Traversable' (T2 m) where
   traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m
 a -> f    (m b))
                      @(forall f a b. Applicative' f => (a -> f b) -> T2 m
 a -> f (T2 m b))
                      traverse'
 }}}

 This defines a variant of `Functor` that has `forall a b. Coercible a b.
 Coercible (m a) (m b)` as a superclass, and also defines versions of
 `Applicative` and `Traversable` that use this `Functor` variant. This is
 towards the ultimate goal of defining `Traversable'` à la
 `GeneralizedNewtypeDeriving`.

 This attempt (using `InstanceSigs`) typechecks:

 {{{#!hs
 newtype T1 m a = MkT1 (m a) deriving Functor'
 instance Traversable' m => Traversable' (T1 m) where
   traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f
 (T1 m b)
   traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                      @((a -> f b) -> T1 m a -> f (T1 m b))
                      traverse'
 }}}

 However, this version (which is closer to what
 `GeneralizedNewtypeDeriving` would actually create) does //not//
 typecheck:

 {{{#!hs
 newtype T2 m a = MkT2 (m a) deriving Functor'
 instance Traversable' m => Traversable' (T2 m) where
   traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m
 a -> f    (m b))
                      @(forall f a b. Applicative' f => (a -> f b) -> T2 m
 a -> f (T2 m b))
                      traverse'
 }}}
 {{{
 $ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:38:15: error:
     • Couldn't match representation of type ‘f1 (m b1)’
                                with that of ‘f1 (T2 m b1)’
         arising from a use of ‘coerce’
       NB: We cannot know what roles the parameters to ‘f1’ have;
         we must assume that the role is nominal
     • In the expression:
         coerce
           @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b))
           @(forall f a b.
             Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
           traverse'
       In an equation for ‘traverse'’:
           traverse'
             = coerce
                 @(forall f a b. Applicative' f => (a -> f b) -> m a -> f
 (m b))
                 @(forall f a b.
                   Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                 traverse'
       In the instance declaration for ‘Traversable' (T2 m)’
     • Relevant bindings include
         traverse' :: (a -> f b) -> T2 m a -> f (T2 m b)
           (bound at Bug.hs:38:3)
    |
 38 |   traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->
 m a -> f    (m b))
    |
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 }}}

 Shouldn't it, though? These instance declarations out to be equivalent
 (morally, at least).

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