GADT bounds are not precise enough

[Blaisorblade]

#1754 is fixed but the error in #3990 seems incorrect:

case class One[T](fst: T)

object Test {
  def bad[T](e: One[T]) = e match {
    case foo: One[a] =>
      val t: T = e.fst
      val nok: Nothing = t // should not compile
      val ok: a = t // does compile
  }
}

The nok line should not compile because T = a, as shown by the ok line, but the error claims that T >: a, which is true but incomplete and misleading:

7   |      val nok: Nothing = t // should not compile
    |                         ^
    |                  found:    T(t)
    |                  required: Nothing
    |
    |                  where:    T is a type in method bad with bounds >: a

[smarter]

The problem is deeper than the error message I think, in the following code the return type of bla in inferred to be One[_ >: T] and not One[T]:

case class One[T](fst: T)

object Test {
  def bad[T](e: One[T]) = e match {
    case foo: One[a] =>
      foo
  }
}

[smarter]

This has the same root cause as what I described in #4069 (comment), we end up with constraints a >:> T and T >:> a but we don't unify them, so a value of type One[a] becomes a value of type One[_ >: T] outside of the scope where a is defined.