[m-users.] Inst problem

[Julien Fischer]

Hi,

On Sat, 1 Nov 2025 at 21:45, Volker Wysk <post at volker-wysk.de> wrote:
>
>
> ------------
> :- type iosupp.res(T)
>     ---> ok(T)
>     ;    error(iosupp.error).
>
> :- inst iosupp.res(I)
>     ---> ok(I)
>     ;    error(ground).
>
> :- type path ---> path(
>     abs :: bool,
>     comps :: list(string)
> ).
>
> :- inst abs_path == bound(path(bound(yes), ground)).
>
> :- pred absolute_path_p(path, iosupp.res(path),   io, io).
> :- mode absolute_path_p(in,   out(res(abs_path)), di, uo) is det.
>
> :- pred current_directory_p(
>     iosupp.res(path)::out(iosupp.res(abs_path)),
>     io::di, io::uo
> ) is det.
>
> absolute_path_p(Path, Res, !IO) :-
>     (
>         if   Path ^ abs = yes
>         then Res = iosupp.ok(Path)
>         else dirsupp.current_directory_p(Res1, !IO),
>              (
>                  Res1 = ok(Cwd),
>                  Res  = ok(path(yes, Cwd ^ comps ++ Path ^ comps))
>              ;
>                  Res1 = iosupp.error(Err),
>                  Res  = iosupp.error(Err)
>              )
>     ).
> ------------
>
>
> And I get this error message from the compiler:
>
> iosupp.m:1065: In clause for `absolute_path_p(in,
> out(iosupp.res(iosupp.abs_path)), di, uo)':
> iosupp.m:1065:   mode error: argument 2 had the wrong instantiatedness.
> iosupp.m:1065:   Final instantiatedness of `Res' was
> iosupp.m:1065:     unique(
> iosupp.m:1065:       error(ground)
> iosupp.m:1065:     ;
> iosupp.m:1065:       ok(
> iosupp.m:1065:         bound(
> iosupp.m:1065:           path(ground, ground)
> iosupp.m:1065:         )
> iosupp.m:1065:       )
> iosupp.m:1065:     ),
> iosupp.m:1065:   expected final instantiatedness was
> iosupp.m:1065:     named inst res(abs_path)
> iosupp.m:1065:     which expands to
> iosupp.m:1065:       bound(
> iosupp.m:1065:         error(ground)
> iosupp.m:1065:       ;
> iosupp.m:1065:         ok(
> iosupp.m:1065:           named inst abs_path
> iosupp.m:1065:           which expands to
> iosupp.m:1065:             bound(
> iosupp.m:1065:               path(
> iosupp.m:1065:                 bound(
> iosupp.m:1065:                   yes
> iosupp.m:1065:                 ),
> iosupp.m:1065:                 ground
> iosupp.m:1065:               )
> iosupp.m:1065:             )
> iosupp.m:1065:         )
> iosupp.m:1065:       ).
>
>
> I think I understand the final instantiatedness of `Res', and that it
> doesn't match the mode line for absolute_path_p. But how *should* it be
> done?

Correct, the final instaniatiedness of 'Res' is set along three goal
paths and when
these are combined they do *not* match the *declared* final instiantedness of
absolute_path_p,

Firstly don't read too much into the context attached to that error
message (iosupp.m:1065),
that looks to be the final unification for 'Res' in source code order,
but actually the message
applies to the entire predicate body.  Also, the 'unique' bit is
probably not so helpful in thie
case.

Second thing to note, if we remove all of the inst subtyping from this
predicate (and also
delete the dirsupp module qualifier -- since we don't have that module
-- and compile with
--allow-stubs), then the predicate compiles without complaint.

So the problem is that along one of the goal paths that sets the final
inst of 'Res',
the mode analyser cannot prove that the final inst is
bound(error(ground) ; ok(bound(path(bound(yes), ground))).

The error message gives us a clue here, because it says that the
inferred inst is:

   unique(error(ground) ; bound(ok(bound(path(ground, ground))))

Note that the last bit, path(ground, ground) does not match
path(bound(yes), ground),
which suggests that problem lies in the following bit of code:

   ( if
        Path ^ abs = yes
    then
        Res = iosupp.ok(Path)
    else ...

According to the mode declaration the variable 'Path' had mode 'in'
(i.e. ground >> ground).
The mode analyser will not propagate the results of the test of the
return value of the field
access function into the inst 'Res', so in the 'then' branch, it does
*not* know that the first
argument of 'Path' is 'yes'.  Given the declared mode, the compiler is
required to be able
to prove that that is the case.

Can it be done?  Yes, for example,

 (
        if Path ^ abs = yes
        then Res = iosupp.ok(path(yes, Path ^ comps))
        else ....

As with many uses of inst-subtying of this kind, the question has to
be asked: what benefit
do you expect this to have?  (At least so far as users of your module
are concerned, it has
the downside of making mode errors more complicated.)

Julien.