It all began with class (Vector (Point x)) => HasSpace x where type Point x :: * So far, so good. I was rather surprised that you _can_ write class (Complete (Completed x)) => Incomplete x where type Completed x :: * complete :: x -> Completed x I was almost as surprised to discover that you _cannot_ write class (HasSpace x, Complete (Completed x), HasSpace (Completed x), Point x ~ Point (Completed x)) => Incomplete where... It just means that every time you write an Incomplete instance, you might have to add the Point constraint manually. Which is mildly irritating. More worrying, adding Point foo ~ Point bar to an instance declaration causes GHC to demand that you turn on Undecidable Instances, for reasons beyond my comprehension. It's also interesting that when you write a class instance that has some constraint on it, and then you try to write a subclass instance, you still have to repeat the exact same constraint, even though the superclass instance declaration implies it. The only reason I can think of is that theoretically somebody could add a new superclass instance without the constraint. (Wouldn't that be an overlapping instance though?) And now things get *really* interesting. Consider this: data Foo x = Foo !x !(Point x) Surprisingly, GHC accepts this. This despite the rather obvious fact that "Point x" can exist if and only if "x" has a HasSpace instance. And yet, the type definition appears to say that "x" is simply an unconstrained type variable. Intriguing... Next, you can't derive Eq or Show for this type, but you *can* declare them manually: instance (Show x, Show (Point x)) => Show (Foo x) where show (Foo x px) = "Foo (" ++ show x ++ ") (" ++ show px ++ ")" Again, no hint of the fact that this will only work if we have HasSpace x. And yet GHC happily accepts this. I'm starting to think maybe I'm pushing the type system further than it can cope, and I should just completely redesign the whole thing...