Type subsumption cache: handle unsolved type vars

[majocha]

Description

Fixes #19037

Added repro test case.

The problem was in memoization of TType -> TypeStructure generation.
TType is inherently mutable. One TType instance can result in different TypeFeasiblySubsumesType outcomes and different TypeStructure key fragments, as type arguments get solved. For the purpose of type subsumption caching, we can treat as stable only fully solved types, with solved or rigid type vars. We still want the cache to use the unstable ones, but we must produce new TypeStructures from the TTypes as they evolve towards a solution.

Additionally, caching is now limited only to TType_app cases.

Note:

Cache keys do not take into account constraints. This seems to work in practice, because TypeFeasiblySubsumesType, where the cache is applied, does not use them either.

If this turns out to be a problem, or we ever need to use TypeStructures also somewhere else, we should emit a structural fingerprint of Typar.Constraints, too.

[github-actions]

❗ Release notes required

---

✅ Found changes and release notes in following paths:

Change path	Release notes path	Description
src/Compiler	docs/release-notes/.FSharp.Compiler.Service/11.0.0.md

[majocha]

Yet another bug. This needs a careful look.

I need to run some benchmarks again, too and compare standalone builds with the original Vlad's implementation.

[T-Gro]

@majocha:
If we separated the solved and unsolved form of a typar, why wouldn't we want to cache (type subsumption especially) for both?
.e.g. constraints might be already there and the cache would hold info on type subsumption of generic typars.

It would equally help if two typars are both unsolved, but strip down to the same form.

Wasn't the mistake more the fact that solved/unsolved form of the same TType_var had always the same key (based on Stamp) ?

This is definitely a safe fix, but I wonder if it doesn't too much limit the potential of the cache for typars.

[majocha]

Wasn't the mistake more the fact that solved/unsolved form of the same TType_var had always the same key (based on Stamp) ?

Yes, that makes sense. It makes me wonder if we could also handle unsolved nullness better.

[T-Gro]

Nullness is not stamped, so in the case of unresolved/not yet resolved/ nullness, there is no identifier to hold onto.
The identity of the NullnessVar (possibly the leaf one if multiple are sequentially linked) object itself (via https://learn.microsoft.com/en-us/dotnet/api/system.runtime.compilerservices.runtimehelpers.gethashcode?view=net-9.0 )

[majocha]

This fix is accidental, the real problem is here:

fsharp/src/Compiler/Utilities/TypeHashing.fs

Line 480 in 9670f60

Extras.WeakMap.getOrCreate (fun ty -> accumulateTType ty |> toTypeStructure)

This was intended to speed up things by weakly attaching the computed TypeStructures to their respective TTypes. We cannot do it for not fully solved types, they still mutate and things get outdated.

[majocha]

Wasn't the mistake more the fact that solved/unsolved form of the same TType_var had always the same key (based on Stamp) ?

Yes, in fact in case of typars we don't want the stamp as identity at all. We should use the structure of the solution (TType) if available or a common token for unsolved.

[majocha]

I'm testing this in the IDE with the notorious OpenTK 5.0. It improved things significantly, there are way less cache entries now but much more hits, resulting in 99% ratio with little memory use and no constant churn during edits:

|             Cache name              | hit-ratio | adds | updates |  hits   | misses | 
|-------------------------------------|-----------|------|---------|---------|--------|
| typeSubsumptionCache                |    99.94% | 2752 |       0 | 4618992 |   2752 |

[majocha]

The huge mistake that causes a lot of inefficiency was emitting typar stamps as part of the cache key. This causes a lot of equivalent but really unusable keys polluting the cache. The increased churn is especially heavy on the IDE. I cannot see a solution to this, that would guarantee soundness.

[T-Gro]

The huge mistake that causes a lot of inefficiency was emitting typar stamps as part of the cache key. This causes a lot of equivalent but really unusable keys polluting the cache. The increased churn is especially heavy on the IDE. I cannot see a solution to this, that would guarantee soundness.

What about skipping cache for them?
For unsolved typars, the typefeasiblysubsubsumestypes is a quick decision in case of TType_var anyway.

Of course it somewhat limits the genericity of the cache, and is special-tailored to the place of application.

The typesubsumption was really needed for concrete types, with super types and interface hierarchies.
Maybe if Ttype_var is not part of it (after stripping), we can have both correctness and good cache contents?

I was thinking of content-based hashing, but you would need to hash all type constraints content-wise as they are mutable as well. Maybe the inherent mutation for solutions and constraints of a type var are good enough reasons to treat them differently?
(mutation is not well suited for cache keys)

[majocha]

So, basically, we care only about caching TType_app _ pairs.
But most of them have type vars. Often still unsolved when they end up in the checkSubsumes call, just like in the test here.
I tried to not cache the types with unsolved vars but the results are abysmal, looking at OpenTK 5.0 project as baseline build times go from 10 sec to forever.

I wonder if the constraints are really a problem wrt to type subsumption cache. Because the current situation where we emit only a stamp as typar identity worked so far ( the bug this PR tries to fix is elsewhere). A given typar can very well have its constraints mutated while the stamp stays constant, so it is already not collision free in general. It just does not collide in practice for this usage. I think it was like this since the original Vlad's implementation.

Copilot when asked says:

Q: which typar constraints can influence the result of TypeFeasiblySubsumesType? I wonder because I need to know what should take part in keying the TypeSubsumptionCache.

A: Short answer: none of the typar constraints affect TypeFeasiblySubsumesType.
Details:
• In TypeFeasiblySubsumesType, if either side is a type variable (TType_var), the function immediately returns true and does not consult the variable’s constraints.
• For nominal types (TType_app) with the same tycon, it delegates to TypesFeasiblyEquiv for each type argument. TypesFeasiblyEquiv also returns true when it encounters a TType_var (and ignores its constraints), and treats measure types as feasibly equivalent without comparing the actual measures.
• For tuples/anon/funs, it uses TypesFeasiblyEquiv similarly, so constraints are again ignored.
• The remaining branches follow nominal inheritance and interface chains of the concrete right-hand type. This depends on the type definitions/instantiations (and ultimately on metadata reachable via g/amap), not on typar constraint sets.
Implications for the cache key:
• You do not need to include any typar constraint environment in the TypeSubsumptionCache key.
• The existing key of stripped nominal type structures (when both sides are TType_app) plus CanCoerce is correct. This aligns with how the algorithm makes decisions.
• The cache is already partitioned per TcGlobals via the weak map, so differences in loaded metadata are naturally isolated.

hmm.

[majocha]

I quickly asked copilot:

Q: Does TypeFeasiblySubsumesType take nullness into account ?

A:

Short answer: No. The predicate is intentionally nullness-agnostic.
Why:
• In the core match it compares constructed types as TType_app (tc1, l1, _), TType_app (tc2, l2, ) and discards the third field (), which is where the nullness marker lives. Only tycon equality and argument feasibility are checked via TypesFeasiblyEquiv, which likewise ignores nullness.
• The special-case for object uses isObjTyAnyNullness g ty1, i.e., any nullness of obj is accepted as a supertype of any reference type, again ignoring nullness compatibility.
• Supertype/interface traversal (GetSuperTypeOfType, GetImmediateInterfacesOfType) calls back into TypeFeasiblySubsumesType without reconciling nullness.
Related:
• FindUniqueFeasibleSupertype preserves the nullness of ty2 in the result (addNullnessToTy n2 t), but the feasibility test itself still uses TypeFeasiblySubsumesType and thus ignores nullness.
• ChooseTyparSolution may add nullness due to constraints, but that’s orthogonal to the subsumption check.
If you need a nullness-aware check, compare nullnessOfTy g ty1 and nullnessOfTy g ty2 explicitly alongside calling TypeFeasiblySubsumesType.

[majocha]

As usual I'm testing this in the IDE. I see way less cache churn now and good hit ratio. For example after some minutes of copilot work in this solution:

Cache name	hit-ratio	adds	updates	hits	misses	evictions	eviction-fails
typeSubsumptionCache	89.44%	106412	0	900806	106412	66867	0

[T-Gro]

As usual I'm testing this in the IDE. I see way less cache churn now and good hit ratio. For example after some minutes of copilot work in this solution:

Cache name hit-ratio adds updates hits misses evictions eviction-fails
typeSubsumptionCache 89.44% 106412 0 900806 106412 66867 0

Would it make sense to publish a built release .vsix for marklam from Discord?
Since he does have a private solution, which was however exercising the mechanism quite heavily.

[majocha]

Not sure if it goes through
VisualFSharpFull.zip

[majocha]

Another potential problem to check, given that we operate on stripped types, can we really trust that a type that looks like it has no type vars at all wouldn't reverse into an unsolved one in the course of Trace.Undo? It looks to me more and more like the whole idea of memoizing TType -> TypeStructure is not great. We really cannot pretend this is a pure function.
Maybe we should instead optimize the shit out of generating type structures.

[T-Gro]

Another potential problem to check, given that we operate on stripped types, can we really trust that a type that looks like it has no type vars at all wouldn't reverse into an unsolved one in the course of Trace.Undo? It looks to me more and more like the whole idea of memoizing TType -> TypeStructure is not great. We really cannot pretend this is a pure function. Maybe we should instead optimize the shit out of generating type structures.

Actually, the fact that the function strips first, and then looks into the weak cache, is of help here.
If ConstraintSolver sets a (possibly speculative) solution to a type var, stripping will then reduce it to the solution itself.
So in that first pass, you would actually get the solution, e.g. a TType_app, as the key.

When that solution is undone, stripping will not kick in (or stop at the last ttype_var) and you would get the TType_var as the key.

Stripping helps to ensure that when we have a solved Ttype_var, it will not go as cache key, but rather its solution will go.

The hypothetical problem is with speculative additions of constraints, since stripping does not change the reference there.
But for that purpose unsolved ttype_vars should not be used as cache entries inside the weak cache, which was done 👍

[T-Gro]

@majocha : I would want to merge this in and start dogfooding, WDYT ?

[majocha]

@majocha : I would want to merge this in and start dogfooding, WDYT ?

Yes I think this is fine now, I'm using it and not seeing any anomalies.