Add value kinds on blocks

[chambart]

This PR adds one more case on the Lambda.value_kind type: Blocks, and populates it when the type of a variable is obviously a block.

This is not used in the compiler, but is useful for flambda2. In particular it helps in some complex unboxing situations.

Since types could be quite large and to avoid problems with recursive types that wouldn't be detected by the crude check, there is a fuel counter to prevent producing deep value_kind. In practice there isn't too much information loss by keeping that limit low as most of the time when accessing deeply nested structure, there would be multiple points with type annotations, allowing to recover the full type where it is needed.

I'm not completely sure that the Transient_expr thing is correct or that it is the way it is supposed to be used.

[lthls]

Note: the scary Transient_expr stuff has been removed (it wasn't doing what we wanted anyway).
We would still like a review of the code in typeopt to compute value kinds from someone with knowledge of the type-checker.

[garrigue]

The code in Typeopt looks fine to me.
It could of course do more, but at least what it infers seems correct.

On a side note, I am bit surprised that scrape_ty calls correct_levels for every expansion. This should not be strictly needed (type definitions in the environment are supposed to only contain types at generic level), but maybe it's better to stay on the safe side.

[gasche]

Note that the call to correct_levels has been linked to performance issues with the generalized usage of scrape_ty. It was changed recently to be used only on Tconstr nodes rather than all types, for performance reasons: see #8776 and #10624.

[gasche]

I'm disheartened by the addition of fuel in yet another place. Fuel in general marks that we gave up on understanding the termination properties of our algorithms, and I suspect that having fuel in more places is a form of technical debt that we are building up. Some remarks on this.

Doing without fuel?

In #10479 we propose to rewrite get_unboxed_type_representation to avoid fuel. It may be the case that the same technique lets us do without fuel here -- I'm not sure which are the situations where your fuel is necessary for non-termination. The consensus on #10479 is that we want to merge it eventually, but it still requires more work in particular to measure the performance impact, and I don't have time to push on this right now. So I'm not suggesting that the present PR should wait on #10479, but I would prefer to understand whether it's the same sort of non-termination we are talking about, or something different, etc.

Factoring the code?

There are many analyses in the compiler that work on the type expressions -- they all require termination control due to cyclic and/or recursive types, and that logic is subtle. We could think of factoring the termination-control as a reusable service, but could we also factor the analysis code? This would also be useful for our work-in-progress on constructor unboxing, where we compute the "shape" of datatypes in a way that seems related to the present analysis (we approximate blocks by their tags, with no information on the leaves except eventually the arity, but we have a more fine-grained approximation of unions, keeping a set of tags). Is there a mother-analysis that could be implemented once, and then partially-erased to derive simpler approximations?

Explaining the code

What's above are what-ifs for the medium term. In the short term, if we are to have another kind of fuel in the compiler codebase, could you please explain in comments:

• what the fuel is for (what is the recursive structure of the function, and what are the known sources of non-termination?)
• how the fuel limit was chosen?

Different kinds of fuel

There seems to be two different usage modes of things called "fuel" in the compiler:

• One notion of fuel is only present to avoid non-termination, and avoids infinite traversals on circular objects. We typically choose a somewhat-high fuel limit (1000?) to accept all human-written programs, even large ones; we never expect the fuel limit to be reached on natural code. This is the sort of fuel used in get_unboxed_type_representation.
• One notion of fuel is used to avoid combinatorial explosions in traversal time or space, in situations where we have decided to approximate the final result. We typically choose a low fuel limit (10? less?), and we expect the limit to be reached in typical usage of the compiler. This is the sort of fuel used for wildcard explosion during pattern-matching typing in typecore.

(In both cases, tuning of the fuel limit is important for performance, even though the limits are very different.)

I think that we should be careful to distinguish those, and keep track of which is which. Ideally we would even use different names. For example we could use fuel only for the first situation (avoid non-termination), and cutoff or depth in the second situation (avoid combinatorial explosion).

I'm not sure that I understand, from quickly looking at the code, which of these two sorts of fuel is being added here. It may be that the fuel is doing both things at once. (The combinatorial-explosion fuel can always be used as termination-control fuel due to its low limit, but the converse is not true.) It might be enlightening to actually distinguish two kinds of fuel in the same process, to clarify the situation.

[gasche]

(cc @stedolan and @lpw25, who looked at #10479 and might by now have developed similar deviant interests in fuelology.)

[lthls]

The fuel variable might have been named depth here (so fits better with your second case). We know that without a limiting factor we could loop forever (i.e. on type 'a t = T of 'a * 'a t), but more importantly most of the time we're only interested in the "head" shape of the block so it's better to stop quickly (in addition, no sharing is done with these block shapes so we could end up allocating a lot if we went deeper).
The current code uses an initial value of 2, which means that we go one step further than strictly needed, but this could still be useful in cases like x.foo.bar, where no variable would hold the shape of x.foo.

[gasche]

Out of curiosity: why support x.foo.bar but not x.foo.bar.baz?

If we were serious about the property that we only care about "head" shapes, this could be made clear in the types (type value_kind = Flat of flat_kind | Block of .. * flat_kind list; or possibly polymorphic variants to avoid the Flat constructor), and then the code would be written without fuel/depth, but an auxiliary function that only computes flat shapes.
But if I understand what you are saying, having depth=2 is just a natural choice for the approximation, not a strong/structural property of the system, so maybe the current, more flexible presentation is better.

[chambart]

Is there a mother-analysis that could be implemented once, and then partially-erased to derive simpler approximations?

If it is possible for other analyses, I'm all for it. We don't need something much more complex than that for a first version, but if is there is something to expose the shape of all kinds of value, we can use that.

As to which fuel/depth value to use as @lthls said, it is a trade-off between cost and benefit. We don't expect many situations where more than a depth 2 would be useful, so it might not be worth doubling the cost for those rare cases. While I did notice some normal examples where 2 was required. So this is very heuristic. If the representation was shared in memory between multiple annotations, it would be ok to build something really deeper. Otherwise, for most situations depth 1 would be sufficient with also an annotation on the getfield, but that would not be always sufficient.
We might later want to increase that limit for some contexes. In particular to generate optimized versions of polymorphic comparisons.

The general type traversal is not going to be doable soon, so this is not an option right now. What would you suggest changing on that code for it to be ok ?

[gasche]

I suggested doing the "Explaining the code" part for now. (Note: I won't be able to do an actual review on the patchset before a few weeks, so please don't count on me for the approval.)