[m-dev.] Re: array inst bug

[Julien Fischer]

I've cc'd this to the developers list as it's likely to be of interest
there as well.

On Fri, 9 Feb 2007, Simon Taylor wrote:

> The module below demonstrates problems with the insts defined in the
> array module.
>
> The `array' constructor in the insts of arrays is made up.  The mode
> checker doesn't refer back to the types when working out the determinism
> of the unifications in `test' and `test2' (to do so would be expensive
> even for code which doesn't perform this kind of inst trick), and decides
> that they must be `det' and `failure' based on the insts, which is wrong
> because the outcome of the unifications depends on the array sizes as well.
>
> The compiler then goes on to generate a unification procedure for an
> abstract imported type for which it can't generate code.
>
> These insts should be disallowed.  IMHO all bound insts should be
> required to be type annotated if a unique type is not obvious from
> the set of constructors specified in the inst, and an error reported
> if a constructor doesn't exist in the type.

I agree.  (We actually already emit warnings for contructors in insts that
don't match a visible type constructor, --warn-insts-without-matching-type;
but that is disabled for the array module.)

> I suspect that exported
> bound insts referring to constructors of abstract exported types
> can cause similar problems.

Probably, but there's not a lot we can do about that since we
don't currently support abstract insts.  (Actually, in that situation
we should just make sure that the the definitions of the abstract
exported types end up in the "implementation" section of the interface
files.)

> The short term fix is to change the bogus array insts to just be
> `ground', which I will do.
>
> Simon.
>
>
> array_test.m:009: In `test'(in($typed_inst((array.array((bool.bool))),
> array_test.m:009:   array.uniq_array(bound(yes)))),
> array_test.m:009:   in($typed_inst((array.array((bool.bool))),
> array_test.m:009:   array.uniq_array(bound(yes))))):
> array_test.m:009:   warning: determinism declaration could be tighter.
> array_test.m:009:   Declared `semidet', inferred `det'.
> array_test.m:012: In `test2'(in($typed_inst((array.array((bool.bool))),
> array_test.m:012:   array.uniq_array(bound(no)))),
> array_test.m:012:   in($typed_inst((array.array((bool.bool))),
> array_test.m:012:   array.uniq_array(bound(yes))))):
> array_test.m:012:   warning: determinism declaration could be tighter.
> array_test.m:012:   Declared `semidet', inferred `failure'.
> array_test.o:array_test.c:(.text+0x229): undefined reference to `<unification predicate for type 'array_test:array.array'/1 mode 1>'
>
>
> :- module array_test.
>
> :- interface.
>
> :- import_module array, bool, io.
>
> :- pred main(io::di, io::uo) is det.
>
> :- pred test(array(bool)::in(uniq_array(bound(yes))),
> 		array(bool)::in(uniq_array(bound(yes)))) is semidet.
>
> :- pred test2(array(bool)::in(uniq_array(bound(no))),
> 		array(bool)::in(uniq_array(bound(yes)))) is semidet.
>
> :- implementation.
>
> main(!IO) :-
> 	io.write_string("succeeded\n", !IO).
>
> test(X, X).
>
> test2(X, X).
>
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------