Compiler issues unnecessary warning when it "knows" better

[DavidGoodenough]

Compiler version

3.6.3

Minimized code

case class CaseClass(a:Int)
case class Error(a:Int)

abstract class fred{
  def method:CaseClass | Error

  method match {
    case t:CaseClass => // use t which is a CaseClass
    case e:Error => // use e which is an error
    }

  def method2:Seq[CaseClass] | Error

  method2 match {
    case s:Seq[CaseClass] => // issues an unnecessary warning that the class of the elements can not be checked
    case e:Error => // use e which is an error
    }
  method2 match {
    case s:Seq[?] => s.asInstanceOf[Seq[CaseClass]] // is needed to let the code here know what type s is
    case e:Error =>
    }
  }

Output

The compiler will issue a warning that the type of the elements of the first call to method2 can not be checked at runtime. Having to use an asInstanceOf to bypass this warning is an admisssion of failure.

Expectation

The compiler should realise that there is no need to check this at runtime as it would not have allowed anything other than CaseClass elements to in the Seq in the implementation of method2.

[s5bug]

The compiler is correct in warning you here (as in, this is not a bug): that match case is unsound. Error is not final, meaning I could define a class such as

class Foo extends Error(???) with Seq[SomethingUnrelated]

This means that method2 could produce Foo, which would match against Seq, but not be a Seq[CaseClass].

Make Error final via final case class Error(... and you will not see this warning.

[arturaz]

The error message could be better than :)

[s5bug]

The full error message is

the type test for Seq[CaseClass] cannot be checked at runtime because its type arguments can't be determined from Error

Maybe extra explanation is warranted when Error is a non-final, non-sealed case class.

[DavidGoodenough]

Following on from @s5bug 's first comment, I thought that perhaps another solution would be to reverse the order of the cases. That way all the non-final-ness of Error would have been removed from the equation when it came to the second case. But no, the same error persists.

so:-

method2 match {
  case e:Error => e // e is an Error
  case s:Seq[CaseClass] => s  // is a Seq[CaseClass] but still gives the same warning
  }

and even leaving the class qualification off the second case:-

method2 match {
  case e:Error => e // is an Error
  case s => s // is a Seq[CaseClass] | Error 

I do not understand, given that as I read the spec cases are evaluated in the order they are in the source code,
how s could be an Error2 as already been collected by the first case.