Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.h..., Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_...: A Framework for Extended Algebraic Data Types. FLOPS 2006http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#Sulzm...: 47-64 describes such a system, fully implemented in Chameleon, but this system is no longer maintained. Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other. Local constraints are an orthogonal extension. In terms of type inference, type families + local constraints and fundeps + local constraints pose the same challenges. Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints. Apologies, Martin, you are quite right. Indeed, you were the first to teach me about implication constraints, which are the key to combining local constraints and functional dependencies. Chameleon implements such a system, using (I believe) the Constraint Handling Rule framework to solve the resulting constraints. However as you mention we could not figure out a good way to combine this approach to constraint solving with evidence generation, although it seems that in principle it should be possible. As you say Well, the point is that System FC is geared toward type families. The two possible solutions are (a) either consider fundeps as syntactic sugar for type families (doesn't quite work once you throw in overlapping instances), (b) design a variant System FC_fundep which has built-in support for fundeps. Why is FC is geared towards type families? It's not an accidental bias; it's more that I know how to do (a) and I don't know how to do (b). I'll write separately about the issue of overlap Simon