(This is a "thinking out loud" remark with no actual change suggestions for the present PR, apologies for the noise.)

In this function I find the use of Type_immediacy.Unknown perplexing, because that immediacy is supposed to mean "we don't know whether the type is immediate or not" (it is the immediacy of an abstract type with no immediacy annotation on it), but we use it here for types that we know are not immediate. I would rather expect a Type_immediacy.Never value in this case.

I vaguely remember that I proposed such a "not immediate" immediacy to @stedolan in one of the earlier attempts (in the context of a fairly different approach to computing and checking immediacies), and that he was not convinced. I still think that it would be more natural than the code we write here -- or in other parts of the immediacy computation.

On the other hand, having this should not be a requirement for the present PR, whose scope is to make the computation of immediacy "on-demand" rather than store it for each type. I am not suggesting that it must be added now, I think it could be something to consider for another PR.

Currently immediacies form a lattice

Immediate <= Immediate64 <= Unknown

and we would have instead

Immediate <= Immediate64 <= Unknown
NonImmediate <= Unknown

I agree it would great to have a way to record that types are never immediate.

In addition to clarifying this code, it could be a performance win - as you observed below, the immediacy recorded in type kinds is an upper bound, so when we see Type_immediacy.Unknown on a type abbreviation we sometimes expand the manifest to check whether the upper bound was conservative. This is potentially expensive, and could be skipped if we had a way to record types were NonImmediate even after substitutions. We've been considering different designs for this in the context of our "unboxed types" prototype (which essentially just expands the lattice you suggest with still more options - different "layouts"), but haven't settled on anything and plan to revisit it in the future.

I find the logic here a bit strange. One may think of type_immediacy_head as computing the immediacy of a type constructor, but its result is actually incorrect on unboxed types, which are not taken into account in kind_immediacy. So if we get a failure, we try again after calling `get_unboxed_type_represeentation.

Two questions:

1. Why not always get the unboxed type representation first? Performance reasons, I suppose: we want to avoid expanding abbreviations, because abbreviations already carry correct immediacy information in their kind.
2. Why not have kind_immediacy handle unboxed datatypes, so that type_immediacy_head returns the correct result for all types? Would we still need a fallback in this case? What would be the downside?

Why not always get the unboxed type representation first?

You are exactly correct - this is for performance reasons. get_unboxed_type_representation is potentially expensive, so in the case of a Tconstr we first look at the kind and see if it yields a definitive answer. If not, we perform the expensive expansion and unboxing.

This optimization was already present in the previous version of this PR, but it was implemented by a recursive call in check_type_immediate in the case we needed to call get_unboxed_type_representation. That approach was somewhat confusing, so here I've incorporated a suggestion from @lpw25 from that PR to eliminate the recursion by breaking it into two functions (check_type_immediate and type_immediacy_head).

The intent, then, is that type_immediacy_head is a cheap look at the "head" of the type, which check_type_immediate tries and then calls get_unboxed_type_representation if it doesn't provide a definitive answer.

Why not have kind_immediacy handle unboxed datatypes, so that type_immediacy_head returns the correct result for all types?

kind_immediacy may return an approximation in two cases: unboxed types, and abbreviations (because the immediacy recorded on Type_abstract is a conservative upper bound, as you observe elsewhere). As the fallback in both cases is the same (check_type_immediate calls get_unboxed_type_representation), it seemed cleanest to leave the unboxing logic there.

An alternative design would be to duplicate more of the logic of get_unboxed_type_representation here. In particular, one advantage would be that we could check whether we have a definitive immediacy after each recursive step of expansion and unboxing. But as this function and its fuel parameter are somewhat unfortunate, and it sounds like there are medium term plans to replace it, my instinct is not to do this.

So, to summarize, I do think we need some fallback in any event to deal with abbreviations, and it therefore seems cleanest not to complicate kind_immediacy. But let me know if you disagree. And in any event the situation should be documented - I'll add a comment if that sounds reasonable.

I find the current state disturbing: there is a notion of "the immediacy of a kind", which would be an inexact approximation of "the immediacy of the type", but it is not what kind_immediacy currently computes. But it is not so simple to compute the "right" thing (as I suggested earlier) because it the case of unboxed datatypes we would need to recursively call type_immediacy_head.

In the short term, I thing maybe you could just add a comment to point out that kind_immediacy is incorrect on unboxed datatypes.

I have changed the name to kind_immediacy_approx and added a comment to the mli.

Note: there is a non-obvious design choice being made here, which is that abbreviations (with use Typ_abstract kind with a Some ty manifest) will carry an immediacy. One may think that it is not necessary to store an immediacy for abbreviation as it can always be computed on-demand from the definition, and only "truly abstract" types without a manifest need an immediacy. (If we wanted to go "full on-demand" we would consider that.) The current state is a compromise, which is fine with me. It may also work better in presence of type constructors that are not fully abstract but whose definition is not in the environment / has been forgotten.

But: if I understand correctly, sometimes the information in this 'immediate' field may be stale / incorrect / a pessimistic approximation. (Otherwise we would not need the fallback logic in this case in check_decl_immediate.) I think that this happens in the functor-instantation scenarios that were discussed in the previous iterations of the PR, where currently the computation of variance and other type properties is not redone after substitution.

I think this should be documented: the immediacy information in the kind here may be an imprecise approximation of the immediacy of the manifest (when available), which is the "true" immediacy of the type.

Yes. I think we can end up in the conservative approximation situation even without functors (e.g., type 'a t = 'a is not immediate, but int t is). I've added a comment mentioning this and directing readers to the original motivating examples for details, but let me know if it's not quite what you wanted.

here again, we would not need this case if kind_immediacy worked correctly with unboxed datatypes, right?

Agreed - I guess I'd say there's a tradeoff, either we perform this check here, or check_type_immediate will potentially perform it twice (once in kind_immediacy and again when we fall back to get_unboxed_type_representation).

One awkward thing about this function is that there is code to "check" the declaration error cases in three distinct places:

1. the one for the unboxed attribute above
2. the one for the immediacy attribute here
3. the one for constraints below

Case (3) is fairly different in nature, but for cases (1) and (2) it is annoying that there is no common structure to the placement: (1) is placed right when the attribute is accessed, while (2) is placed after a bunch of non-trivial logic. There is an explanation (the check (1) is self-contained from the information already there, the check (2) requires building more of the declaration to make sense), but the code remains slightly inconsistent. If I was adding support for yet another kind of attribute, where would I put the checking code? "In a random place that works" is what the current code says.

My suggestion:

• move the logic of both checks (1) and (2) to auxiliary functions, verify_unboxed_attr and verify_immediacy_attr or something
• call both those functions at the same place in the code, for example at the current point (2) or after the let decl = ... in declaration.

I think this would make the code both more readable and easier to extend.

Agreed - that does sound better. I'll take a stab at this tomorrow.

I made the change you suggested. However, while doing so, I realized there remains an issue. In particular, this PR will reject the following declaration which is accepted by current ocaml.

type t = { x : int } [@@unboxed] [@@immediate]

This behavior is present in the previous iteration of this PR (#10041) but I suppose was not noticed at that time. As the issue is that kind_immediacy does not traverse through @@unboxed, I feel this somewhat vindicates your unhappiness with that function :).

I can think of a few solutions. The most obvious is to rename kind_immediacy to something like kind_immediacy_approx, and write a new kind_immediacy that does unbox things. I think this new function would need to call get_unboxed_type_representation if it sees an unboxed type - unboxing just one level is potentially insufficient. And it's possible the check needs to be moved later in transl_type_decl to accommodate mutually recursive or circular types (but I haven't thought that through yet). But I thought I'd get your opinion before implementing something.

Ah, good catch! (If you haven't done this yet, you should add the example to the testsuite.)

I agree with your suggestion to rename kind_immediacy intokind_immediacy_approx to make things more obvious. This will encourage us to consider this issue for each callsites, which we initially forgot to do ourselves.

Regarding how to fix this: my naive reaction is that we were wrong to call only kind_immediacy here and should have called the proper immediacy-checking function that uses the backtracking behavior, check_decl_immediate. Is there a reason that we cannot do this at this step, on the decl below? (Maybe the declaration is not fully-formed or not already in the typing environment or something, or we end up trusting the annotation before checking it?)

OK, I've pushed a possible fix. Here's my thinking:

We can not perform the kind check in transl_declaration. The issue is mutually defined types like:

type t = { x : s } [@@unboxed] [@@immediate]
and s = int

Checking that t's kind is compatible with the [@@immediate] attribute requires access to s's manifest, but the environment used for transl_declaration doesn't have accurate manifests for mutually defined types. This declaration is accepted by today's OCaml, so we don't want to reject it.

So we must perform this later - after the call to update_type in transl_type_decl. It seems sensible to put it with the other checks in that function after the ill-formed abbrevs check.

I've done that now. So in transl_type_decl we simply copy the immediacy attribute into the kind (for the abstract case), and we check it later. Here I describe why I think the check I've added is sufficient, in combination with check_coherence:

• We might have an [@@unboxed] type, in which case we call check_type_immediate on the inner thing. This inner thing might be an mutually defined abstract type whose annotation we have trusted, but in that case its manifest is checked by check_coherence later.
• Otherwise, we just use kind_immediacy_approx. The two cases where this is innaccurate are unboxed types (already handled) and abstract types, which are either purely abstract (fine) or abbreviations (checked by check_coherence).

The last question is whether check_coherence itself can be trusted. In particular, it checks that the manifests of abbreviations marked [@@immediate] are actually immediate, and the manifest may mention other abbreviation from the mutually recursive group. But this is fine, because their manifests will also be checked. And if there is a cycle, it's fine to treat all of them as immediate.

One consequence is that this declaration is allowed by this PR but is rejected by current OCaml:

type t = { x : s } [@@unboxed] [@@immediate]
and s = t [@@immediate]

This seems fine. Unfortunately, this similar declaration is not allowed, and could be:

type t = { x : s } [@@unboxed] [@@immediate]
and s = t

The difference is that in the former case s's kind records it is immediate, hitting the fast path of immediacy checking, while in the latter case we must expand, which runs out of fuel. This seems acceptable, if unfortunate, to me. But we can revisit the design if you disagree (I think it can be fixed, but at some cost in the complexity of the immediacy checking code, which doesn't seem worth it for such a silly type).

I find the new definition harder to read than before. It comes from previous design iterations of this PR, which had functions to check whether a given type satisfied a given immediacy, but no function to actually compute the immediacy of a type. But this is not the case anymore. Could we write the following?

let is_immediate env ty =
  match Ctype.(type_immediacy_head env ty) with
  ...

?

(I think this would require tuning type_immediacy to work correctly on unboxed types, as suggested in another comment.)

Interesting! I found the old version confusing (particularly, is_immediate seemed an odd name for a Type_immediacy.t -> bool).

I think we still do not have a function to calculate the exact immediacy - as described above the issue is not just unboxed types but also the approximation in the kind for abbreviations. We could add such a function - an analogue of check_type_immediate that returns the immediacy. My instinct is that this would be unnecessarily duplicative if it's only used in this one place, but I'm open to other opinions.