Comment author: @garrigue

Indeed, let T x = T 3 in expr is handled as syntactic sugar for match T 3 with T x -> expr.
This is not the case for the two other constructs.
This should probably be documented.

Comment author: @alainfrisch

Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings?

Comment author: @garrigue

Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings?

There are several cases:

• simple let bindings (not rec, no and) are already supported.

• multiple non-recursive let-bindings could probably be supported with some effort.
  Part of the problem is the semantics: if we use the classical approach of converting to a big tuple, we have the side-effect that equations are propagated from the left to the right. Do we really want that? Is there any other approach.

• recursive let bindings: honestly I don't know what it would mean for an existential type variable to be accessed in the body of its own definition...

So don't hold your breath.
Do you have any practical example where this would be handy?

Comment author: @gasche

Part of the problem is the semantics: if we use the classical approach of converting to a big tuple, we have the side-effect that equations are propagated from the left to the right. Do we really want that? Is there any other approach.

How can the propagation be a problem? Can we run into, say, ambiguity errors that wouldn't have existed in absence of propagation? I think people would expect let p1 = e1 and p2 = e2 in e3 and match e1,e2 with p1,p2 -> e3 to have the same behavior. They also expect nonrec-"and"-bindings to be independent and reorderable, but they can probably live with the idea that opening GADTs breaks this property. This will in any case be much less surprising than single-let succeeding and let-and failing to type-check.

• recursive let bindings: honestly I don't know what it would mean for an existential type variable to be accessed in the body of its own definition...

Pattern-matching is not allowed as the defined-part of a let rec (only in function arguments), so I don't see how GADTs can be opened in that case.

Comment author: @alainfrisch

Part of the problem is the semantics: if we use the classical approach of converting to a big tuple

My question was rather: can we support directly, at reasonable cost, the opening of GADTs existentials in the normal type-checking of let bindings, without going to an encoding into a "match".

Non-recursive "let and" bindings are not very different from a sequence of single let bindings, except for scope management, but this does not seem very deep (we could just type-check each let-binding in the same initial environment, no?). So supporting them again by a translation to match cases should be doable (but it might not justify the effort, I agree).

Comment author: @garrigue

I don't think it would be a good idea to duplicate the code in type_let, as this just increases the chances for bugs.
If we agree that the semantics should be that of a big a tuple, it shall probably be fine.
I don't think there is any overhead involved, at least for native code.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

If anybody is still interested by that, we can go through the tuple encoding.

I'm still in favour of this feature.

But I'm not sure about the tuple encoding, especially for equalities. Currently

let p1 = e1 and p2 = e2 in e

can be (and is) evaluated in the order e1, p1, e2, p2. With the tuple encoding

let p1, p2 = e1, e2 in e

the order changes to e1, e2, p1, p2.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.