fundeps help

[Simon Peyton-Jones]

| 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