Why does my functional dependency conflict disappear when I expand the definition?

Question

I was trying to implement Integers at the type level in Haskell. To start I implemented natural numbers with

data Zero
data Succ a

I then extended this to the integers with

data NegSucc a

I decided to then create an Increment class that would increment integers. Here is how I did that:

{-# Language FunctionalDependencies #-}
{-# Language UndecidableInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}

import Prelude ()

-- Peano Naturals --

data Zero
data Succ a

class Peano a
instance Peano Zero
instance (Peano a) => Peano (Succ a)

-- Integers --

data NegSucc a -- `NegSucc a` is -(a+1) so that 0 can only be expressed one way

class Integer a
instance (Peano a) => Integer a
instance (Peano a) => Integer (NegSucc a)

-- Arithmetic Operations --

class Increment a b | a -> b
instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero
instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

However when I run this GHC complains that Functional dependencies conflict between instance declarations, and cites all three of my increment instances. This error doesn't make much sense to me, I don't see any conflict between the separate declarations. What confuses me even further is that if I change the first instance to two separate instances

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

The compiler stops complaining altogether. However the rules that define Peano a tell me that these two things should be the same.

Why do I get a functional dependency conflict when I write the single line version but none when I write the two line version?

Answer 1

This answer is an expansion of this comment, which lead me to understanding what was going on

In Haskell type classes are an open class, this means that new instances of the class can be made after the declaration.

This means that we cannot infer that NegSucc a is not a member of Peano, because it is always possible that it could be declared one later.

instance Peano (NegSucc a)

Thus when the compiler sees

instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero

it cannot know that NegSucc Zero will not be an instance of Peano. If NegSucc Zero is an instance of Peano it would increment to both Zero and Succ (NegSucc Zero), which is a functional dependency conflict. So we must throw an error. The same applies to

instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

Here (NegSucc (Succ a)) could also be an instance of Peano.

The reason it looks as if there is no conflict is that we implicitly assume that there are not other instances of Peano than the ones that we know of. When I transformed the single instance to two new isntances I made that assumption formal.

In the new code

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

it is not possible to add anything to preexisting type classes to cause a type to match multiple conflicting instances.