Why does this code produce an unchecked refinement warning?

Question
1 
import scala.language.strictEquality

sealed trait A:
  type B

trait C extends A:
  val value: B 
  
class D extends A 

def fn(a: A{ type B }, b: A{ type B = a.B})(using CanEqual[a.B, a.B]) = 
  (a,b) match 
    case (_a: C{type B = a.B}, _b: C) => 
      _a.value == _b.value

The behavior in this code is a little confusing to me. _b pattern matched to C has the refinements indicating that it’s value is the same type as a.A. In order to get the compiler to recognize that _a.value is the same type as a.B, I have to use the refinement type in the match pattern, but then the compiler complains that this refinement is unchecked at runtime. I realize that the refinement cannot actually be checked at runtime, but at the same time, following the definition of everything, I do not see how _a.value can be anything but the type a.B and so I’m not sure why the compiler cannot figure this out (but can in the case of _b).

2

The typer does not now that _a is a, but we can let it know by adding an explicit type:

def fn(a: A{ type B }, b: A{ type B = a.B})(using CanEqual[a.B, a.B]) = 
  (a,b) match 
    case (_a: (a.type & C), _b: C) => // match on a.type, which cannot fail
      _a.value == _b.value

The question then becomes, why doesn’t the rest of the compiler tell the typer ? (that _a also has type a)
That I’m not sure, I assume it’s because it would make errors less legible, or that nobody thought of doing it

Concerning the noisier errors, it’s already what happens with a.nn which has type a.type & ..., those are used much less often however

3

Oh and _a: C{ type B = a.B} is another way to make the typer know, but crucially, it cannot be checked (something something erasure)

On the other hand _a: a.type can be checked at runtime: _a == a

1 Like