Okay, we seem to be having a debate where, to caricature only a little, I'm arguing that Fundeps/UndecidableInstances are ugly but useful, and other people are arguing that they are truly absolutely horrible in their current GHC implementation. I think the debate boils down to where you see the scope of the implicit universal quantification of free type variables in instances. Consider the following: class C a b | a -> b where aDefault :: a aTobC :: a -> b class D a b where -- no fundep aTobD :: a -> b instance (D Int b) => C Int b where -- should this be allowed? aDefault = 0 aTobC = aTobD GHC accepts this above code, which makes sense to me because I read the instance declaration as essentially (in pseudo-Haskell): forall b. instance (D Int b) => C Int b or, equivalently: instance C Int (forall b. (D Int b) => b) In English, "there's only one instance of C with (a ~ Int), but, in that instance, the aTobC method returns a value of type b for any b you want, except that in order to produce the value, it needs access to an appropriate dictionary of class D." One corollary of this view is that it is impossible to violate functional dependencies without defining more than one instance of a class. The alternate reading (and please correct me if I'm mis-characterizing the argument), is that we should apply the functional dependencies of a class to each individual instance, where any universal quantification happens across the fundep. According to this view, we should read C's instance declaration as: forall b. (instance (D Int b) => C Int b | Int -> b) and find that "forall b. ... | Int -> b" fails. Hence, we have violated functional dependencies with a single instance of the class. There's a less explicit but equally important question underlying this discussion about how much contexts should play into instance validation. Some have suggested GHC should reject the above instance of C, but should nonetheless accept the following instance of C': class C' a b | a -> b class E a b | a -> b -- unlike above, we now have a fundep instance (E a b) => C' a b Oleg, you haven't weighed in this specific question, but I think many of your ideas require the ability to write instances like C', even if you advocate disallowing C. On this question, I am opposed, because I find it too reminiscent of an aspect of C++ I dislike, namely that ad-hoc polymorphism interacts with templates, implicit promotion, and the most-specific match rule to make it hard to understand code. (And since, unlike C++, Haskell allows polymorphic return types, there's a potential for things to get even more complicated.) Fortunately, GHC's current approach is quite simple: The instance head is always sufficient to determine whether or not an instance matches, two instances overlap, or functional dependencies are violated. The context may tell you what dictionaries must be around if you actually want to use an instance, but if you know that a program compiles, you can ignore the context when reading and reasoning about the code. Another reason that I oppose too much reliance on the context is that I want the ability to load code dynamically. If the assumption about ground type equality is pushed too far--e.g., allowing coercion based on reasoning about fundeps--then dynamically loading modules with contradictory fundeps could undermine memory safety. One of my objections to type families is the difficulty of guaranteeing safety in the presence of dynamic loading. At any rate, this is the haskell-prime mailing list, not the how-much-do-you-hate-some-current-ghc-option-implementation list. I've already taken a lot of people's time with this thread, so let me propose to do something useful for the haskell prime effort. I could start a compilation (probably a wiki page) of things you can do or might want to do with fundeps and undecidable/overlapping instances. This could serve as a kind of wish list for Haskell prime. Examples off the top of my head might be: - Type-safe dynamic loading - Sqrt(N) reduction in code size for mtl instances - HList/OO-Haskell - Enforcing simple recursively-defined properties on types. (E.g., with GHC 7.2's new generic deriving framework, you might want to specify the constraint that a type's Representation doesn't include NoSelector.) - Using data types to represent ad-hoc polymorphic functions you can pass as arguments to functions. E.g., using a class like: class Function f a b | f a -> b where funcall :: f -> a -> b you can define types f of class Function and use them to do maps over tuples. Someone thinking of implementing an idea (e.g., closed type families) could look at the wish list and determine out how much of it the new feature would cover. Others could add to the wish list. Oleg, I realize the list might resemble your bibliography, but the idea would be to list the simplest possible cases (like C' above), rather than examples that unleash the full power of the extension. We can link to your web site for people who want to delve deeper into the motivation. If that sounds like a useful idea, the next question is where to put such a list. The Haskell prime wiki seems like a logical place, but it should be someplace where multiple people can edit it. (And, though I have an account on the Haskell prime wiki, username David, I can't seem to edit stuff there.) David