Commit 7e47294
committed
Fix provablyDisjoint handling of HK types
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.1 parent 5439e98 commit 7e47294
File tree
2 files changed
+17
-3
lines changed- compiler/src/dotty/tools/dotc/core
- tests/pos
2 files changed
+17
-3
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
2841 | 2841 | | |
2842 | 2842 | | |
2843 | 2843 | | |
2844 | | - | |
2845 | | - | |
| 2844 | + | |
| 2845 | + | |
| 2846 | + | |
2846 | 2847 | | |
2847 | | - | |
| 2848 | + | |
| 2849 | + | |
2848 | 2850 | | |
2849 | 2851 | | |
2850 | 2852 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
0 commit comments