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

changed weight to 5

added Tbug Trac import typechecker labels

Another example in the same vein:

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

import Data.Coerce
import Data.Kind

type Phantom1 p = (forall a b. Coercible (p a) (p b) :: Constraint)

class Foo a where
  bar :: Phantom1 proxy => proxy a -> Int

instance Foo Int where
  bar _ = 42

-- Typecheck
newtype Age1 = MkAge1 Int
instance Foo Age1 where
  bar :: forall proxy. Phantom1 proxy => proxy Age1 -> Int
  bar = coerce @(proxy Int  -> Int)
               @(proxy Age1 -> Int)
               bar

-- Doesn't typecheck
newtype Age2 = MkAge2 Int
instance Foo Age2 where
  bar = coerce @(forall proxy. Phantom1 proxy => proxy Int  -> Int)
               @(forall proxy. Phantom1 proxy => proxy Age2 -> Int)
               bar

Here's a simpler version of the original program, if Traversable is too dense:

{-# 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 Distributive g where
  distribute :: Representational1 f => f (g a) -> g (f a)

-- Typechecks
newtype T1 g a = MkT1 (g a)
instance Distributive g => Distributive (T1 g) where
  distribute :: forall f a. Representational1 f => f (T1 g a) -> T1 g (f a)
  distribute = coerce @(f    (g a) ->    g (f a))
                      @(f (T1 g a) -> T1 g (f a))
                      distribute

-- Doesn't typecheck
newtype T2 g a = MkT2 (g a)
instance Distributive g => Distributive (T2 g) where
  distribute = coerce @(forall f a. Representational1 f => f    (g a) ->    g (f a))
                      @(forall f a. Representational1 f => f (T2 g a) -> T2 g (f a))
                      distribute

mentioned in issue #15290 (closed)

It turns out the original program now panics due to #15290 (closed), so that ticket is blocking this one.

Trac metadata

Trac field	Value
BlockedBy	- → #15290 (closed)

In light of #15290 (closed)#ticket:14883#comment:155301, perhaps it's best that we not pursue making the impredicative variants typecheck. If we incorporate the change to deriving that Simon suggests in that ticket, then the code that would be generated for the original program would be:

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))
                     traverse'

Which, conveniently enough, is pretty much exactly the -- Typechecks variant! So that's convenient.

I'll keep this ticket open since as a reminder to check in these two lovely test cases, but implementing the deriving change in #15290 (closed) should make this whole issue moot.

Trac metadata

Trac field	Value
Related	- → #15290 (closed)

implementing the deriving change in #15290 (closed) should make this whole issue moot.

Hurrah!

Trac metadata

Trac field	Value
BlockedBy	#15290 (closed) →

Trac metadata

Trac field	Value
Differential revisions	- → D4895

mentioned in commit 132273f3

closed

changed milestone to %8.6.1

As noted in ticket:14883#comment:155373, #15290 (closed) completely obviates the need for a setup like the Traversable' instance for T2, so this issue can be closed.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added 1 deleted label

added Pnormal label

mentioned in issue #10184

mentioned in merge request !13187 (closed)