with-kinds #3284
with-kinds #3284
Conversation
Parser Change ChecklistThis PR modifies the parser. Please check that the following tests are updated:
This test should have examples of every new bit of syntax you are adding. Feel free to just check the box if your PR does not actually change the syntax (because it is refactoring the parser, say). |
goldfirere
force-pushed
the
rae/const-sorts-in-transl
branch
from
ab43d23 to
540cc23
Compare
goldfirere
force-pushed
the
rae/with-kinds
branch
2 times, most recently
from
07eb6ed to
a0096f3
Compare
goldfirere
force-pushed
the
rae/with-kinds
branch
from
a0096f3 to
32dbf8c
Compare
goldfirere
force-pushed
the
rae/const-sorts-in-transl
branch
from
540cc23 to
05c3424
Compare
goldfirere
force-pushed
the
rae/with-kinds
branch
from
ad170e9 to
011331a
Compare
goldfirere
force-pushed
the
rae/with-kinds
branch
from
16e83fa to
70cf6eb
Compare
This causes trouble after with-kinds, because we get a jkind error where a kind error would be much, much clearer.
goldfirere
force-pushed
the
rae/with-kinds
branch
from
70cf6eb to
25eadb9
Compare
|
This is now ready for review. 🎉 🎁 🎄 I have updated the top comment with a review plan, involving @rtjoa, @ccasin, @liam923, and @riaqn (and a tiny bit for @lpw25). @dkalinichenko-js could likely do some review, too, but given the fact that @liam923 and @riaqn have already taken a spin at the implementation here, it seems to make the most sense to have them review. But if the review burden here seems too high, looping in @dkalinichenko-js is a possible way to spread it out. |
This seems to be what we want; there was a comment here saying we shouldn't have any baggage but I think that was incorrect. And in fact, using Ctype.type_equal to check type equality makes a number of tests pass that we had marked as expecting to pass.
|
| (* TEST | ||
| readonly_files = "shadow_stdlib.ml bug.ml ref.ml"; | ||
| setup-ocamlc.byte-build-env; | ||
| module = "ref.ml"; | ||
| flags = "-allow-illegal-crossing"; | ||
| ocamlc.byte; | ||
| module = "shadow_stdlib.ml"; | ||
| flags = ""; | ||
| ocamlc.byte; | ||
| flags = "-allow-illegal-crossing"; | ||
| module = "bug.ml"; | ||
| ocamlc.byte; | ||
| check-ocamlc.byte-output; | ||
| *) |
There was a problem hiding this comment.
I'm surprised that the -allow-illegal-crossing flag has anything to do with this error since illegal crossing isn't actually used anywhere. But I do agree that the error only occurs when the flag is included. Do you know what's going on here? I had thought that maybe the check in Type_decl.check_kind_coherence that happens only when illegal crossing is enabled was responsible, but based on testing, that doesn't seem to be the case. This leads me to the conclusion that add_portability_and_contention_crossing isn't a no-op when no annotation is written, which I didn't expect.
There was a problem hiding this comment.
type_jkind sometimes gets stuff other than an annotation. I don't think it's worth the archaeology here, especially because -allow-illegal-crossing is on the chopping block.
|
Thanks for the review so far! I've handled the comments above. There is a little more review then:
Thanks! |
|
@goldfirere Please review: |
| |}] | ||
|
|
||
| type ('a, 'b) t : value mod portable uncontended = { a : 'a; b : 'b } | ||
| [%%expect {| | ||
| type ('a, 'b) t : value mod uncontended portable = { a : 'a; b : 'b; } | ||
| type ('a, 'b) t : immutable_data = { a : 'a; b : 'b; } |
There was a problem hiding this comment.
This seems wrong - t should only cross linearity with 'a and 'b. Unless it's just the printing that's wrong? If it's just the printing that's wrong, could you add a test that demonstrates that?
There's more instances of this in the file, but I'm not going to comment on those.
| type b : value mod portable = { a : int; b : int } | ||
| [%%expect {| | ||
| type a | ||
| type b : value mod portable = { a : int; b : int; } | ||
| type b = { a : int; b : int; } | ||
| |}] |
There was a problem hiding this comment.
This test is no longer testing the thing it was meant to test. b is meant to have a type that is normally inferred to not be portable. So I think the ints should be replaced with a type that doesn't cross portability.
The same is true for most of the tests in this file. But maybe this isn't worth the effort of fixing, because:
- We plan to remove illegal crossing very soon, and I believe @glittershark plans to delete this file rather than incorporating it into the trust-me annotation tests.
- I see that you've added some tests where the inferred type does not cross.
| |}] | ||
| (* CR layouts v2.8: this should be accepted *) |
There was a problem hiding this comment.
It's very satisfying to see these crs go away
| type 'a t4_val | ||
| type t4 = M4.s t4_val | ||
| |}] | ||
| (* CR layouts v2.8: The appearance of [immutable_data] there is just wrong. *) |
There was a problem hiding this comment.
I'm pleasantly surprised by this output - I think this is right? In F4, s should have kind immutable_data with X.t. And then after the functor application, X.t is t = T, which is immediate. So M4.s really is immutable_data
| type 'a t4_val | ||
| type ('a : void) t4_void | ||
| type t4 = M4.s t4_val | ||
| |}] | ||
| (* CR layouts v2.8: The appearance of [immutable_data] there is just wrong. *) |
There was a problem hiding this comment.
For the same reason as the test in modules.ml, I think this is right
| | No_baggage, b -> b | ||
| | b, No_baggage -> b (* CR layouts v2.8: List concatentation is slow. *) | ||
| | Baggage (ty1, tys1), Baggage (ty2, tys2) -> | ||
| Baggage (ty1, tys1 @ (ty2 :: tys2)) |
There was a problem hiding this comment.
Is this a good enough excuse for use to create Misc.Nonempty_list? Feel free to tell me no.
|
|
||
| (** Map a function over types in [upper_bounds] *) | ||
| val map_type_expr : | ||
| (Types.type_expr -> Types.type_expr) -> (allowed * 'r) t -> (allowed * 'r) t |
There was a problem hiding this comment.
The impl is already polymorphic over lr-ness - may as well make the signature be too, even if it's not used.
| val round_up : | ||
| type_equal:(Types.type_expr -> Types.type_expr -> bool) -> | ||
| jkind_of_type:(Types.type_expr -> jkind_l option) -> | ||
| (allowed * 'r) t -> |
There was a problem hiding this comment.
The impl doesn't require the input to be a left - maybe remove that constraint from the sig?
| (* CR layouts v2.8: This is sad, but I don't know how to account for | ||
| existentials in the baggage. See doc named "Existential | ||
| baggage". *) | ||
| then Builtin.value ~why:Boxed_variant |
There was a problem hiding this comment.
We could probably make some cases happier by only doing this when there are existentials. But I don't think we have a compelling reason to do this yet, so that can be future work.
| (fun (lbl : Types.label_declaration) -> add_baggage ~baggage:lbl.ld_type) | ||
| lbls jkind | ||
|
|
||
| (* CR layouts v2.8: This should take modalities into account. *) |
There was a problem hiding this comment.
This is implicitly making the assumption that modalities can only strengthen a kind, not weaken it. Otherwise it would be unsound to ignore them.
I and @glittershark agree that it is currently true, and seems that it will be true for the foreseeable future. I just want to flag that if that were to ever change, this is unsafe.
| let jkind_of_type = type_jkind_purely_if_principal env in | ||
| let jkind1 = Jkind.round_up ~type_equal ~jkind_of_type jkind1 in | ||
| let jkind2 = Jkind.round_up ~type_equal ~jkind_of_type jkind2 in | ||
| Jkind.intersection_or_error ~type_equal ~jkind_of_type ~reason jkind1 jkind2 |
There was a problem hiding this comment.
I don't understand what's going on here, but an alarm bell is going off in my head because we're rounding up and then intersecting, which seems like it would accept things that it shouldn't. Is this intentionally permissive?
|
As a meta-point, I think someone should review that the review tasks @goldfirere assigned are exhaustive. That is, make sure all changes are actually getting reviewed. I think |
| let failure = Error (Violation.of_ (Not_a_subjkind (sub, super))) in | ||
| (* First try normal subjkinding, if the right-hand jkind has the right | ||
| shape. *) | ||
| match try_allow_r super with |
There was a problem hiding this comment.
I think this is redundant with the try_allow_r that happens axis-wise
| let baggage1 = Baggage.as_list bound1.baggage in | ||
| let baggage2 = Baggage.as_list bound2.baggage in | ||
| let modifiers = | ||
| Bound_ops.equal bound1.modifier bound2.modifier |
There was a problem hiding this comment.
Can't this be le, not just equal? (although this would only matter in the rare case of checking _ mod external_ with t <= _ mod external64 with t )
| Bound_ops.equal bound1.modifier bound2.modifier | ||
| in | ||
| let baggages = | ||
| List.compare_lengths baggage1 baggage2 = 0 |
There was a problem hiding this comment.
Maybe leave a comment about why you're not using List.compare so that this optimization doesn't accidentally get removed in the future.
| | Less | Equal -> | ||
| Ok { sub with history = combine_histories Subjkind (Pack sub) (Pack super) } | ||
| | Not_le -> Error (Violation.of_ (Not_a_subjkind (sub, super))) | ||
| let sub_jkind_l ~type_equal ~jkind_of_type sub super = |
There was a problem hiding this comment.
A special case that I don't think is being handled is when sub is has the min modifier with no baggage, in which case it's always successful. I'm not sure if this case would really get us much, but it seems cheap.
| in | ||
| let baggages = | ||
| List.compare_lengths baggage1 baggage2 = 0 | ||
| && List.for_all2 type_equal baggage1 baggage2 |
There was a problem hiding this comment.
There's redundant type equality checks happening between axes - avoiding so would presumably help performance. But I presume @glittershark 's upcoming change that transposes the representation will do this, so I guess we can leave it.
| Continue | ||
| { t with constr = Path.Map.add p (fuel - 1, args) constr } | ||
| else Stop) | ||
| | Tvar _ | Tarrow _ | Tunboxed_tuple _ | Tobject _ | Tfield _ | Tnil |
There was a problem hiding this comment.
Should Tunboxed_tuple be treated similarly to Ttuple? Or does it not have the same recursion issue?
| @@ -200,21 +174,34 @@ module Axis = struct | |||
| | Modal Contention -> "contention" | |||
| | Nonmodal Externality -> "externality" | |||
| | Nonmodal Nullability -> "nullability" | |||
|
|
|||
| let is_deep (type a) : a t -> bool = function | |||
There was a problem hiding this comment.
Maybe rename this to is_modal? I.e., our modes are by default deep, and given the current axes as samples, the distinction seems to be between modal vs nonmodal? Do we have imaginary axes violating that?
This is also a good place to insert a CR saying that Externality is in fact Modal and will be made so in the future.
This adds
with-kinds to the compiler.It is a very preliminary version. Importantly, you should not use an actual
with-kind in your code and expect anything to work. Instead, this just provides inferredwith-kinds, but that should be sufficient for looking through lists,options, and arrays.A rebase of this work (at https://github.com/ocaml-flambda/flambda-backend/tree/aspsmith/with-kinds-on-portable-stdlib) has been observed to build Base and Core, and this passes all the tests in the compiler testsuite. It is thus ready for review.
It is strongly suspected not to be performant enough for merging, though this fact has not been adequately assessed. I expect to follow this PR with another one to improve its performance. Search for an internal doc titled "Normalization for with-kinds" for more thoughts on how to do this. But nevertheless, I think this PR is now (Dec 24 '24) ready for correctness review.
Review is roughly by commit, as I enumerate:
narrow_to_manifest_jkindto useestimate_type_jkindinstead oftype_jkind_purely. I don't remember my incentive for doing so, other than my general animosity towardtype_jkind_purely(as documented in an internal doc titled "Let's kill type_jkind_purely"). You'll see some test case changes; please check these for reasonableness. The last commit undoes this change (restoring the use oftype_jkind_purely) along with a long comment explaining why and how to do better. The last commit also contains several other small changes, mostly in response to unboxed-records work. (Some of the changes are not from that; feel free to delegate review of some files to @liam923 or @riaqn.) Some of the changes involve differences in behavior between principal-mode and non-principal-mode; these differences echo differences elsewhere and will be addressed later. (We basically don't care so much about principal mode.)from_substfeature ofunify_varin favor of thein_subst_modecheck (which came temporally afterfrom_substbut serves the same purpose and is propagated further). The change was necessary withwith-kinds.with-kinds. Not anymore.with-kinds to unboxed records and includes the deletion of the reimplementation ofestimate_type_jkind.templatestest has already been approved by @lukemaurer. (This test is about parameterized modules.)univar_pairsin ctype.And that's everything.
Now to break down the review of the main payload. The high-level overview is that much of this code was actually written by @liam923 and @riaqn in an early version of
with-kinds. They should review. I break down where I have taken their code essentially as-is and where I have changed it (necessitating further review). The places where I took the code as-is do not need further review, as I reviewed the code as I adapted it. You can find your previous work at https://github.com/goldfirere/flambda-backend/pull/3/files.jane/doc: @riaqn. These are updates to the uniqueness documentation in light ofwith-kinds.parsing: @liam923. Just some comments.testsuite: @liam923. You're the most familiar with tests here -- as well as the expected use ofwith-kinds in base and core. I believe you probably already reviewedwith.mlwhile you were writing new tests.tools: @liam923. This is a tiny change. (The reason for the eta-expansion is to avoid the value restriction.)ctype.ml/ctype.mli: I think @riaqn. (I'm not sure exactly which of you did which pieces.)instance_parameterized_kind,instance_declaration,jkind_subst, andis_principalare unchanged from your previous work.estimate_type_jkindjust has a small tweak compared to previous work (but would benefit from quick review)type_jkind_purely_if_principalis unchangedconstrain_type_jkindjust uses a different approach to gettingtype_equalthan previously; pretty boring.check_decl_jkindandconstrain_decl_jkindhave been moved to the bottom of the file so that they could accesstype_equal(before I made the ref). Maybe this decision should be reversed.intersect_type_jkindand below are new; please review with care.includecore.ml: @riaqn. The mode-cross stuff could use your expertise (though looks straightforward). The change intype_declarationsis harder, but I already went over the basic idea with @ccasin (who agrees the approach is sound).jkind_axis.ml/jkind_axis.mli: @riaqn. This is very directly inspired by previous work, but I added a bunch more functions toAxis_collection.jkind_types.ml/jkind_types.mli: @riaqn. This is mostly boilerplate-y, but there is some stuff with left/right logic that you are the expert in.jkind.ml/jkind.mli/printtyp.ml: Some combination of @liam923 and @riaqn (please work this out).Bound.reduce_baggage, which is a completely fresh reimplementation ofreduce_boundfrom previous work.of_user_written_annotation_unchecked_levelare very close to prior work; compare the two to reduce review burden.add_portability_and_contention_crossingwere a bit tricky in order to try to get decent behavior from this feature.for_boxed_record,for_boxed_variantare new and deserve scrutiny. These functions power the inference ofwith-kinds; an error here could easily lead to unsoundness.round_upfunction is new; see usage sites for more context.sub_jkind_lfunction is horrid, but still needs to be sound. It will get improved later yet deserves a careful read-through here, too.mode.ml/mode_intf.mli: @riaqn. This is just some refactoring.predef.ml/predef.mli: Either @liam923 or @riaqn. This is basically all new (but easy).subst.ml: Either @liam923 or @riaqn. This was easier than prior work due to Use constant sorts in transl #3266.typecore.ml: Probably @riaqn. These changes are straightforward adaptations to the new types exposed byJkind.typedecl.ml/typedecl.mli: Not sure. I recommend either @liam923 or @riaqn take a spin, but if the going gets tough, let's loop in @ccasin. This file was hard, as you will see by the trail of comments I have left.typemode.ml/typemode.mli: Whoever did this the first time around. I basically just adapted the prior work here. Only light review required.misc.ml/misc.mli: Anyone. I guess this is what happens when Jane Street hires a Haskeller.datarepr.ml,typedecl_separability.ml,typemod.ml,typeopt.ml,types.ml,types.mli): Anyone. These are all small changes.Thanks, all!