No you can't, at least not without specifying something more to mkProxy
.
The way the ST monad works is by requiring the escaping computation to generate something of type forall s. ST s a
which prevents s
from appearing free in a
.
In your case however, you're doing two identical computations so generating a different type for each could be used to do evil things. For example, if mkInt 1
generated different types each time it was called,
class Evil a b c | a, b -> c where
foo :: a -> b -> c
let x = mkProxy 1 in foo x x
Would be different than
foo (mkProxy 1) (mkProxy 1)
and we've lost some very nice properties in our code.
We can however do some extra leg work and make the fact that a
and b
can't unify explicit
{-# LANGUAGE DataKinds #-}
data Nat = S Nat | Z
data Proxy (n :: Nat) a = Proxy a
based :: a -> Proxy Z a
based = Proxy
fresh :: Proxy n a -> a -> Proxy (S n) a
fresh (Proxy _) a = Proxy a
So now you need to do something like
a = based 1
b = fresh a 2