Hello Conal,
the implementation of fun-deps in GHC is quite limited, and they don't do what you'd expect with existential types (like in your example), type-signatures, or GADTs. Basically, GHC only uses fun-deps to fill-in types for unification variables, but it won't use them to reason about quantified variables.
Here is an example that shows the problem, just using type signatures:
> class F a b | a -> b where
> f :: a -> b -> ()
>
> instance F Bool Char where
> f _ _ = ()
>
> test :: F Bool a => a -> Char
> test a = a
GHC rejects the declaration for `test` because there it needs to prove that `a ~ Char`. Using the theory of fun-deps, the equality follows because from the fun-dep we know that:
forall x y z. (F x y, F x z) => (y ~ z)
Now, if we instantiate this axiom with `Bool`, `Char`, and `a`, we can prove that `Char ~ a` by combining the instance and the local assumption from the signature.
Unfortunately, this is exactly the kind of reasoning GHC does not do. I am not 100% sure on why not, but at present GHC will basically do all the work to ensure that the fun-dep axiom for each class is valid (that's all the checking that instances are consistent with their fun-deps), but then it won't use that invariant when solving equalities.
I hope this helps!
-Iavor