[Haskell-cafe] The Coverage Condition of functional dependencies
petr.mvd at gmail.com
Wed Jan 23 21:49:33 CET 2013
Hi, trying to understand UndecidableInstances (and to find and answer to <
http://stackoverflow.com/q/14476230/1333025>), I was trying to find out why
"mtl" needs UndecidableInstances.
The reason is that instances like
> instance MonadState s m => MonadState s (ContT r m) where
don't satisfy the Coverage Condition:
"The Coverage Condition. For each functional dependency, tvsleft ->
tvsright, of the class, every type variable in S(tvsright) must appear in
S(tvsleft), where S is the substitution mapping each type variable in the
class declaration to the corresponding type in the instance declaration. "
In other words, "s" isn't expressed using type variables in "ContT r m".
But in these cases, it's actually possible. Because of the assertion
"MonadState s m" and its dependency "m -> s" we know that "s" will be
always deducible from "m".
I wonder, would it be possible to augment the type checker to realize this?
It seems reasonable: Before comparing if S(tvsright) is a subset of
S(tvsleft), we'd add every type variable to S(tvsleft) that is determined
from it using functional dependencies in the assertion of the instance.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe