Re: [GHC] #10447: DeriveFoldable rejects instances with constraints in last argument of data type

26 May 2015

      #10447: DeriveFoldable rejects instances with constraints in last argument of data
type
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.10.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:  #8678             |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 To be a bit more explicit, {{{TcDeriv}}} specifies
 [http://git.haskell.org/ghc.git/blob/9f968e97a0de9c2509da00f6337b612dd72a0389...
 these rules] for {{{DeriveFunctor}}}, {{{DeriveFoldable}}}, and
 {{{DeriveTraversable}}}:

 {{{
 -- OK for Functor/Foldable/Traversable class
 -- Currently: (a) at least one argument
 --            (b) don't use argument contravariantly
 --            (c) don't use argument in the wrong place, e.g. data T a = T
 (X a a)
 --            (d) optionally: don't use function types
 --            (e) no "stupid context" on data type
 }}}

 These conditions are OK. I propose that
 [http://git.haskell.org/ghc.git/blob/9f968e97a0de9c2509da00f6337b612dd72a0389...
 these additional rules] from {{{TcDeriv}}} only be used for
 {{{DeriveFunctor}}} and {{{DeriveTraversable}}}, not for
 {{{DeriveFoldable}}}:

 {{{
 Note [Check that the type variable is truly universal]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For Functor, Foldable, Traversable, we must check that the *last argument*
 of the type constructor is used truly universally quantified.  Example

    data T a b where
      T1 :: a -> b -> T a b      -- Fine! Vanilla H-98
      T2 :: b -> c -> T a b      -- Fine! Existential c, but we can still
 map over 'b'
      T3 :: b -> T Int b         -- Fine! Constraint 'a', but 'b' is still
 polymorphic
      T4 :: Ord b => b -> T a b  -- No!  'b' is constrained
      T5 :: b -> T b b           -- No!  'b' is constrained
      T6 :: T a (b,b)            -- No!  'b' is constrained

 Notice that only the first of these constructors is vanilla H-98. We only
 need to take care about the last argument (b in this case).  See Trac
 #8678.
 Eg. for T1-T3 we can write

      fmap f (T1 a b) = T1 a (f b)
      fmap f (T2 b c) = T2 (f b) c
      fmap f (T3 x)   = T3 (f x)
 }}}

 These rules must hold for {{{Functor}}} and {{{Traversable}}} instances
 because the type signatures of {{{fmap :: Functor t => (a -> b) -> t a ->
 t b}}} and {{{traverse :: (Applicative f, Traversable t) => (a -> f b) ->
 t a -> f (t b)}}} require that the last type argument be truly
 polymorphic, since it must be instantiated with two arbitrary types, {{{t
 a}}} and {{{t b}}}. As evidence, if you try to make a {{{Functor T}}}
 instance using what {{{DeriveFunctor}}} would (hypothetically) generate:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 module T where

 data T a where
     MkT :: Int -> T Int

 instance Functor T where
     fmap f (MkT a) = MkT (f a)
 }}}

 it will be rejected:

 {{{
 T.hs:8:22:
     Could not deduce (b ~ Int)
     from the context (a ~ Int)
       bound by a pattern with constructor
                  MkT :: Int -> T Int,
                in an equation for ‘fmap’
       at T.hs:8:13-17
       ‘b’ is a rigid type variable bound by
           the type signature for fmap :: (a -> b) -> T a -> T b at
 T.hs:8:5
     Expected type: T b
       Actual type: T Int
     Relevant bindings include
       f :: a -> b (bound at T.hs:8:10)
       fmap :: (a -> b) -> T a -> T b (bound at T.hs:8:5)
     In the expression: MkT (f a)
     In an equation for ‘fmap’: fmap f (MkT a) = MkT (f a)
 }}}

 On the other hand, {{{Foldable}}} instances do not require the last type
 argument to be truly polymorphic, since all of the {{{Foldable}}} methods
 only parameterize {{{t}}} over a single type variable:

 {{{
 class Foldable t where
     fold :: Monoid m => t m -> m
     foldMap :: Monoid m => (a -> m) -> t a -> m
     foldr :: (a -> b -> b) -> b -> t a -> b
     foldr' :: (a -> b -> b) -> b -> t a -> b
     foldl :: (b -> a -> b) -> b -> t a -> b
     foldl' :: (b -> a -> b) -> b -> t a -> b
     foldr1 :: (a -> a -> a) -> t a -> a
     foldl1 :: (a -> a -> a) -> t a -> a
     toList :: t a -> [a]
     null :: t a -> Bool
     length :: t a -> Int
     elem :: Eq a => a -> t a -> Bool
     maximum :: forall a. Ord a => t a -> a
     minimum :: forall a. Ord a => t a -> a
     sum :: Num a => t a -> a
     product :: Num a => t a -> a
 }}}

 As a result, the type parameter can be safely constrained. If you plug in
 the code that {{{DeriveFoldable}}} would (hypothetically) generate for
 {{{T}}}:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 module T where

 data T a where
     MkT :: Int -> T Int

 instance Foldable T where
     foldr f z (MkT a) = f a z
     foldMap f (MkT a) = f a
 }}}

 it compiles without problems, since pattern-matching on the GADT
 constructor specializes {{{foldr}}} to the type {{{(Int -> b -> b) -> b ->
 T Int -> b}}} and {{{foldMap}}} to the type {{{Monoid m => (Int -> m) -> T
 Int -> m}}}.

 Again, this only works with {{{Foldable}}} since the type signatures of
 its methods allow for {{{t a}}} to be refined safely. {{{Functor}}} and
 {{{Traversable}}} do not permit this, so the universal polymorphism check
 would still apply for them.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10447#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler