Manuel M T Chakravarty:
Hugo Pacheco:
I would simply like the compiler not to use that instance if the equality constraint does not hold, like some another instance dependency constraint, but I assume that is not possible.
This is independent of type families. The selection of type class instances does *never* dependent on the instance context, only on the instance head. I know that this is sometimes annoying, but type checking would be a a lot more complicated/expensive without that rule.
What Hugo Pacheco wants *is* possible, in GHC as it is (and even as it was back in 2004). Although the selection of type class instances indeed depends only on the instance head, on the surface, the dependence on context is quite easy to accomplish. Here's is the outline of the idea. Suppose we wish to select one of the two instances, depending on whether the constraint C x hold or not: instance C x => CMain x instance CMain x We encode this as follows: class CMain x instance (CPred x flag, CMain' flag x) => CMain x The main class has only one instance, and there is no longer any overlapping. The main selection is done in an auxiliary class class CMain' flag x instance CMain' HTrue x -- will be selected when CPred holds instance CMain' HFalse x -- otherwise Note there are no overlapping instances required. The trick is to re-write constraint C x into the form CPred x flag (where flag functionally depends on x). Whereas C x succeeds, CPred x flag should succeed and unify flag with HTrue. Should C x fail, CPred should still succeed and unify flag with HFalse. TypeEq is such a predicate in the case of type equality. CPred is easy to implement with type-classes, and probably even easier with type families. The HList and OOHaskell papers use this technique to great extent. The following message describes that even backtracking is possible: http://okmij.org/ftp/Haskell/poly2.txt