Fix the scope handling to detect ambiguous results of applications by garrigue · Pull Request #9815 · ocaml/ocaml

garrigue · 2020-07-31T04:12:24Z

Following the discovery of cases where ambiguity was not correctly detected, this extends Ctype.update_scope to update scopes recursively.

See ambivalent_apply.ml for examples.

garrigue · 2020-07-31T04:18:04Z

Note that I plan to completely remove the trace_gadt_instances flag.
The real criterion is wether there are local constraints in the environment.

lpw25

The improved tests look good. The changes to update_scope and the switch to use Env.has_local_constraints instead of trace_gadt_instances seem fine. A couple of small changes are not clear to me and I've left comments on those.

lpw25 · 2020-07-31T08:09:58Z

typing/typecore.ml

-  match expand_head env ty_expected' with
-    {desc = Tarrow(Nolabel,ty_arg,ty_res,_); level = lv}
+  let lv = (repr ty_expected').level in
+  match expand_head env (correct_levels ty_expected') with


The appearance of correct_levels makes me nervous. I tend to think that we should never really need to use it -- the levels should already be correct. Could you add a comment explaining why it is needed here?

The other name of correct_levels is duplicate_type.
Here this allows to check the expansion of ty_expected' without changing the scopes in the original type.
Otherwise we get spurious ambivalence, even though the type doesn't have an interesting shape. We then expand the real type if we know that it is going to be useful.

Note that all this means that there is a high potential that this PR as a whole introduces spurious ambivalence in other similar places. I should probably find a better way to do it, and review all uses of expand_head.

lpw25 · 2020-07-31T08:18:09Z

typing/ctype.ml

      | Tconstr (p, tl, _) ->
-          let abbrevs = proper_abbrevs p tl !abbreviations in
-          begin match find_repr p !abbrevs with
+          (*let abbrevs = proper_abbrevs env p tl !abbreviations in*)


I'm surprised by the removal of proper_abbrevs here. I assume it is just because copy does not currently take an environment, which proper_abbrev now needs. Morally, I think that copy should take an environment anyway, since it creates a type at the current level, which is closely tied to the environment. So it would probably be better to add an environment parameter to copy.

FTR. it did take an environment until 7f0e819

@lpw25 I need a better analysis of the code, but this doesn't seem to make a difference.
Actually, I wonder whether the original version was correct or no. This change returns the code to what it was in ocaml 2.04.
@trefs Indeed, at some point copy used the environment, but your scope mechanism removed this need. Since I'm not sure it's really needed here, it seems simpler for now to get rid of some dubious code.

garrigue · 2020-07-31T22:48:22Z

Thanks for your comments
Just to clarify: this is really work in progress, following the discovery of a small error in the theory.
So I'm checking experimentally that the solution I have in mind works (I'm pleased it seems to be the case).
I would prefer to get the theory straight before merging, even if there is anyway a gap between the theory and implementation.
While this bug clearly loses principality, as the examples show, I don't think it impacts soundness (i.e. if a node is physically linked to a potentially incompatible one, it already cannot be leaked).

lpw25 · 2020-08-01T06:30:18Z

Just to clarify: this is really work in progress, following the discovery of a small error in the theory.
So I'm checking experimentally that the solution I have in mind works (I'm pleased it seems to be the case).

Recently GitHub added the ability to create a "draft" pull request (IIRC it is a drop down option from one of the buttons you press when making a PR). I think it would be good if we used those on PRs that we do not yet think are ready for review.

garrigue · 2020-08-01T09:26:19Z

Recently GitHub added the ability to create a "draft" pull request (IIRC it is a drop down option from one of the buttons you press when making a PR). I think it would be good if we used those on PRs that we do not yet think are ready for review.

I didn't know. I'll do that in the future.
Anyway, your feedback is useful, and I will keep it in mind.

garrigue · 2021-02-03T10:07:27Z

After discussion with @diremy and @trefis, we agree that this is the correct solution to the problem, so this is no longer a draft PR, although it probably requires some polishing. I'm accepting input.

trefis · 2021-02-03T10:27:28Z

I'm going to be annoying, but: while I agree that the change to update_scope makes sense and that expand_abbrev should indeed be calling that function, it's not clear to me how the removal of trace_gadt_instance is related to that change.

To be honest, I've never tried to understand why the thing was there in the first place, and how it was better than just checking Env.has_local_constraints as you're doing here (I assume it was meant as some kind of optimization?). It seems a bit silly to ask now that you propose to remove it. But … there you go. Are the two changes really connected? Couldn't the removal of the "tracing" be done in a separate PR?

garrigue · 2021-02-03T11:34:08Z

The trace_gadt_instance stuff was need when we were keeping the scopes in the equation scopes in the environment.
Since you introduces scopes inside type_expr, it was actually useless, but removing it was just something I was always postponing. But this time, this came in the way, so I decided to remove it, and didn't really think of splitting the PR.
So, the two parts are not really related, but if they're not done together, then probably the removal of trace_gadt_instance should come first.

garrigue · 2021-02-03T11:58:03Z

I should also integrate Leo's comments before asking for more...

garrigue · 2021-04-19T04:13:13Z

Subsumed by #10277.

garrigue added the work-in-progress label Jul 31, 2020

lpw25 reviewed Jul 31, 2020

View reviewed changes

garrigue marked this pull request as draft August 6, 2020 13:09

garrigue force-pushed the update_scope_rec branch from 6a695ce to 92fe56f Compare February 3, 2021 10:04

garrigue added bug and removed work-in-progress labels Feb 3, 2021

garrigue marked this pull request as ready for review February 3, 2021 10:06

Fix the scope handling to detect ambiguous results of applications

15e931a

garrigue force-pushed the update_scope_rec branch from 7889b80 to 15e931a Compare March 3, 2021 06:13

garrigue mentioned this pull request Mar 8, 2021

make update_scope recursive while keeping trace_gadt_instances #10277

Merged

garrigue closed this Apr 19, 2021

Conversation

garrigue commented Jul 31, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

garrigue commented Jul 31, 2020

Uh oh!

lpw25 left a comment

Choose a reason for hiding this comment

Uh oh!

lpw25 Jul 31, 2020

Choose a reason for hiding this comment

Uh oh!

garrigue Jul 31, 2020

Choose a reason for hiding this comment

Uh oh!

lpw25 Jul 31, 2020

Choose a reason for hiding this comment

Uh oh!

trefis Jul 31, 2020

Choose a reason for hiding this comment

Uh oh!

garrigue Jul 31, 2020

Choose a reason for hiding this comment

Uh oh!

garrigue commented Jul 31, 2020

Uh oh!

lpw25 commented Aug 1, 2020

Uh oh!

garrigue commented Aug 1, 2020

Uh oh!

garrigue commented Feb 3, 2021

Uh oh!

trefis commented Feb 3, 2021

Uh oh!

garrigue commented Feb 3, 2021

Uh oh!

garrigue commented Feb 3, 2021

Uh oh!

garrigue commented Apr 19, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

garrigue commented Jul 31, 2020 •

edited

Loading