On Thu, Jul 21, 2011 at 9:58 AM, Thomas
So my understanding is this: In my example both 'a' and 'b' were of the same typeclass. In fact they were of the same type, too, since in the example the class had only one instance. However, the compiler/type checker could not prove this to be true.
Actually they had different types and the compiler could see it :). Let's see that if again: if n < 0 then k else BeginCont k (n - 1) Let's say that 'k' has type X. What is the type of 'BeginCont k (n - 1)'? Well, we have data BeginCont a = BeginCont a Int so given that the first parameter of the 'BeginCont' is 'k', which has type 'X', then 'BeginCont k (n-1)' has type 'BeginCont X'. So this is what we have: if n < 0 then (k :: X) else (BeginCont k (n-1) :: BeginCont X) What is the type of the whole 'if'? It must be the unification of 'X' and 'BeginCont X'. But we can't unify these types. It doesn't really matter that both 'X' and 'BeginCont X' are instances of some typeclass MyTC, and that the function that will take the result of the 'if' just needs the typeclass and nothing else. We can't typecheck the 'if'.
But if this was the case then I should be able to convince the compiler via type annotations like if p then (a :: (MyTC a) => a) else (b :: (MyTC a) => a) which does not work ('Inferred type is less polymorphic then expected.')
It is less polymorphic because 'k' has a rigid, defined type. Its type was chosen by the one who called the function. He gave you some 'k' that satisfy the class constraint, but you don't know which one. HTH, =) -- Felipe.