Why are higher rank types so fragile in Haskell

Question

I was messing around with the runST function. Which has type (forall s. ST s a) -> a and it seems like trying to use it in any way that isn't directly applying without any indirection breaks it in pretty nasty ways.

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

so by substituting a in const for forall s. ST s a you should get the type of const runST

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

but instead GHC says that it can't match a with (forall s. ST s a) -> a but since a literally means forall a. a which is satisfied by every type I don't see what is invalid about that.

As it turns out using \_ -> runST instead actually works just fine and gives the correct type.

Once I had constST with the correct type I wanted to see if I could uncurry it, but unsurprisingly that also breaks. But it seems like it really shouldn't, although admittedly this case seems less obvious than the previous one:

constST :: b -> (forall s. ST s a) -> a
uncurry :: (a -> b -> c) -> (a, b) -> c

So then surely the a in uncurry could be replaced with the b in constST and the b in uncurry could be replaced with the (forall s. ST s a) in constST and the a in uncurry could be replaced with the c in constST. This gives us:

uncurry constST :: (b, forall s. ST s a) -> a

Now admittedly this type is impredicative which I know is pretty problematic. But technically Just mempty is also impredicative when substituting directly without moving the implicit forall quantification.

Just :: a -> Maybe a
mempty :: forall a. Monoid a => a
Just mempty :: Maybe (forall a. Monoid a => a)

But the forall is automatically floated up to give you:

Just mempty :: forall a. Monoid a => Maybe a

Now if we do the same thing for uncurry constST we should get the sensible and as far as I can tell correct type of:

uncurry constST :: (forall s. (b, ST s a)) -> a

Which is higher rank but not impredicative.

Can someone explain to me why basically none of the above actually works with GHC 8, is there something more fundamental that makes the above very complicated in the general case? Because if not it seems like it would be really nice to have the above work, if only to get rid of the annoying special casing of $ purely for the sake of runST.

On a side note is it possible that instead of all the forall floating we could instead have ImpredicativeTypes just work correctly. It correctly infers the type for Just mempty as Maybe (forall a. Monoid a => a) but it seems like actually using it is not that easy. I have heard that impredicative type inference is not really doable but would it work to somehow limit type inference to predicative types except when you provide type signatures to indicate otherwise. Similar to how MonoLocalBinds makes local bindings monomorphic by default for the sake of type inference.

Answer 1

To be able to write const runST, you need to active the Impredicative types extension (on GHCi: :set -XImpredicativeTypes).

Answer 2

You have answered your own question:

... by substituting a in const for forall s. ST s a ...

This is the definition of impredictive polymorphism - the ability to instantiate a type variable with a polytype, which is (loosely) a type with a forall quantifier at the leftmost side of the type.

From the GHC trac page on the subject:

GHC does not (yet) support impredicative polymorphism

and furthermore

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.

So do not use ImpredictiveTypes - it won't help.

---

Now for the gory details - why do all the specific examples work as they do?

You've noted that in the expression Just mempty, the impredictive type Maybe (forall a. Monoid a => a) is not inferred; instead, the forall is 'floated out'. You also noted that performing the same process for uncurry constST gives a type "which is higher rank but not impredicative". The GHC user guide has this to say about higher rank types:

In general, type inference for arbitrary-rank types is undecidable. ...

For a lambda-bound or case-bound variable, x, either the programmer provides an explicit polymorphic type for x, or GHC’s type inference will assume that x’s type has no foralls in it.

So you really have to help it quite a bit, and that usually precludes using higher-order functions alltogether (note the above says nothing about arbitrary applications, only about bound variables - and uncurry constST has no bound variables!). The correct type for Just mempty is rank 1, so there is no issue inferring it, with or without additional type signatures.

For example, you can write your (forall s. (b, ST s a)) -> a function as such (on GHC 8.0.1 at least):

constST' :: forall a b . (forall s . (b, ST s a)) -> a
constST' z = runST z' 
  where z' :: forall s . ST s a
        z' = snd z

and also note that you cannot even pattern match on the pair, because this immediately instantiates the bound b type var:

constST' :: forall a b . (forall s . (b, ST s a)) -> a
constST' (a,b) = _res 

Using typed holes, you get:

* Found hole: _res :: a
  Where: `a' is a rigid type variable bound by
           the type signature for:
             constST' :: forall a b. (forall s. (b, ST s a)) -> a
* In the expression: _res
  In an equation for constST': constST' (a, b) = _res
* Relevant bindings include
    b :: ST s0 a 
    a :: b 

Note the type of b is ST s0 a for some fresh type variable s0, not the required forall s . ST s a for runST. There is no way to get the old type back.

---

The simplest solution to such things is probably to define a newtype, as the GHC trac page suggests:

newtype RunnableST a = RST (forall s . ST s a)

rrunST :: RunnableST a -> a 
rrunST (RST a) = runST a 

And store your ST actions which are ready to run in this container:

doSomething :: RunnableST X
doSomething = RST $ do ...