You raise a vexed question, which has been discussed a lot. Should this typecheck? class C a b | a -> b instance C Int Bool f :: forall a. C Int a => a -> a f x = x GHC rejects the type signature for f, because we can see that 'a' *must be* Bool, so it's a bit misleading to universally quantify it. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Dirk Reckmann | Sent: 21 July 2005 10:30 | To: glasgow-haskell-users@haskell.org | Subject: Functional Dependencies | | 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