[m-dev.] compiler abort: coercing abstract type
Julien Fischer
jfischer at opturion.com
Wed Nov 5 15:07:34 AEDT 2025
On Wed, 5 Nov 2025 at 14:35, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
> 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.
I had a feeling something like that would be the case. Within that limitation,
the only other thing I can think of is that
1. Some abstract types are composed of function symbols entirely from their
defining module (e.g tree234, rbtree from the standard library).
Within the
interface file framework, we should be able to determine if they
are coerce-safe.
2. For standard library types, we can simply cheat and build information about
whether they are coerce-safe into the compiler.
Those two things should be sufficient for us to determine that cords
are coerce-safe.
3. We could have a pragma that allows programmers to promise that abstract types
are coerce-safe.
Julien.
More information about the developers
mailing list