[m-dev.] handling of impossible insts

[Andrew Bromage]

G'day.

Fergus Henderson wrote:

> I seem to remember that Andrew and/or Tom had made a change to
> mode analysis so that it checked for bound(...) insts with an
> empty list of possible insts, and set the whole instmap to unreachable
> for those cases.  Apparently this has not yet been committed.
> Do you still have the patch?

I have my version of the patch which I've just updated to include the
split of inst_match and is bootchecking as I'm writing this.

While waiting for that bootcheck, one question which I'll throw open.
Consider this program (this is the test case for the patch):

<<
:- module empty_bound_inst_list.

:- interface.

:- pred p is failure.

:- implementation.
:- import_module std_util.

:- type some_functors ---> foo ; bar ; baz.

p :-
	( Y = yes(bar), Z = foo
	; Y = yes(baz), Z = foo
	),
	Y = yes(Z).
>>

Without the empty bound_inst list patch, p is classified as being
semidet.  The bound_inst list patch correctly identifies the final
unification as having determinism failure.

However should p/0 be given determinism failure (with the unification
being replaced with fail by the mode checker in a manner analogous
to what we currently do with det simple_tests), or should the compiler
report a mode error?

The current compiler with the patch applied gives a mode error:

<<
empty_bound_inst_list.m:015: In clause for `p':
empty_bound_inst_list.m:015:   mode error in unification of `Y' and `std_util:yes(Z)'.
empty_bound_inst_list.m:015:   Variable `Y' has instantiatedness `unique(std_util:yes(unique(empty_bound_inst_list:bar ; empty_bound_inst_list:baz)))',
empty_bound_inst_list.m:015:   term `std_util:yes(Z)'
empty_bound_inst_list.m:015:   has instantiatedness `std_util:yes(unique(empty_bound_inst_list:foo))'.
>>

Cheers,
Andrew Bromage