where
(first_ty : _) = tys
- head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
- text "where T is not a synonym, and a,b,c are distinct type variables")
+ 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*")
-- 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.