| I'm trying to understand what fundeps do and don't let me do. One | particular source of confusion is why the following program doesn't | typecheck: | | {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} | module Fundeps where | | class Dep a b | a -> b, b -> a | | conv :: (Dep a b1,Dep a b2) => b1 -> b2 | conv = id | {- end of program -} GHC implements "improvement" by *identifying* the two equal types. Here they cannot be identified because they are separate type variables. A good way to think of this is to imagine translating the program into System F: you can't do it. Functional dependencies guide type inference by adding extra unifications, resolving types that would otherwise be under-constrained and ambiguous -- but fundeps (or at least GHC's implementation thereof) does not deal with the case where the types become *over*-constrained. GHC's new intermediate language, System FC, is specifically designed to do this. Currently we're in transition: equality constraints are starting to work, but fundeps are implemented as they always were. I hope we can eventually switch over to implementing fundeps using equality constraints, and then the above program will work. Meanwhile, in the HEAD you can write conv :: (a~b) => a -> b conv = id Which, IHMO, is a much clearer way to say it! You may also like to try the paper that Martin and I and others wrote about fundeps: http://research.microsoft.com/%7Esimonpj/papers/fd-chr Simon