Refine specification of :consistent with respect to world age.

[Keno]

The description of consistency currently has the following note:

  │ Note
  │
  │  The :consistent-cy assertion is made world-age wise. More formally, write fᵢ for the evaluation of f in
  │  world-age i, then we require:
  │
  │  ∀ i, x, y: x ≡ y → fᵢ(x) ≡ fᵢ(y)
  │
  │  However, for two world ages i, j s.t. i ≠ j, we may have fᵢ(x) ≢ fⱼ(y).
  │
  │  A further implication is that :consistent functions may not make their return value dependent on the state of
  │  the heap or any other global state that is not constant for a given world age.

This is a true description of that the :consistent effect means, but it assumes that inferences was able to determine all backedges for the called function. Having an inference-determined :consistent effect implies this, but it need not be true for a :consistent override annotation. I think our options are:

1. Always truncate the world range for :consistent overrides to just the evaluated world range.
2. Add a separate annotation :globally_consistent (or something) that removes the world-age specific language from the specification.
3. Add a separate (non-overridable) effect that determines if inference has total backedge information to compute accurate world-age bounds.
4. Ignore all of this and just drop this language from the annotation doc and put it into the doc for the effect itself.

[vtjnash]

1. Would be so bad for compile performance it is effectively impossible.

This issue is essentially why the old pure annotation has previously refused to refer to worlds at all, and pure is pretty much the same as the newer-and-better consistent annotation

[Keno]

This has become more thorny with bpart. I want to think about it again for the 1.12 release, so putting it on the milestone, so we don't forget.

[DanielFrantes]

Heya,
Is this still relevant?
Cause I want to work on this.

Cheers
Dan

[vtjnash]

You can, but we don't allow reserving issues for working on