QuantifiedConstraints: Can't use forall'd variable in context

This fails to typecheck, to my surprise:

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

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