[GHC] #14861: QuantifiedConstraints: Can't use forall'd variable in context

27 Feb 2018

      #14861: QuantifiedConstraints: Can't use forall'd variable in context
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints wipT2893     |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This fails to typecheck, to my surprise:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind

 data ECC1 :: (Type -> Constraint) -> (Type -> Type) -> Type -> Type where
   ECC1 :: c p => f p -> ECC1 c f p

 class Foldable' f where
   foldMap' :: Monoid m => (a -> m) -> f a -> m

 instance (forall p. c p => Foldable' f) => Foldable' (ECC1 c f) where
   foldMap' f (ECC1 x) = foldMap' f x

 instance Foldable' [] where
   foldMap' = foldMap

 test :: ECC1 Show [] Ordering -> Ordering
 test = foldMap' id
 }}}

 {{{
 $ 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:18:25: error:
     • Could not deduce: c p0 arising from a use of ‘foldMap'’
       from the context: forall p. c p => Foldable' f
         bound by the instance declaration at Bug.hs:17:10-63
       or from: Monoid m
         bound by the type signature for:
                    foldMap' :: forall m a. Monoid m => (a -> m) -> ECC1 c
 f a -> m
         at Bug.hs:18:3-10
       or from: c a
         bound by a pattern with constructor:
                    ECC1 :: forall (f :: * -> *) p (c :: * -> Constraint).
                            c p =>
                            f p -> ECC1 c f p,
                  in an equation for ‘foldMap'’
         at Bug.hs:18:15-20
     • In the expression: foldMap' f x
       In an equation for ‘foldMap'’: foldMap' f (ECC1 x) = foldMap' f x
       In the instance declaration for ‘Foldable' (ECC1 c f)’
     • Relevant bindings include
         foldMap' :: (a -> m) -> ECC1 c f a -> m (bound at Bug.hs:18:3)
    |
 18 |   foldMap' f (ECC1 x) = foldMap' f x
    |                         ^^^^^^^^^^^^
 }}}

 I would have expected the `(forall p. c p => Foldable' f)` quantified
 constraint to kick in there.

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