Match types are broken (or documentation is wrong)

[tabdulradi]

Hello 👋 I copied Match types example from the docs into Scastie, but it didn't compile.

Compiler version

3.0.0-M3

Minimized code

type LeafElem[X] = X match
   case String => Char
   case Array[t] => LeafElem[t]
   case Iterable[t] => LeafElem[t]
   case AnyVal => X

def leafElem[X](x: X): LeafElem[X] = x match
   case x: String      => x.charAt(0)
   case x: Array[t]    => leafElem(x(9))
   // case x: Iterable[t] => leafElem(x.next())
   case x: AnyVal      => x

Output

Found: Char
Required: LeafElem[X]
where: X is a type in method leafElem with bounds >: (?1 : String)

Found: t
Required: X
where: X is a type in method leafElem with bounds >: (?2 : Array[t])

Found: (x : X & AnyVal)
Required: LeafElem[X]
where: X is a type in method leafElem with bounds >: (?3 : AnyVal)
​

Expectation

Code should compile

[OlivierBlanvillain]

There is a typo in the docs, it should be .head and not .next() (the next method is not defined on scala.collection.Iterable).

However I don't think the code you wrote in the issue should compile, the match expression has one less case than the match type, so it doesn't fulfill the 3rd requirement stated in the Dependent Typing section (the match expression and the match type have the same number of cases).

[LPTK]

@OlivierBlanvillain it would be really helpful if the compiler could give the reason why the match could not be type-checked successfully, in the original code. Instead, it currently yields many errors that point the programmer in the wrong direction. I did not know there was special reasoning in the compiler for making matches in types and terms match, so I thought the problem was with GADT-style reasoning and the like (as the errors seemed to imply).