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()

score 3 · Accepted Answer · answered Apr 15 '23 at 03:19

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())
}

This was so helpful, thank you. I had no idea that =:= was callable like that — fehrvuerh93, Apr 15 '23 at 21:51

Dmytro Mitin · Answer 2 · 2023-04-16T17:08:51.947

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()
}

I'm not sure I understand your first bullet point (isn't `flip` quite literally a proof of the symmetric property, namely that `A =:= B` implies the existence of `B =:= A`?). But that is really interesting to know that Scala will use `=:=` constraints automatically if the `given` is in the right order. Is that a new feature in Scala 3 or did I just never notice it before? — Silvio Mayolo, Apr 16 '23 at 15:50
@SilvioMayolo *"isn't `flip` quite literally a proof of the symmetric property"* It is but it's not an implicit. If there is implicit `A =:= B` then generally there is no implicit `B =:= A` generated by compiler automatically. *"Is that a new feature in Scala 3"* It exists in 2.x too. `A =:= B` extends `A => B`, so it defines an implicit conversion. — Dmytro Mitin, Apr 16 '23 at 16:04

Proving that a match type resolves to a specific concrete type

2 Answers2

Linked