Match type reduction failure on opaque type

Question
1

The code

object Scope:
  opaque type W[+I <: Int] = I

import Scope.*

type Equal[I, J] = I match
  case J => true
  case Any => false

summon[Equal[W[0], W[1]] =:= false]

leads to a compile error on the last line:

Cannot prove that Equal[W[(0 : Int)], W[(1 : Int)]] =:= (false : Boolean).

Note: a match type could not be fully reduced:

  trying to reduce  Equal[W[(0 : Int)], W[(1 : Int)]]
  failed since selector W[(0 : Int)]
  does not match  case W[(1 : Int)] => (true : Boolean)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case Any => (false : Boolean)

Why is that? Is there any way to fix it while keeping W opaque?

2

Outside of Scope, all you know is that W is some
type W[+I <: Int] >: Nothing <: Any.

Clearly that can never be enough information to prove W[0] disjoint from W[1]. One particular instance of W that make them definitely not disjoint would be
type W[+I <: Int] = String.

Using match types with opaque type aliases will almost never do something useful, because opaque type aliases deliberately hide the information that match types need.

5 Likes
3

I see. Thank you. I thought it was the other way around: outside of the scope where the opaque type is defined, it would always be considered disjoint from any other type, even the one it’s defined to be underneath.

That is how opaque types behave otherwise. The fact that both W[0] and W[1] both happen to be “implemented” by String underneath seems irrelevant from a typing perspective outside of Scope. None of the methods from String are available on either, for example.

But I guess it unfortunately has to be this way, due to the dynamic nature of normal pattern matching in Scala. In this sense, opaque types are not actually fully opaque, but somewhat leaky. Perhaps match types with opaque types should raise some kind of compiler warning (which could be extended to similar matches at the term level).