Functional Dependencies

[Dirk Reckmann]

Hello everybody!

I wanted to have some fun with functional dependencies (see 
http://www.cs.chalmers.se/~hallgren/Papers/wm01.html), and tried some 
examples from this paper as well as some own experiments. The idea is to use 
the type checker for computations by "abuse" of type classes with functional 
dependencies.

The example in the attached file is taken from the above paper. Due to the 
functional dependencies, I expected the type of seven to be uniquely 
determined to be (Succ (Succ (Succ ...))), i. e. seven, but ghc (version 6.4) 
gives me following error message:

Add.hs:14:0:
    Couldn't match the rigid variable `a' against `Succ s'
      `a' is bound by the type signature for `seven'
      Expected type: Succ s
      Inferred type: a
    When using functional dependencies to combine
      Add (Succ n) m (Succ s), arising from the instance declaration at 
Add.hs:11:0
      Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) a,
        arising from the type signature for `seven' at Add.hs:13:0-77
    When generalising the type(s) for `seven'

However, using the definition of Add to define Fibonacci numbers does work, 
and a similar function declaration can be used to compute numbers by the type 
checker.

The same definition of Add works in Hugs...

So, is this a bug in ghc, or am I doing something wrong?

Thanks in advance,
	Dirk Reckmann
-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}

module Add where

data Zero
data Succ n

class Add n m s | n m -> s

instance Add Zero m m
instance Add n m s => Add (Succ n) m (Succ s)

seven :: Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) a => a
seven = undefined