Folks, I have recently been referred to a paper by Duggan and Ophel, about "Type-checking Multi-parameter type classes" [1]. I think it will be useful to consider the following. ---------------------------------------------------------------------- 1. "Domain-driven unifying overload resolution" (DDUOR, so-called in definition 4.1 in [1]) should not fail to terminate; i.e. satisfiability is not undecidable (see system CT [2]). DDUOR should consider the *set* of constraints (in C, in def. 4.1), instead of one after another, for finding unifying substitions (\theta'' in def. 4.1). For the example (page 17 of [1]): class F a b where f:: a -> b -> Int instance F Int Float where f x y = 0 instance F a b => F [a] [b] where f [x] [y] = f x y g x y = (f [x] y) + (f y [x]) the definition of g will be detected as erroneous (not well-typed) if the *set* of constraints is considered for finding the unifying substitution, instead of one constraint after another. In this way, DDUOR terminates. I think full details will not be needed, but this can be (easily) understood by reading/following the definition of sats in system CT. -------------------------------------------------------------------- 2. The usefulness of multi-parameter type classes has been hindered by the restrictiveness of the rule for detecting ambiguity. Instead of tv(P) \subseteq tv(t), where P is the set of constraints and t is the simple type, the rule for nonambiguity should be P = P |* tv (t,G) where |* denotes "constraint projection" and G the typing context. For the definition of |* see [3]; the idea is to include constraints that have type variables in t and G and constraints that have type variables previously included. In the example: For: P = F a b and t = a We have that: P => t is not ambiguous Since: P |* {a} = P This rule would allow multi-parameter type classes to be used in (well-known) compelling examples, without giving rise to ambiguities. Carlos [1] Type-checking multi-parameter type classes, Dominic Duggan and John Ophel, to appear in JFP. [2] Type Inference for Overloading, Carlos Camarão and Lucília Figueiredo, Technical report UFMG, available at http://www.dcc.ufmg.br/~camarao/jfp-ct.ps.gz. [3] Overloading and Coherence, Carlos Camarão and Lucília Figueiredo, Technical report UFMG, available at http://www.dcc.ufmg.br/~camarao/overloading-and-coherence.ps.gz .