Comment by tom_mellior

Prolog variables are metavariables, if you use them as such.

    ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ).
    Typ = [_G947, _G948]^ ((_G947->_G948)->_G947->_G948) .

    ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ), apply_type(Typ, a, Ta), apply_type(Ta, b, Tab), apply_type(Typ, c, Tc), apply_type(Tc, d, Tcd).
    Typ = [_G1179, _G1180]^ ((_G1179->_G1180)->_G1179->_G1180),
    Ta = [_G1213]^ ((a->_G1213)->a->_G1213),
    Tab = ((a->b)->a->b),
    Tc = [_G1251]^ ((c->_G1251)->c->_G1251),
    Tcd = ((c->d)->c->d) .

Note how both Tab and Tcd arise from instantiating the same schema Typ, which is unchanged.

To avoid binding variables in the schema, you just make sure to only instantiate instances (copies) of the schema:

    abstract_type(Term, Typ) :-
        type(Term, [], T),      % type/3 defined by parent
        term_variables(T, Vars),
        Typ = Vars^T.

    apply_type(Typ, Arg, Result) :-
        copy_term(Typ, TypCopy),  
        TypCopy = Vars^T,
        Vars = [Arg | RemainingVars],
        (   RemainingVars = []
        ->  Result = T
        ;   Result = RemainingVars^T ).