[m-rev.] for review: Modecheck coerce of terms with existential types.

[Julien Fischer]

Hi Peter,

On Mon, 8 Jul 2024 at 16:24, Peter Wang <novalazy at gmail.com> wrote:
>
> The modechecking for coerce did not take into account existentially
> typed arguments in the term being coerced. There are two main changes:
>
> 1. If the input (sub)term being coerced has an existential type, the
>    result must have the same type. Therefore, we can use the inst
>    approximating the input (sub)term for the result.
>
> 2. Each existentially quantified type variable or existential class
>    constraint on a data constructor adds a type_info or type_class_info
>    to the resulting heap cell. Internally, the inst for that cell will
>    include insts for those extra arguments, which the modechecker for
>    coerce will need to be aware of.

...


> diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
> index 25e156c38..c97cf3514 100644
> --- a/compiler/modecheck_coerce.m
> +++ b/compiler/modecheck_coerce.m

...

> @@ -432,14 +441,71 @@ modecheck_coerce_from_bound_make_bound_functors(ModuleInfo, TVarSet, LiveX,
>      ;       bioe_other_error.    % error kept separately
>
>  :- pred modecheck_coerce_from_bound_make_bound_functor(module_info::in,
> -    tvarset::in, is_live::in, rev_term_path::in, mer_type::in, mer_type::in,
> -    expanded_insts::in, bound_inst::in, bound_inst_or_error::out,
> +    tvarset::in, is_live::in, existq_tvars::in, rev_term_path::in,
> +    mer_type::in, mer_type::in, expanded_insts::in,
> +    bound_inst::in, bound_inst_or_error::out,
>      list(coerce_error)::in, list(coerce_error)::out) is det.
>
>  modecheck_coerce_from_bound_make_bound_functor(ModuleInfo, TVarSet, LiveX,
> -        RevTermPath0, TypeX, TypeY, ExpandedInsts0, BoundInstX,
> -        MaybeBoundInstY, !Errors) :-
> +        ConsExistQTVars, RevTermPath0, TypeX, TypeY, ExpandedInsts0,
> +        BoundInstX, MaybeBoundInstY, !Errors) :-
>      BoundInstX = bound_functor(ConsIdX, ArgInstsX),
> +    (
> +        ( ConsIdX = du_data_ctor(_)
> +        ; ConsIdX = tuple_cons(_)
> +        ; ConsIdX = some_int_const(_)
> +        ; ConsIdX = float_const(_)
> +        ; ConsIdX = char_const(_)
> +        ; ConsIdX = string_const(_)
> +        ),
> +        ( if existq_tvars_contains(ConsExistQTVars, TypeX) then
> +            % TypeX is an existential type. We can assume that TypeX = TypeY,
> +            % so BoundInstX is acceptable for the result term as well.
> +            % The only thing we do is to make the remove uniqueness in the
> +            % result inst if the input remains live (this may or may not
> +            % really be necessary?).

That last sentence doesn't make sense.

That looks fine otherwise.

Julien.