[m-users.] Is this a compiler bug?

[Julien Fischer]

On Sat, 12 Nov 2022, Volker Wysk wrote:

> The following program fails to compile:
>
> :- module pairbug.
> :- interface.
> :- import_module io.
>
> :- pred main(io::di, io::uo) is det.
>
> :- implementation.
> :- import_module pair, string.
>
> :- pred p(pair(string, string)::out, io::di, io::uo) is det.
> p("foo" - "bar", !IO).
>
> main(!IO) :-
>    p(A - B, !IO).    % <- line 19
>
>
> The message is:
>
> pairbug.m:006: In `main'(di, uo):
> pairbug.m:006:   error: determinism declaration not satisfied.
> pairbug.m:006:   Declared `det', inferred `semidet'.
> pairbug.m:006:   The reason for the difference is the following.
> pairbug.m:019:   In argument 1 of call to predicate `pairbug.p'/3:
> pairbug.m:019:   unification with `V_9' can fail.
>
>
> But the following works:
>
> main(!IO) :-
>    p(P, !IO),
>    P = A - B.
>
>
> This must either be something stupid or a compiler bug...

It is a consequence of the following:

- how the clauses are translated into superhomogenous form;
- the fact that A and B are unused;
- the fact that the current Mercury implementation does not support
   partial instantiation properly.

(Superhomogenous form is the form by which clauses are represented
inside the compiler.)

Here's what the compiler sees for the first version immediately
before mode analysis:

    main(STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
       V_8 = A - B,
       p(V_9, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO),
       V_8 = V_9.

(The variables prefixed with 'V_' or 'STATE_VARIABLE_' are introduced
by the compiler.)

Here's what the compiler sees for the second version immediately
before mode analysis:

    main(STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
        p(P, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO),
        P = A - B.

The first version constructs a partially-instantiated term, e.g.
pair(<<free>>, <<free>>), puts the output of p/3 into V_9 and then
attempts to unify them (which I suspect is where it falls over).
Is that what you were intending?

You might ask: why doesn't mode analysis reorder the first version to
be like the second. The answer is: it doesn't have any reason to do
such reordering.

One of the other pieces of compiler you get from that program is:

    pairbug.m:014: In clause for predicate `main'/2:
    pairbug.m:014:   warning: variables `A, B' occur only once in this scope.

If I have a version of the program, that uses A or B, e.g.

     main(!IO) :-
       p(A - B, !IO),
       io.print(A, !IO).

then mode analysis will reorder things appropriately.

Julien.