[m-rev.] for discussion: subtypes documentation

[Fergus Henderson]

On 25-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> The mode system uses covariant subtyping for the
> final insts and contravariant subtyping for the initial insts.
> Using covariant subtyping for the initial insts would be unsafe.
> 
> Hmm, looking at the source, I see that although we use contravariant
> subtyping for inst_matches_final, like we should, currently we are
> using covariant subtyping for inst_matches_initial.  Ouch -- that looks
> like a bug... 
> 
> Yep, it sure is.  I just got it to seg fault when running an example
> program.  (See attached.)

Actually, looking more closely at the source, I see that in fact
inst_matches_initial uses *invariant* subtyping for the initial
insts of higher-order insts.  pred_inst_matches_initial
first checks that the initial insts match covariantly,
by calling pred_inst_argmodes_match_initial
and then (this is the point I didn't notice originally)
it also calls pred_inst_argmodes_matches, which checks that
they also match contravariantly.  By checking that they
match in both directions, it is enforcing "invariant" subtyping --
in other words, no subtyping at all (the subtype information in the two
insts must match exactly).

This is safe, but overly conservative.

David, was this deliberate?  What's the rationale for doing the covariant
inst_matches_initial check in pred_inst_argmodes_match_initial?

P.S.
The bug which caused a seg fault in the example attached to my previous
post is just another instance of problems caused by a known problem in
mode analysis:

                % XXX enabling the check for bound_inst_list_is_complete
                % for type makes the mode checker too conservative in
                % the absence of alias tracking, so we currently always
                % succeed, even if this check fails.

Using complete insts, e.g. using mode in(list_skel(ground)) instead of in,
avoids this bug; if those are used, the compiler correctly rejects the
program with a mode error.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------