[Haskell-beginners] Typeclasses vs. Data

[Felipe Almeida Lessa]

On Thu, Jul 21, 2011 at 9:58 AM, Thomas <haskell at phirho.com> wrote:
> 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.