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

[Julien Fischer]

On Mon, 3 Nov 2025 at 19:05, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
> I just got a compiler abort. This is the simplified version
> of the code involved:
>
> :- pred foo(list(citrus)::in, list(fruit)::out) is det.
> :- pred bar(cord(citrus)::in, cord(fruit)::out) is det.
>
> foo(CitrusList, FruitList) :-
>     FruitList = coerce(CitrusList).
>
> bar(CitrusCord, FruitCord) :-
>     FruitCord = coerce(CitrusCord).
>
> The compiler handles foo ok, but crashes on bar with
>
> Uncaught Mercury exception:
> Software Error: predicate `check_hlds.typecheck_coerce.compute_which_type_params_must_be_invariant'/5: Unexpected: not du type
>
> The reason is that while cord is a du type, it is a du type
> that is defined *behind* an abstraction barrier, and so in
> the module containing this code, cord/1 is an abstract type.
>
> I can see two ways to fix the problem.
>
> The first way is to move the test for the common base type_ctor (in this case cord/1)
> being a du type into compute_which_type_params_must_be_invariant's
> caller, which is semidet. This would avoid the crash, but do so
> by effectively saying that coerce works only if all the types involved
> have their definitions visible at the site of the coerce.

That doesn't seem like a very desirable state of affairs.

> The second way is to say that if the from-type and the to-type
> share the same actual type_ctor (in this case cord/1) and not just
> the same *base* type_ctor, then for the coerce to succeed, it is sufficient
> for *its arguments* to be coercable between the from_type and the to_type,
> and it does not matter whether the actual shared_type_ctor is du or abstract.
> This would say that if a type_ctor's coerceability is not an issue because it is
> the same in both the from-type and the to-type, then its definition need not
> be visible.
>
> 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.
>
> Both ways are backwards compatible; neither rejects any code that
> the compiler has accepted up to now.
>
> I would prefer the second way.

As do I.

Julien.