As a termination test, how about no restrictions on context and head except: Each assertion in the context must satisfy * the variables of the assertion are a sub-multiset of those of the head (though they may be the same), and * the assertion has fewer type constructors and variables (taken together and counting repetitions) than the head. This ensures that under any ground substitution the context assertion has fewer type constructors than the head. It would accept all instances accepted by the current test, plus instance C a instance C (s a) => C (Sized s a) instance (C1 a, C2 b) => C a b instance C1 Int a => C2 Bool [a] instance C1 Int a => C2 [a] b instance C a a => C [a] [a] But not things like instance (C1 a, C2 a, C3 a) => C a because that would need to check other instances as well.