Failure to unify types in pattern match

[nrinaudo]

Compiler version

scalac -version
Scala compiler version 3.6.2 -- Copyright 2002-2024, LAMP/EPFL

Minimized code

enum Type:
  case Num
  case Bool

enum TypedExpr[A <: Type]:
  case Num(value: Int) extends TypedExpr[Type.Num.type]
  case Bool(value: Boolean) extends TypedExpr[Type.Bool.type]

case class Typing[A <: Type](expr: TypedExpr[A], tpe: A):
  def cast[B <: Type](to: B): Either[String, TypedExpr[B]] = this match
    case Typing(expr, `to`) => Right(expr)
    case _                  => Left("Failed")

Output

-- [E007] Type Mismatch Error: Test.scala:12:35 --------------------------------
12 |  case Typing(expr, `to`) => Right(expr)
   |                                   ^^^^
   |                Found:    (expr : TypedExpr[A])
   |                Required: TypedExpr[B]
   |
   |                where:    A is a type in method cast with bounds <: Type
   |                          B is a type in method cast with bounds <: Type
   |
   | longer explanation available when compiling with `-explain`

Expectation

I would expect the compiler to understand that:

• to is equal to repr, so they must be of the same type.
• this implies that A and B are the same type.
• which implies that expr is a legal TypedExpr[B].

This might be an unreasonable expectation on my part, but I think it's born out by the fact that the following works flawlessly (keeping the same Type and TypedExpr:

enum TypeRepr[A <: Type]:
  case Num extends TypeRepr[Type.Num.type]
  case Bool extends TypeRepr[Type.Bool.type]

case class Typing[A <: Type](expr: TypedExpr[A], repr: TypeRepr[A]):
  def cast[B <: Type](to: TypeRepr[B]): Either[String, TypedExpr[B]] = this match
    case Typing(expr, `to`) => Right(expr)
    case _                  => Left("Failed")

With that code, the compiler seems perfectly happy to concluse that A and B are the same type and expr is a valid TypedExpr[B].

The only difference, as far as I understand, is that TypeRepr is indexed on Type rather than being a Type directly, but I'm not sure what additional information / confidence this gives the compiler.

[nrinaudo]

I was looking at the code of boundary and wonder whether this wouldn't help.

Couldn't such a feature make it possible to refactor the following code?

catch case ex: Break[T] @unchecked =>
  if ex.label eq local then ex.value
  else throw ex

I feel we could rewrite it entirely to:

catch case Break(local, value) => value