[m-dev.] insts for existential data

[Mark Brown]

Hi all,

When specifying the inst for an existentially typed data constructor, are
we expected to add a `ground' argument for the automatically inserted
type_info?  I would have thought not, but leaving it out leads to mode
errors.

Unfortunately, adding it in also leads to problems because deconstruction
unifications are inferred to always fail.

The following test case illustrates the problem.

	:- module existential_data_inst_bug.
	:- interface.

		% This fails mode checking because the deconstruction
		% unification in the clause for get_s expects an extra
		% argument for the type_info.
		%
	:- type s ---> some [P] s(P).
	:- inst s ---> s(ground).
	:- some [P] pred get_s(s::in(s), P::out) is det.

		% If on the other hand we supply the extra argument, the
		% deconstruction unification is inferred to always fail
		% because the extra argument is not accounted for.
		%
	:- type t ---> some [P] t(P).
	:- inst t ---> t(ground, ground).
	:- some [P] pred get_t(t::in(t), P::out) is det.

	:- implementation.

	get_s(s(M), M).
	get_t(t(M), M).

The error messages look like this:

existential_data_inst_bug.m:021: In clause for
existential_data_inst_bug.m:021:   `get_s(in((existential_data_inst_bug.s)),
existential_data_inst_bug.m:021:   out)':
existential_data_inst_bug.m:021:   in argument 1 of clause head:
existential_data_inst_bug.m:021:   mode error in unification of `HeadVar__1'
existential_data_inst_bug.m:021:   and
existential_data_inst_bug.m:021:   `existential_data_inst_bug.s(TypeInfo_for_P,
existential_data_inst_bug.m:021:   M)'.
existential_data_inst_bug.m:021:   Variable `HeadVar__1' has instantiatedness
existential_data_inst_bug.m:021:   `bound(existential_data_inst_bug.s(ground))',
existential_data_inst_bug.m:021:   term
existential_data_inst_bug.m:021:   `existential_data_inst_bug.s(TypeInfo_for_P,
existential_data_inst_bug.m:021:   M)' has instantiatedness
existential_data_inst_bug.m:021:   `existential_data_inst_bug.s(
existential_data_inst_bug.m:021:     free,
existential_data_inst_bug.m:021:     free
existential_data_inst_bug.m:021:   )'.
existential_data_inst_bug.m:017: In
existential_data_inst_bug.m:017: `get_t'(in($typed_inst((existential_data_inst_bug.t),
existential_data_inst_bug.m:017:   (existential_data_inst_bug.t))), out):
existential_data_inst_bug.m:017:   error: determinism declaration not
existential_data_inst_bug.m:017:   satisfied.
existential_data_inst_bug.m:017:   Declared `det', inferred `failure'.

Cheers,
Mark.

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