[m-dev.] Partial Instantiated structures (free -> free)

[Fergus Henderson]

Mark Wielaard, you wrote:
> :- interface.
> 
> :- pred destroy_success(int::free->free) is det.
> :- pred destroy_failure(int::free->free) is failure.
> 
> :- pred fail_it is failure. % Is just fail, but to fool the compiler.
> 
> :- implementation.
> 
> destroy_success(1).
> destroy_failure(1) :- fail_it.
> 
> fail_it :- fail.
> 
> So what is the difference between these two predicates?
> destroy_success isn't accepted by the compiler:
> destroy.m:018:   mode error: argument 1 became too instantiated.
> But destroy_failure is!

The final inst of the head variable is `ground' in destroy_success,
but it is `not_reached' in destroy_failure.

> The final hlds gives:
> 
> destroy:destroy_failure(HeadVar__1) :-
>         HeadVar__1 = 1,
>         fail_it.
> 
> (OK, OK, you have to give it a -O -1 to disable all optimizations, because
> otherwise it optimizes the assignment away. BTW it would be nice to know
> what kind of unification the = represents, I am pretty sure this is an
> assignment unification, but how can I be sure while looking at the hlds?)

If you use -D (--verbose-dump-hlds), then it prints out ":=" for
constructions and assignments, "=>" for deconstructions that cannot
fail, "?=" for deconstructions that can fail, "==" for simple tests,
and the mode and can_fail/cannot_fail for complicated unifications.
(You can read the code in compiler/hlds_out.m.)

> (Can you really say "the benefits would outweigh the gains"?)

No, I meant "... outweigh the drawbacks".

> You are right, I described how I would like the mode system to be, not
> what the mode system currently does. But I hope you are convinced by the
> above examples that there is something strange with the current definition
> of well-modedness

No, the current definition is not strange, IMHO.
However, your alternative suggestion might be more _useful_.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.