Support clever expansion of gadt equations in presence of local module #10348

garrigue · 2021-04-16T07:10:20Z

@lpw25 remarked in #10277 that when combining local modules with GADTs, one could end up expanding a local equation during unification, leading to a spurious error.

This fixes that by allowing the special case for unification of two abstract local types to be used for other types too.

garrigue · 2021-04-16T08:01:12Z

A further relaxation would be to allow expanding parametric types. But this can be tricky.

lpw25

I think this code is definitely an improvement. I have a couple of suggestions/questions, once they are addressed I think this is good to merge.

testsuite/tests/typing-gadts/or_patterns.ml

lpw25 · 2021-05-24T09:22:09Z

typing/ctype.ml

+  if unify_eq t1 t2 then () else
+  match (t1.desc, t2.desc) with
+  | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
+    when is_public_type env p1 && is_public_type env p2 ->


Do we actually need this when clause? It's not clear to me why the type being private or being a variant/record would make the actions in this clause unsound.

I shall probably write a more explicit comment.
Contrary to unify2, this code forgets the abbreviations it is expanding.
In particular this means that since unify2 should be called on the non-expanded types, we cannot call it directly here, hence the exception Cannot_expand when reverting to unify2.
Since we do not want to do useless work, and the case which interests us is when there is a risk of superfluously expanding a GADT equation, we stop as soon as there is no chance to reach one.
Since GADT equations are only defined for abstract types, and since an abstract type can only be reached by expanding a public type, it is sufficient to consider public types.

lpw25 · 2021-05-24T09:23:25Z

typing/ctype.ml

-          unify2 env t1 t2
-        end
+    | (Tconstr _, Tconstr _) when Env.has_local_constraints !env ->
+        (try unify_public !env t1 t2  with Cannot_expand -> unify2 env t1 t2)


Rather than raising Cannot_expand, would it be better to just call straight into unify2 from unify_public? It seems like that might save us from redoing some expansion work at the start of unify2.

As indicated above, unify2 should be called with the non-expanded version of the type.
Note that thanks to memoization, redoing expansions just amounts to looking them up , without any allocation.
This small cost could be avoided by having unify2 receive both the original and partly expanded forms, like unify3. Since we only do extra work when expanding non-parametric type abbreviations, I'm not sure it is worth adding extra complexity to the code to optimize that case.

having unify2 receive both the original and partly expanded forms

Yes, that is what I had in mind. I think it is a tiny change and if it would allow us to remove the is_public_type conditions then I think the code would overall be simpler.

Since we only do extra work when expanding non-parametric type abbreviations

I don't see why the work is only for non-parametric type abbreviations. It seems to be for all type abbreviations. I think that is fine, especially if we reuse the work by adding the extra parameters to unify2.

garrigue · 2021-05-26T08:50:45Z

Thanks for your comments. I will at least add explanations to the code, as it may be a bit terse currently.

garrigue · 2021-05-28T10:08:45Z

Ok, I did as suggested.
Retrospectively, the only reason my first version was conservative was probably that it was a proof of concept avoiding disruption. In presence of non-contractive types, we may indeed need to expand lazily parametric types too.

I'm still a bit concerned about the interaction between scope and expansion (unify2_rec and unify2 may be updating scopes on different node), but this looks orthogonal, i.e. I'm starting to think that there is something fishy in the way scopes are shared.

Here is an example that should not be typable, but is allowed in both 4.12 and trunk. Interestingly, it is rejected with this PR, but I'm not sure this means that this PR is safer.

type (_,_) eq = Refl : ('a,'a) eq;;
let f (type a b c) (w1 : (a,b) eq) (w2 : (b,c) eq) (a : a) (b : b) (c : c) =
  let Refl = w1 in ignore (let Refl = w2 in let x = if true then a else if true then b else c in x);;

Namely, the result of the if expression uses both equations, so it should not be allowed to escape from the matching of w2.

lpw25

Looks good. I still have a couple of questions.

lpw25 · 2021-06-02T10:26:46Z

typing/ctype.ml

+  if unify_eq t1 t2 then () else
+  try match (t1.desc, t2.desc) with
+  | (Tconstr (p1, tl1, a1), Tconstr (p2, tl2, a2)) ->
+      if Path.same p1 p2 && tl1 = [] && tl2 = [] && is_public_type !env p1


I don't see why we still need the is_public_type test here.

Actually, this is mostly conservatism.
is_public_type only checks type_kind and type_private, and if it fails for either reason the type cannot be expanded anyway, so we will just end up doing the same unification in unify3.
Maybe it is ok to just remove it. It could change error messages though (see below).

I think it would be best to just remove it. It makes the code harder to think about and doesn't really add anything.

typing/ctype.ml

garrigue · 2021-07-15T09:42:52Z

I have rebased.
This seems OK, except for the already noticed changed in error messages (not incorrect, but a bit less informative).
I also tried another approach to keep more abbreviations.
This improves some error messages, but makes a warning in gadts-and-principality.ml meaningless.
Here is the diff: COCTI/ocaml@clever_expand...COCTI:clever_expand_keep_abbrev

garrigue · 2022-06-16T06:17:04Z

@lpw25 rebased again

lpw25

I think this is good to merge, although I would prefer it if is_public_type were removed.

lpw25 · 2022-07-02T08:10:39Z

typing/ctype.ml

+  if unify_eq t1 t2 then () else
+  try match (t1.desc, t2.desc) with
+  | (Tconstr (p1, tl1, a1), Tconstr (p2, tl2, a2)) ->
+      if Path.same p1 p2 && tl1 = [] && tl2 = [] && is_public_type !env p1


I think it would be best to just remove it. It makes the code harder to think about and doesn't really add anything.

garrigue · 2022-07-04T02:56:07Z

Removing is_public_type didn't change any output in the test suite, so let's go the simpler way.
Thanks for the review.

ocaml#10348)

garrigue added the no-change-entry-needed label Apr 16, 2021

garrigue marked this pull request as draft April 16, 2021 07:40

garrigue mentioned this pull request Apr 16, 2021

make update_scope recursive while keeping trace_gadt_instances #10277

Merged

lpw25 reviewed May 24, 2021

View reviewed changes

garrigue force-pushed the clever_expand branch from 6a916b9 to 7850df1 Compare May 28, 2021 09:12

garrigue added typing-GADTS GADT typing and exhaustiveness bugs and removed no-change-entry-needed labels May 31, 2021

garrigue marked this pull request as ready for review May 31, 2021 09:15

lpw25 reviewed Jun 2, 2021

View reviewed changes

garrigue force-pushed the clever_expand branch from 14fcd8a to eefb096 Compare July 14, 2021 03:44

garrigue force-pushed the clever_expand branch from eefb096 to d4ce893 Compare June 16, 2022 06:15

garrigue mentioned this pull request Jun 21, 2022

Fix module+GADT typechecking regression #11339

Closed

lpw25 approved these changes Jul 2, 2022

View reviewed changes

garrigue added 2 commits July 4, 2022 09:50

Support clever expansion of gadt equations in presence of local module

6796872

remove Ctype.is_public_type, move log message

db9c728

garrigue force-pushed the clever_expand branch from d4ce893 to db9c728 Compare July 4, 2022 02:02

garrigue merged commit 70aa10f into ocaml:trunk Jul 4, 2022

garrigue added a commit to COCTI/ocaml that referenced this pull request Jul 19, 2022

Support clever expansion of gadt equations in presence of local module (

f3f7c5c

ocaml#10348)

sadiqj mentioned this pull request Sep 23, 2022

Regression from #10348 causes compilation failure #11560

Closed

Octachron mentioned this pull request Sep 23, 2022

#11560: typechecker internal error on missing gadts #11561

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support clever expansion of gadt equations in presence of local module #10348

Support clever expansion of gadt equations in presence of local module #10348

garrigue commented Apr 16, 2021

garrigue commented Apr 16, 2021

lpw25 left a comment

lpw25 May 24, 2021

garrigue May 26, 2021

lpw25 May 24, 2021

garrigue May 26, 2021

lpw25 May 26, 2021

garrigue commented May 26, 2021

garrigue commented May 28, 2021

lpw25 left a comment

lpw25 Jun 2, 2021

garrigue Jun 3, 2021 •

edited

lpw25 Jul 2, 2022

garrigue commented Jul 15, 2021 •

edited

garrigue commented Jun 16, 2022

lpw25 left a comment

lpw25 Jul 2, 2022

garrigue commented Jul 4, 2022

Support clever expansion of gadt equations in presence of local module #10348

Support clever expansion of gadt equations in presence of local module #10348

Conversation

garrigue commented Apr 16, 2021

garrigue commented Apr 16, 2021

lpw25 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

garrigue commented May 26, 2021

garrigue commented May 28, 2021

lpw25 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

garrigue Jun 3, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

garrigue commented Jul 15, 2021 • edited

garrigue commented Jun 16, 2022

lpw25 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

garrigue commented Jul 4, 2022

garrigue Jun 3, 2021 •

edited

garrigue commented Jul 15, 2021 •

edited