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.

Inoculation

I don't know the full underlying theory, but type inference with higher ranked polytypes is hard -- IIRC, undecidable. Hence, polymorphism has to be somehow limited to make inference possible. A typical restriction is to allow each type variable forall a. ... to be instantiated only with monotypes (including data, newtypes). Impredicative types do relax this restriction, but right now they do not work fine in GHC. – Mambo

@chi, my vague understanding is that Haskell 98 + rank-2 types can be inferred with difficulty, but that adding higher ranks or various type system extensions makes inference impossible. – Obsecrate

Answer 1

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

Hyperion

I think that more or less makes sense. But I still am not sure why having type inference able to substitute poly types and then float the foralls is all that crazy. Is inferring const runST correctly really that problematic with a limited subset of higher rank type inference? I realize that it won't be able to safely create higher rank types out of nothing, but once you already have a higher rank type it seems like it wouldn't be that big of a deal to allow it to be passed around a bit. – Inoculation

The problem with identifying and implementing a 'limited subset' of higher rank type inference is you need a formal semantics for it - without impredicative types, there isn't even a way to state at which type const is instantiated in const runST, because that type is impredicative, even though the result type is not. The typechecker therefore would need to support impredicative types, solving the problem we were trying to avoid having to solve in the first place. It seems such a limited subset would be even more limited than your particular example (which is already very simple). – Hyperion

Ok I think I see what you are saying, this seems like one of those: simple on paper for one example and a bit of common sense, but really horrible from a computational and general case perspective. Well hopefully eventually ImpredicativeTypes will be supported. – Inoculation

Answer 2

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

Brunhilde

ImpredicativeTypes is un-supported as of GHC 8, and it does not work by any reasonable standard of working. – Meniscus

@AndrásKovács, it's been less-officially unsupported since long before that. If I'm not mistaken it came in with boxy types and then stuck around like a drunk party-goer after that was replaced by OutsideIn(X). – Obsecrate