[m-rev.] for review: Require subtypes to repeat existential type vars and constraints exactly.

[Peter Wang]

On Wed, 13 Nov 2024 05:10:49 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> On 2024-07-08 17:46 +10:00 AEDT, "Peter Wang" <novalazy at gmail.com> wrote:
> >> > +:- pred build_existq_tvars_mapping(tvar::in, tvar::in,
> >> > +    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
> >> > +
> >> > +build_existq_tvars_mapping(VarA, VarB, !ExistQVarsMapping) :-
> >> > +    ( if bimap.insert(VarB, VarA, !ExistQVarsMapping) then
> >> > +        true
> >> > +    else
> >> > +        % The reference manual does not require distinct type variables in a
> >> > +        % existential quantifier list of a constructor definition (whether or
> >> > +        % not a du type is a subtype). This might be an oversight.
> >> 
> >> I don't think it "might be"; like you, I think it *is* an oversight. It should be fixed,
> >> though probably in a separate diff.
> >> 
> > 
> > Right.
> 
> The attached diff documents this restriction.
> 
> This is not a breaking change, because the compiler already enforces
> this restriction. This is done by through the call chain
> 
> - parse_du_type_defn
> - parse_maybe_exist_quant_constructors
> - parse_maybe_exist_quant_constructors_loop
> - parse_maybe_exist_quant_constructor
> - parse_and_check_quant_vars
> 
> with the last of these predicates reporting an error for any duplicates.
> 
> For post-commit review by anyone.
> 
> Zoltan.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 552a3b797..8fdcb8c56 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -8295,7 +8295,24 @@ The reason for the restriction is simple:
>  without it, how can one decide whether
>  the argument of @samp{f2} is universally or existentially quantified?

As an aside, the full context for the question above is:

    @example
    :- type t12(T)
	--->    f1(T)
	;       some [T] f2(T).
    @end example

    The reason for the restriction is simple:
    without it, how can one decide whether
    the argument of @samp{f2} is universally or existentially quantified?

It would be a reasonable design choice for the existential quantifier
to shadow the universal quantifier, making the argument of `f2'
existentially quantified. I suggest we delete that paragraph.

> -The other restriction is that every existentially quantified type variable
> +A second restriction is that
> +the list of type variables
> +listed in the existential type quantifier before the data constructor
> +may contain any type variable at most once.
> +The same requirement applies to the
> +list of type variables listed as arguments of the type constructor,
> +whether the data constructors of that type
> +have existential types or not.

Here is my attempt at rewording it, which you can apply or not:

diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 8fdcb8c56..7fdf9064f 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -8278,7 +8278,7 @@ process_list(cons(Head, Tail)) = [show(Head) | process_list(Tail)].
 There are some restrictions on the forms that
 existentially typed data constructors can take.

-One restriction is that no type variable may be quantified
+The first restriction is that no type variable may be quantified
 both universally, by being listed as an argument of the type constructor,
 and existentially, by being listed in the existential type quantifier
 before the data constructor.
@@ -8295,14 +8295,14 @@ The reason for the restriction is simple:
 without it, how can one decide whether
 the argument of @samp{f2} is universally or existentially quantified?

-A second restriction is that
-the list of type variables
-listed in the existential type quantifier before the data constructor
-may contain any type variable at most once.
-The same requirement applies to the
-list of type variables listed as arguments of the type constructor,
-whether the data constructors of that type
-have existential types or not.
+The second restriction is that
+type variables listed
+in the existential type quantifier before the data constructor
+cannot be repeated.
+Type variables in the argument list of the type constructor
+also cannot be repeated,
+whether or not the data constructors of that type
+have existential types.
 The type @samp{t34} violates both these restrictions:

 @example


Peter