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

[Zoltan Somogyi]

On 2024-11-13 11:21 +11:00 AEDT, "Peter Wang" <novalazy at gmail.com> wrote:
>> 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.

That design choice is one that one *could* make, but one that one
*shouldn't* make. I will reword the last two thirds of that sentence
to give the reason as shadowing being both potentially confusing to readers,
and trivially avoidable.

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

I will apply it after lunch.

Zoltan.