[mercury-users] Typeclass problem (bug, misunderstanding, oth er?)

[Ralph Becket]

> From: Fergus Henderson [mailto:fjh at cs.mu.OZ.AU]
> 
> > Ahh.  This looks like a hole in type inference to me, now.
> > From the typeclass definition and the typeclass constraint
> > on solve/5 it can be deduced that PoppedNodes must have
> > the same type as DummyNode:
> 
> No, it can't.
> 
> > :- typeclass csp(T, N) <= node(N) where [
> > 	...
> > 	pred pop_stack(list(N), T, T),
> > 	...
> > ].
> > 
> > :- pred solve(conflict_fn, bool, N, T, T) <= csp(T, N).
> >
> > So, N is related to T, the pop_stack/3 method returns a
> > list of N, and we know that N is a polymorphically typed
> > argument.
> 
> You're assuming here that the csp(T, N) instance
> in the call to `solve' must be the same as that
> in the call to `pop_stack'.  But there is no such
> requirement.

Now I am totally confused.  If I write

:- typeclass csp(T, N) where [ pred pop_stack(list(N), T, T), ... ].

is it not the case that
(1) T and N are *type* variables and that 
(2) given an instance csp(A, B) with X0:A, X:A (using : as a typing
operator), declared as a typeclass constraint on a pred, then
(3) a method call pop_stack(Ys, X0, X) in the body of the pred 
implies that Ys:list(B).  

The deduction Ys:list(B) relies purely on the typeclass definition,
the typeclass constraint on the pred, the type of X0 and X, and the
signature of the method call.

If we take a trivial example:

:- pred eg(N, T, T) <= csp(T, N).
:- mode eg(unused, in, out) is det.

eg(DummyN, T0, T) :-
	pop_stack(Ns, T0, T1),
	push_agenda(Ns, T1, T).

I just can't get my head around why the N in DummyN:N could be
different from the N in Ns:list(N).  T0, T1, and T all have the
same type.

Is anybody else finding this hard going?

Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------