[mercury-users] typeclass error

[Mark Brown]

On 18-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> Hello,
> 
> What's wrong with the following program?
> 
> :- module tc.
> 
> :- interface.
> 
> :- import_module io.
> 
> :- pred main(io::di, io::uo) is det.
> 
> :- implementation.
> 
> :- import_module list, int.
> 
> main(!IO) :-
>         nl(!IO).
> 
> :- typeclass tc1(A, C) where [
>         func a_to_c(A) = C
> ].
> 
> :- typeclass tc2(B, C) where [
>         func b_to_c(B) = C
> ].
> 
> :- func f(A, B) = C <= (tc1(A, C), tc2(B, C)).
> 
> f(A, B) =
>         ( if a_to_c(A) = b_to_c(B) then
>                 a_to_c(A)
>         else
>                 b_to_c(B)
>         ).

First, here's the clause with some explicit type annotations:

	f(A, B):C0 =
		( if a_to_c(A):C1 = b_to_c(B):C2 then
			a_to_c(A):C3
		else
			b_to_c(A):C4
		):C5.

Because of the result unification, we know that C0 = C5.  Because of the
semantics of if-then-else expressions, we know that C3 = C5 and C4 = C5.
Because of the unification in the condition, we know that C1 = C2.  So at
this stage there are two equivalence classes: {C0,C3,C4,C5} and {C1,C2}.
There is nothing in the clause which implies that these two equivalence
classes are the same.

The first equivalence class is the type of the function result, so it is
bound to the universally quantified C from the func declaration.  Hence
the method calls in the "then" and "else" branches will call methods in
those dictionaries that are passed in as hidden arguments to f (that is,
the dictionaries that correspond to the two constraints on the func
declaration).

The second equivalence class remains unbound.  Hence there are no assumed
constraints (e.g., constraints on the func declaration) that can satisfy
the constraints on the method calls in the condition; this explains the
first part of the error message.  The warning you get is because unbound
type variables are generally never what the programmer intends.

> 
> I get the following error when I try to compile it:
> 
> tc.m:024: In function `tc.f/2':
> tc.m:024:   type error: unsatisfied typeclass constraints:
> tc.m:024:       `tc.tc1(A, C)'
> tc.m:024:       `tc.tc2(B, C)'
> tc.m:024: In function `tc.f/2':
> tc.m:024:   warning: unresolved polymorphism.
> tc.m:024:   The variable with an unbound type was:
> tc.m:024:       V_6: C
> tc.m:024:   The unbound type variable(s) will be implicitly
> tc.m:024:   bound to the builtin type `void'.

The error message would be better if the location of the place where the
constraint arose in the clause was reported, rather than the location of
the func declaration.  But the compiler doesn't currently keep enough
information to be able to do that, unfortunately.

Here are two ways that you can get the code to compile:

a) Rewrite the clause so that there are unifications that imply that C1 and
C2 are the same as C.  For example:

	f(A, B) = C :-
		C0 = a_to_c(A),
		( if C0 = b_to_c(B) then
			C = C0
		else
			C = b_to_c(B)
		).

b) Add functional dependencies so that the compiler can "improve" the types
C1 and C2 to be equal to C.  For example:

	:- typeclass tc1(A, C) <= (A -> C) where [ ... ].

or

	:- typeclass tc2(B, C) <= (B -> C) where [ ... ].

or both.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------