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.

[Katrix]

Hmmm. I see. I managed to find a case where the code LPTK posted also does not reduce. Is it a bug that I found such a case then, or is it a bug that the code LPTK posted works here? I can't imagine both versions being valid.

[OlivierBlanvillain]

Can you send an updated example? (I'm really unfamiliar with this FieldType2/KeyTag2 encoding)

[Katrix]

object DoesntWork {
  type FieldType[K, +V] = V with KeyTag[K, V]
  type KeyTag[K, +V]
  
  type ->>[K, +V] = FieldType[K, V]

  type FindField[R <: scala.Tuple, K] = R match {
    case FieldType[K, f] *: t => f
    case _ *: t => FindField[t, K]
  }

  type R = ("A" ->> Int) *: ("B" ->> Double) *: ("C" ->> String) *: ("D" ->> Boolean) *: EmptyTuple
  summon[FindField[R, "B"] =:= Double]
}

FindField[R, "A"] =:= Int works, but none of the others

[LPTK]

@Katrix we should certainly get to the bottom of your issue and determine if it should or shouldn't fail, but in the meantime I wonder why you wouldn't use a much simpler encoding for this thing you're trying to do.

The following works:

object MyLib:
  opaque type FieldType[K, +V] = V
  type KeyTag[K, +V]
  type ->>[K, +V] = FieldType[K, V]
  type FindField[R <: scala.Tuple, K] = R match
    case FieldType[K, f] *: t => f
    case _ *: t => FindField[t, K]
import MyLib._

object Works:
  type R = ("A" ->> Int) *: ("B" ->> Double) *: ("C" ->> String) *: ("D" ->> Boolean) *: EmptyTuple
  summon[FindField[R, "B"] =:= Double]

[OlivierBlanvillain]

@Katrix I don't think the compiler can safely conclude that FieldType("A", Int) and FieldType("B", f) are disjoint (for any f). These types dealias to Int with KeyTag["A", Int] and f with KeyTag["B", f]. Int and f are clearly overlapping, and KeyTag is just an abstract type, so who knows what it will be instantiated to (as far as the compiler is concerned object foo extends DoesntWork { type KeyTag[K, +V] = Any } would break any disjointness result).

[joroKr21]

Does opaque type FieldType[K, +V] <: V = V work?

[Katrix]

It does yes, and what's currently used