Geek Answers Handbook

Newtype around ST causes a type error

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

{-# LANGUAGE RankNTypes #-} import Control.Monad.ST newtype M sa = M { unM :: ST sa } runM :: (forall s. M sa) -> a runM (M m) = runST m

The following message failed to complete:

 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 sa 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 several transformers stacked on top; this is just a minimal case.)

EDIT : adding let seems to fix the problem:

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

However, if TypeFamilies enabled (as in my real code), it does not work again.

+7
polymorphism haskell higher-rank-types
source share
1 answer

This is a problem with matching templates + rankntypes.

GHC tells m to be of type ST ??? a ST ??? a where ??? is a type variable that can be combined with anything and must be combined with something *. Therefore, we pass it to runST , and runST wants ST sa , so m combines with it, and ??? combined with s . But wait, now we are teaming up with s outside the area where s defines the scope, so it’s a disaster.

A simpler example:

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

And again, we get the same error, because we are trying to combine with type m with t , but t is too small.

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

  test m = runST (unM m)

here unM returns a good and true polymorphic ST that satisfies runST . You can use let because it is polymorphic by default, but since -XTypeFamilies will make it monomorphic, it will explode just like pattern matching as you discovered.

** It seems that m monomorphic. let is polymorphic without type families, so I suspect this is what happens. It behaves like

 test :: forall a. (forall t. M ta) -> () 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 variable of monomorphic type. Why does any strange type error that I find seem to hide some kind of type of monomorphic type.

+11
source share

More articles:


All Articles