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?

Beseech

NegSucc (NegSucc Zero) is -(-(0 + 1) + 1) = -(-1 + 1) = -0 = 0, so you have multiple representations of 0 anyway. – Spill

Think about open world assumption. What if someone else make NegSucc an instance of Peano? – Badr

@Spill NegSucc (NegSucc Zero) is not an Integer, because Integers are either peano numerals or the NegSucc of peano numerals. NegSucc (NegSucc Zero) cannot be incremented either since only Integers can be incremented. You might be able to argue that NegSucc (NegSucc Zero) is equivalent to Zero but I don't think it is very meaningful. – Beseech

@Badr Your question leads me to understanding the difference. If you would like to write up a full answer I'd be happy to accept. If you don't want to spend the time I'd be happy to write up the answer myself. – Beseech

@WheatWizard sorry, I don't know enough about functional dependencies to make a real answer, I just made an intuitive guess. I hope someone will write an answer and describe all the technical details. – Badr

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.

Beseech

Answer 2

Here's the error message I see with the original version:

negsucc.hs:28:10: error:
    Functional dependencies conflict between instance declarations:
      instance Peano a => Increment a (Succ a)
        -- Defined at negsucc.hs:28:10
      instance Increment (NegSucc Zero) Zero
        -- Defined at negsucc.hs:29:10
      instance Peano a => Increment (NegSucc (Succ a)) (NegSucc a)
        -- Defined at negsucc.hs:30:10

My loose understanding here is:

• the functional dependency a -> b means that GHC will "pattern match" on the type a, and will expect to discover b based on a.
• GHC does not include superclass constraints in this "pattern matching" logic. This is important. Intuitively, you know that NegSucc is not an instance of Peano. However GHC does not know how to look at a NegSucc and rule out the instance that requires Peano NegSucc. (This is simply a matter of knowing how GHC instance selection works. One could imagine that a future improvement to GHC might improve on this situation.)
• instance Peano a => Increment a (Succ a) will therefore always be selected by GHC, because it is the catch-all Increment a. Any other defined instances will conflict with this instance.

Now, isn't that what UndecidableInstances is for? To allow for conflicting instances, and allow GHC to select the most specific one that applies? You might think so. I thought so. However, note that the error message is specifically talking about the Functional dependencies conflict, meaning I don't think UndecidableInstances is implemented adequately to handle overlapping FunDeps in this way.

-- pseudocode for the fundep a -> b
increment a = Succ a
increment (NegSucc Zero) = Zero
increment (NegSucc (Succ a)) = NegSucc a
-- note that this is just pseudocode; unlike Haskell,
-- instead of trying cases from top to bottom
-- all cases will be tried simultaneously

However, this issue doesn't exist if you "expand" the definition, as you did.

-- pseudocode for the fundep a -> b with expanded defs
increment Zero = Succ Zero
increment (Succ a) = Succ (Succ a)
increment (NegSucc Zero) = Zero
increment (NegSucc (Succ a)) = NegSucc a
-- notice how there is now no overlap on the LHS pattern matches

You could also solve the problem by flipping the fundep around with the original defs.

-- pseudocode for the fundep b -> a with original defs
-- I called it "decrement" instead,
-- because from the b -> a point of view, that is what it does
decrement (Succ a) = a
decrement Zero = NegSucc Zero
decrement (NegSucc a) = NegSucc (Succ a)
-- notice how there is no overlap on the LHS pattern matches

I am stretching my own knowledge of fundeps here, so someone please correct me if I'm wrong.

Hopping