Pattern matching on classes containing generalized type constraints

Not an answer but something to think about:

case class Sub1[A, B](a: A, f: B => B)
case class Sub2[A, B](a: A, f: B => Unit)

def foo[A, B](a: A, f: B => B)(implicit ev: A =:= B) = f(a)
def bar[A, B](a: A, f: B => Unit)(implicit ev: A =:= B) = f(a)

def dispatch(obj: Any) = obj match {
    case Sub1(a, f) => foo(a, f)
    case Sub2(a, f) => bar(a, f) // type mismatch: found: Nothing => Unit. required: B => Unit
}

This code have the same problem as yours but Sub1 and Sub2 case classes don't even have implicit blocks.

implicit section in case class doesn't effect pattern resolution. This section is just syntax sugar for calling apply(a: A, f: B => B)(implicit val ev: A =:= B) method on Sub1/2's companion objects. Pattern matching use unapply method to match the pattern at runtime and this unapply don't even know about evidences.

But I'm still wondering why first case is compiled without having this evidence.

Edit: Adding helpful comment from @AlexeyRomanov

More type inference than type erasure. But yes, the compiler infers type Any for a and Any => Any for f and then produces and uses evidence that Any =:= Any. In the second case it infers Nothing => Unit for f, because B => Unit is contravariant in B, and fails to find Any =:= Nothing.

You can actually make it work using type variable patterns:

def dispatch(obj: Sup) = {
    obj match {
      case obj: Sub[a, b] => foo(obj.a, obj.f)(obj.ev)
      case obj: Sub2[a, b] => bar(obj.a, obj.f)(obj.ev)
    }
  }

This part is an answer to the comments, because it doesn't really fit in there:

Btw, there is still one subtlety I do not get: why is B => Unit contravariant in B

what is compiler's logic for this Nothing => Unit inference staff

You need to start with function variance. X => Y is a subtype of X1 => Y1 if and only if X is a supertype of X1 and Y is a subtype of Y1. We say it's contravariant in X and covariant in Y.

So if you fix Y = Unit, what remains is just contravariant in X. Any => Unit is a subtype of String => Unit, which is a subtype of Nothing => Unit. In fact, Nothing => Unit is the most general of all B => Unit, and that's why it gets inferred in the Sub2 case.

and B => B not (since it infers Any => Any) ?

The situation with B => B is different: String => String is neither a subtype nor a supertype of Any => Any, or of Nothing => Nothing. That is, B => B is invariant. So there is no principled reason to infer any specific B, and in this case the compiler uses the upper bound for B (Any), and B => B becomes Any => Any.