Safe LightSwitch using phantom types and typelevel calculation

lightswitch.scala

sealed abstract class Power
final abstract class On extends Power
final abstract class Off extends Power

class LightSwitch[State <: Power] private {
  def on(implicit ev: State =:= Off) = LightSwitch.on
  def off(implicit ev: State =:= On) = LightSwitch.off
  def toggleP[S<:Power](implicit t: ToggleP[State,S]): LightSwitch[S] = new LightSwitch[S]
  def toggleM[S<:Power](implicit t: ToggleM.Aux[State,S]): LightSwitch[S] =
    new LightSwitch[S]
}

object LightSwitch {
  val on: LightSwitch[On] = new LightSwitch
  val off: LightSwitch[Off] = new LightSwitch
}

// Type parameter version, subtle because the second parameter is by
// convention calculated through an implicit search
final class ToggleP[Before <: Power, After <: Power]
object ToggleP {
  implicit val toggleOn: ToggleP[On,Off] = new ToggleP[On,Off]
  implicit val toggleOff: ToggleP[Off,On] = new ToggleP[Off,On]
}

// Type member version, hiding the result type, a little more verbose,
// but more explicit about relation of parameter and member
sealed class ToggleM[Before <: Power] { type After <: Power }
object ToggleM {
  type Aux[A0<:Power,B0<:Power] = ToggleM[A0] { type After = B0 }
  implicit val toggleOn: ToggleM.Aux[On,Off] = new ToggleM[On] { type After = Off }
  implicit val toggleOff: ToggleM.Aux[Off,On] = new ToggleM[Off] { type After = On }
}

object Main extends App {
  val ls1: LightSwitch[On] = LightSwitch.on
  val ls2: LightSwitch[Off] = ls1.off
  val ls3: LightSwitch[On] = ls2.toggleP
  // ls3.on
  // error: Cannot prove that On =:= Off
  val ls4: LightSwitch[Off] = ls3.toggleM
  // ls4.off
  // error: Cannot prove that Off =:= On
}