[m-rev.] for review: improve readability of coerce code

[Peter Wang]

On Sat, 12 Jul 2025 14:45:10 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> Improve readability of coerce checking code.
> 
> compiler/typecheck_coerce.m:
>     Give some predicates, types and variables more descriptive,
>     and in some cases more consistent, names.
> 
>     Simplify some code.
> 
>     Add some comments.
> 
> compiler/modecheck_coerce.m:
>     Give the names of the predicates that this module
>     copies-with-modification from typecheck_coerce.m an _mc suffix.
> 
>     Add some comments.
> 
> compiler/type_util.m:
>     Use more consistent variable names.

> diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
> index c87c478d9..4b4e7089f 100644
> --- a/compiler/modecheck_coerce.m
> +++ b/compiler/modecheck_coerce.m
> @@ -1019,36 +1019,54 @@ copy_inst_for_coerce_result(LiveX, InstX, InstY) :-
...
> +    % In typecheck_coerce.m, the reason for allowing the Comparison parameter
> +    % to be compare_equal is that types_compare_as_given (no _mc) can modify
> +    % the type assignment to enforce equality. The code here does not do that,
> +    % which means that calling types_compare_as_given_mc with compare_equal
> +    % is equivalent to invoking "TypeA = TypeB".
> +    %
> +    % The only advantage of handling compare_equal is reducing the textual
> +    % difference between the code in typecheck_coerce.m andthe code here.

and the

> +    % However, this is enough, because even though "TypeA = TypeB" would
> +    % be faster, this does not matter, due to the rarity of coercion.
> +    %
> +    % XXX Peter, is the above correct?
> +    %

It took a while to understand what the comment refers to.
Yes, calling types_compare_as_given_mc with compare_equal is (or should be)
the same as comparing two higher-order types using builtin unification.
Performance is not a concern here, and I prefer to similarity to the
same code in typecheck_coerce.m.

>      ;
> -        CtorArgType = higher_order_type(_PredOrFunc, ArgTypes, _HOInstInfo,
> -            _Purity),
> +        RhsType = higher_order_type(_PoF, ArgTypes, _HOInstInfo, _Purity),
> +        % We do not support any subtyping of higher order types.
> +        % Since the higher order components on the right-hand side of a
> +        % type definition must be identical in the from-type and the to-type,
> +        % all type paramaters that occur in the such higher order types
> +        % must be bound to the exact same value in the from-type and to-type.

parameters

I think "Therefore" would be better than "Since" as it's a consequence
of the preceding statement.

>  %---------------------%
>  
> -:- pred check_coerce_type_params(type_table::in, tvarset::in,
> -    invariant_set::in, list(tvar)::in, list(mer_type)::in, list(mer_type)::in,
> +    % are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars,
> +    %   TypeParams, FromArgTypes, ToArgTypes, !TypeAssign):
> +    %
> +    % FromArgTypes and ToArgTypes are the actual types bound to TypeParams
> +    % in the from-type and to-type of the coercion respectively.
> +    % If a given type parameter is in InvariantTVars, then the types bound
> +    % to that parameter in the from-type and to-type must be identical,
> +    % while for the type parameters that are not in InvariantTVars,
> +    % it is enough that one is a subtypp of the other (in either direction).

subtype

> +    %
> +    % If e.g. neither the first nor second TypeParam is in InvariantTVars,
> +    % we can succeed if the first FromArgType is a subtype of the first
> +    % ToArgType, but the second ToArgType is a subtype of the second
> +    % FromArgType. The direction of which is the subrtype of the other

subtype

> +    % does NOT need to be consistent. This allows us to support coercion
> +    % from any subtype of the base type to any other of its subtypes;
> +    % the from-type and the to-type do not need to be in a subtype-supertype
> +    % relationship.
> +    %
> +    % XXX Peter, is the above correct?
> +    %

Correct.

That looks fine to me.

Peter