class BuildList a r | r-> a where build' :: [a] -> a -> r
instance BuildList a [a] where build' l x = reverse$ x:l
instance BuildList a r => BuildList a (a->r) where build' l x y = build' (x:l) y
So they key here appears to be that the type-checker can distinguish between function application and other uses of an expression?
I'm sorry I'm late with the reply. Indeed, the trick is straightforward -- merely basic typechecking. Indeed, let us consider an expression build' [] 'a' 'b' ++ [] or, in a more abstract syntax (++) ((build' [] 'a') 'b') [] We make use of the familiar typing rule G |- e1: t1->t2 G |- e2: t1 <===> G |- (e1 e2) : t2 where G is the typing environment (which associates types with the variables that appear free in expressions e1 and e2). The typing rule can be applied in either direction. Operator (++) has the type [t1] -> [t1] -> [t1]. Given that fact and applying the typing rule twice, we infer that ((build' [] 'a') 'b') has the type [t1], [] has the type [t1], and so the whole expression has the type [t1]. We have inferred that ((build' [] 'a') 'b') :: [t1] Applying the rule in reverse direction, we find that (build' [] 'a'):: t3->[t1] 'b':: t3 Or, because 'b' has the type Char, t3 unifies with Char, which gives us (build' [] 'a') :: Char->[t1] Applying the typing rule several more times, we find []:: t4 'a' :: t5 build':: t4 -> t5 -> (Char->[t1]) or []::t4 build' :: t4 -> Char -> (Char->[t1])
From the declaration of the BuildList class, we know that build' :: [a] -> a -> r unifying the two signatures, we find build' :: [Char] -> Char -> (Char->[t1])
Of the two instances of BuildList, the second obviously matches. The functional dependency r->a essentially tells us that 'r' is the primary key in the instance selection. That is, if we use (Char->[t1]) to match with the second parameter of the instance and found the matching instance, we can be sure that it is the only matching instance -- no matter how many instances are added in the future or contained in other modules. So, we commit to the second instance and assign the type to build' in the original expression as build'_2 :: [Char] -> Char -> (Char->[t1]) However, the second instance of BuildList includes the term "build' (x:l) y", and we have to type in turn. We know that (x:l)::[Char] (build' (x:l) y)::[t1] from which we determine, with the same typing rule, build'::[Char] -> t6 -> [t1] or, unifying with the signature for build', build'::[Char] -> Char -> [t1] Again, we search for the appropriate instance of BuildList. Now, the first instance matches. Again, we can commit to it. Unifying 'a' with Char and [t1] with [a] gives us build'_1 :: [Char] -> Char -> [Char] and the type of the whole (++) expression as [Char]. Typechecking succeeds, and we were able to unambiguously choose instances. The details of the actual typechecking algorithm most likely differ, yet the general idea -- and the outcome -- are the same.