Forbidden to narrow a type with match?

devlaam · March 10, 2023, 9:57am

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:

remove the constraint type Z <: C it compiles just fine
but also if you replace case Other => X by case _ => X
even when you extend Worker with Other.

What am I missing here?

sangamon · March 10, 2023, 8:02pm

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.

devlaam · March 10, 2023, 8:34pm

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

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

DmytroMitin · March 14, 2023, 12:40am

devlaam · March 14, 2023, 11:17am

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?

DmytroMitin · March 14, 2023, 4:44pm

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.

devlaam · March 15, 2023, 9:59pm

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.

DmytroMitin · March 15, 2023, 10:48pm

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.

DmytroMitin · April 1, 2023, 10:27am

github.com/lampepfl/dotty-feature-requests

Match types should be subtypes of the union of their case right-hand sides

opened 03:46PM - 30 Dec 19 UTC

LPTK

A match type is apparently not a subtype of the union of it branches. So this fo…r instance does not work: ```Scala def flip: (x: 0 | 1) => x.type match { case 0 => 1 case 1 => 0 } = ??? val n: 0 | 1 = if ??? then 0 else 1 flip(n) // works flip(flip(n)) // does not work: we don't have flip(n).type <: 0 | 1 val m: n.type match { case 0 => 1 case 1 => 0 } = flip(n) flip(m) // does not work ``` ```Scala -- [E007] Type Mismatch Error: tests/pos/i7807.scala:15:8 -------------------------------------------------------------- 15 | flip(m) | ^ | Found: (Test.m : | (Test.n : (0 : Int) | (1 : Int)) match { | case (0 : Int) => (1 : Int) | case (1 : Int) => (0 : Int) | } | ) | Required: (0 : Int) | (1 : Int) ``` I would have expected it to work. ---- This was originally reported here: https://github.com/lampepfl/dotty/pull/7835#discussion_r361741296. I think it ought to work, because whatever a match type reduces to, it is always one of its right-hand-sides, given some values for the types extracted from the pattern. Conceptually, the match type would be a subtype of the union of the match right-hand sides with the extracted type variables converted to wildcards (or otherwise avoided); for example we should treat `X match { case List[t] => (t, t) }` as a subtype of `(_, _)`. The algorithm could be the following: when solving a subtyping constraint with a match type on the left, try each right-hand side of the match type separately, making the pattern-extracted type variables rigid skolem variables (it looks like this can be done with the `typer.ProtoTypes.constrained(_: TypeLambda)` method). I have tried adapting `recur` in `TypeComparer` to try the `alternatives` of a match type: ```diff - recur(tp1.underlying, tp2) || compareMatch + recur(tp1.bound, tp2) || tp1.alternatives.forall(recur(_, tp2)) || compareMatch ``` But this has problems with recursive match types: indeed, for these we will get into infinite deep subtyping recursions! I did not find a way to detect if a match type is recursive. However, it should be possible to use the following approximation: if the match type has an explicit bound, assume it may be recursive; otherwise, use the algorithm above. This is sound because a recursive match type without a bound will give a cycle error anyways. There is currently no way to test if a bound was provided explicitly (currently `Any` is picked during type assignment if no bound was given), but it could probably be done. An alternative would be to pick the type union as the bound itself when no bound is given. What do you think?

github.com/lampepfl/dotty

Use union of cases as default bound of match types

lampepfl:master ← dotty-staging:fix-90

opened 02:38PM - 23 Jan 20 UTC

OlivierBlanvillain

+48 -31

Fix https://github.com/lampepfl/dotty-feature-requests/issues/90 This PR impl…ements what @LPTK suggested at the end of the issue, which is to use the union of cases as the bound of match types when no bounds are provided. Unfortunatly the snippet from the linked issue still doesn't compile, but I think the remaining issue might be unrelated to match type (see #8084).

DmytroMitin · April 1, 2023, 10:29am

M.Odersky:

I believe it would be not at all easy to implement since it can cause new cycles. What is the upper bound of a recursive match type?