[Haskell-cafe] Why do I need UndecidableInstances?

[Stijn van Drongelen]

On Thu, Oct 24, 2013 at 12:37 PM, Alejandro Serrano Mena
<trupill at gmail.com>wrote:

> Dear café,
> I'm trying to compile a set of simple examples using Functional
> Dependencies. One of the first ones is the case of natural numbers, which
> I've defined along with some operations as:
>
> data Zero
> data Succ a
>
> class Plus x y z | x y -> z
> instance Plus Zero x x
> instance Plus x y z => Plus (Succ x) y (Succ z)
>
> class Max x y z | x y -> z
> instance Max Zero     y    y
> instance Max (Succ x) Zero (Succ x)
> instance Max x y z => Max (Succ x) (Succ y) (Succ z)
>
> I thought the compiler would accept this only with the extensions
> EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies and
> FlexibleInstances. But, to my surprise, GHC is also asking me for
> UndecidableInstances. Why is this the case?
>
> Thanks in advance :)
>

Hi Alejandro,

The error messages mention that the 'Coverage Condition' fails for the last
instance of both classes. This condition is defined in the manual of GHC (
http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/type-class-extensions.html#instance-rules
):

> For each functional dependency, tvs_left -> tvs_right, of the class,
every type variable in S(tvs_right) must appear in S(tvs_left), where S is
the substitution mapping each type variable in the class declaration to the
corresponding type in the instance declaration.

Let's look at the Plus instance: every type variable in S(z) must appear in
S(x) or S(y). This is false for both the context and the instance type: the
variable 'z' in "Plus x y z" occurs in neither 'x' or 'y', and the variable
'z' in "Plus (Succ x) y (Succ z)" occurs in neither 'Succ x' or 'y'.

I'm not familiar enough (yet) with the reasons behind this rule to explain
why it's there (if anyone can explain this in detail, please do!), but this
should be a direct answer to your question: it's against the rules.

Kind regards,

Stijn van Drongelen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131024/07dfc38d/attachment.html>