Type Function Alias behaves differently from the inlined version of the type alias

[dlwh]

Compiler version

3.0.2, 3.1.0-RC1

Minimized code

The core of it seems to be that the Demote type function causes an error (in this specific place _2d) when it's behind a type alias (here Sub), but it's fine when the type alias is inlined (as in _2c)

Sorry this is so long. I tried to minimize as much as I could, but without understanding what's really going on I couldn't get it reduced any further.

It's possible to fix by removing the Tuple1[t] case in Demote, but there are no Tuple1s involved in calls to Demote so I don't understand why that should impact it.

object Meta:
  type Shape = String | Tuple

  type Demote[S <: Tuple]<: Shape = S match
    case Tuple1[t] => t & Shape
    case Tuple => S

  type If[T <: Boolean, R1, R2] <: R1 | R2 = T match
    case true => R1
    case false => R2

  type Contains[T <: Tuple, X] <: Boolean = T match
    case X *: r => true
    case _ *: r => Contains[r, X]
    case _ => false

  type RemoveStrict[T <: Tuple, X] <: Tuple = T match
    case head *: tail => head match
      case X => tail
      case _ => head *: RemoveStrict[tail, X]

  type WithoutStrict[T <: Tuple, T2 <: Tuple] <: Tuple = T2 match
    case head *: tail => WithoutStrict[RemoveStrict[T, head], tail]
    case EmptyTuple => T

  /** Removes all elems from ToReplace and replaces the first replaced elem with replacement */
  type ReplaceAllStrict[T <: Tuple, ToReplace <: Tuple, Replacement] <: Tuple = T match
    case head *: tail =>
      If[Contains[ToReplace, head],
          Replacement *: WithoutStrict[tail, RemoveStrict[ToReplace, head]],
          head *: ReplaceAllStrict[tail, ToReplace, Replacement]]
    case EmptyTuple => T

  type Sub[S <: Tuple, ToReplace <: Tuple, Replacement <: String] =
    Demote[ReplaceAllStrict[S, ToReplace, Replacement]]

object Foo:
  import Meta._
 // val _0: Sub["batch" *: EmptyTuple, Int *: EmptyTuple, "batch"] = "batch"
 //  val _1: Sub[("batch", "len"), ("batch", "len"), "batch"] = "batch"
 //  val _2a: ReplaceAllStrict[("batch", "len", "embed"), "batch" *: EmptyTuple, "b"] = ("b", "len", "embed")
  type S = ("batch", "len")
  type ToReplace = "batch" *: EmptyTuple
  type Replacement = "b"
  val _2b: ReplaceAllStrict[S, ToReplace, Replacement] = ("b", "len") // ok
  val _2c: Demote[ReplaceAllStrict[S, ToReplace, Replacement]] = ("b", "len") // ok
  val _2d: Sub[S, ToReplace, Replacement] = ("b", "len") // error, see below

Output

48 |  val _2d: Sub[S, ToReplace, Replacement] = ("b", "len")
   |                                            ^^^^^^^^^^^^
   |Found:    (String, String)
   |Required: Meta.Sub[Foo.S, Foo.ToReplace, Foo.Replacement]
   |
   |Note: a match type could not be fully reduced:
   |
   |  trying to reduce  Meta.Sub[Foo.S, Foo.ToReplace, Foo.Replacement]
   |  trying to reduce  Meta.Demote[Meta.ReplaceAllStrict[Foo.S, Foo.ToReplace, Foo.Replacement]]
   |  failed since selector  Foo.Replacement *: 
   |  Meta.WithoutStrict[("len" : String) *: EmptyTuple.type, 
   |    Meta.RemoveStrict[Foo.ToReplace, ("batch" : String)]
   |  ]
   |  does not match  case Tuple1[t] => t & Meta.Shape
   |  and cannot be shown to be disjoint from it either.
   |  Therefore, reduction cannot advance to the remaining case
   |
   |    case Tuple => Meta.ReplaceAllStrict[Foo.S, Foo.ToReplace, Foo.Replacement]

Expectation

I would expect that type aliases should behave identically to the "inlining" of them