SI-5900 Fix pattern inference regression

[retronym]

Deets in the commits, review by @adriaanm

/cc @paulp (we'll take another swing at SI-7886 in 2.12)

[paulp]

FYI, if it's not apparent, I went after "Any" specifically because I thought at the time that its kind-polymorphic properties were creating the problem. I might have experienced confirmation bias on that point. But I wouldn't special-case a fix for "Any" knowing that the issue would remain with a slightly less general type.

When it comes to inferring types, Any is like Null's equally evil twin - a nice division by zero to help you prove whatever you want.

[retronym]

Yep, you documented that in the relevant commit comments. Which of course led me to believe it too :)

But after a bit of digging I unbelieved: no HK type params were in the vicinity.

I didn't feel like a real fix was all that far away, but ran out of road.

[paulp]

Having done a bit of reading the last few months, I am convinced that we grossly underestimate the difficulty of sound gadt typing.

[retronym]

My ambitions for the real fix were a bit more modest: I'd like parity between:

trait Contra[-A] { def accept(p: A): Unit }

trait T

object CC {
  case class Unravel[A](m: Contra[A], msg: A) extends T

  object Test {
    def g(m: Contra[Any]): Unit = m accept 5
    def f(x: T): Unit = x match {
      case Unravel(m, msg) => g(m) // allowed, unsound
      case _               =>
    }
    def main(args: Array[String]) {
      f(new Unravel[String](new Contra[String] { def accept(x: String) = x.length }, ""))
    }
  }
}

object Extractor {
  class Unravel[A](m: Contra[A], msg: A) extends T
  object Unravel { def unapply[A](m: Unravel[A]): Option[(Contra[A], A)] = ??? }

  object Test {
    def g(m: Contra[Any]): Unit = m accept 5
    def f(x: T): Unit = x match {
      case Unravel(m, msg) => g(m) // found   : Contra[A] where type A, required: Contra[Any]
      case _               =>
    }
  }
}

I agree the general problem, especially when you throw variance in the mix, is pretty grim.

[paulp]

I agree the general problem, especially when you throw variance in the mix, is pretty grim.

Indeed it is variance which makes me render that verdict.

[paulp]

I guess it's not news that having parallel implementations for case classes and extractors is just a full programmer employment act. Nice job taking the "findMember" count back to one, by the way.

[adriaanm]

I am convinced that we grossly underestimate the difficulty of sound gadt typing.

and here I was, thinking it was near impossible

[adriaanm]

LGTM

The only GADT inference I see as feasible is for hierarchies that accurately model ADTs: sealed and invariant. Then there's the technical challenge: the current implementation for gadt inference is hopeless.

[paulp]

@adriaanm It occurred to me that a practical approach for you guys and your hopeless implementation might be to perform type inference as if everything were invariant, then weaken the inferred types based on the variances of the abstract types to which they correspond. I think this would be a lot easier to do soundly, though it might reject more programs than whatever the theoretically optimal approach is.

[adriaanm]

rebased over yonder