On Tue, Jun 14, 2011 at 1:19 PM,
No, these are not equivalent. The first one "TypeEq a b c" is just declaring an instance that works "forall c". The second is declaring multiple instances, which, if there were class methods, could have different code. The second one is illegal, because given just the first two types, a and b, you cannot tell which instance to pick.
Then why am I not allowed to write: class C a b | a -> b instance C T [a] without undecidable instances? GHC actually complains in that case that the coverage condition is violated. But it is a single well specified instance that works for all a. The answer is that such an instance actually violates the functional dependency, but UndecidableInstances just turns off the checks to make sure that fundeps are actually functional. It's a, "trust me," switch in this case (not just a, "my types might loop," switch). So I guess HList will still work fine, and UndecidableInstances are actually more evil than I'd previously thought (thanks for the correction, Andrea :)).
A functional dependency such as "| a b -> c d" just guarantees that a and b uniquely determine the instance. Hence, it is okay to have class methods that do not mention type variables c and d, because the compiler will still know which instance to pick.
It specifies that a and b uniquely determine c and d, so the choice of instances is unambiguous based only on a and b. This is the basis for type level computation that people do with fundeps, because a fundep 'a b -> c' allows one to compute a unique c for each pair of types. If it were just about variable sets determining the instance, then we could just list those. But I can write: class C a b c d | a b -> c And it will actually be a, b and d that determine the particular instance, but just listing 'a b d', or using the fundep 'a b d -> c' is wrong, because the fundep above specifies that there is a single choice of c for each a and b. So we could have: C Int Int Char Int C Int Int Char Double C Int Int Char Float but trying to add: C Int Int Int Char to the first three would be an error, because the first two parameters determine the third, rather than the first, second and fourth. Being allowed to elide variables from the types of methods is one of the uses of fundeps, and probably why they were introduced, but it is not what fundeps mean.
On the other hand, though the compiler won't accept it, you could at least theoretically allow code such as the following:
instance C [Char] where type Foo [Char] = forall b. () => b
The fundep equivalent of this is not 'instance C [Char] b'. It is: instance C [Char] (forall b. b) except types like that aren't allowed in instances (for good reason in general). The closest you could come to 'instance C T b' would be something like: type instance F T = b except that is probably interpreted by GHC as being (forall b. b). -- Dan