[m-dev.] help with polymorphic modes

[Mark Brown]

Hi Peter,

On Tue, Sep 2, 2014 at 3:30 PM, Peter Wang <novalazy at gmail.com> wrote:
> On Tue, 2 Sep 2014 15:19:44 +1000, Peter Wang <novalazy at gmail.com> wrote:
>> Hi,
>>
>> Just to make sure, this is mode incorrect, yes?
>>
>>     :- pred p(pred(T), T).
>>     :- mode p(pred(in(I =< ground)) is det, in) is det.
>>
>>     p(P, X) :- P(X).
>
> That doesn't make sense.  Then what about this?

It doesn't make sense without outputs, but aside from that you are
right that it is mode incorrect. The constraint arising from `P(X)' is
that ground matches the inst variable I, which we can't prove because
all we know about I is that I =< ground.

Note that, since I comes from the head of the clause, it is already
bound, so we can't solve the constraint by binding I to ground.

>
>     :- type fruit --->  apple ; orange.
>     :- inst apple --->  apple.
>
>     :- pred apple_only(fruit).
>     :- mode apple_only(in(I =< apple)) is det.
>
>     apple_only(_).
>
>     test :- p(apple_only, orange).

In this case, assuming the above declaration for p, the constraints we
need to solve are

    I1 =< apple
    I2 =< ground
    I2 matches I1

This time the inst variables come from the body, so they are free (and
renamed apart), and we can solve the constraints with I1 = I2 = apple.
Hence the error should be detected in p and not in test.

If the declaration of p instead was:

    :- mode p(pred(in(I)) is det, in(I)) is det.

then we only need to prove that I matches I, which is trivially true,
so p would be mode correct. On the other hand, the constraints for
test would be

    I1 =< apple
    I2 =< ground
    I2 matches I1
    orange matches I2

and these are unsatisfiable so the error should be detected here.

Cheers,
Mark.