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
If refineUsingParent/instantiateToSubType is passed a HK then it's
not possible to instantiate a class to that type (at the moment and
perhaps ever). So it's important we guard against that.
This came up while trying to see if Mark[?] and Foo[Int] (from
pos/i19031.ci-reg1.scala) are provably disjoint - which they should be
reported not to be. Because they're not applied types of the same type
constructor we end up trying to prove that HK type Mark is disjoint from
HK type Foo. Because we don't know how to instantiate Foo's subclasses
(e.g Bar2) such that it's a subtype of higher-kinded type "Mark", we end
up discarding all of Foo's subclasses, which implies that Foo & Mark is
uninhabited, thus they are provably disjoint - which is incorrect.
We originally didn't encounter this because we eagerly decomposed in
Space intersection, while now we've dispatched it to provablyDisjoint.
(edit) We allow for some kindness in provablyDisjoint.
0 commit comments