[Question] Implementing <!:<

[s5bug]

Prologue

One can define =!:= like so:

trait =!:=[A, B] { 
  def impossible(proof: A =:= B): Nothing 
}

And by defining an invariant type-level Tuple2:

sealed trait InvT[X, Y]

can implement it like so:

implicit val unitNotNothing: Unit =!:= Nothing = new =!:=[Unit, Nothing] {
  type Map[X, Y] = InvT[X, Y] match {
    case InvT[Unit, Nothing] => Unit
    case InvT[Nothing, Unit] => Nothing
  }
  
  override def impossible(proof: Unit =:= Nothing): Nothing =
    proof.flip.substituteBoth[Map](())
}

implicit val oneNotTwo: 1 =!:= 2 = new =!:=[1, 2] {
  type Map[X, Y] = InvT[X, Y] match {
    case InvT[1, 2] => Unit
    case InvT[2, 1] => Nothing
  }
  
  override def impossible(proof: 1 =:= 2): Nothing =
    proof.flip.substituteBoth[Map](())
}

implicit val intNotString: Int =!:= String = new =!:=[Int, String] {
  type Map[X, Y] = InvT[X, Y] match {
    case InvT[Int, String] => Unit
    case InvT[String, Int] => Nothing
  }
  
  override def impossible(proof: Int =:= String): Nothing =
    proof.flip.substituteBoth[Map](())
}

implicit val anyNotString: Any =!:= String = new =!:=[Any, String] {
  type Map[X, Y] = InvT[X, Y] match {
    case InvT[String, Any] => Unit
    case InvT[Any, String] => Nothing
  }
  
  override def impossible(proof: Any =:= String): Nothing =
    proof.substituteBoth[Map](())
}

Chapter 1: Subtyping Rules

1. It is true that =!:= is invariant on both sides.
2. <!:< should be covariant on the subtype side: If A <: C, then (A <!:< B) <: (C <!:< B). That is to say, if you have a proof that A <!:< B, and A <: C, then it must not be that C <: B due to subtyping transitivity.
3. Likewise, <!:< should be contravariant on the supertype side: If B >: D, then (A <!:< B) <: (A <!:< D). That is to say, if you have a proof that A <!:< B, and D <: B, then it must not be that A <: D due to subtyping transitivity.
4. It should be that (A <!:< B) <: (A =!:= B): If two types are not subtypes, they are also not equal, due to subtyping reflexivity.

Immediately we run into some issues:

// variance already doesn't match
trait <!:<[+A, -B] extends =!:=[A, B]

trait <!:<[+A, -B] extends =!:=[? <: A, ? >: B] {
  // variance still doesn't match, nevermind the missing `A <:< B => Nothing` method
  override def impossible(proof: (? <: A) =:= (? >: B)): Nothing
}

And if we even decide to discard variance, making the impossible method more general doesn't work anyways:

trait <!:<[A, B] extends =!:=[A, B] {
  // signature doesn't match `impossible(proof: A =:= B): Nothing`
  override def impossible(proof: A <:< B): Nothing
}

Chapter 2: Mapping Sides

Say we ditch the <!:<-implies-=!:=:

trait <!:<[+A, -B] {
  def impossible(proof: A <:< B): Nothing
}

I could find no such solution that allows one to map the proof to get a Unit <:< Nothing when the types are truly distinct.

Replacing the spirit of InvT with any of

sealed trait Co[+X] // for use with liftCo
sealed trait Contra[-X] // for use with liftContra
sealed trait Arr[-X, +Y] // for use with substituteBoth

always leaves one with errors. For example, with Arr:

implicit def intIsNotString: Int <:!< String = new <:!<[Int, String] {
  type Map[-X, +Y] = Arr[X, Y] match {
    case Arr[String, Int] => Unit
    case Arr[Int, String] => Nothing
  }
  
  override def impossible(proof: Int <:< String): Nothing = {
    proof.substituteBoth[Map](())
  }
}

-- [E007] Type Mismatch Error: -------------------------------------------------
8 |    proof.substituteBoth[Map](())
  |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |    Found:    Map[Int, String]
  |    Required: Nothing
  |
  |    Note: a match type could not be fully reduced:
  |
  |      trying to reduce  Map[Int, String]
  |      failed since selector  Arr[Int, String]
  |      does not match  case Arr[String, Int] => Unit
  |      and cannot be shown to be disjoint from it either.
  |      Therefore, reduction cannot advance to the remaining case
  |
  |        case Arr[Int, String] => Nothing

Explanation
===========

Tree: proof.substituteBoth[Map](())

I tried to show that
  Map[Int, String]
conforms to
  Nothing
but the comparison trace ended with `false`:

  ==> Map[Int, String]  <:  Nothing
    ==> Map[Int, String]  <:  Nothing (recurring)
      ==> Arr[Int, String] match {
  case Arr[String, Int] => Unit
  case Arr[Int, String] => Nothing
}  <:  Nothing (recurring)
        ==> Any  <:  Nothing (recurring)
        <== Any  <:  Nothing (recurring) = false
      <== Arr[Int, String] match {
  case Arr[String, Int] => Unit
  case Arr[Int, String] => Nothing
}  <:  Nothing (recurring) = false
    <== Map[Int, String]  <:  Nothing (recurring) = false
  <== Map[Int, String]  <:  Nothing = false

The tests were made under the empty constraint

How should one implement <!:<?