[GHC] #15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)

2 Jul 2018

      #15334: (forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       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 code:

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

 {{{#!hs
 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.

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