However, this implies that values defined inside M are also brought to the scope.

It's useless to do so, but I don't see why this would be problematic. Do you see such a reason?

No, as far as I can see, bringing values to the scope should not create any problem. It just feels non optimal to add values in the environment which are never used.

For the issue of performance of local opens, see also http://caml.inria.fr/mantis/view.php?id=6826.

I'm not familiar with the type-checking of patterns, and in particular about why an "Env.t ref" is passed (and not an Env.t) in type_pat. The new case for Tpat_open loose sharing these references. Does it matter?

It does matter. In presence of gadt constructor, the env reference is used as a side-channel to share type equalities discovered during type unification. So the current code breaks gadt typing in pattern!

Thanks for pointing this stupid mistake, I will correct it soon.

I updated the pull request to fix the problem when mixing gadt and pattern open.

The new commit fix this problem by controlling more finely which information is shared between environment during pattern typing:

• GADT type equalities need to be shared with the "outside" environment
• Types, constructors (and values) introduced in a pattern open should not be shared.

To solve these constraints, I have added an environment stack in type_pat. When entering a pattern open, the signature of the associated module is added to a copy of the current environment. This new env is then pushed on the environment stack and poped when exiting the pattern open. Environment changes during pattern typing are then propagated to the whole stack.

A major caveat of this approach is that type equalities are recomputed at each level of the stack. Fortunately, it should mainly affect patterns with gadt constructors deeply nested inside pattern open. It seems sensible to conjecture, for now, that these patterns will be uncommon. If this cause performance problems in the future, it should be possible to optimise this behavior. However, I think that this optimisation would probably need more invasive changes, whereas the current code does not alter pattern typing in absence of pattern open.

• The test suite have been updated to better detect problems with pattern open and gadt. However, it is still probably incomplete. I will fix this point later.

Jacques Garrigue is working on a branch ( http://caml.inria.fr/cgi-bin/viewvc.cgi/ocaml/branches/gadt-warnings/ ) with a much revised version of pattern type-checking (for better support of GADTs). It would be useful to synchronize with him on this topic.

I'm not so fond of the stack approach. It seems the environment is used for two different purposes (collecting equalities, resolving lookups); isn't there a way to separate these uses and keep only two environments, one for each use?

The stack solution is clearly hackish. A better long-term solution might be to split the environment between a shared part and an immutable part during type unification. Splitting the environment might also slightly facilitate the environment backtracking in the gadt-warning branch. I would have a look at this idea this week.

I have added a new version which does not use an environment stack when typing a local open in pattern.

To achieve this goal, I have added an Env.mut type which splits the environment into a local and shared components. During type unification or pattern typing, the shared environment is used to share type equalities, whereas the local environment is used in local pattern open to locally pull in scope the components of the opened module. When the partial sharing is not needed anymore, the two parts of the environment are merged back together in a standard Env.t.

I have also added an id field to Env.t to replace the physical equality check in Ctype.check_abbrev_env which was unruly in presence of shared mutable environment. This new id is essentially here to track changes in the environment and to ensure that the transformation Env.(freeze @@ thaw x) is correctly identified as the identity transformation.

(For the record, I asked Jacques for an opinion on the patch, but he needs more time for a review.)

Since the gadt-warning branch have been merged back to trunk, I have rebased this pull request to solve the resulting merge conflicts. Most of the changes were quite trivial. The only exception might be the function Typecore.save_state which now saves only the mutable part of the environment rather than the full environment.

After some hesitations, I have also added the syntactic sugar for M.() and M.[] to better mirror the local open for expressions.

@garrigue do you have time to review this patch?

@Octachron Could you add an entry in Changes?

I have added a change entry in Changes and updated the local open section in the manual.

I have also cleaned a little bit the code: comments have been somewhat improved and the french-influenced envf was replaced by the more explicit frozen_env.

Were the pull request accepted, I would clean the history to clear up the wandering between implementations.

(side-note: parallel builds of world.opt have been broken once again due to a desynchronized .depend file )

Sorry, I won't have time for this until next week.

Some minor changes: I have cleaned the PR history and rebased onto trunk. I have also simplified a little the code by removing the environment id change.

After reading the code, I have no problem with the basic idea, but the freeze/thaw seems an overkill.
Actually, there is no real need to merge environments (and doing just append is not correct for gadt_instances).
My idea would be to split the local constraints from the types in the evironment, so that one would only have to copy them over when leaving the scope of an open. This should make more sense in the long run.
I'm going to propose my own version of the patch, avoiding changes in Ctype.

I have opened a new pull request #578 for my branch of this patch.
The idea there is to thread the local information by hand, rather than not-so-well understood merge.

Thanks for the review and the code change. Threading just the local type information looks indeed much better. I am closing this PR in favor of #578.

I rebased the two patchsets together and merged in trunk ( 2d33e16 ). Thanks for the work!