Type inference

[Thomas Charles CONWAY]

Hi

The following program stresses type-inference. It is inspired by
an equivalent functional program given to me by harald. If you change
the call to cc in t to a call to dd, and uncomment the equation for
dd, type inference takes ages (I haven't observed it to terminate,
but then I only waited a few minutes).

Enjoy,
Thomas
-- 
ZZ:wq!
^X^C
Thomas Conway               				      conway at cs.mu.oz.au
AD DEUM ET VINUM	  			      Every sword has two edges.

:- module t.

:- pred t is det.

:- implementation.

:- type unit ---> void.

t :-
	_X = apply(cc, void).
%		   ^^ change this to dd

p(X, Y, Z) = Z(X, Y).

aa(X) = p(X, X).

bb(X) = Z(X) :- Z = aa.aa.

cc(X) = Z(X) :- Z = bb.bb.

% uncomment the following line.
% dd(X) = Z(X) :- Z = cc.cc.

:- func (func(T1) = T2).(func(T2) = T3) = (func(T1) = T3).

X.Y = Z :-
	Z = (func(A) = B :- B = apply(Y, apply(X, A))).