[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 <!:<?

[smarter]

How should one implement <!:<?

I don't think that's possible using match types, in fact the definition of type Map[-X, +Y] you give is already illegal by itself, if you replace the body of impossible by ???, the Typer phase is completed, but an error is emitted in the PostTyper phase:

-- Error: try/negst.scala:10:14 ------------------------------------------------
10 |    type Map[-X, +Y] = Arr[X, Y] match {
   |             ^^
   |contravariant type parameter X occurs in invariant position in Arr[X, Y] match {
   |  case Arr[String, Int] => Unit
   |  case Arr[Int, String] => Nothing
   |}

The scrutinee of the match is considered to be an invariant position (I don't recall why, but it was probably unsound otherwise).

To implement what you want it seems that the language would need to expose the provablyDisjoint operator used in the implementation of match types more directly, perhaps as a ProvablyDisjoint[A, B] type-level operator.

[s5bug]

Say ProvablyDisjoint did exist: How could it be used for <!:<? I'm not immediately seeing the solution, especially since provablyDisjoint looks to be commutative.

[smarter]

Ah yeah I guess that wouldn't help really, if you know that A and B are disjoint, then neither A <: B nor B <: A can hold, but there's no equivalent method that gives you only one of these two things.

[s5bug]

Solved! https://scastie.scala-lang.org/O4YhUozxSnO2PdXGKwivwQ compiles in both Scala 2 and Scala 3! Next step is figuring out how to generate the implementations with a macro...