Proving that a match type resolves to a specific concrete type

Question

I am trying to create an implementation of a trait that uses a match type, where the right-hand-side of that match type is known in advance. However, I can't seem to get the compiler to accept my "proof" of this. This is pretty new to me, so sorry if this is really obvious. Can someone help me understand if/how I can achieve what I want?

Here's some minimal code (Scastie) to illustrate what I'm doing:

class NumberBox {}

class LongBox {}

trait Boxer[T] {
  def box(): Boxer.Box[T]
}

object Boxer {
  type Box[T] = T match
    case Long => LongBox
    case _ => NumberBox
}

case class Val[T](v: T) extends Boxer[T] {
  def box(): Boxer.Box[T] = v match
    case _: Long => new LongBox()
    case _ => new NumberBox()
}

// here we prove that Boxer.Box[T] is a NumberBox
case class NoLongs[T](v: Boxer[T])(using Boxer.Box[T] =:= NumberBox) extends Boxer[T] {
  override def box(): Boxer.Box[T] = new NumberBox()
}

NoLongs(Val(1))

But this fails with:

Found:    NumberBox
Required: Boxer.Box[T]

Note: a match type could not be fully reduced:

  trying to reduce  Boxer.Box[T]
  failed since selector  T
  does not match  case Long => LongBox
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => NumberBox
    override def box(): Boxer.Box[T] = new NumberBox()

Answer 1

Scala doesn't automatically apply proofs in the way you're looking for. But you're right that you do have a proof. In fact, your proof constitutes a callable object: the type =:=[From, To] defines a method called apply:

override def apply(f: From): To

Now, you have a value of type Boxer.Box[T] =:= NumberBox, which means that apply would convert a Boxer.Box[T] to a NumberBox. You want the opposite: to convert a NumberBox into a Boxer.Box[T]. So we need to flip your proof around and then apply it.

def flip: To =:= From

In your specific use case, consider

case class NoLongs[T](v: Boxer[T])(using eq: Boxer.Box[T] =:= NumberBox) extends Boxer[T] {
  override def box(): Boxer.Box[T] = eq.flip(new NumberBox())
}

We give the proof argument a name, eq, and then we apply its symmetric proof (that NumberBox =:= Boxer.Box[T]) to our NumberBox to convert it to the desired type.

You could also just take a proof that NumberBox =:= Boxer.Box[T] directly and get rid of the flip, if desired.

case class NoLongs[T](v: Boxer[T])(using eq: NumberBox =:= Boxer.Box[T]) extends Boxer[T] {
  override def box(): Boxer.Box[T] = eq(new NumberBox())
}

Answer 2

I'll just add to @SilvioMayolo's answer that

• type class =:= is not symmetric (i.e. if there is implicit A =:= B then generally there is no implicit B =:= A generated by compiler automatically)

Why this scala code has a compilation error type mismatch

T <: A, return T method

https://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html

https://typelevel.org/blog/2014/09/20/higher_leibniz.html

In scala 3, is it possible to make covariant/contravariant type constructor to honour coercive subtyping?

• you don't have to call eq explicitly

case class NoLongs[T](v: Boxer[T])(using NumberBox =:= Boxer.Box[T]) extends Boxer[T] {
  override def box(): Boxer.Box[T] = new NumberBox()
}

case class NoLongs[T](v: Boxer[T])(using eq: Boxer.Box[T] =:= NumberBox) extends Boxer[T] {
  given (NumberBox =:= Boxer.Box[T]) = eq.flip
  override def box(): Boxer.Box[T] = new NumberBox()
}

• you can have constraints in both directions

case class NoLongs[T](v: Boxer[T])(using Boxer.Box[T] =:= NumberBox, NumberBox =:= Boxer.Box[T]) extends Boxer[T] {
  override def box(): Boxer.Box[T] = new NumberBox()
}