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