Skip to content

Remove subsumed fix for #4862#12932

Merged
garrigue merged 4 commits into
ocaml:trunkfrom
COCTI:remove_subsumed_fix_for_4862
Jan 26, 2024
Merged

Remove subsumed fix for #4862#12932
garrigue merged 4 commits into
ocaml:trunkfrom
COCTI:remove_subsumed_fix_for_4862

Conversation

@garrigue
Copy link
Copy Markdown
Contributor

@garrigue garrigue commented Jan 24, 2024

#4862 was fixed in 3.12 by using backtracking in Typecore.type_label_exp.
However, it seems that this has been useless for a long time now (checked that the example compiles fine in 4.07 without backtracking).
So let us remove this useless backtracking.
Also, properly call enforce_current_level when there are no variables, and remove a superfluous generalize_structure in type_exp/Pexp_let.

@gasche
Copy link
Copy Markdown
Member

gasche commented Jan 24, 2024

It's ironic that we spent a fair amount of effort discussing this backtracking code, which turns out to be unnecessary after all :-)

Two questions:

  • Is the testcase of small bug in relaxed value restriction #4862 part of the testsuite?
  • The problem with small bug in relaxed value restriction #4862 came from an expected_type annotation introducing a contravariant occurrence, which would then block generalization. Can you explain how the current implementation avoids this issue? (Is it still avoided if the user writes an explicit annotation, { f = (lazy (raise Not_found) : ('a list -> int) Lazy.t) }?)

@garrigue
Copy link
Copy Markdown
Contributor Author

  • The test is in typing-poly/poly.ml.
  • { f = (lazy (raise Not_found) : ('a list -> int) Lazy.t) } has never been accepted, as named variables are not generalizable locally.
  • maybe you meant { f = (lazy (raise Not_found) : (_ list -> int) Lazy.t) }, which still works after removal.

Copy link
Copy Markdown
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm still not sure why the example works when it did not work before, but I can tell that the code is vastly simpler so I'm all for it if it still passes the testsuite. Approved.

@garrigue
Copy link
Copy Markdown
Contributor Author

Since the original fix was introduced in 3.12, before the addition of GADTs, a lot has changed since then. It is not too surprising that this kind of bug was actually fixed by other changes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants