Functional Dependencies

Dirk Reckmann reckmann at
Thu Jul 21 05:30:03 EDT 2005

Hello everybody!

I wanted to have some fun with functional dependencies (see, 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 

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:

    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 (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 

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

More information about the Glasgow-haskell-users mailing list