Dotty: Dependent Typing example no longer works with `-source:3.1` and `Matchable`

[deanwampler]

Minimized code

The example here, https://dotty.epfl.ch/docs/reference/new-types/match-types.html#dependent-typing fails when 3.1 is enabled. I'm posting this as a bug, because it's not clear to me how to make it work. Reproducing the code here, the match type definition works fine:

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

But the method doesn't:

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

The error messages are these:

2 |   case x: String      => x.charAt(0)
  |           ^^^^^^
  |           pattern selector should be an instance of Matchable,
  |           but it has unmatchable type X instead
3 |   case x: Array[t]    => leafElem(x(9))
  |           ^^^^^^^^
  |           pattern selector should be an instance of Matchable,
  |           but it has unmatchable type X instead
4 |   case x: Iterable[t] => leafElem(x.next())
  |           ^^^^^^^^^^^
  |           pattern selector should be an instance of Matchable,
  |           but it has unmatchable type X instead
5 |   case x: AnyVal      => x
  |           ^^^^^^
  |           pattern selector should be an instance of Matchable,
  |           but it has unmatchable type X instead
4 |   case x: Iterable[t] => leafElem(x.next())
  |                                   ^^^^^^
  |value next is not a member of X & Iterable[t] - did you mean x.head?
  |
  |where:    X is a type in method leafElem with bounds >: (?1 : Iterable[t])

(There's also a bug in the Iterable line; it doesn't like x.next(). Using x.head does work...)

Adding a bound to X reduces the problem to the Array and Iterable lines:

scala> def leafElem[X <: Matchable](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.head)
     |    case x: AnyVal      => x
     |
3 |   case x: Array[t]    => leafElem(x(9))
  |                                   ^^^^
  |                                 value should be an instance of Matchable,
  |                                 but it has unmatchable type t instead
4 |   case x: Iterable[t] => leafElem(x.head)
  |                                   ^^^^^^
  |                                 value should be an instance of Matchable,
  |                                 but it has unmatchable type t instead

I've tried various ways to fix those warnings, like the following, which fail for different reasons:

def leafElem[X <: Matchable, X2 <: Matchable](x: X): LeafElem[X] = x match
   case x: String       => x.charAt(0)
   case x: Array[X2]    => leafElem(x(9))
   case x: Iterable[X2] => leafElem(x.head)
   case x: AnyVal       => x

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

Output

Inline above.

Expectation

Defining leafElem would be as straightforward as it is with Scala 3.0 flexibility.

[odersky]

Thanks for the example, Dean! I tried:

def leafElem[X](x: X): LeafElem[X] = a.asInstanceOf[Matchable] match
   case x: String      => x.charAt(0)
   case x: Array[t]    => leafElem(x(9))
   case x: Iterable[t] => leafElem(x.head)
   case x: AnyVal      => x

but that does not work either since the match does not reduce. Looks like we have to do something about this class of cases.
I see three possibilities:

1. Make the code with the asInstanceOf reduce correctly. Not sure how hard that would be. @OlivierBlanvillain, what do you think?
2. Provide an escape hatch to allow matches against opaque scrutinees. Maybe re-use unchecked:
   scala def leafElem[X](x: X): LeafElem[X] = (a: @unchecked) match case x: String => x.charAt(0) case x: Array[t] => leafElem(x(9)) case x: Iterable[t] => leafElem(x.head) case x: AnyVal => x
   This means we conflate @unchecked for exhaustivity warnings and matchability warnings. But that's not a big issue since
   no exhaustivity warnings would work for unmatchable scrutinees anyway.
3. Same as (2), but with unchecked on each pattern.
   scala def leafElem[X](x: X): LeafElem[X] = a match case x: String: @unchecked => x.charAt(0) case x: Array[t]: @unchecked => leafElem(x(9)) case x: Iterable[t]: @unchecked => leafElem(x.head) case x: AnyVal: @unchecked => x
   This is closer in spirit to the other use of unchecked on patterns (i.e. here's a type that we cannot check at runtime), but a lot more annoying to write.
4. Same as (2) but with a different annotation, e.g. @uncheckedMatchable.

Opinions?

[abgruszecki]

I think it makes sense to have the Matchable warning look for an annotation on the scrutinee, since it's intuitively the first place we look to check if the warning applies or not. In general, I think annotations that turn warnings off should be as precise as is reasonable, but here it also makes sense to me to have @unchecked turn off both exhaustivity and Matchable warnings - I can't think of a case where we want to turn off one and not the other.

[OlivierBlanvillain]

This seems to work:

def leafElem[X](x: X): LeafElem[X] = x.asInstanceOf[Matchable & X] match { ... }

If that's the recommended escape hatch to match on Any then I guess it's good enough for the docs...

[odersky]

Good that x.asInstanceOf[Matchable & X] works. But it might be too
non-obvious as a recommendation. So I'd tend towards @unchecked as a
simpler alternative.

On Wed, Dec 30, 2020 at 7:32 AM Olivier Blanvillain <
[email protected]> wrote:

This seems to work:

def leafElemX: LeafElem[X] = x.asInstanceOf[Matchable & X] match { ... }

If that's the recommended escape hatch to match on Any then I guess it's
good enough for the docs...

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/lampepfl/dotty/issues/10930#issuecomment-752345845,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/AAGCKVRWMHMW6GIOAKC25A3SXLCPLANCNFSM4VLIAS6Q
.

--
Prof. Martin Odersky
LAMP/IC, EPFL