Type-level "IsPermutation" match type in Scala 3

Question

I'm doing some exercises to get a feel for Dotty's match types etc., and I'm having some trouble. In particular, I'd like to write a (recursive) match type IsPermutation[T1 <: Tuple, T2 <: Tuple] that evaluates to true if T1 and T2 are permutations, allowing for duplicates.

The behavior I'd like is:

  val _1 : IsPermutation[(Int, Int), (Int, Int)] = true
  val _2 : IsPermutation[(Int, String), (String, Int)] = true
  val _3 : IsPermutation[(Int, String), (Int, Int)] = false
  val _4 : IsPermutation[(Int, Int, Int), (Int, Int)] = false
  val _5 : IsPermutation[(Int, Int), Tuple1[Int]] = false

What I've come up with is:

  type IsPermutation[T <: Tuple, T2 <: Tuple] <: Boolean = (T, T2) match {
    case (EmptyTuple, EmptyTuple) => true
    case (EmptyTuple, _) => false
    case (_, EmptyTuple) => false
    case (h *: tail, _) => IsPermutation[tail, Remove[T2, h]]
  }

  type Remove[T <: Tuple, X] <: Tuple = T match {
    case EmptyTuple => EmptyTuple
    case head *: tail => head match {
      case X => tail
      case _ => head *: Remove[tail, X]
    }
  }

I get errors like:

[error] -- [E007] Type Mismatch Error: /home/dlwh/src/bora/src/test/scala/bora/MetaTest.scala:23:53 
[error] 23 |    val _1 : IsPermutation[(Int, Int), (Int, Int)] = true
[error]    |                                                     ^^^^
[error]    |Found:    (true : Boolean)
[error]    |Required: bora.Meta.IsPermutation[Int *: scala.Tuple$package.EmptyTuple.type, 
[error]    |  bora.Meta.Remove[(Int, Int), Int]
[error]    |]
^[c[error] -- [E007] Type Mismatch Error: /home/dlwh/src/bora/src/test/scala/bora/MetaTest.scala:24:59 
[error] 24 |    val _2 : IsPermutation[(Int, String), (String, Int)] = true
[error]    |                                                           ^^^^
[error]    |Found:    (true : Boolean)
[error]    |Required: bora.Meta.IsPermutation[String *: scala.Tuple$package.EmptyTuple.type, 
[error]    |  bora.Meta.Remove[(String, Int), Int]
[error]    |]
[error] -- [E007] Type Mismatch Error: /home/dlwh/src/bora/src/test/scala/bora/MetaTest.scala:25:56 
[error] 25 |    val _3 : IsPermutation[(Int, String), (Int, Int)] = false
[error]    |                                                        ^^^^^
[error]    |Found:    (false : Boolean)
[error]    |Required: bora.Meta.IsPermutation[String *: scala.Tuple$package.EmptyTuple.type, 
[error]    |  bora.Meta.Remove[(Int, Int), Int]
[error]    |]
[error] -- [E007] Type Mismatch Error: /home/dlwh/src/bora/src/test/scala/bora/MetaTest.scala:26:58 
[error] 26 |    val _4 : IsPermutation[(Int, Int, Int), (Int, Int)] = false
[error]    |                                                          ^^^^^
[error]    |Found:    (false : Boolean)
[error]    |Required: bora.Meta.IsPermutation[(Int, Int), bora.Meta.Remove[(Int, Int), Int]]

I was expecting reductions like

  //   IsPermutation[(Int, String), (String, Int)]
  // = IsPermutation[(String,)    , Remove[(String, Int), Int]]
  // = IsPermutation[(String,)    , (String,)]
  // = IsPermutation[EmptyTuple    , Remove[(String,), String] ]
  // = IsPermutation[EmptyTuple    ,  EmptyTuple]
  // = true

EDIT: This appears to work but I'd really like to know why the first approach doesn't work.

  type Remove[T <: Tuple, X] <: Tuple = T match {
    case EmptyTuple => EmptyTuple
    case head *: tail => head match {
      case X => tail
      case _ => head *: Remove[tail, X]
    }
  }

// this doesn't work, even after removing various type bounds and things
//  type Without[T <: Tuple, T2 <: Tuple] = Tuple.Fold[T2, T, Remove]
  type Without[T <: Tuple, T2 <: Tuple] <: Tuple = T2 match {
    case head *: tail => Without[Remove[T, head], tail]
    case EmptyTuple => T
  }
  type IsEmpty[T <: Tuple]<: Boolean = T match {
    case EmptyTuple => true
    case _ => false
  }

  type IsPermutation[T <: Tuple, T2 <: Tuple] = (IsEmpty[Without[T, T2]] && IsEmpty[Without[T2, T]])