[m-users.] Inst problem

[Volker Wysk]

Am Sonntag, dem 02.11.2025 um 14:15 +1100 schrieb 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.

Yes, the message can be misleading. I'd like to suggest two small
improvements:

1. Change the reported line number to that of the head of the clause. This
would suggest that it's an issue with the predicate (clause) as a whole,
which it is.

2. Add a few words to the error message. "Final instantiatedness of `Res'
was..." could be changed to "The final instantiatedness of `Res' in the
clause body was...".

> 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.

Why won't the mode analyser propagate the results of the "Path ^ abs = yes"
part?

And, take a look at the following, cleaner definition of absolute_path_p:

absolute_path_p(Path, Res, !IO) :-
    (
        Path = path(yes, _),
        Res = iosupp.ok(Path)
    ;
        Path = path(no, _),
        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)
        )
    ).

This still fails to compile. It seems like the instantiatedness information
of "Path" in the construction "Res = iosupp.ok(Path)" is lost, when building
"Res". 

> 
> 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.)

I wanted to catch bugs by introducing that abs_path inst. I've tried it like
you described (actually, I had the same idea before I read your reply). But
it didn't work out. The standard libraries don't provide proper modes for
inst subtyping. It's all "in" or "out" (and "di" and "uo"), when it should,
theoretically, be "in(I)" and "out(J)", in order to allow for extra inst
information in the arguments.

Cheers,
Volker