[junke]

Thanks!

Just to expand on my previous example, I can simply modify how bindings are looked up and generalize the associated type when it is not unknown:

    type(V,Env,T) :-
        ground(V),
        member(V:P,Env),
        generalize(P,T).

    generalize(P,T) :- nonvar(P), !, copy_term(P,T).
    generalize(T,T).

Let's add two rules for tuples and addition, and change the syntax of let for clarity:

    type((A,B),Env,TA * TB) :-
        type(A,Env,TA),
        type(B,Env,TB).

    type(A+B,Env,number) :-
        type(A,Env,number),
        type(B,Env,number).

    type(let(X == XE, E),Env,ET) :-
        type(XE,Env,XT),
        type(E,[X:XT|Env],ET).

Then, typing this:

    let(identity == lambda(v,v),
        let(increment == lambda(x,x+1),
            let(compose ==
                lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),
                (apply(apply(compose,identity),identity),
                 apply(apply(compose,increment),increment)))))

... gives:

    (_1775 -> _1775) * (number -> number)

You could also make use of meta attributes, ie. data stored inside variables, to control what happens during unification.