Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Enumerate refinement type's subtypes by deSkolemizing
- Loading branch information
Showing
8 changed files
with
194 additions
and
6 deletions.
There are no files selected for viewing
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,28 @@ | ||
// scalac: -Werror | ||
|
||
// like pos/t9657 | ||
// but with a more plausible reason for why to have a method type parameter | ||
|
||
sealed trait PowerSource | ||
sealed trait NonRenewablePowerSource extends PowerSource | ||
|
||
case object Petrol extends NonRenewablePowerSource | ||
case object Coal extends NonRenewablePowerSource | ||
case object Pedal extends PowerSource | ||
|
||
sealed abstract class Vehicle { type A <: PowerSource } | ||
case object Bicycle extends Vehicle { type A = Pedal.type } | ||
case class Bus(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
case class Car(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
|
||
object Test { | ||
def refuel[P <: NonRenewablePowerSource](vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning | ||
} | ||
|
||
def main(args: Array[String]): Unit = { | ||
println(refuel(Car(100))) | ||
println(refuel(Bus(5))) | ||
} | ||
} |
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,9 @@ | ||
t9657-less-fishy.scala:27: warning: unreachable code | ||
case Bicycle => ??? // expected unreachable 1 | ||
^ | ||
t9657-less-fishy.scala:33: warning: unreachable code | ||
case _: Bicycle.type => ??? // expected unreachable 2 | ||
^ | ||
error: No warnings can be incurred under -Werror. | ||
2 warnings | ||
1 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,49 @@ | ||
// scalac: -Werror | ||
|
||
// like {pos,neg}/t9657 | ||
// but with a more plausible reason for why to have a method type parameter | ||
|
||
sealed trait PowerSource | ||
sealed trait NonRenewablePowerSource extends PowerSource | ||
|
||
case object Petrol extends NonRenewablePowerSource | ||
case object Coal extends NonRenewablePowerSource | ||
case object Pedal extends PowerSource | ||
|
||
sealed abstract class Vehicle { type A <: PowerSource } | ||
case object Bicycle extends Vehicle { type A = Pedal.type } | ||
case class Bus(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
case class Car(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
|
||
object Test { | ||
def refuel2[P <: NonRenewablePowerSource](vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 2 | ||
case Bicycle => ??? // expected unreachable 1 | ||
} | ||
|
||
def refuel3[P <: NonRenewablePowerSource](vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 3 | ||
case _: Bicycle.type => ??? // expected unreachable 2 | ||
} | ||
} | ||
|
||
class Test[P <: NonRenewablePowerSource] { | ||
def refuel(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 4 | ||
} | ||
|
||
def refuel2(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 5 | ||
case Bicycle => ??? // expected unreachable 3 | ||
} | ||
|
||
def refuel3(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 6 | ||
case _: Bicycle.type => ??? // expected unreachable 4 | ||
} | ||
} |
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,9 @@ | ||
t9657.scala:15: warning: unreachable code | ||
case Bicycle => ??? // expected unreachable 1 | ||
^ | ||
t9657.scala:21: warning: unreachable code | ||
case _: Bicycle.type => ??? // expected unreachable 2 | ||
^ | ||
error: No warnings can be incurred under -Werror. | ||
2 warnings | ||
1 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,37 @@ | ||
// scalac: -Werror | ||
sealed trait PowerSource | ||
case object Petrol extends PowerSource | ||
case object Pedal extends PowerSource | ||
|
||
sealed abstract class Vehicle { type A <: PowerSource } | ||
case object Bicycle extends Vehicle { type A = Pedal.type } | ||
case class Bus(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
case class Car(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
|
||
object Test { | ||
def refuel1[P <: Petrol.type](vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 1 | ||
case Bicycle => ??? // expected unreachable 1 | ||
} | ||
|
||
def refuel2[P <: Petrol.type](vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 2 | ||
case _: Bicycle.type => ??? // expected unreachable 2 | ||
} | ||
} | ||
|
||
class Test[P <: Petrol.type] { | ||
def refuel1(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 3 | ||
case Bicycle => ??? // expected unreachable 3 | ||
} | ||
|
||
def refuel2(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 4 | ||
case _: Bicycle.type => ??? // expected unreachable 4 | ||
} | ||
} |
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,23 @@ | ||
// scalac: -Werror | ||
|
||
// like pos/t9657 | ||
// but with a more plausible reason for why to have a method type parameter | ||
|
||
sealed trait PowerSource | ||
sealed trait NonRenewablePowerSource extends PowerSource | ||
|
||
case object Petrol extends NonRenewablePowerSource | ||
case object Coal extends NonRenewablePowerSource | ||
case object Pedal extends PowerSource | ||
|
||
sealed abstract class Vehicle { type A <: PowerSource } | ||
case object Bicycle extends Vehicle { type A = Pedal.type } | ||
case class Bus(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
case class Car(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
|
||
class Test[P <: NonRenewablePowerSource] { | ||
def refuel(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 2 | ||
} | ||
} |
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 @@ | ||
// scalac: -Werror | ||
sealed trait PowerSource | ||
case object Petrol extends PowerSource | ||
case object Pedal extends PowerSource | ||
|
||
sealed abstract class Vehicle { type A <: PowerSource } | ||
case object Bicycle extends Vehicle { type A = Pedal.type } | ||
case class Bus(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
case class Car(fuel: Int) extends Vehicle { type A = Petrol.type } | ||
|
||
class Test[P <: Petrol.type] { | ||
def refuel(vehicle: Vehicle { type A = P }): Vehicle = vehicle match { | ||
case Car(_) => Car(100) | ||
case Bus(_) => Bus(100) // was: "unreachable code" warning 2 | ||
} | ||
} |