scala - 路径相关类型:从Idris到Scala

我写了一个示例，从Idris的Type-Driven Development with Idris到Scala：

Idris（与Idris一起来自TDD）

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
           Bicycle : Vehicle Pedal
           Car : (fuel : Nat) -> Vehicle Petrol
           Bus : (fuel : Nat) -> Vehicle Petrol

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200

斯卡拉

scala> sealed trait PowerSource
defined trait PowerSource

scala> case object Petrol extends PowerSource
defined object Petrol

scala> case object Pedal extends PowerSource
defined object Pedal

scala> sealed abstract class Vehicle {
     |   type A <: PowerSource
     | }
defined class Vehicle

scala> case object Bicycle extends Vehicle {
     |   type A = Pedal.type
     | }

scala> case class Bus(fuel: Int) extends Vehicle {
     |   type A = Petrol.type
     | }
defined class Bus

scala> case class Car(fuel: Int) extends Vehicle {
     |   type A = Petrol.type
     | }

但是，在尝试实现refuel时遇到了麻烦：

scala> def refuel[P <: Petrol.type](vehicle: Vehicle {type A = P} ): Vehicle = vehicle match {
     |   case Car(_) => Car(100)
     |   case Bus(_) => Bus(100)
     | }
<console>:20: warning: unreachable code
         case Bus(_) => Bus(100)
                           ^
refuel: [P <: Petrol.type](vehicle: Vehicle{type A = P})Vehicle

scala> refuel(Car(100))
res6: Vehicle = Car(100)

scala> refuel(Bus(5))
res7: Vehicle = Bus(100)

scala> refuel(Bicycle)
<console>:22: error: inferred type arguments [Bicycle.A] do not conform to method refuel's type parameter bounds [P <: Petrol.type]
       refuel(Bicycle)
       ^
<console>:22: error: type mismatch;
 found   : Bicycle.type
 required: Vehicle{type A = P}
       refuel(Bicycle)
              ^

请批评/纠正我的方法，并在Scala中帮助我使用refuel。

最佳答案

unreachable code警告似乎是虚假的：如果不是，则可以将Bus强制为Car（不正确）并导致ClassCastExeception ...不会出现成为可能。

虚假警告是scalac bug。 Scala问题跟踪器中有相关的错误，但这似乎是一个不同的变体，您应该报告它。