newtype around ST causes type error

Question

When I try to load the following code under GHC 7.4.1:

{-# LANGUAGE RankNTypes #-}

import Control.Monad.ST

newtype M s a = M { unM :: ST s a }

runM :: (forall s. M s a) -> a
runM (M m) = runST m

It fails with the following message:

test.hs:9:14:
    Couldn't match type `s0' with `s'
      because type variable `s' would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: ST s a
    The following variables have types that mention s0
      m :: ST s0 a (bound at test.hs:9:9)
    In the first argument of `runST', namely `m'
    In the expression: runST m
    In an equation for `runM': runM (M m) = runST m

Why does this fail, when M is just a wrapper around ST?

(My actual program has a few transformers stacked on top – this is just a minimal case.)

---

EDIT: It seems adding a let fixes the issue:

runM m = let M m' = m in runST m

However, if TypeFamilies is enabled (as it is in my real code), it fails again.

Answer 1

It's a problem with the pattern matches + rankntypes.

GHC infers m to have the type ST ??? a where ??? is a type variable that can unify with anything and has to unify with something*. So we then pass it along to runST and runST wants an ST s a so m unifies with it and ??? unifies with s. But wait, now we're unifying with s outside the scope where s is defined scope so disaster.

A simpler example is

test (M m) = (m :: forall t . ST t a) `seq` ()

And again we get the same error because we attempt to unify with the type of m using t, but t is in too small a scope.

The simplest solution is simply not to create this type variable with

 test m = runST (unM m)

here unM returns a good and true polymorphic ST that runST is happy with. You can use let since it's by default polymorphic but since -XTypeFamilies will make let monomorphic it will blow up just like pattern matching as you've discovered.

---

** It appears that m is monomorphic. let is polymorphic without type families so I suspect this is what's going on. It behaves like it

test :: forall a. (forall t. M t a) -> ()
test (M m) = (m :: ST Bool a) `seq` (m :: ST Int a) `seq` ()

Errors trying to unify Bool and Int as you would expect from a monomorphic type variable. Why does every weird type error I find seem to hide some form of monomorphic type variable..