+ do { cois <- unifyTheta theta1 theta
+ ; -- Check whether all coercions are identity coercions
+ -- That can happen if we have, say
+ -- f :: C [a] => ...
+ -- g :: C (F a) => ...
+ -- where F is a type function and (F a ~ [a])
+ -- Then unification might succeed with a coercion. But it's much
+ -- much simpler to require that such signatures have identical contexts
+ checkTc (all isIdentityCoercion cois)
+ (ptext SLIT("Mutually dependent functions have syntactically distinct contexts"))
+ }