| > 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. | | Ok, maybe this is a reasonable choice. But why does the attached program work? | ghci presents a unique type for the universal quantified function 'eight': | | *Add> :t eight | eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))
From the instance declaration instance Fib Zero (Succ Zero) we get the improvement rule Fib Zero a ==> a=(Succ Zero) We get a similar rule from instance Fib (Succ Zero) (Succ Zero) But the instance declaration instance (Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum ) => Fib (Succ (Succ n)) sum Fib Zero a gives only Fib Zero a ===> exists b. b=a which does nothing useful.
So when GHC sees the type signature, it's quite happy. No improvement takes place. If you compile Fib with -ddump-types you'll see it gets the type you specify. HOWEVER, when you say ":t eight", GHC does not simply report the type of "eight". You can type an arbitrary expression there (e.g. ":t (reverse "hello")"). So GHC typechecks the expression "eight". So it instantiates its type, and then tries to solve the constraint (Fib (Succ (Succ...)) n). Now it must use the instance declarations to simplify it, and in doing so that exposes more constraints that do force n to be the type you get. I agree this is desperately confusing, and I'm not saying that GHC is doing the Right Thing here; but I wanted to explain what it is doing. Functional dependencies are very slippery. I do not think their behaviour in GHC is necessarily best, nor is their exact behaviour specified anywhere, but I do think the behaviour is consistent. My current belief is that fundeps are too slippery to be given to programmers at all. They are not a good way to express type-level computation. Perhaps associated types might be a better way to express this stuff (see my home page). Simon