Dependent type isn't inferred correctly in the body

[peter-jerry-ye]

Compiler version

3.2.0

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(0))
  case x: Iterable[t] => leafElem(x.head)
  case x: AnyVal      => {
    val p: LeafElem[X] = x
    p
  }

Output

the p is not inferred correctly

Expectation

p, which has the same type signature as the return type, gets inferred correctly.

[markehammons]

After reviewing with Marco and Sherwin, I don't think this is actually an inference bug.

Per our understanding, X here refers to a type with very little known about it within leafElem. That's why the type of the shadowed x in the final case is X&AnyVal as opposed to AnyVal. Therefore, it's only appropriate that LeafElem[X] fails to reduce in the context of the fourth case, X != AnyVal (or any of the other cases in the match type) within leafElem, and so the match type stays unreduced. Since x: X & AnyVal doesn't equal LeafElem[X], the first type failure occurs, and since LeafElem[X] cannot be reduced to X within leafElem, the second error occurs when the user tries to return p: LeafElem[X]

cc: @dwijnand

[som-snytt]

   |                           trying to reduce  LeafElem[X]
   |                           failed since selector  X
   |                           does not match  case String => Char
   |                           and cannot be shown to be disjoint from it either.

Intersectionless Scala 2 disallows the pattern match on AnyVal.

In Scala 3, the pattern match really means Any, but it doesn't warn me about that.

[markehammons]

Would saying failed since selector Any be less confusing than failed since selector X here? Maybe if there was an indication that X is roughly equivalent to Any within leafNode?

[markehammons]

To illustrate why this isn't actually a bug:

type LeafElem[X] = X match
  case String => Char
  case Int => Float


def leafElem[X](x: X, y: X): LeafElem[X] = x match
  case x: String      => x.charAt(0)
  case x: Int           => {
     val p: LeafElem[Int] = y.asInstanceOf[Int].toFloat
     p
  }

//class cast exception: Class java.lang.String cannot be cast to Integer
leafElem(4, "hello")

With the match type, we are providing proof of a refined type for a shadowed value x. That refined type does not automatically correspond to X, as evidenced by both x and y in my modified code having type X but having different concrete types.

[dwijnand]

I agree. But, @peter-jerry-ye, feel free to comment if we missed something.

[peter-jerry-ye]

@markehammons Thanks for explaining, now I see that the problem is that X was never replaced in the pattern match expression. Seems that I've misunderstood how things work. Maybe I should just sit and wait for @mbovel to make scala better suited for dependent typed programs.