Use constant sorts in transl

[goldfirere]

As discussed with @ccasin, all of the transl functions can really work over Sort.Const.t, not Sort.t. This PR makes this change.

Motivation: The second commit, which replaces Jkind.t with Jkind.Sort.Const.t in variant_representation, label_description, and record_representation. This actually was possible without the first commit, but there were a sad number of calls to Jkind.Sort.of_const to reconsistute the non-constant sorts for transl... so I wrote the first commit.

Review: commit-by-commit. The changes are very boring; it's the design change that's interesting.

• 1. f39bd0a changes the transl functions to work over Jkind.Sort.Const.t instead of Jkind.Sort.t (aka Jkind.sort). The there are two sad bits. (a) There are lots more calls to default_for_transl_and_get. Previously, we called this function only in Typeopt when we actually needed the sort. Now this function has to be called for every sort stored in the typedtree. I think this is OK, though, because though the function call is written more, it is executed either less or the same amount (previously, sometimes a sort flowed through multiple paths, and it had to be gotten more than once). It might be reasonable to object to this commit based on the new calls. (b) There is a sad little dance in typedtree because a function needs to deal with both constant and non-constant sorts. The dance is local, but regrettable.
• 2. 540cc23 changes the representations of structures to use Jkind.Sort.Const.t. This, in turn, is motivated by trying to use kinds as little as possible, because they're about to get a lot more complicated. But actually it's a nice change on its own.

If you like (2) but don't like (1) (reasonable! I'm not sure about (1) myself), you can check out goldfirere@ce8f169, which is a version of commit (2) without needing (1). It works. But see the number of of_const calls in translcore. These made me sad and is the concrete motivation for (1).

If you say to take (2) with the sad of_consts because that's better than (1), I won't push back.

Review: I'd love @ccasin to push back on the design. If he doesn't want to review the rest of the details, I'm sure @dkalinichenko-js could do so. I recommend looking at the commits separately.

[goldfirere]

I have rebased this to accommodate the fact that #3224 has been merged.

[dkalinichenko-js]

I'm up to review this if you want.

[ccasin]

Sorry - this has been behind review of Ryan's unboxed records PR on my stack. I hope to finish that today.

I'm broadly happy for @dkalinichenko-js to review this. But, question regarding the second commit: I believe we want, soon, to allow, e.g., record declarations to have fields with layout any, and check for representability just when actually needed by the program. How will that look after this change?

[goldfirere]

A good question. I think that moving to checking representability at construction would effectively remove the second commit. We won't be storing any sort information in these structures after that change, constant or no. Nothing in this patch makes the change you propose harder or easier, I believe.

[ccasin]

A good question. I think that moving to checking representability at construction would effectively remove the second commit. We won't be storing any sort information in these structures after that change, constant or no. Nothing in this patch makes the change you propose harder or easier, I believe.

Seems right. Or maybe this field becomes an option to optimize the common case where it is known at declaration time.

Anyway, I recall our earlier conversation and still have no objections to this direction if it works (as it seems to). So I think @dkalinichenko-js should review, including the questions about whether the first commit is a win. Thanks in advance, Diana.

[goldfirere]

Seems right. Or maybe this field becomes an option to optimize the common case where it is known at declaration time.

Yes, that sounds likely.

[dkalinichenko-js]

I don't think we should do (1). default_for_transl_and_get is a much more suspicious function than of_const, and we should keep the places it is called in to a minimum. Even if the number of calls stays the same, it becomes harder to keep track of them after (1).

[dkalinichenko-js]

goldfirere@ce8f169 seems reasonable.

[goldfirere]

I don't think we should do (1).

I'm fine with that conclusion, but

default_for_transl_and_get is a much more suspicious function than of_const, and we should keep the places it is called in to a minimum.

I pretty strongly disagree here. default_for_transl_and_get means "I'm done type-checking now; let's carry on with the best possible sort". It has to get called on every sort that flows through the type checker and is (to me) not at all suspicious. (A use in the type-checker would be very suspicious!) On the other hand, of_const takes a constant sort and injects it into the potentially-variable sort type, just to satisfy the type-checker. This constant-sort-that-looks-like-it-might-be-a-variable now needs to be gotten when used, and the of_const itself has to allocate a new node. So I find of_const to be somewhat sad.

So I just want to check that we agree on the reasoning before worrying so much about the conclusion (because perhaps as we discuss the reasoning, your conclusion might change).

[dkalinichenko-js]

On the other hand, of_const takes a constant sort and injects it into the potentially-variable sort type, just to satisfy the type-checker. This constant-sort-that-looks-like-it-might-be-a-variable now needs to be gotten when used, and the of_const itself has to allocate a new node. So I find of_const to be somewhat sad.

Yes, I find that unproblematic – of_const is injective and so does not lose any information. default_for_transl_and_get, on the other hand, does.

I pretty strongly disagree here. default_for_transl_and_get means "I'm done type-checking now; let's carry on with the best possible sort". It has to get called on every sort that flows through the type checker and is (to me) not at all suspicious. (A use in the type-checker would be very suspicious!)

I see. But uses of default_for_transl_and_get in lambda seem to me even more suspicious than uses in the typechecker. Why would the middle-end even know about sort variables in the first place?

Thinking through that, even though (1) creates more callsites for default_for_transl_and_get in lambda, it actually moves us closer to a future where the middle-end does not care about sort variables, and all defaulting is done in the translation part. So now I approve of (1). Your thoughts on eventually eliminating default_for_transl_and_get from lambda?

[goldfirere]

Your thoughts on eventually eliminating default_for_transl_and_get from lambda?

Never? In theory, there could be another pass through the AST after type-checking and before translation; this pass would remove all sort variables. This would make great sense, and do a better job separating concerns. (GHC has this pass.) But it means reconstructing the entire AST! And it's so easy to do as a little initial step in translation.

One annoyance here is that the lambda/ folder really contains at least two different things: the lambda language (part of the middle end) and the translation from typedtree into lambda (the interface between the front and the middle). I don't see a big problem with the translation being aware of aspects of the type-checker -- though I agree that having a separate pass to do defaulting would be cleaner in this regard.

So in some sense this patch brings the call to default_for_transl_and_get right to the boundary between the type-checker and the middle-end.... it's just perhaps on the wrong side of that boundary. But still better than deep in the bowels of Typeopt! (Recall that Typeopt is actually part of lambda, not the type-checker. It's just in the wrong directory.)