Intersection, match types and tuples don't work together

[Katrix]

Compiler version 3.0.0

Seems the compiler doesn't like it when intersection, match types and tuples are used together. Yes, opaque types are a better match here, but need this for Shapeless, and don't want to break the API here.

Minimized code

Use only one definition of WrapUpper and Wrap in the below code. The one relying on tuples does not work, while the one using a sealed trait does

type FieldType2[K, +V] = V with KeyTag2[K, V]
trait KeyTag2[K, +V] extends Any

//summon[TupleToHList[Tuple1[FieldType2["i", Int]]] =:= (FieldType2["i", Int] :: HNil)]

sealed trait ABox
trait Box[A] extends ABox

//Works
//type WrapUpper = ABox
//type Wrap[A] = Box[A]

//Doesn't work
type WrapUpper = Tuple
type Wrap[A] = Tuple1[A]

type Extract[A <: WrapUpper] = A match {
  case Wrap[h] => h
}

type ExtractWrap1[A, Wrap[_]] = Wrap[A] match {
  case Wrap[h] => h
}

type ExtractWrap2[A] = Extract[Wrap[A]]

summon[Extract[Wrap[Int]] =:= Int] //Works
summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]] //Does not reduce
summon[ExtractWrap1[FieldType2["foo", Int], Wrap] =:= FieldType2["foo", Int]] //Works
summon[ExtractWrap2[FieldType2["foo", Int]] =:= FieldType2["foo", Int]] //Works

Output

[error] -- Error: D:\DevProjects\Incubating\shapeless2-port-start\src\main\scala\shapeless\testing.scala:61:74
[error] 61 |  summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]] //Does not reduce
[error]    |                                                                          ^
[error]    |           Cannot prove that shapeless.TypeBug.Extract[
[error]    |             Tuple1[shapeless.TypeBug.FieldType2[("foo" : String), Int]]
[error]    |           ] =:= shapeless.TypeBug.FieldType2[("foo" : String), Int].

Expectation

It should compile. Putting the Extract and Wrap types closer together does work fine, which works counter to how I would expect them to work. Either none, or all.

[LPTK]

type FieldType2[K, +V] = V with KeyTag2[K, V]
trait KeyTag2[K, +V] extends Any

Note that this encoding is unsafe, as was explained time and time again on the contributors forum.

It seems this (sound) version works fine:

type FieldType2[K, +V] = V with KeyTag2[K, V]
type KeyTag2[K, +V]

[romanowski]

@smarter would it be possible to detect such cases and warn about unsoundness in failure message?

[smarter]

Not sure what you mean, the unsoudness @LPTK mentioned comes from using asInstanceOf which isn't present in the code in this issue. Concerning the match type itself I'll let @OlivierBlanvillain decide if this should reduce or not.

[OlivierBlanvillain]

This is working as intended, the non-reducing case does not reduce because of the following line from the spec:

If the scrutinee type S is an empty set of values (such as Nothing or String & Int), do not reduce.

Here Tuple1[FieldType2["foo", Int]] is uninhabited because is has a field of type FieldType2["foo", Int] which is itself uninhabited because "foo" with KeyTag2[...] is uninhabited (String is final and does not extend KeyTag2).

In the reducing cases (with ExtractWrap1 and ExtractWrap2), the compiler doesn't see the issue because reduction happens "in the abstract" (A and Wrap are not substituted). Although I agree that this is surprising, I don't think this could be exploited to get a soundness hole because the compiler doesn't generate any erroneous subtyping/disjointness evidence.