Re: [Caml-list] Covariant GADTs

[Lukasz Stafiniak <lukstafi@gmail.com>]

On Tue, Sep 20, 2016 at 11:07 PM, Markus Mottl <markus.mottl@gmail.com> wrote:
>
> Existentially quantified type variables need a well-defined scope.
> It's easy to define this scope with GADTs and first class modules: it
> starts with a pattern match or when unpacking the module.  But
> accessing a record field as such doesn't create a binding.  This would
> require some care when establishing the scope.  Maybe one could define
> the start as the topmost binding whose type depends on a given
> existential type as obtained through field accesses.
>
> Another issue: when accessing an immutable field twice, one could
> assign the same existential type to bindings of their values.  But
> accessing a mutable field twice would require two distinct existential
> types, because intermittent changes to the field could substitute
> values of incompatible types.  Maybe there are even more awkward
> things that I haven't thought about.
>
> Any thoughts?

A simple solution would be to "A-transform" (IIRC the term) accesses
to fields with existential type variables. This would give a more
narrow scope on the expression level than you suggest, but a
well-defined one prior to type inference. To broaden the scope you
would need to let-bind the field access yourself at the appropriate
level.