[m-dev.] compiler abort: coercing abstract type

[Zoltan Somogyi]

On Wed, 5 Nov 2025 14:11:06 +1100, Julien Fischer <jfischer at opturion.com> wrote:
> > > > In this case, the shared type_ctor is a du type behind the abstraction barrier,
> > > > but I do not see any reason why the second way would not work even if
> > > > it is an equivalence type or even a foreign or solver type.
> >
> > No, it would introduce unsoundness into the system, by bypassing the
> > type parameter invariance restriction.
> >
> > For example, assume this type is abstract exported:
> >
> >     :- type abs(T)
> >         --->    abs((func) = T).
> >
> > If you could coerce a value of this type from abs(fruit) to abs(citrus),
> > you could call the function expecting it to return a 'citrus',
> > but it actually returns a 'fruit'.
> 
> We obviously don't want make the type system unsound, however the situation
> with abstract types and coerceability is undesirable, in that it
> limits what can be
> done with subtypes quite a bit.
> 
> Presumably, it is possible to identify abstract types where coercions
> of the type
> proposed by Zoltan are safe (in the sense that the type parameter invariance
> restriction cannot be violated) and write that information to one of
> the interface
> files?  Importing modules could then look to see if a coercion is safe or not.

I already thought about that when I read Peter's email. I am afraid
that the answer to that question is "no".

The reason is that the higher-order value may be contained inside
not just one function symbol in one type, but inside many function
symbols in many types, and these types may be defined in different
modules. Basically, our system of interface files does not allow you
to look inside an unbounded number of types. And modifying the system
make such a look possible would be way overkill.

> Are there examples of types that might violate the restriction, other than those
> container higher-order values?

Given the answer to the previous question, the answer to this one
does not matter.

When a committed the change to typecheck_coerce.m that avoided
the compiler abort, I intended it to be only a stepping stone to the
solution that allowed coercions of e.g. cords. When I read Peter's email,
I knew that that this stone actually had to be the last one in this sequence.

Zoltan.