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