Hm.

In general I'm not too excited about the idea that we don't compute correct signatures for our types and modules, and that we will actually compute their static properties at the use-site rather than fix the problem. In theory I would prefer fixing the problem (and have a correct eager computation). In practice I understand that it may be difficult to do so (our recent stint with merge_constraint, see for example #9623, has shown that such changes can be painful).

Now, let's consider how such an on-demand check would be best implemented. I must say that I am not a-priori convinced by your approach. What your PR do is to first perform the current "eager" computation (using modularly-computed signatures), admitting that it is incomplete, and then at the use-site perform a "lazy" computation if the eager result is not good enough for the use-site needs. I must say that I find this a bit complex/redundant.

Here is an alternative proposal:

• Add a new immediacy Never (or the clearer Not_immediate), that is used when we know that the type is not immediate.
  Always/Immediate and Never/Not_immediate answers are stable by substitution,
  Unknown is used when we don't know a stable answer.
  (I think that Always_on_64bits should be interpreted as Not_immediate on 32bits rather than Unknown.)
• When computing immediacies, expand type constructors exactly when their immediacy is Unknown.

I believe that the end-result would be the same as with your system. More precisely:

• The strategy of trying to expand is only useful for truly-unknown results, so successful expansions in your check would always correspond to expansions with my proposal.
• In fact, my intuition is that failures-leading-to-expansion in your check only occur when we expect an immediate result (obviously checking against Unknown is not going to expand, but also unnecessary) and immediacy is Unknown, so in fact all expansions in my proposal may correspond to expansions in your check.
• The more precise immediacy information means that my proposal may expand less in various cases (type 'a t = int * 'a I guess?).

Regarding eager vs. lazy: I think static properties are often computed lazily in the typechecker, and this mechanism of expanding abbreviations to avert an error is fairly widespread. For instance, if checking well-formedness of the type foo t where type 'a t constraint 'a = int, we do not precompute whether foo = int, but expand as needed.

In fact, I suspect that in the cases where we do precompute static properties, there are likely to be bugs such as this one lurking. For instance, I just noticed this issue with variance computation (I'm not sure whether this is a known issue):

# module type T = sig type 'a t type 'a s = 'a t end;;
module type T = sig type 'a t type 'a s = 'a t end
# module F (X : T with type 'a t = 'a) = struct type +'a foo = 'a X.s end;;
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be covariant,
       but it is invariant.

Here, X.s is not recognised as covariant, even though it is equal to the covariant X.t.

I suspect that correctly computing static properties eagerly would require some sort of cache invalidation mechanism for use during substitutions and the like, which sounds complicated.

Regarding the alternative proposal: I find this one more complicated, not less! In my version, type constructor immediacies are sound overapproximations of the actual immediacy, used to avoid extra expansions. In yours, you're additionally caching negative information (Not_immediate), but I don't think that buys you very much.

Also, I don't think this proposal works well with more than two possibilities. There are currently three, so this case goes wrong:

module type T = sig
  type s [@@immediate64]
  type t = s [@@immediate64]
end
module F (X : T with type s = int) = struct
  type i = X.t [@@immediate]
end

Here, your algorithm says that nothing is Unknown: all types have an immediacy declaration. However, the definition of type i fails, as the immediacy of X.t is Always_on_64bits, not Always, despite X.t being equal to int.

In my algorithm, the immediacy is only ever an over-approximation, and substitutions / refinements / etc. can only ever lower immediacies, in the order:

Always <= Always_on_64bits <= Unknown

So, my algorithm checks type i by checking X.t against Always. Since X.t is merely Always_on_64bits, it expands X.t to X.s, and then the check succeeds.

(Thinking out loud.) Well obviously type t [@@immediate64] has an immediacy that is not robust to substitutions, so it should not be Immediate nor Not_immediate. You are completely correct that if we want to have precise immediacy information, we would need to represent this as a partially-unknown immediacy. Maybe the correct approach in this direction would be to carry upper and lower bounds around, as we do for variances. We have "concrete immediacies" Immediate, Immediate_on_64bits, Not_immediate, and immediacy information is a coherent set of concrete immediacies. We expand whenever the immediacy of a constructor is not tight (not a singleton).

Right, that would definitely work. We could annotate types with an interval [l,u] of immediacies, so that no matter what substitutions later occur, the interval can only shrink. For some types (e.g. int, string), we'd have a singleton interval (one where l=u), so we'd know there's no more information to learn.

When we need to check an immediacy constraint a <= b, where b is the annotation the user wrote (e.g. [@@immediate64]) and a is the immediacy of some type expression which we know lies in the interval [l, u], then we can do the following:

1. If u <= b, then the check passes (with no expansion needed)

2. If b does not lie in the interval [l, u], then the check fails (with no expansion needed)
   Particularly, this can occur if l=u (for instance, a is string) and b <> u.

3. Otherwise, b lies somewhere in the interval [l, u] so we need to expand the type and try again, or fail if it cannot be expanded.

My proposal here can be viewed as a special case of this algorithm, where the lower bound l is always the least immediacy (in other words, only information about upper bounds is tracked). This means that case (2) above is unused.

The lack of case (2) means that if l = u and b < u, then an extra expansion is performed. For instance, my algorithm will do one extra expansion before rejecting this signature:

type s = string
type t = s [@@immediate]

However, this extra expansion can only occur right when an immediacy error is about to be produced, so I'm not sure what we win by avoiding it.

Another special case of the general algorithm (which I think is closer to what you have in mind) is that we could restrict intervals to always be of the form [_|_, u] or [u, u] - that is, either an upper bound or a singleton.

This would be less complicated than the full interval approach, but would still avoid some expansions-before-errors. It's still more complicated than the upper-bounds approach, though.

The algorithm I had in mind has no clever "check" mode (checking is just inferring the immediacy and verifying that it is a subset of the expected immediacy), and "inference" works like this:

• if we have a concrete datatype, infer a precise "concrete immediacy", and return it as a singleton
• if we have an abstract type, possibly with attributes, return the appropriate set
• if we have a type constructor:
  • if its type immediacy is a singleton, return it
  • if it is not a singleton, try to expand the type constructor, using its immediacy as a fallback

@gasche I find your suggested approach much harder to think about than Stephen's, and it seems to result in doing more expansions too. Could you expand on why you think it is better?

There are two things that I don't like with this approach:

1. It introduces two ways to compute immediacy, one being an "approximation" and the other one being precise.
2. The semantics of expansion is not defined in terms of the value we compute and its properties, but the expectation we have, and the failure scenarios. To me this is the equivalent of backtracking during type-checking: the semantics we give to "immediacy" is "well try that, and if that fails do that other thing". I don't like this; I would like a definition of what immediacy is that does not involve failure/backtracking.

My proposal comes from studying Stephen's approach to understand when the current scenario falls short. It is not perfect (it could be made more precise by using different, yet more precise forms of immediacy), but it avoids the criticism above and I think it would work as well as Stephen's approach in practice. How it avoids the criticisms above:

• It doesn't use two different ways to compute immediacies, there is only a single computation.
  (We distinguish results that are "precise" and those that are "imprecise", so the notion of approximation is not completely gone.)
• The semantics of expansion is related only to intermediate results of the computation (we expand the type synonyms whose immediacy information is imprecise) rather than the request/expectation or failure of a check.

Note:

In yours, you're additionally caching negative information (Not_immediate), but I don't think that buys you very much.

I think that Not_immediate is not negative information, but positive information. It is an abstraction of a set of concrete value-formers (float, string etc.) that must be positively known, just like Immediate or Immediate_on_64bits. In contrast, Unknown denotes the absence of information (but also used in the current implementation to represent Not_immediate. I think this is sound but conceptually wrong / imprecise.)

[your approach] seems to result in doing more expansions too

Currently the two proposals are incomparable: having Not_immediate avoids expansions in many cases that currently expand. (Stephen mentions that these cases only occur in immediacy-incorrect programs, so skipping those expansions does not accelerate well-typed programs.) On the other hand, my proposal expands in cases where the constructor immediacy is {Immediate, ImmediateOn64Bits}, even if we just want to request that the result accepts ImmediateOn64Bits so we could skip the expansion.

I think that those expansions have very little cost in practice; if there was a consensus on the idea that the approach is simpler, we could accept the extra expansions as a cost of simplicity. We could also consider adding a checking mode to my proposal, to cut early in exactly this scenario. This would be mostly equivalent to Stephen's implementation then, with the difference of my criticism (2): we have a clear specification of when we should expand, and the checking mode can sometimes optimize by skipping expansions if the result is precise enough (instead of having the expand-or-not decision be specified by failures, and only part of the checking specification).

Finally, there could be other points in the design space to consider, for example: if we consider that the immediacy information of type constructors is fundamentally incorrect, maybe we should get rid of it? (Only keep it on abstract types that have no definition.) Then we would be back with a single check, no approximation (so my criticism (1) is solved), and we would expand all the time (so (2) is solved). We would have to discuss useless recomputations and possibly consider caching within type expressions (possibly only the Tconstr ones), but maybe those wouldn't be issues in practice and/or the solutions would lead to simple systems as well.

It introduces two ways to compute immediacy, one being an "approximation" and the other one being precise.
[...]
To me this is the equivalent of backtracking during type-checking: the semantics we give to "immediacy" is "well try that, and if that fails do that other thing"

I don't think this is an accurate comparison at all. There is only a single way to compute immediacy, but you can stop computation -- and crucially expansion -- early when you have enough information to make the decision you are trying to make.

As far as I can tell, your proposal is just "Always assume that the check you are performing requires the most precise possible information". This means that you never take into account why you are checking immediacy: which seems to be the property you are aiming for. I can't see why you would want it as a property though, and it obviously requires doing more computation/expansion.

The PR documents the following new interface:

val approx_immediacy : Env.t -> type_expr -> Type_immediacy.t
       (* Compute an over-approximation of the immediacy of a type *)
val check_immediacy : Env.t -> as_:Type_immediacy.t -> type_expr ->
  (unit, Type_immediacy.Violation.t) result
       (* Verify that a type has a specified immediacy *)

I ask: what is the immediacy of a type? How does it relate to the proposed implementation? What I like about my solution is that the code answers this question clearly, whereas the current proposal (currently) does not, as far as I can tell. (The best definition of immediacy I can give from this API is to consider calls to check_immediacy on all possible immediacies, and select the best immediacy that does not fail this check.)

In order to have a simple answer, I propose (a better description of immediacies, including a Not_immediate case, and) an algorithm that performs more expansions in some cases. We don't expect it to be a performance concern at all, given that we only perform weak head normalization. I also mentioned a variant that is more complex than my proposal, similar in total "weight" to the current proposal, but still answers those questions more clearly.

Thanks, that makes things clearer. Judging from that API, I think that the current PR isn't quite doing what I would expect (or if it is then the API should change). I would expect to have an immediacy function that always gave the fully accurate immediacy, rather than approx_immediacy. I would expect the behaviour of the immediacy function to match roughly what you have described: expand things whenever they might produce more precise information.

The point where I disagree with you is on the removal of check_immediacy, I think it is better to take advantage of knowing what you are checking against to avoid unnecessary expansions.

I also much prefer the view of ranges with an upper and lower bound, rather than thinking in terms of sets. In particular, I think that view will be more natural when this same mechanism is used for layouts in unboxed types.

The point where I disagree with you is on the removal of check_immediacy, I think it is better to take advantage of knowing what you are checking against to avoid unnecessary expansions.

I'm not opposed to having a clever check_immediacy function, although I don't know that it is important with regard to the slight extra complexity. @stedolan should do as he prefers.

I also much prefer the view of ranges with an upper and lower bound, rather than thinking in terms of sets. In particular, I think that view will be more natural when this same mechanism is used for layouts in unboxed types.

This all depends on how we represent the static information on concrete types. If it is given as a partially-ordered set, then the natural notion of its abstractions are convex subsets (if a, c \in S and a <= b <= c then b \in S). In particular if it is a totally-ordered set, then you get intervals, but this is a chance property that does not occur in general. Here I think that it would be natural and conceptually nicer to distinguish Unknown and Not_immediate, in which case you get a non-total partial order (Immediate and Not_immediate are not comparable).

@gasche I think perhaps I have not gotten across what's going on in this algorithm. In particular, this paragraph of yours describing a possible design:

Then we would be back with a single check, no approximation (so my criticism (1) is solved), and we would expand all the time (so (2) is solved). We would have to discuss useless recomputations and possibly consider caching within type expressions (possibly only the Tconstr ones), but maybe those wouldn't be issues in practice and/or the solutions would lead to simple systems as well.

reads to me like a reasonable description of what's already in this PR, so something's definitely been misunderstood. I'll have a go at explaining it properly.

The problem

Types can be classified by "immediacy", which is an element of the following poset:

Always <= Always_on_64bits <= Unknown

These correspond to annotations [@@immediate], [@@immediate64] and no annotation, respectively. (This is at present a total order, but I agree it would be unwise to rely on this.)

There is a monotonicity / subtyping property here: a type of immediacy i is also a type of immediacy j, whenever i <= j.

The problem that the compiler must solve is to verify immediacy annotations on types. There is currently an eager / inference-based algorithm, which verifies annotations by (a) computing the least immediacy for each type constructor and (b) comparing this with an annotation, if present.

This algorithm is incorrect: the immediacy of a type alias can be refined by substitutions and/or may depend on type parameters (for instance, an abstract un-annotated type with Unknown immediacy could be replaced with int, which is Immediate). This causes the precomputed immediacies of type aliases to become stale.

Note that substitutions can only move a type downward in the immediacy poset: an abstract Unknown type can be replaced with int, but an abstract Always type cannot be replaced with string. This, together with the monotonicity / subtyping property, ensures that substitutions do not break previously-verified constraints.

Checking-based algorithm

What I'm proposing here is to switch from an inference-based to a checking-based algorithm. The fundamental operation is to check that a type has a given immediacy, rather than to infer the immediacy of a type from scratch.

The simple version of this algorithm verifies an immediacy constraint on a type by first expanding the type fully (that is, until the head of the type is not an alias), and then checking the immediacy against the expanded type (or against its annotation, if abstract).

An optimisation is possible here, and is implemented in the present PR. Sometimes, a type alias will always expand to an immediate type, regardless of parameters or substitutions. In such cases, we could speed up checking by avoiding some expansions. So, this patch associates with each type constructor an upper bound of its possible immediacies, allowing the check to be short-circuited sometimes.

There is no backtracking here, just a short-circuit optimisation for some easy cases not requiring expansion. The optimisation is the same one as is currently present in unification (and elsewhere): the semantics of unification are as though type aliases are always expanded, but in some easy and common cases (e.g. unifying a type alias with no parameters with itself) it is possible to determine the result of unification without needing to expand.

(I think there is some confusion here because I introduced the checking-based algorithm and the optimisation simultaneously, perhaps making it seem like the algorithm depended on both checking and inference, rather than checking + an optimisation to make checking faster in common cases. If it helps, I can prepare a version of this patch without the optimisation, which will only have Ctype.check_immediacy)

Corrected inference-based algorithm

The algorithm that you're proposing instead is to stick with inference, but fix the inference based algorithm by tracking in its result whether or not the result is "stable" (that is, whether it can be refined by future environment substitutions). If it is not stable, then future inference computations will expand aliases rather than trusting the possibly-stale precomputed result.

I don't like this approach because I think it is both more complicated and slower than the above. The complexity is because it requires keeping track of some notion of immediacy which is more detailed than what users can write in source code, involving a stability flag, intervals or convex subsets.

The slowness is because of unnecessary expansion. For instance, consider an environment which contains a chain of type aliases ending in an abstract type:

type a
type b = a
type c = b
...

This signature contains no immediacy annotations, but IIUC your proposal will spend O(n^2) time computing immediacies here, because each alias has Unknown immediacy and must therefore be re-expanded during inference.

The complexity is because it requires keeping track of some notion of immediacy which is more detailed than what users can write in source code, involving a stability flag, intervals or convex subsets.

Well if you insist on keeping exactly the current language of immediacies (I think it was a mistake in the original implement to not include Not_immediate, but oh well), we don't need to talk explicitly about abstractions, it suffices to consider that Always is stable and that the others are not.

For instance, consider an environment which contains a chain of type aliases ending in an abstract type: [..] quadratic time.

Yes indeed, but (1) is it a problem in practice? and (2) similar examples exist with your approach as well, they only look even more theoretical (take this signature, add the equality a = int after the fact, and check that all types are immediates). If we wanted to guarantee against unnecessary expansions, we would ensure that substitutions correctly update immediacies, and have a representation for parametrized types whose immediacy depends on its parameters'.

I think that we may now have spent enough time discussion the philosophy of immediacy together. It's a lot of fun and I shall be happy to do it again (variance, separability, representational kinds or what have you), but in this instance we may be running out of productive comments that I can make to you, the Person Doing the Actual Work.

I gave a more concise description of my API-level criticism in this comment, it might suggest improvements to your proposed API. Whether it does or not, if you prefer to keep the current approach I think that the productive next step for me would be to review the code.

Yes indeed, but (1) is it a problem in practice? and (2) similar examples exist with your approach as well, they only look even more theoretical (take this signature, add the equality a = int after the fact, and check that all types are immediates).

Right. Checking immediacy is worst-case O(n), so without fancy caching I imagine that checking n immediacy annotations is worst-case O(n^2). The thing I am (mildly!) concerned about is spending O(n^2) time computing immediacy in a program with 0 immediacy annotations.

'.I think that we may now have spent enough time discussion the philosophy of immediacy together. It's a lot of fun and I shall be happy to do it again (variance, separability, representational kinds or what have you), but in this instance we may be running out of productive comments that I can make to you, the Person Doing the Actual Work.

I gave a more concise description of my API-level criticism in this comment, it might suggest improvements to your proposed API. Whether it does or not, if you prefer to keep the current approach I think that the productive next step for me would be to review the code.

Maybe hold off on detailed review for a bit? I've been thinking about an approach that doesn't approximate or cache anything, and I'll try and have a PR ready next week in that style.

I think that the contentious part here has centered on the type_immediate field of a type declaration. Because of parameters and substitutions, the contents of this field can become stale, with types having a more precise immediacy then their type_immediate field would suggest.

I proposed dealing with this by only ever treating the type_immediate field as a conservative over-approximation and expanding to recompute immediacy when it's not precise enough, and you proposed dealing with this by also tracking whether the type_immediate field is final or subject to change and expanding to recompute immediacy when it's possible that it's been invalidated.

I now think that the better approach is not to have a type_immediate field at all, and expand where needed to check immediacy. The only types that really need to store immediacy data are abstract types, so a better place for it is the Type_abstract constructor of type_kind. This is a somewhat larger change than the present PR, but I think it might end up being simpler than any of the proposals here or the current system.

See #10041

This is subsumed by #11841, closing.