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

[Julien Fischer]

Hi  Peter,

On Mon, 22 Jul 2024 at 14:49, Peter Wang <novalazy at gmail.com> wrote:
>
> On Mon, 22 Jul 2024 11:33:22 +1000 Julien Fischer <jfischer at opturion.com> wrote:
> > Hi,
> >
> > I assume the fact that the frontend accepts existentially quantified
> > data constructors
> > with repeated type variables is an oversight, e.g.
> >
> >     :- type process_unit
> >          ---> some [T, T] process_unit(T)
> >
> > The above type causes all four of our code generators to abort.
>
> Yes, Zoltan and I both think it should be rejected. It was brought up in
> the recent thread "Require subtypes to repeat existential type vars and
> constraints exactly."

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.

Julien.