[m-rev.] for review: check "for type_ctor" annotations on insts

[Julien Fischer]

On Wed, 29 Dec 2021, Zoltan Somogyi wrote:

> Check "for type_ctor" annotations on user insts.

...

> diff --git a/compiler/inst_mode_type_prop.m b/compiler/inst_mode_type_prop.m
> index 8686aafd6..8d2d16c4f 100644
> --- a/compiler/inst_mode_type_prop.m
> +++ b/compiler/inst_mode_type_prop.m
> @@ -68,26 +69,86 @@
>      %
>      % This predicate is exported for use by inst_user.m.
>      %
> -:- pred propagate_type_into_bound_inst(module_info::in, mer_type::in,
> -    mer_inst::in(mer_inst_is_bound), mer_inst::out) is det.
> +:- pred propagate_unchecked_type_into_bound_inst(module_info::in,
> +    mer_type::in, mer_inst::in(mer_inst_is_bound), mer_inst::out) is det.
>
>  %---------------------------------------------------------------------------%
>  %
>  % Propagating type information into modes.
>  %
> 
> +:- type tprop_context
> +    --->    tprop_arg_list_slot(tprop_args, int)
> +            % The inst is in the argument list specified by the first argument
> +            % at the position given by the second argument.
> +            % (The first argument is argument #1.)
> +    ;       tprop_inst_name_expansion(sym_name_arity, tprop_context).
> +            % The inst is the expansion of the named user inst, which
> +            % occurs in the given context.
> +
> +    % Values of this type specify the origin of a list of insts.
> +    %
> +    % These usually come from a list of modes, as each mode specifies
> +    % an initial and a final inst. For input modes, the initial and final
> +    % insts may be identical or at least similar, which means that if
> +    % a final inst applies a user-defined inst name to a value of a type
> +    % that has different type constructor from the one that the inst name
> +    % is declared to be for, that error is quite likely to be present
> +    % in the mode's initial inst as well.
> +    %
> +    % We "handle" the problem by simply not including in the error message
> +    % any reference to whether the inst being complained about came from
> +    % the initial or the final inst. If the error is present in both insts,
> +    % then we will generate one error for each inst, but these will be
> +    % identical in every respect, so sort_error_specs in error_util.m
> +    % will keep only one out of every pair of duplicate messages.
> +    %
> +    % The argument lists can be divided into two caregories.

s/caregories/categories/

> +    % The first two, ta_pred and ta_lambda, stand on their own, in that
> +    % the insts in their lists are not part of a bigger inst. The last three
> +    % describe inst lists that *are* part of a bigger inst, whose context
> +    % is given by their last arguments.
> +    %
> +    % The pred_or_func flag and arity arguments of ta_lambda and ta_ho_inst
> +    % are needed to decidse an inst refers to the inst of an ordinary
> +    % function argument, or the inst of the function result argument.
> +    % For arguments of predicates, cons_ids and tuples, the distinction
> +    % is moot.
> +    %

...

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 84b5df1c8..ffb80de72 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -3699,8 +3699,9 @@ after the name of the inst, like this:
>
>  @noindent
>  This can be useful documentation,
> -even though the compiler does not (yet) prevent
> -the use of such insts on values of other types.
> +and the compiler will generate an error message
> +an inst that was declared to be intended for values of one type constructor

... *when* an inst

Also, I think you can drop the words "to be intended".

> +is applied to values of another type constructor.

That looks fine otherwise.

Julien.