(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)

Consider the following code:

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind

type family F a :: Type -> Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)

data SomeF b = forall a. MkSomeF (WrappedF a b)

deriving instance (forall a. Functor (WrappedF a))  => Functor SomeF
deriving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF
deriving instance ( forall a. Functor (WrappedF a)
                  , forall a. Foldable (WrappedF a)
                  , forall a. Traversable (WrappedF a)
                  ) => Traversable SomeF

This typechecks. However, the last Traversable SomeF is a bit unfortunate in that is uses three separate forall a.s. I attempted to factor this out, like so:

deriving instance (forall a. ( Functor (WrappedF a)
                             , Foldable (WrappedF a)
                             , Traversable (WrappedF a)
                             )) => Traversable SomeF

But then the file no longer typechecked!

$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

Foo.hs:21:1: error:
    • Could not deduce (Functor (F a))
        arising from the superclasses of an instance declaration
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
    • In the instance declaration for ‘Traversable SomeF’
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Foo.hs:21:1: error:
    • Could not deduce (Foldable (F a))
        arising from the superclasses of an instance declaration
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
    • In the instance declaration for ‘Traversable SomeF’
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Foo.hs:21:1: error:
    • Could not deduce (Traversable (F a1))
        arising from a use of ‘traverse’
      from the context: forall a.
                        (Functor (WrappedF a), Foldable (WrappedF a),
                         Traversable (WrappedF a))
        bound by the instance declaration at Foo.hs:(21,1)-(24,52)
      or from: Applicative f
        bound by the type signature for:
                   traverse :: forall (f :: * -> *) a b.
                               Applicative f =>
                               (a -> f b) -> SomeF a -> f (SomeF b)
        at Foo.hs:(21,1)-(24,52)
    • In the second argument of ‘fmap’, namely ‘(traverse f a1)’
      In the expression: fmap (\ b1 -> MkSomeF b1) (traverse f a1)
      In an equation for ‘traverse’:
          traverse f (MkSomeF a1) = fmap (\ b1 -> MkSomeF b1) (traverse f a1)
      When typechecking the code for ‘traverse’
        in a derived instance for ‘Traversable SomeF’:
        To see the code I am typechecking, use -ddump-deriv
   |
21 | deriving instance (forall a. ( Functor (WrappedF a)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.

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