Unboxed tuples

[ccasin]

This adds our first composite layout, products, and a type that uses it, unboxed tuples. There are two commits, the first is some middle-end fixes that will be reviewed in #2837 and can be ignored.

Known remaining issues

• The tests include an example of a value let rec that crashes closure conversion in the native code compiler. We should do something about this before merging this PR, but I'm still discussing with the middle end team. It's an odd example, because the value rec check today will never reject a let rec that's not actually recursive, and it seems we need to start doing that.
• Errors can be improved! Currently a kind error involving two products does not point to the component of the product that is the problem. Probably histories should become product histories to support that. I think this will be some work and we should plan to merge this PR in its current state (with respect to those errors) but improve them before moving unboxed tuples out of beta. I will make a ticket in our internal system for this.
• Modes: I've written (* XXX modes *) in some places where someone more expert on our mode inference should check what I've done.

Some notes about the design and implementation

• I've given sort variables unique ids. We considered this in the initial layouts PR, but I didn't think we needed them then because sort variables are in types and types have unique ids. But now that we have complex layouts, you can have multiple sort vars in a type, and the unique ids become very useful for debugging. Many tests change because we now print these ids instead of the old system for sort variables.
• I regrouped the statically allocated values in the sort module into some inner modules. We want statically allocated versions of consts, sorts, and sort options and it was becoming unwieldy/confusing (at least to me) to have them all in the same namespace. It's possible we should be doing dynamic memoization of products in some of these cases, but I haven't yet.
• Limiting use to beta: We've agreed to limit the use of unboxed products to beta until we've had a chance to do some more real-world testing. I've done that by doing an extension check at the places where we typecheck the relevant syntax (unboxed tuple expressions, patterns, and type expressions, and unboxed product kind expressions). This of course means you can try to slip in an unboxed product from a library, for which there is a backup check in typeopt, as has been our practice.
• We have discussed the possibility of splitting up the core implementation of constrain_type_jkind into multiple functions - one which checks layouts and traverses types deeply to handle products, and another which handles the rest of the kind and can be shallower. I have not done that. It was not necessary, and while this means the new implementation of constrain_type_jkind does some unnecessary checking of the other kind bits when dealing with unboxed products, it allows for (in my view) a pretty clean and understandable implementation of kind checking. It's possible we should split this up in the future, but I think that will require adjusting how we think about kind errors and histories, as right now they live at the level of the whole kind but the checks wouldn't be operating on whole kinds. Either way, we should probably leave that exploration for a future PR, as this one already makes enough changes to kind checking.

Review: @goldfirere

[goldfirere]

Nearly done with jkind.ml.

[goldfirere]

I was hoping to get further here before my vacation -- and I may return during some downtime if no one beats me to it -- but I wanted to post where I had gotten in case someone else wants to pick up.

I have reviewed:

• All the testsuite changes
• All files alphabetically from typing/jkind.ml to typing/patterns.ml
• typedtree.ml{i}
• types.ml{i}
• utils/misc.ml{i}

[lthls]

• The tests include an example of a value let rec that crashes closure conversion in the native code compiler. We should do something about this before merging this PR, but I'm still discussing with the middle end team. It's an odd example, because the value rec check today will never reject a let rec that's not actually recursive, and it seems we need to start doing that.

Its possible that there are places in the compilation of let rec where we use layout_letrec (which is Value) whereas we should be using the actual layout.
I think we can sort recursive definitions into three cases:

• Actually recursive definitions with non-value layouts should be rejected. The current compilation scheme cannot easily be modified to allow them.
• Definitions that are not actually recursive should be handled properly, which may require patching a few things in Value_rec_compiler.
• There is a special case for definitions that are not ultimately recursive but where the definition mentions a recursive variable (let rec x = let _ = x in ()). The handling for these is weird (it's the Constant case in Value_rec_compiler`), and I would argue that we shouldn't support that for non-value layouts.

The important part, I think, is to ensure that Value_rec_check doesn't misclassify as Static something that has non-value layout. Static implies that it can be pre-allocated using a scheme that only applies for (a subset of) values, so even though some non-value expressions could be supported through the Constant hack I think it is better to not support it, at least at the beginning.

[ccasin]

• The tests include an example of a value let rec that crashes closure conversion in the native code compiler. We should do something about this before merging this PR, but I'm still discussing with the middle end team. It's an odd example, because the value rec check today will never reject a let rec that's not actually recursive, and it seems we need to start doing that.

Its possible that there are places in the compilation of let rec where we use layout_letrec (which is Value) whereas we should be using the actual layout. I think we can sort recursive definitions into three cases:

• Actually recursive definitions with non-value layouts should be rejected. The current compilation scheme cannot easily be modified to allow them.
• Definitions that are not actually recursive should be handled properly, which may require patching a few things in Value_rec_compiler.
• There is a special case for definitions that are not ultimately recursive but where the definition mentions a recursive variable (let rec x = let _ = x in ()). The handling for these is weird (it's the Constant case in Value_rec_compiler`), and I would argue that we shouldn't support that for non-value layouts.

The important part, I think, is to ensure that Value_rec_check doesn't misclassify as Static something that has non-value layout. Static implies that it can be pre-allocated using a scheme that only applies for (a subset of) values, so even though some non-value expressions could be supported through the Constant hack I think it is better to not support it, at least at the beginning.

Thanks for this summary, @lthls. In the interest of keeping things simple, I am tempted to make a PR that just bans any pattern variable in a value let-rec from having a non-value layout. I think that considering the existence of layout_letrec, we probably intended to ban these and it's just a missing check. This would ban a few things that we could actually compile (like let recs that aren't actually recursive), but that seems like a small price to pay for a simple implementation and nice understandable rule.

What do you think?

[goldfirere]

A little bit more: ctype, btype, and all the files in typing up to and including printtyped.

[lthls]

Banning non-value layouts in recursive declarations seems reasonable.
If there is demand to support the non-recursive case, I can implement it (it's a simple matter of passing the layouts to Value_rec_compiler).

[mshinwell]

I rebased (my own branch of this) onto b22fb1a970c763952da11b188a471368747ba50d which made the flambda2 diffs go away. I then read the changes to bytecomp/, file_formats/ and lambda/ in that rebase, all of which are ok. I left one minor comment.

[riaqn]

I've reviewed the following files:

 ocaml/parsing/ast_helper.ml                               |   5 ++++
 ocaml/parsing/ast_helper.mli                              |   7 ++++++
 ocaml/parsing/ast_iterator.ml                             |  24 ++++++++------------
 ocaml/parsing/ast_mapper.ml                               |  27 +++++++++++-----------
 ocaml/parsing/depend.ml                                   |  18 +++++++++------
 ocaml/parsing/jane_syntax.ml                              |   6 +++++
 ocaml/parsing/jane_syntax.mli                             |   1 +
 ocaml/parsing/lexer.mll                                   |   1 +
 ocaml/parsing/parser.mly                                  |  41 ++++++++++++++++++++++++++++++++-
 ocaml/parsing/parsetree.mli                               |  23 +++++++++++++++++++
 ocaml/parsing/pprintast.ml                                |   1 +
 ocaml/parsing/printast.ml                                 |  13 +++++++++++
 ocaml/toplevel/genprintval.ml                             |   4 ++++
 ocaml/typing/subst.ml                                     |   9 ++++++--
 ocaml/typing/tast_iterator.ml                             |   3 +++
 ocaml/typing/tast_mapper.ml                               |   9 ++++++++
 ocaml/typing/typecore.ml                                  | 163 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 ocaml/typing/typedecl.ml                                  |  86 ++++++++++++++++++++++++++++++++++++++++++++++-----------------------
 ocaml/typing/typedecl.mli                                 |   1 +
 ocaml/typing/typedecl_separability.ml                     |   3 +++
 ocaml/typing/typedecl_variance.ml                         |   2 ++
 ocaml/typing/typemod.ml                                   |  10 ++++----
 ocaml/typing/typeopt.ml                                   | 100 ++++++++++++++++++++++++++++++++++++++++++++++++++++----------------------------
 ocaml/typing/typeopt.mli                                  |   4 ++--
 ocaml/typing/typetexp.ml                                  |  17 +++++++++++++-
 ocaml/typing/uniqueness_analysis.ml                       |  14 ++++++++++++
 ocaml/typing/untypeast.ml                                 |  10 ++++++++
 ocaml/typing/value_rec_check.ml                           |   6 +++++
 printer/printast_with_mappings.ml                         |  13 +++++++++++

I'm unconfident about typedecl.ml and typeopt.ml, which we will discuss via other channels.

[goldfirere]

Would it be helpful for me to review typedecl and typeopt?

[ccasin]

Would it be helpful for me to review typedecl and typeopt?

I believe @riaqn has reviewed everything remaining, but you are of course welcome to take a look!

I plan to clean this up this week.

[ccasin]

This PR is ready for final review and merging.

I have squashed all the changes in response to review down into one commit, mainly to make rebasing easier, and this has been rebased on current main. Tests suggested in review turned up a few issues, all of which have been fixed except one - see Test 11 in typing-layouts-products/basics.ml. That test is broken due to an issue in jkind checking that is orthogonal to unboxed products, and after discussion will fix it separately.

One open question is chamelon. If CI passes I think we are OK to merge, but probably some changes are needed to support minimizing programs involving unboxed products, and I will discuss that separately with @Ekdohibs.

@riaqn Please take the following steps:

• Look through all the unresolved conversations, and resolve them if you agree the current state of affairs is reasonable to merge. Some of them will lead to longer conversations, but I think there are no big outstanding questions that should block merging.
• Glance at the changes to the typechecking files in the commit that integrates the review feedback. You will see a few fixed bugs (e.g., I added some missing cases in parmatch.ml, and made a change to type_jkind_sub in ctype where previously checking whether a type has layout any (which should always succeed) could fail if the type had a product layout).
• Approve and merge.

[riaqn]

I reviewed the chagnes to all typing except jkind_*, and parsing. I think they are good to go.

[ccasin]

I have resolved all the outstanding conversations here so we can merge, but @goldfirere you will probably find it useful to go through and read the responses at some point.