[m-dev.] Repeated type variables in existentially quantified data constructors

[Zoltan Somogyi]

On Mon, 22 Jul 2024 16:43:50 +1000, Julien Fischer <jfischer at opturion.com> wrote:
> I just posted a diff that disallowed repeated type variables in that context.
> Looking at other uses of quantifiers in the language, repeated variables are
> not allowed in quantifiers in goals but are (apparently) allowed in
> predicate and function declarations.
> For example, the following will not generate an error:
> 
>     :- some [T, T] pred (T).
>     :- all [T, T] pred(T).
> 
> Again, I think that is probably just an oversight and we should
> require all variable lists in quantifiers
> to be distinct.

Agreed.

There is one possibly arguable exception. We use some [Vars] scopes
to quantify both state variables and normal, non-state variables, so a scope
such as "some [!X, X]" contains two copies of the variable X, but only one
represents X itself; the other represents a series of variables whose real names are
STATE_VARIABLE_X or STATE_VARIABLE_X_N for some N.

Despite the lack of overlap in the *final* names of the variables between X
and STATE_VARIABLE_X*, I think we should still detect and report such
scopes as errors, because the *readers* can still be confused. This error
would have to be reported separately though, with a message that makes it clear
that this potential confusion is the reason for which this is not allowed.

Zoltan.