[m-rev.] for review: Parse and check subtype definitions.

[Peter Wang]

On Tue, 16 Feb 2021 16:41:00 +1100 Julien Fischer <jfischer at opturion.com> wrote:
> 
> >>> doc/reference_manual.texi:
> >>>    Add documentation for subtypes.
> >>>
> >>>    Add documentation for a proposed `coerce' operation, commented out
> >>>    for now.
> >>>
> >>>    Add "=<" to the list of reserved type names.
> >>
> >> If you are intending to commit this to the trunk then all of the new
> >> doucumentation should be commited out for now with the exception of of
> >> "=<" being a reserved type name.
> >
> > Subtype definitions do work as described. What if I just write at the
> > top of the section:
> >
> >    (This is a new and experimental feature, subject to change.)
> 
> That's fine.
> 
> I had a look through the code and couldn't see anything obviously amiss.
> (You may want to wait a bit before committing in case anyone else has
> any feedback.)

An update on this.

I found a problem with the design. Well, it's the usual variance problem
with subtyping and higher order types, and with mutability :P

Consider mutables:

    :- type foo(T)
	--->	wrap(io_mutvar(T)).
    :- type bar(T) =< foo(T)
	--->	wrap(io_mutvar(T)).

Then we can write:

    new_mutvar(orange : citrus, Var0, !IO),
    Bar = wrap(Var0) : bar(citrus),
    Foo = coerce(Bar),
    Foo = wrap(Var) : foo(fruit)

Now Var and Var0 refer to the same mutvar with two different types,
io_mutvar(fruit) and io_mutvar(citrus), which is clearly unsound.

The coerce expression is type-correct by the rule that I wrote
previously, since after replacing subtypes with base types we have
foo(fruit) == foo(fruit). Normally we would rely on the insts to
reject unsafe coercions, but it doesn't work for mutables.

In a similar way, you could coerce a pred(citrus::in) to
pred(fruit::in), which is also unsound.

Subtypes are actually not needed at all. You could coerce a term from
foo(citrus) to foo(fruit) with the same result. Therefore, I'm thinking
that the solution is to introduce stronger typing rules for coerce
expressions rather than additional restrictions on subtype definitions.

Peter