-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
SIP-56-extended: Simpler provablyDisjoint test.
- Loading branch information
Showing
15 changed files
with
418 additions
and
141 deletions.
There are no files selected for viewing
358 changes: 238 additions & 120 deletions
358
compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
-- Error: tests/neg/6314-6.scala:26:3 ---------------------------------------------------------------------------------- | ||
26 | (new YY {}).boom // error: object creation impossible | ||
| ^ | ||
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test3 is not defined | ||
|(Note that | ||
| parameter String in def apply(fa: String): Int in trait XX in object Test3 does not match | ||
| parameter Test3.Bar[X & Object with Test3.YY {...}#Foo] in def apply(fa: Test3.Bar[X & YY.this.Foo]): Test3.Bar[Y & YY.this.Foo] in trait YY in object Test3 | ||
| ) | ||
-- Error: tests/neg/6314-6.scala:52:3 ---------------------------------------------------------------------------------- | ||
52 | (new YY {}).boom // error: object creation impossible | ||
| ^ | ||
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test4 is not defined | ||
|(Note that | ||
| parameter String in def apply(fa: String): Int in trait XX in object Test4 does not match | ||
| parameter Test4.Bar[X & Object with Test4.YY {...}#FooAlias] in def apply(fa: Test4.Bar[X & YY.this.FooAlias]): Test4.Bar[Y & YY.this.FooAlias] in trait YY in object Test4 | ||
| ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
-- [E007] Type Mismatch Error: tests/neg/6314.scala:28:27 -------------------------------------------------------------- | ||
28 | val i: Bar[Y | Type] = 1 // error | ||
| ^ | ||
| Found: (1 : Int) | ||
| Required: Test1Bis.Bar[Test1Bis.Y | Test.this.Type] | ||
| | ||
| Note: a match type could not be fully reduced: | ||
| | ||
| trying to reduce Test1Bis.Bar[Test1Bis.Y | Test.this.Type] | ||
| failed since selector Test1Bis.Y | Test.this.Type | ||
| does not match case Test1Bis.X & Test1Bis.Y => String | ||
| and cannot be shown to be disjoint from it either. | ||
| Therefore, reduction cannot advance to the remaining case | ||
| | ||
| case Any => Int | ||
| | ||
| longer explanation available when compiling with `-explain` | ||
-- [E007] Type Mismatch Error: tests/neg/6314.scala:45:33 -------------------------------------------------------------- | ||
45 | def right(fa: Bar[L]): Int = fa // error | ||
| ^^ | ||
| Found: (fa : Wizzle.this.Bar[L]) | ||
| Required: Int | ||
| | ||
| where: L is a type in trait Wizzle with bounds <: Int & Singleton | ||
| | ||
| longer explanation available when compiling with `-explain` | ||
-- [E007] Type Mismatch Error: tests/neg/6314.scala:55:33 -------------------------------------------------------------- | ||
55 | def right(fa: Bar[L]): Int = fa // error | ||
| ^^ | ||
| Found: (fa : Wazzlo.this.Bar[L]) | ||
| Required: Int | ||
| | ||
| where: L is a type in trait Wazzlo with bounds <: Int & AnyVal | ||
| | ||
| longer explanation available when compiling with `-explain` | ||
-- [E007] Type Mismatch Error: tests/neg/6314.scala:65:33 -------------------------------------------------------------- | ||
65 | def right(fa: Bar[L]): Int = fa // error | ||
| ^^ | ||
| Found: (fa : Wuzzlu.this.Bar[L]) | ||
| Required: Int | ||
| | ||
| where: L is a type in trait Wuzzlu with bounds <: String & AnyRef | ||
| | ||
| longer explanation available when compiling with `-explain` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
|
||
-- [E172] Type Error: tests/neg/i13190/B_2.scala:14:38 ----------------------------------------------------------------- | ||
14 | summon[FindField[R, "B"] =:= Double] // error | ||
| ^ | ||
| Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double. | ||
| | ||
| Note: a match type could not be fully reduced: | ||
| | ||
| trying to reduce Test.FindField[Test.R, ("B" : String)] | ||
| failed since selector Test.R | ||
| does not match case Opaque.FieldType[("B" : String), f] *: t => f | ||
| and cannot be shown to be disjoint from it either. | ||
| Therefore, reduction cannot advance to the remaining case | ||
| | ||
| case _ *: t => Test.FindField[t, ("B" : String)] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,3 @@ | ||
object Opaque { | ||
opaque type FieldType[K, +V] <: V = V | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
-- [E172] Type Error: tests/neg/i13190b.scala:18:38 -------------------------------------------------------------------- | ||
18 | summon[FindField[R, "B"] =:= Double] // error | ||
| ^ | ||
| Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double. | ||
| | ||
| Note: a match type could not be fully reduced: | ||
| | ||
| trying to reduce Test.FindField[Test.R, ("B" : String)] | ||
| failed since selector Test.R | ||
| does not match case Opaque.FieldType[("B" : String), f] *: t => f | ||
| and cannot be shown to be disjoint from it either. | ||
| Therefore, reduction cannot advance to the remaining case | ||
| | ||
| case _ *: t => Test.FindField[t, ("B" : String)] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
object Opaque { | ||
opaque type FieldType[K, +V] <: V = V | ||
} | ||
|
||
import Opaque.* | ||
|
||
object Test { | ||
type FindField[R <: scala.Tuple, K] = R match { | ||
case FieldType[K, f] *: t => f | ||
case _ *: t => FindField[t, K] | ||
} | ||
|
||
val f: FieldType["A", Int] = ??? | ||
val f1: Int = f | ||
//val f2: Int = f | ||
|
||
type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple | ||
summon[FindField[R, "B"] =:= Double] // error | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
-- [E007] Type Mismatch Error: tests/neg/i15312.scala:7:27 ------------------------------------------------------------- | ||
7 |val b: F[{type A = Int}] = "asd" // error | ||
| ^^^^^ | ||
| Found: ("asd" : String) | ||
| Required: F[Object{type A = Int}] | ||
| | ||
| Note: a match type could not be fully reduced: | ||
| | ||
| trying to reduce F[Object{type A = Int}] | ||
| failed since selector Object{type A = Int} | ||
| does not match case Object{type A = Float} => Int | ||
| and cannot be shown to be disjoint from it either. | ||
| Therefore, reduction cannot advance to the remaining case | ||
| | ||
| case Object{type A = Int} => String | ||
| | ||
| longer explanation available when compiling with `-explain` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,5 @@ | ||
// scalac: -Yno-deep-subtypes:false | ||
|
||
class Inv[A] | ||
|
||
class Foo[B, M[_]] | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
class Parent[T](val x: T) | ||
|
||
class Child[T](x: T) extends Parent(x) | ||
|
||
type MT[X] = X match | ||
case Parent[Int] => Int | ||
case Parent[Boolean] => Boolean | ||
|
||
def test(): Unit = | ||
summon[MT[Parent[Int]] =:= Int] | ||
summon[MT[Parent[Boolean]] =:= Boolean] | ||
//summon[MT[Parent[Any]] =:= Int] | ||
|
||
summon[MT[Child[Int]] =:= Int] | ||
summon[MT[Child[Boolean]] =:= Boolean] | ||
end test |