Hello everyone I think I'm close to useful results on the instance restrictions. First there's an obvious extension to the Haskell98 rule. The H98 rule says the instance head must be a type constructor applied to type variables, and the context must mention only those type variables. This gives a termination proof by counting constructors. If the rule is weakened to allow an arbitrary type expression in the head and require that the context mention only strict subexpressions of the head, the same proof still applies. I'm not sure how useful this is, but we might as well allow it. Second, I have half a result in the direction of allowing the context to mention types that arise from applying type constructors used in the instance head. This requires accepting regular derivations, which means the compiler would need to track all previous goals while deriving an instance, and handle a second occurance of a goal by producing a reference to the dictionary for the first occurance (which may not be constructed yet), rather than blindly continuing the derivation. First I will explain the proof method. It's related to structural induction, but not quite the same. Suppose we have a subexpression relation on type expressions such that every type expression has only a finite number of subexpressions. If instance contexts only mention subexpressions of the head, then searching for an instance for a type can only generate #of subexpressions*#of classes distinct goals. Therefore, in finite time either the derivation will fail, or we will product a regular derivaiton. Alternately, we only try to derivive an instance the first time it arises as a goal, so each time we apply an instance rule there is one less goal in the pool of possible goals, which must eventually be exhausted. The syntactic subexpression relation obviously has these properties, but it's often useful to refer to types that show up when we apply type constructors. For example, my case and a simplification of Ashley's: data Mu f = In (f (Mu f)) instance C (f (Mu f)) => C (Mu f) On the other hand, we can't unfold all type constructors because some types are irregular, or, we encounter an infinite number of types while expanding the type constructors. Define a kind indexed family of predicates on type constructors, R_K(T), where the property is true if T::K, T is regular (including expanding the insides of lambdas), and if K=K1->K2, then R_K2(T t) for all t such that R_K1(t). Say a type is regularity preserving if it satisfies the predicate corresponding to its kind. Any type expression build entirely from regularity preserving type constructors will be regular. I think that a subexpression relation that allows expanding applications regularity preserving type constructors will give any type a finite number of subexpressions, but I don't know enough about the structure of regularity preserving type constructors to prove it. The missing half here is an algorithm for testing whether a type constructor is regularity preserving. For this the body of the type constructor can be simplified to consist of just the type constructor applications in the body. Apply the type constructor to skolem arguments, and check whether the resulting tree is regular. I don't know how to do this. Another approach is to draw out a dependency graph between type constructors, with an edge from A to B for each use of B in the definition of A, labeled with the arguments used. Then the question is whether starting from out type applied to tyvars we can find some path through the graph that generates an infinite number of types, where we keep track of the current node and the current arguments, and modify the arguments as directed by a label when moving along an edge. I don't know if the search can even a tail repeating path that witnesses the irregularity, let alone a family of paths that can be tested. Any assistance here would be appreciated. Thanks Brandon