Tuple.Filter doesn't work if the result tuple type is of length more than 1

[prolativ]

Minimized code

import Tuple.Filter

type IsString[x] = x match {
  case String => true
  case _ => false
}

val x = summon[Filter[(Char, Int), IsString] =:= EmptyTuple]
val y = summon[Filter[("abc", Int), IsString] =:= Tuple1["abc"]]
val z = summon[Filter[("abc", "def"), IsString] =:= Tuple2["abc", "def"]]

Output

val z = summon[Filter[("abc", "def"), IsString] =:= Tuple2["abc", "def"]]
                                                                         ^
Type argument IsString does not conform to upper bound [_$6] =>> Boolean in subpart scala.Tuple.Filter[scala.Tuple$package.EmptyTuple.type, IsString] of inferred type 
  (("abc" : String) *: ("def" : String) *: 
    scala.Tuple.Filter[scala.Tuple$package.EmptyTuple.type, IsString]
  )

Expectation

This should compile and an evidence for type equality should be correctly synthesized

[prolativ]

It looks like the example can be fixed by adding a type bound on the match type

type IsString[x] <: Boolean = x match {
  case String => true
  case _ => false
}

Now the question is: is the fact that the compiler cannot inter the bounds actually a bug or is this an inherent limitation of match types?
Also is there a way to express type bounds when using a type lambda?

One more suspicious thing is that if the bounds are not specified then

val x = summon[Filter[(Char, Int), IsString] =:= EmptyTuple]

does work even though

type Filtered = Filter[(Char, Int), IsString]

itself does not compile

[nicolasstucki]

@OlivierBlanvillain is the match type x match { case String => true; case _ => false } supposed to be a subtype of type true | false?

[OlivierBlanvillain]

@nicolasstucki No: http://dotty.epfl.ch/docs/reference/new-types/match-types.html#subtyping-rules-for-match-types

[nicolasstucki]

Does that mean that the current behavior is correct (i.e. we need the extra <: Boolean)?

[prolativ]

The noncompiling snippet was taken from the documentation of Tuple.Filter so if the conclusion is that this behaviour is correct then we should at least update the docs but I'm still wondering whether this used to compile in the past and if so why this couldn't continue to compile

[nicolasstucki]

Indeed, we should update the docs

[mbovel]

Documentation seems to have been fixed by 7af9a40.

[mbovel]

Does that mean that the current behavior is correct (i.e. we need the extra <: Boolean)?

Seems legit to me. By the current typing rules, match types are not subtypes of the union of their cases.