You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Fix derivesFrom false negative in provablyDisjointClasses (#23834)
Fix derivesFrom false negative in provablyDisjointClasses
Before the addition of `SymDenotation#mayDeriveFrom`,
tests/neg/i17132.min.scala was unsoundly accepted without a type error
because `R[T]` is reduced to `Any` where `T <: P[Any]`
by testing `provablyDisjointClasses` before `P` is added as a baseClass of `Q`.
Now, a recursion overflows occurs because:
- reducing `R[T] := T match case Q[t] => R[t]; case ...` requires
- proving `T` disjoint from `Q[t]` where `T <: P[Any]`, which asks
- whether existsCommonBaseTypeWithDisjointArguments, which requires
- normalizing the type arg to the base class P for the class Q, i.e. R[t]
- ...
In short, despite the use of the pending set in provablyDisjoint, diverging is
still possible when there is "cycle" in the type arguments in the base classes,
(and where the pending set is thus reset for a separate normalization problem).
One could attempt to add some more logic to detect these loops
s.t. they are considered "stuck", as opposed to reporting an error.
But it isn't clear that there are any concrete motivations for this.
0 commit comments