Forbidden to narrow a type with match?

Question
#1

It is unclear to me why the following does not compile:

trait C
trait XC extends C
trait YC extends C

trait Top :
  type Z <: C

trait Other

trait Worker[X <: XC,Y <: YC] extends Top :
  type Z = this.type match
    case Other  => X
    case _      => Y

On the type Z definition it states:

error overriding type Z in trait Top with bounds <: C;
  type Z with bounds = 
  (Worker.this : Worker[X, Y]) match {
    case Other => X
    case Any => Y
  } has incompatible type

When you let the compiler explain itself it ends op with:

 ==> Any  <:  C
 <== Any  <:  C = false

Why should you compare Any with the trait C at all? On the other hand if you:

What am I missing here?

#2

It also seems to work when you double down on the constraint:

type Z <: C = this.type match
  case Other  => X
  case _      => Y

…so it seems to be some kind of inference bug.

1 Like
#3

Nice catch! Work around and bug confirmation in one. Thanks a lot! :smiley:

BTW: the use of this.type causes some problems of its own, which is kind of understandable, since it is not exactly a value known at compile time. However, the situation is the same when using a type parameter:

trait C { def show: Unit }
class XC extends C { def show = println("XC") }
class YC extends C { def show = println("YC") }
   
trait Top :
  type Z <: C

trait Other

trait Worker[X <: XC,Y <: YC, Q] extends Top :
  type Z <: C = Q match
    case Other  => X
    case _      => Y

class Test1() extends Worker[XC,YC,Other] :
  val z: Z = new XC

class Test2() extends Worker[XC,YC,String] :
  val z: Z = new YC

Test1().z.show
Test2().z.show

works with type Z <: C = Q match ... and does not work with only type Z = Q match ...

What still remains a mystery to me is that this works for String (or Int,Long) but not when you put an other trait in like this:

trait That
...
class Test2() extends Worker[XC,YC,That] :
  val z: Z = new YC

which gives the error:

[error] 77 |  val z: Z = new YC
[error]    |             ^^^^^^
[error]    |             Found:   TestZ.YC
[error]    |             Required: Test2.this.Z
#4
1 Like
#5

Thank you. So, the match type is not reduced because it cannot be proven that the types That and Other are disjoint for every instance of Q? And how can i convince the compiler of this?

#6

So, the match type is not reduced because it cannot be proven that the types That and Other are disjoint for every instance of Q?

Why did you make such conclusion?

And how can i convince the compiler of this?

As @sangamon told, you should add the upper bound to the match type.

#7

Why did you make such conclusion?

Well, if you let the compiler explain itself you can observe that the match type was not reduced:

[error]    | Tree: new YC()
[error]    | I tried to show that
[error]    |   YC
[error]    | conforms to
[error]    |   Test2.this.Z
[error]    | but the comparison trace ended with `false`:
[error]    |
[error]    |   ==> YC  <:  Test2.this.Z
[error]    |     ==> YC  <:  That match {   case Other => XC   case Any => YC } <: C (right is approximated)
[error]    |     <== YC  <:  That match {   case Other => XC   case Any => YC } <: C (right is approximated) = false
[error]    |   <== YC  <:  Test2.this.Z = false

as these are the rules for match reduction:

The compiler implements the following reduction algorithm:

* If the scrutinee type S is an empty set of values (such as Nothing or String & Int), do not reduce.
* Sequentially consider each pattern Pi
  a. If S <: Pi reduce to Ti.
  b. Otherwise, try constructing a proof that S and Pi are disjoint, or, in other words, that no value s of type S is also of type Pi.
  If such proof is found, proceed to the next case (Pi+1), otherwise, do not reduce.

Disjointness proofs rely on the following properties of Scala types:
1. Single inheritance of classes
2. Final classes cannot be extended
3. Constant types with distinct values are nonintersecting
4. Singleton paths to distinct values are nonintersecting, such as object definitions or singleton enum cases.

Since (a) is clearly not the case, only (b) can cause reduction. And it looks like That and Other indeed do not supply enough evidence for any of (1) to (4) to be conclusive.

As @sangamon told, you should add the upper bound to the match type.

I interpreted his reply somewhat different but it makes sense, as long as you still provide enough evidence for the compiler to start the reduction. For example with literal types:

trait C { def show: Unit }
class XC extends C { def show = println("XC") }
class YC extends C { def show = println("YC") }
   
trait Top :
  type Z <: C

trait Worker[X <: XC,Y <: YC, Q <: Boolean] extends Top :
  type Z <: C = Q match
    case true  => X
    case false => Y

class Test1() extends Worker[XC,YC,true] :
  val z: Z = new XC

class Test2() extends Worker[XC,YC,false] :
  val z: Z = new YC

Test1().z.show
Test2().z.show

or with object types:

trait C { def show: Unit }
class XC extends C { def show = println("XC") }
class YC extends C { def show = println("YC") }

trait Top:
  type Z <: C

sealed trait Selector
case object Other extends Selector
case object That extends Selector

trait Worker[X <: XC, Y <: YC, Q <: Selector] extends Top:
  type Z <: C = Q match
    case Other.type => X
    case That.type  => Y

class Test1() extends Worker[XC, YC, Other.type]:
  val z: Z = new XC

class Test2() extends Worker[XC, YC, That.type]:
  val z: Z = new YC

Test1().z.show
Test2().z.show

But i think we have it all clear now. Again, thx for the help, i learned that matching a type is not the same as a match type. :wink:

1 Like
#8

But you don’t need reduction rules. this.type match { case Other => X; case _ => Y} can’t reduce for arbitrary this.type. The error error overriding type Z in trait Top with bounds <: C you quoted in the 1st post means that the compiler can’t see that the match type <: C. So you need subtyping rules rather than reduction rules. And none of the 3 subtyping rules is applicable now as I wrote at Stackoverflow. The 3rd rule becomes applicable if you add the upper bound.

1 Like