QuantifiedConstraints conflated with impredicative polymorphism?

This works:

{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language KindSignatures #-}
{-# Language RankNTypes #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language TypeOperators #-}

import Data.Kind

data D c where
  D :: c => D c

newtype a :- b = Sub (a => D b)

class    (forall xx. f xx) => Limit f
instance (forall xx. f xx) => Limit f

proof :: Limit Eq :- Eq (Int -> Float)
proof = Sub D

If we replace Limit Eq with (forall xx. Eq xx) it is considered impredicative polymorphism, but is it?

174-quantifiedconstraints.hs:20:10: error:
    • Illegal polymorphic type: forall xx. Eq xx
      GHC doesn't yet support impredicative polymorphism
    • In the type signature:
        proof :: (forall xx. Eq xx) :- Eq (Int -> Float)
   |
20 | proof :: (forall xx. Eq xx) :- Eq (Int -> Float)
   |          ^^^^^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture