[m-dev.] not_reached inst

[Simon Taylor]

I wrote:
> For example, inst_util.abstractly_unify_inst gives the unification
> of a not_reached inst with anything a determinism of `det', where it should
> probably be `failure'.

Actually, it can't be `failure' because that would break the axiom 
"all [X] X = X".  It has to be `erroneous', and the compiler would need to
replace the unification with a goal that throws an exception (or calls
MR_fatal_error) and prune away the rest of the conjunction to avoid
compiler aborts later.  Terms with inst `not_reached' are a bit like quiet
NaNs (see the comment in float.m), except that there is no way to create
them.

> A hack that might give you what you want without any change is to use a
> constructor in the bound inst that isn't valid for the type (e.g. bound([])
> for this example).  That should be illegal but currently the compiler doesn't
> check.

And that won't work because unification of two terms with that inst will
be found to be det.

Simon.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------