returnM (tyVarsOfTypes tys)
zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
+zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
\end{code}
(first_ty : _) = tys
head_shape_msg = parens (text "The instance type must be of form (T a1 ... an)" $$
- text "where T is not a synonym, and a1 ... an are distinct type variables")
+ text "where T is not a synonym, and a1 ... an are distinct type *variables*")
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
undecidableMsg])
\end{code}
-Termination test: each assertion in the context satisfies
+Termination test: the so-called "Paterson conditions" (see Section 5 of
+"Understanding functionsl dependencies via Constraint Handling Rules,
+JFP Jan 2007).
+
+We check that each assertion in the context satisfies:
(1) no variable has more occurrences in the assertion than in the head, and
(2) the assertion has fewer constructors and variables (taken together
and counting repetitions) than the head.