Scala 2 with or type

or.scala

sealed trait AST
case class ConstInt(x: Int) extends AST
case class ConstDouble(x: Double) extends AST
case class SomethingElse() extends AST

type ¬[A] = A => Nothing
type ∨[T, U] = ¬[¬[T] with ¬[U]]
type ¬¬[A] = ¬[¬[A]]
type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }

def size[T: (Int |∨| String)#λ](t: T) =
  t match {
    case i: Int => i
    case s: String => s.length
  }

object ANumber {
  def unapply[T : (Int |∨| String)#λ](ast: AST): Option[T] = {
    ast match {
      case ConstInt(n: Int)=> Some(n)
      /*
 type mismatch;
 found   : n.type (with underlying type Int)
 required: T
      */
      case ConstDouble(n)=> Some(n)
      case _ => None
    }
  }
}

def interpret(x: AST) = {
  x match {
    case ANumber(int_or_double)  => "number"
    case SomethingElse() => "???"    
  }
}

package example

sealed trait AST

case class ConstInt(x: Int) extends AST

case class ConstDouble(x: Double) extends AST

case class SomethingElse() extends AST

object T {
  type ¬[A] = A => Nothing
  type ∨[T, U] = ¬[¬[T] with ¬[U]]
  type ¬¬[A] = ¬[¬[A]]
  type |∨|[T, U] = {
    type λ[X] = ¬¬[X] <:< (T ∨ U)
  }

  implicit def axiom[A]: A =:= ¬¬[A] = ???

  @inline def toUnion[T, U](x: T): ∨[T, U] =
    implicitly[(T |∨| U)#λ[T]].apply(implicitly[T =:= ¬¬[T]].apply(x))

  @inline def fromUnion[L, R, S](t: ∨[L, R])(leftProj: L => S, rightProj: R => S) =
    t match {
      case l: L => leftProj(l)
      case r: R => rightProj(r)
    }

  object ANumber {
    def unapply(ast: AST): Option[Int ∨ Double] = {
      ast match {
        case ConstInt(n) => Some(toUnion[Int, Double](n))
        case ConstDouble(n) => Some(toUnion[Double, Int](n))
        case _ => None
      }
    }
  }

  def size[T: (Int |∨| String)#λ](t: T) =
    t match {
      case i: Int => i
      case s: String => s.length
    }

  def interpret(x: AST) = {
    x match {
      case ANumber(int_or_double) =>
        fromUnion(int_or_double)(
          _.toOctalString, // toOctalString belongs to Int and not for Double so we proved that it is Int
          _.isInfinity 
        )
      case SomethingElse() => "???"
    }
  }

  def main(args: Array[String]): Unit = {

  }
}