QuantifiedConstraints don't kick in when used in TypeApplications

Consider the following program:

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

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:

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).

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture