Petr P | 23 Jan 21:49 2013
Picon

The Coverage Condition of functional dependencies

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.

  Best regards,
  Petr
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane