Eta-equivalence violation in curried argument to `solutions()`

[ulidtko]

This code compiles:

:- pred foo is semidet.
foo :-
    P = (pred(A::in, V::out) is nondet :- V = A + 1),
    solutions(
        (pred(Y::out) is nondet :- P(13, Y)),
        _)
    .

This (supposedly equivalent) modification does not:

:- pred foo is semidet.
foo :-
    P = (pred(A::in, V::out) is nondet :- V = A + 1),
    solutions(
        P(13),
        _)
    .

Error message:

$ mmc --grade hlc.gc.pregen -E hello.m
hello.m:017: In clause for predicate `foo'/0:
hello.m:017:   in argument 1 of call to predicate `solutions'/2:
hello.m:017:   in unification of argument
hello.m:017:   and term `P(V_9)':
hello.m:017:   type error in argument(s) of higher-order term (with arity 1).
hello.m:017:   Functor (P) has type `pred(int, int)',
hello.m:017:   expected type was `((func V_3) = V_4)'.

which is obscure and completely unhelpful. What does even a type ((func V_3) = V_4) mean?