wiki:ImpredicativePolymorphism

Impredicative polymorphism

GHC does not (yet) support impredicative polymorphism, but it's a topic that comes up regularly, so this page collects the state of play.

See the new plan at ImpredicativePolymorphism/Impredicative-2015

Tickets

Use Keyword = ImpredicativeTypes to ensure that a ticket ends up on these lists.

Open Tickets:

#1330
Impredicativity bug: Church2 test gives a rather confusing error with the HEAD
#4281
Make impredicativity work properly
#4295
Review higher-rank and impredicative types
#8808
ImpredicativeTypes type checking fails depending on syntax of arguments
#9420
Impredicative type instantiation without -XImpredicativeTypes
#9730
Polymorphism and type classes
#10709
Using ($) allows sneaky impredicativity on its left
#11319
ImpredicativeTypes even more broken than usual
#11514
Impredicativity is still sneaking in

Closed Tickets:

#4347
Bug in unification of polymorphic and not-yet-polymorphic type
#7264
Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
#10619
Order matters when type-checking
#11428
ImpredicativeTypes causes GHC panic with 8.0.1-rc1
#12557
Regression in type inference with RankNTypes

What is impredicative polymorphism?

Consider this

foo :: (forall a. a -> a) -> Int
bar :: forall b. Bool -> b -> b

test1 :: Bool -> Int
test1 x = foo (bar x)

test2 :: Bool -> Int
test2 = foo . bar

Should test1 typecheck? Yes: GHC can see that foo's argument should have type forall a. a->a, and indeed bar x has that type. It involves higher-rank type inference (see Practical type inference for higher rank types), but GHC has supported this for ages.

What about test2? After all, it's just an eta-abstracted version of test1. No, test2 is rejected. Remember the type of (.):

(.) :: forall p q r. (q -> r) -> (p -> q) -> p -> r

To make this work in test2 we must instantiate q := forall a. a->a, to make the type of (.)'s first argument match foo's type. So we have to instantiate a polymorphic type variable q with a polymorphic type. This is called impredicative polymorphism, and GHC's type inference engine simply does not support it.

Constraints also trigger impredicative polymorhism

Although it does not appear to involve instantiating any polymorphic type variables with polymorphic types, instantiating a polymorphic type variable with qualified type will also trigger the "GHC doesn't yet support impredicative polymorphism" error.

For example

type Monadic m a = Monad m => m a
monadics :: [Monadic m a]
monadics = undefined

is not allowed.

A workaround for cases like this remove the constraint from the type synonym and add it at the use sites. I.e., the above example works if we change it to

type Monadic m a = m a
monadics :: Monad m => [Monadic m a]
monadics = undefined

Special case for ($)

Consider

runST :: (forall s. ST s a) -> a

foo = runST $ do { ...blah... }

Here again we need impredicative polymorphism, to instantiate ($)'s type, very much like (.) above. So foo would be rejected. But Haskell programmers use ($) so much, to avoid writing parentheses, that GHC's type inference has an ad-hoc special case for ($) that allows it to do type inference for (e1 $ e2), even when impredicative polymorphism is needed.

The internal language

All of this concerns the source language. GHC's internal language, System FC, is fully impredicative. This works fine because there is no type inference in System FC. It's only type inference that is the problem with impredicativity.

What about -XImpredicativeTypes?

We've made various attempts to support impredicativity, so there is a flag -XImpredicativeTypes. But it doesn't work, and is absolutely unsupported. If you use it, you are on your own; I make no promises about what will happen.

Workarounds

So if you need impredicativity and -XImpredicativeTypes doesn't work, what can you do? The main workaround is this: define a newtype to wrap the polymorphic function.

For example, you can't have a list of polymorphic functions, say [forall a. [a] -> [a]]. But you can wrap it like this:

newtype ListList = LL { unLL :: forall a. [a] -> [a] }

Now [ListList] is a perfectly fine type. The downside is that you have to wrap and unwrap, with LL and unLL, which is tiresome.

Reading

Here are some useful papers about type inference for impredicative polymorphism;

The way forward

Personally I think there are two ways forward:

  • Add explicit type application in some shape or form. That is, tell GHC exactly how to instantiate those polymorphic type variables. Explicit type application is what happens in the intermediate language, System FC, and there are many reasons for wanting it in the source language. See the explicit type application wiki page.
  • Do something along the lines of QML.

The key is to be less ambitious than our previous attempts. Anything in FC should be expressible in source Haskell, but we may have to accept relatively-intrusive type annotations to achieve it.

Last modified 2 months ago Last modified on Apr 24, 2017 8:22:38 AM