Unwrapping the STT monad in a transformer stack?

Question

This question is apparently related to the problem discussed here and here. Unfortunately, my requirement is slightly different to those questions, and the answers given don't apply to me. I also don't really understand why runST fails to type check in these cases, which doesn't help.

My problem is this, I have one section of code that uses one monad stack, or rather a single monad:

import Control.Monad.Except
type KErr a = Except KindError a

Another section of code needs to integrate with this that wraps this within the STT monad:

type RunM s a = STT s (Except KindError) a

At the interface between these sections, I clearly need to wrap and unwrap the outer layer. I've got the following function to work in the KErr -> RunM direction:

kerrToRun :: KErr a -> RunM s a
kerrToRun e = either throwError return $ runExcept e

but for some reason I just can't get the converse to type check:

runToKErr :: RunM s a -> KErr a
runToKErr r = runST r

I'm working on the assumption that as the RunM's inner monad has the same structure as KErr, I can just return it once I've unwrapped the STT layer, but I don't seem to be able to get that far, as runST complains about its type arguments:

src/KindLang/Runtime/Eval.hs:18:21:
    Couldn't match type ‘s’ with ‘s1’
      ‘s’ is a rigid type variable bound by
          the type signature for runToKErr :: RunM s a -> KErr a
          at src/KindLang/Runtime/Eval.hs:17:14
      ‘s1’ is a rigid type variable bound by
           a type expected by the context:
             STT s1 (ExceptT KindError Data.Functor.Identity.Identity) a
           at src/KindLang/Runtime/Eval.hs:18:15
    Expected type: STT
                     s1 (ExceptT KindError Data.Functor.Identity.Identity) a
      Actual type: RunM s a

I've also tried:

runToKErr r = either throwError return $ runExcept $ runST r

in order to more strongly isolate runST from its expected return type, in case that was the cause of the issue, but the results are the same.

Where is this s1 type coming from, and how do I persuade ghc that it's the same type as s?

score 5 · Accepted Answer · answered Apr 25 '16 at 01:41

(The below talks about ST s a but applies just the same as STT s m a; I've just avoided the unnecessary complication of talking about the transformer version below)

The problem you are seeing is that runST has type (forall s. ST s a) -> a to isolate any potential (STRef-changing) effects of the computation from the outside, pure world. The whole point of the s phantom type that all ST computations, STRefs, etc. are tagged with, is to track which "ST-domain" they belong to; and the type of runST ensures that nothing can pass between domains.

You can write runToKErr by enforcing the same invariant:

{-# language Rank2Types #-}

runToKErr :: (forall s. RunM s a) -> KErr a
runToKErr = runST

(of course, you might realize further down the road that this restriction is too strong for the program you hope to write; at that point you'll need to lose hope, sorry, I mean you'll need to redesign your program.)

As for the error message, the reason you can't "convince the type checker that s1 and s are the same type" is because if I pass you an ST s a for a given choice of s and a, that is not the same as giving you something which allows you to choose your own s. GHC chose s1 (a Skolemized variable) as s and so tries to unify ST s a with ST s1 a

Unwrapping the STT monad in a transformer stack?

1 Answers1