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

[Julien Fischer]

Hi,

On Mon, 21 Nov 2022, Volker Wysk wrote:

> Am Freitag, dem 18.11.2022 um 22:16 +1100 schrieb Mark Brown:
>> On Fri, Nov 18, 2022 at 4:42 AM Volker Wysk <post at volker-wysk.de> wrote:
>>>
>>> Am Mittwoch, dem 16.11.2022 um 14:27 +1100 schrieb Julien Fischer:
>>>
>>>>
>>>>> The following version of main fails to compile (like expected) with
>>>>> "Unification of `P1' and `P2' can fail". (Here we have the point of
>>>>> failure). Even though that isn't the case:
>>>>>
>>>>> main(!IO) :-
>>>>>    P1 = A - B,
>>>>>    p(P2, !IO),
>>>>>    P1 = P2.
>>>>>
>>>>> I suppose this due to what you described as "the fact that the current
>>>>> Mercury implementation does not support partial instantiation properly".
>>>>
>>>> In this case, the explanation is: the compiler has to generate an
>>>> out-of-line predicate to implement the unification of P1 and P2. That
>>>> generated predicate is declared to be semidet, which is why you are
>>>> getting the determinism error. The unification should to be det, since
>>>> filling in the holes in P1 with the args from P2 will aways succeed.
>>>> The fact that the compiler does not know that is one of the limitations
>>>> I was referring to.
>
> Does this out-of-line predicate fail to have the correct determinism
> category, because one of the terms to be unificated is partially
> instantiated?

The out-of-line predicate has a declared determinism of semidet; the
actual unification is (or should be) det in this case.

> Or what unifications are affected?

Ultimately, this is due to the current incomplete support for partial
instantiation. It looks like the part of the compiler that handles such
unifications will also need changes to properly support partial
instantiation.

>>> The question is, what does a mere user of the Mercury language need to know
>>> in order to understand this, and what does he need to know in order to work
>>> around it?
>>
>> That is a good question. The knowledge and reasoning I used was
>> roughly as follows (this is going to take longer to type than it took
>> to actually happen):
>>
>> 1. The error message points to a unification in the first argument to
>> p, but unifications aren't always explicit. I'll need to think about
>> what unifications the compiler sees.
>>
>> 2. The strict sequential semantics says, "Function calls, conjunctions
>> and disjunctions are all executed in depth-first left-to-right order."
>> I know that this determines what the compiler will see before mode
>> analysis, namely that the "function call" of -/2 will be before the
>> call to p.
>
> So that's the reason why a partially instantiated term is constructed before
> the call to p. My intuition was that the output of p would be deconstructed
> after the call, since it's an output argument.

Note that conversion to superhomogenous form, which is what introduces
the extra unifications, occurs *before* mode analysis (i.e. before the
part of the compiler that deals with "inputs" and "outputs").
The conversion to superhomogenous form does not concern itself with
inputs and outputs (or more properly, producer-consumer relationships
between variables). The idea is that any necessary reordering required
by those will be done as part of mode analysis.

...

>> 6. If I put the unification after the call to p, the mode analyser
>> won't need to reorder it to get it to the right place. Maybe that will
>> avoid the reordering bug?
>
> So the answer is: The mode analyser has issues with partially instantiated
> terms. Such terms will sometimes be implicitly constructed, according to the
> strict sequential semantics. Also, unifications can be implicitly
> constructed in the process. This may lead to non-obvious error messages.
> Making such constructions explicit and moving them around can be the
> solution to the observed error.

For the original version of this program, you might have also paid
attention to the warning that the variables A and B were unused and
either:

1. Done something with them.  (Which as we saw will cause the "obvious"
    reordering to occur.)

2. Deleted the call entirely, since it doesn't do anything ;-)

Julien.