Context: I'm trying to produce an error monad that also keeps track of a list of warnings, something like this:
data Dangerous a = forall e w. (Error e, Show e, Show w) =>
Dangerous (ErrorT e (State [w]) a)
i.e. Dangerous a
is an operation resulting in (Either e a, [w])
where e
is a showable error and w
is showable.
The problem is, I can't seem to actually run the thing, mostly because I don't understand existential types all that well. Observe:
runDangerous :: forall a e w. (Error e, Show e, Show w) =>
Dangerous a -> (Either e a, [w])
runDangerous (Dangerous f) = runState (runErrorT f) []
This doesn't compile, because:
Could not deduce (w1 ~ w)
from the context (Error e, Show e, Show w)
...
`w1' is a rigidtype variable bound by
a pattern with constructor
Dangerous :: forall a e w.
(Error e, Show e, Show w) =>
ErrorT e (State [w]) a -> Dangerous a
...
`w' is a rigid type variable bound by
the type signature for
runDangerous :: (Error e, Show e, Show w) =>
Dangerous a -> (Either e a, [w])
I'm lost. What's w1? Why can't we deduce that it's ~ w
?
An existential is probably not what you want here; there is no way to "observe" the actual types bound to e
or w
in a Dangerous a
value, so you're completely limited to the operations given to you by Error
and Show
.
In other words, the only thing you know about w
is that you can turn it into a String
, so it might as well just be a String
(ignoring precedence to simplify things), and the only thing you know about e
is that you can turn it into a String
, you can turn String
s into it, and you have a distinguished value of it (noMsg
). There is no way to assert or check that these types are the same as any other, so once you put them into a Dangerous
, there's no way to recover any special structure those types may have.
What the error message is saying is that, essentially, your type for runDangerous
claims that you can turn a Dangerous
into an (Either e a, [w])
for any e
and w
that have the relevant instances. This clearly isn't true: you can only turn a Dangerous
into that type for one choice of e
and w
: the one it was created with. The w1
is just because your Dangerous
type is defined with a type variable w
, and so is runDangerous
, so GHC renames one of them to avoid name clashes.
The type you need to give runDangerous
looks like this:
runDangerous
:: (forall e w. (Error e, Show e, Show w) => (Either e a, [w]) -> r)
-> Dangerous a -> r
which, given a function which will accept a value of type (Either e a, [w])
for any choices of e
and w
so long as they have the instances given, and a Dangerous a
, produces that function's result. This is quite hard to get your head around!
The implementation is as simple as
runDangerous f (Dangerous m) = f $ runState (runErrorT m) []
which is a trivial change to your version. If this works for you, great; but I doubt that an existential is the right way to achieve whatever you're trying to do.
Note that you'll need {-# LANGUAGE RankNTypes #-}
to express the type of runDangerous
. Alternatively, you can define another existential for your result type:
data DangerousResult a = forall e w. (Error e, Show e, Show w) =>
DangerousResult (Either e a, [w])
runDangerous :: Dangerous a -> DangerousResult a
runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) []
and extract the result with case
, but you'll have to be careful, or GHC will start complaining that you've let e
or w
escape — which is the equivalent of trying to pass an insufficiently polymorphic function to the other form of runDangerous
; i.e. one that requires more constraints on what e
and w
are beyond what the type of runDangerous
guarantees.