subst(TV,T) :- equals(TV, T), not occurs(TV, T), not typeVar(T), typeVar(TV). equals(A, pointer(TP, subst(TV, T))) :- equals(A, TP), subst(TV, T), not typeVar(TP), occurs(TV, TP). type(pointer(TP, subst(TV, T)), Name, Num) :- type(TP, Name, Num), subst(TV, T), occurs(TV, TP). param(pointer(TP, subst(TV, T)), Param, PNum) :- type(pointer(TP, subst(TV, T)), Name, Num), subst(TV, T), param(TP, Param, PNum), not occurs(TV, Param). param(pointer(TP, subst(TV, T)), pointer(Param, subst(TV, T)), PNum) :- type(pointer(TP, subst(TV, T)), Name, Num), subst(TV, T), param(TP, Param, PNum), occurs(TV, Param).