with-kinds

[goldfirere]

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 inferred with-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:

• 1. 8814e2c56173156b5ba4b55873d999458bab5c55 (first commit) and 25eadb9eb0a5a0ced02456283bd4222be1635eb7 (last commit): @rtjoa (possibly in consultation with @ccasin). The first commit changes narrow_to_manifest_jkind to use estimate_type_jkind instead of type_jkind_purely. I don't remember my incentive for doing so, other than my general animosity toward type_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 of type_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.)
• 2. 53b02d35b9e8513b1db08795d6b1b39cad3b25a3: @ccasin. This just deletes some code without affecting the testsuite. The code got in my way in a later patch.
• 3. 0666ec87ec3b4d80e01da506718eb9647b8222f0: @ccasin. This removes the from_subst feature of unify_var in favor of the in_subst_mode check (which came temporally after from_subst but serves the same purpose and is propagated further). The change was necessary with with-kinds.
• 4. 3274c88eaebec2ad1c62422c4748b750b77a9f63: @ccasin. We were doing a check on an uninstantiated type (essentially, the master copy), which caused trouble with with-kinds. Not anymore.
• 5. 4ab10754812bce8aac26ff4436e625656f17dbdb: @liam923. This is straightforward deletion of dead code.
• 6. 8c85229c20e7c04b082f003c18e2d89ffd81a567: @liam923 and @riaqn. This is the main payload. I have broken it down below.
• 7. 67700378aef9039e2a1079b1307605cab7b8d2da: @rtjoa (consulting with @ccasin or me as necessary). This adapts with-kinds to unboxed records and includes the deletion of the reimplementation of estimate_type_jkind.
• 8. 259365684d7417e10e87e277033aac6f7b61eaa4: @liam923. This just updates test output. The change to the templates test has already been approved by @lukemaurer. (This test is about parameterized modules.)
• 9. c0a9d500bda0ce0c544d5d251d54180aecdad512: me, actually. @liam923 wrote this commit adding lots of tests, and I have already reviewed it.
• 10. f498428c3cfb7b4cd44eb93ebe0c447d5d5bdea9: @liam923. This is the result of my review for the tests.
• 11. 57387ff66836df7ec6591372eb9c2e760bd104ef and a20a171afec9f1e172f1b22d863327e656ef0203: @lpw25 (or possibly @ccasin). This is a test-case/fix pair that changes the use of the global mutable state of univar_pairs in ctype.
• 12. 52da5d6bc7b4adec66b80bb3029ccc21d05c569b and 97650466a699460a61cb42564ffd17245cc6818a: @liam923. This is another test-case/fix pair to fix a bug observed when building base and core.

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.

• In jane/doc: @riaqn. These are updates to the uniqueness documentation in light of with-kinds.
• In parsing: @liam923. Just some comments.
• In testsuite: @liam923. You're the most familiar with tests here -- as well as the expected use of with-kinds in base and core. I believe you probably already reviewed with.ml while you were writing new tests.
• In 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, and is_principal are unchanged from your previous work.
  • estimate_type_jkind just has a small tweak compared to previous work (but would benefit from quick review)
  • type_jkind_purely_if_principal is unchanged
  • constrain_type_jkind just uses a different approach to getting type_equal than previously; pretty boring.
  • check_decl_jkind and constrain_decl_jkind have been moved to the bottom of the file so that they could access type_equal (before I made the ref). Maybe this decision should be reversed.
  • Changes in intersect_type_jkind and below are new; please review with care.
• includecore.ml: @riaqn. The mode-cross stuff could use your expertise (though looks straightforward). The change in type_declarations is 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 to Axis_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).
  • The biggest piece needing careful scrutiny is Bound.reduce_baggage, which is a completely fresh reimplementation of reduce_bound from previous work.
  • Changes to of_user_written_annotation_unchecked_level are very close to prior work; compare the two to reduce review burden.
  • Changes to add_portability_and_contention_crossing were a bit tricky in order to try to get decent behavior from this feature.
  • Changes to for_boxed_record, for_boxed_variant are new and deserve scrutiny. These functions power the inference of with-kinds; an error here could easily lead to unsoundness.
  • The round_up function is new; see usage sites for more context.
  • The new sub_jkind_l function is horrid, but still needs to be sound. It will get improved later yet deserves a careful read-through here, too.
  • Other changes in the file also deserve a read, of course, but they should hopefully be not too hard.
• 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 by Jkind.
• 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.
• Other files (datarepr.ml, typedecl_separability.ml, typemod.ml, typeopt.ml, types.ml, types.mli): Anyone. These are all small changes.

Thanks, all!

[github-actions]

Parser Change Checklist

This PR modifies the parser. Please check that the following tests are updated:

• parsetree/source_jane_street.ml

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]

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.

[liam923]

@goldfirere Please review:

• 59ff14b

[liam923]

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 jkind_intf, for example, did not get assigned anywhere (I have not reviewed that file).

[goldfirere]

• Just pushed 4473fb80b8ade4e09f4bb3a62d1e0ecd4f4d9ace, which undoes a previous commit, as reviewed by @ccasin

This reversion was motivated by trying to post the change upstream and pushback there. It turns out it's unnecessary.

[goldfirere]

@liam923

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 jkind_intf, for example, did not get assigned anywhere (I have not reviewed that file).

Decent point. Anyone is welcome to double-check this. But I should not: jkind_intf did not change in this patch, so there's no evidence I actually missed anything. :)

[goldfirere]

• 5d07d15365b154a1d94379f134bffc1c2609b129 Review responses from @liam923
• d87cfbf7fe5fa674965cfd0c8b82e50860e1beae Review responses from @riaqn

[goldfirere]

• e0320004f375025d8d7985376a60ce628181fd15 @liam923

[goldfirere]

OK. I believe I've responded to all comments up until now. Back to reviewers.

[liam923]

I found a valid program that gets rejected by these changes:

module rec Gadt_option : sig
  type 'a t = T : 'a option -> 'a t [@@unboxed]
end = Gadt_option

and Also_gadt_option : sig
  type 'a t = 'a Gadt_option.t
end = struct
  type 'a t = 'a Gadt_option.t
end

[liam923]

As discussed in person, existential unboxed gadts allow a type to escape its scope as the existential will then appear in the with-bounds.

[liam923]

I found a valid program that gets rejected by these changes:

module rec Gadt_option : sig
  type 'a t = T : 'a option -> 'a t [@@unboxed]
end = Gadt_option

and Also_gadt_option : sig
  type 'a t = 'a Gadt_option.t
end = struct
  type 'a t = 'a Gadt_option.t
end

• I've resolved this in commits 0ca4ba4 and 1835b5d. @goldfirere please review.

[lpw25]

The change in a20a171 is fine, but I would like to understand the bug it fixes better.

[lpw25]

Why is the test being changed from a class to an array?

[goldfirere]

I accidentally added the test in a different commit. But the test didn't actually pass -- that code won't even parse (because it's missing the =). So the change you see here is just fixing the test to parse, and then showing that it isn't accepted.

If memory serves, this is a reduction of a problem that arose during bootstrapping.

[lpw25]

The change in the commit is fine, but do we understand how it fixes the problem? I want to be sure we are missing another place where it should be resetting univar_pairs, or nested calls to functions that aren’t reentrant.

[goldfirere]

I went through all uses of univar_pairs to use the protect-refs approach on all of them, not just the specific places that caused the bug. I sadly don't now remember which specific one it was. I suppose I could remove the fix and re-debug if you wanted more information.

[goldfirere]

About to rebase en route to merging. State before the rebase is preserved at https://github.com/goldfirere/flambda-backend/tree/with-kinds-before-rebase