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

changed weight to 5

added Tbug Trac import labels

closed

it is considered impredicative polymorphism, but is it?

Yes it is. You are instantiating a type variable (the a from newtype a :- b) with a polymorphic type.

I think you need impredicativity here.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

It feels different, there is no way to get around regular impredicativity with type synonyms but in this case we can get around it with the Limit class synonym.

Hypothetically if GHC were to generate an internal class synonym for impredicative constraints what would go wrong? I'm not aware of differences between forall xx. f xx and Limit f.

It would be nice to directly write type a :- b = Dict (a => b) rather than

class    (a => b) => Implies a b
instance (a => b) => Implies a b

type a :- b = Dict (Implies a b)

The difficulty with impredicativity is that, during inference, a unification variable may be unified with a polytype. Thus

f :: forall a. [a] -> [a]

xs :: [forall b. b->b]

...(f xs)..

Here f really has a type argument, and that type is polymorphic. We really have

...(f @(forall b b->b) xs)...

The hard bit is infeering the implicit, invisible type arguments.

But here we are the level of types. With explicit arguments there should be nothing wrong with allowing polytypes. (It's a different matter for the implicit kind arguments, of course.)

So... may it'd be OK. I'm just not sure what a principled story is.

Ok thanks for the response, I'll keep using aliases

Btw, should the following work?

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XGADTs -XQuantifiedConstraints -XConstraintKinds 
Prelude> data Dict c where Dict :: c => Dict c
Prelude> :kind forall a b. Dict (a => b)
forall a b. Dict (a => b) :: *
Prelude> 

added 1 deleted label

added Pnormal label