Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Track newtype level again #1997

Merged
merged 4 commits into from Aug 23, 2018

Conversation

@lpw25
Copy link
Contributor

commented Aug 20, 2018

This PR restores the tracking of the "newtype level" to the environment. It is essentially a revert of f509125. This should fix:

  • MPR#7822
  • MPR#7835
  • MPR#7833
  • Another soundness bug which has been triggered by enough of our code that we've had to revert to 4.06.1 (I'll add this as a test case in this PR shortly)

#1980 should also fix all these issues, and is a better option long term, but it is an invasive change and probably not appropriate for a bugfix release. This PR is intended for inclusion in 4.07.1 to tide us over until the superior fix is merged for 4.08.

@garrigue
Copy link
Contributor

left a comment

This seems a reasonable move.
Of course, test as much as possible :-)
But I believe JS has everything to torture it already.

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 20, 2018

I've tested it by:

  • Building all of jane street's main repo
  • Running the testsuite
  • Testing the example of the soundness bug
  • Testing the minichess example from MPR#7833

Note that this PR also bumps the cmi magic number. My understanding is that we do not normally bump the magic numbers on bugfix releases -- so rather than leave bumping the number until the release I thought it would be a good idea to bump it in the PR itself.

@@ -20,8 +20,9 @@ OCaml 4.07 maintenance branch
- GPR#1915: rec_check.ml is too permissive for certain class declarations.
(Alban Reynaud with Gabriel Scherer, review by Jeremy Yallop)

- MPR#7833, GPR#1946: typecore: only 1k existential per match, not 100k
(Thomas Refis, report by Jerome Simeon, review by Jacques Garrigue)

This comment has been minimized.

Copy link
@gasche

gasche Aug 20, 2018

Member

I find it a bit surprising that GPR#1946 has completely disappeared from the Changes file. Is it reverted by this change? I thought you reverted a part of #1609.

This comment has been minimized.

Copy link
@lpw25

lpw25 Aug 21, 2018

Author Contributor

As Thomas noted in MPR#7835, the limit on existentials per match was not actually doing anything before 4.07.0 because we were always using the newtype level as the binding time. Since we're checking newtype levels again with this patch, I just removed the "limit", which means that the change of the limit from 100k to 1k has essentially been reverted.

@gasche

This comment has been minimized.

Copy link
Member

commented Aug 20, 2018

Bumping the cmi number is fine by me; we should advertise it properly at release time, but I don't think people expect to mix compiled files from two OCaml versions. This means that Merlin will probably need an update, though ( cc @trefis @let-def ).

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 21, 2018

@garrigue Is your review approving the idea of the change, or have you reviewed the code as well? (I ask because your review was so fast, and I want to make sure someone else has looked at the code before I merge it).

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Aug 21, 2018

I looked at the code, but I was assuming that you were only reverting the changes.
Is the only real difference with 4.06 the fact you we removed the +1000?
This should indeed be correct (I wonder why this was not removed before).
Otherwise, I see nothing strange in the diff.

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 21, 2018

Yeah, it is just the revert, the removal of the +1000 and this small change:

https://github.com/ocaml/ocaml/pull/1997/files#diff-ff97e134318d4be6e32d0a612a42cf48R4740

which fixes a small bug I found that caused uncaught Unify exceptions. The +1000 had been making this bug extremely unlikely, but without the +1000 it was happening quite often.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Aug 21, 2018

The problem is a bit mysterious.
I was a bit concerned that the redundancy check would be executed in conditions different from the original typing, which could be unsound (it is used for refutation cases) but here this seems ok.
Actually, one can argue that since newtypes do not use the binding_time, the synchronization in init_env has no meaning anyway. So it should be enough for it to just raise the level and return the current_level:

  let init_env () =
     begin_def ();
    get_current_level ()
  in

I tried, and I just get a changed error message in pr6690.ml.
So this seems to be fine (in pattern-matching we do not need the extra begin_def to check for escape).
Maybe it's better to do the above change, for coherence.
BTW, I tried to export Ctype.get_path_scope function and use it in place of Path.binding_time in Printtyp, but this does not fix the changed error message. I did not analyze further.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Aug 21, 2018

Sorry, my previous answer was misguided.
The level synchronization is not necessary at the beginning of type_cases, but it is indirectly needed in unused_check. Namely, some existential types coming from an outside scope may appear in ty_arg_check and cause incorrect type failures if the level is not high enough. Note that @trefis new identifier scope approach has the same potential problem.
The minimum that should be semantically correct is:

  let unused_check () =
    begin_def ();
    init_def lev;
    List.iter (fun (pat, _, (env, _)) -> check_absent_variant env pat)
      pat_env_list;
    check_unused ~lev env (instance ty_arg_check) cases ;
    Parmatch.check_ambiguous_bindings cases;
    end_def ()
  in

If you see some errors with that, then this is a serious problem that should be fixed properly.
Maybe it's simpler to do a pure rewind, i.e. put back the +1000 for 3.07.1.

@lpw25 lpw25 force-pushed the lpw25:track-newtype-level-again branch from f23b955 to 167c3d3 Aug 21, 2018

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 21, 2018

Ok, I've updated the PR to replace init_env with just doing begin_def, and added calls to begin_def and init_def to unused_check to handle the case where the check is delayed.

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 21, 2018

I'll rerun my testing with the new version to be on the safe side.

@lpw25 lpw25 force-pushed the lpw25:track-newtype-level-again branch from 167c3d3 to 560638b Aug 21, 2018

@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 23, 2018

Tests all passed. Merging.

@lpw25 lpw25 merged commit b669821 into ocaml:4.07 Aug 23, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@lpw25

This comment has been minimized.

Copy link
Contributor Author

commented Aug 23, 2018

@gasche I just realized that I should also have bumped the cmt magic number. When I went to have a look at that I noticed that all the magic numbers are actually synchronised. So should I bump all of them for 4.07.1 or just the ones that actually need to change?

@gasche

This comment has been minimized.

Copy link
Member

commented Aug 23, 2018

I don't know, you should probably ask caml-devel.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.