[m-dev.] existential types

[Thomas Conway]

Hi

I have a type which is for extendable terms:

:- type term
    --->	var(var)
    ;		int(int)
    ;		term(string, list(term))
    ; some [T]	(ext(T) => unifiable(T))
    .

:- typeclass unifiable(T) where [
    (pred unify(T, T, map(var, term), map(var, term)),
    (mode unify(in, in, in, out) is semidet)
].

In my unifyTerms pred I'd like to write:

unifyTerms(LHS, RHS, Bind0, Bind) :-
    LHS = ext(LData),
    (
    	RHS = ext(RData),
	unify(LData, RData, Bind0, Bind)
    ;
    	RHS = var(_),
	unifyTerms(RHS, LHS, Bind0, Bind)
    ).

But this gives the following error message:
script.m:236: In clause for predicate `script:unifyTerms/4':
script.m:236:   in argument 2 of call to predicate `unify/4':
script.m:236:   type error: variable `RData' has type `T',
script.m:236:   expected type was `T'.

Which apart from the fact that it calls both extistentially
quantified variables the same name, is more or less what I
expected, though of course not what I wanted. What I wanted
was for the implied type unification to happen, and if it
succeeds then to call the unify method on the two data items.
If I was using univs this would work, except that I couldn't
then constrain the value to be 'unifiable/1'.

So, how do I get the behaviour I want?

-- 
 Thomas Conway              Unicode for terrorists: U+0001 300C
 <conway at cs.mu.oz.au>         "Tie his hands behind his back"
 Mercurian )O+  
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------