|  Also, what is the difference between fundeps and type families
|  wrt local type constraints? I had always assumed them to be
|  equivalent, if fully implemented. Similar to logic vs functional
|  programming, where Haskellers tend to find the latter more
|  convenient. Functional logic programming shows that there
|  are some tricks missing if one just drops the logic part.

Until now, no one has know how to combine fundeps and local constraints.  For example

 class C a b | a->b where
   op :: a -> b

 instance C Int Bool where

   op n = n>0

 data T a where
   T1 :: T a
   T2 :: T Int

 -- Does this typecheck?
 f :: C a b => T a -> Bool
 f T1 = True
 f T2 = op 3

The function f "should" typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool).  But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it.