Incorrect code ends up passing the typechecker due to GADT logic misfiring

[djspiewak]

Minimized code

This could probably be minimized further.

import cats.Order
import cats.implicits._

def test[F[_], B](lhs: F[B], tolerance: B)(implicit ord: Order[F[B]]): Boolean =
  (lhs: F[B]) <= (tolerance: B)

Cats 2.1.1 compiled for Scala 2.13.

Output

Compiles and results in a ClassCastException.

Expectation

Shouldn't compile. The ascriptions aren't necessary to trigger the bug, I just included them for clarity.

This may be specific to the Scala 2 unpickler. I wasn't able to reproduce it with this pure-Dotty minimization:

object Foo {

  implicit def toSyntax[A](a: A): Syntax[A] =
    new Syntax[A](a)

  class Syntax[A](self: A) {
    def <=(other: A)(implicit A: Order[A]): Boolean = true
  }

  def test[F[_], B](lhs: F[B], tolerance: B)(implicit ord: Order[F[B]]): Boolean =
    (lhs: F[B]) <= (tolerance: B)
}

The above fails to compile, as I would expect.

[smarter]

[log typer]           ==> adapting cats.implicits.catsSyntaxPartialOrder[F[B]](lhs:F[B])(ord) to ?{ <= : [applied to (tolerance:B) returning ?] } 
?
adapt to subtype cats.syntax.PartialOrderOps[F[B]] !<:< ?{ <= : [applied to (tolerance:B) returning ?] }
approx F(param)1, from below = false, bound = [_$1] =>> Any, inst = [_$1] =>> Any
approx B(param)1, from below = false, bound = Any, inst = Any
[log typer]           <== adapting cats.implicits.catsSyntaxPartialOrder[F[B]](lhs:F[B])(ord) to ?{ <= : [applied to (tolerance:B) returning ?] } 
 = cats.implicits.catsSyntaxPartialOrder[F[B]](lhs:F[B])(ord):
  cats.syntax.PartialOrderOps[Any]

This is very weird, we have a value of type cats.syntax.PartialOrderOps[F[B]], then somehow we end up instantiating F to [X] => Any and B to Any which doesn't make sense since they're type parameters of the enclosing method, and from that we get an ascription cats.syntax.PartialOrderOps[Any] which is unsound since PartialOrderOps is invariant.

[smarter]

This is somehow caused by the GADT logic, if I comment out the following lines: https://github.com/lampepfl/dotty/blob/8a4c442acd67591c672a80d0fd865fbc5cc110c5/compiler/src/dotty/tools/dotc/typer/Typer.scala#L3377-L3397
then typechecking fails as expected.

I don't know how to reproduce this without cats either, but it's not too difficult to try out from the dotty repo:

• Install coursier: https://get-coursier.io/
• get the classpath using cs fetch -p org.typelevel:cats-core_2.13:2.1.0

[smarter]

What I gather is happening:

• When typechecking a def, we unconditionally add its type parameters to the GADT constraint set, in case we end up constraining them in a pattern match: https://github.com/lampepfl/dotty/blob/8a4c442acd67591c672a80d0fd865fbc5cc110c5/compiler/src/dotty/tools/dotc/typer/Typer.scala#L1904 I guess that's OK though a bit wasteful.
• When adapting a tree to match its expected type, we call ApproximateGadtAccumulator, which will happily replace any reference to a symbol in the GADT constraint set by its approximation, regardless of the context we're in: https://github.com/lampepfl/dotty/blob/8a4c442acd67591c672a80d0fd865fbc5cc110c5/compiler/src/dotty/tools/dotc/typer/Inferencing.scala#L201-L206 that's definitely not OK as shown by this issue.

[smarter]

/cc @radeusgd since ApproximateGadtAccumulator was added in #8728

[abgruszecki]

@smarter I've been suspecting that I cut a bit too many shortcuts when writing ApproximateGadtAccumulator, I'll take a look at this one.

[abgruszecki]

Oh, and before I forget to write this here for clarity/posterity: adding type parameters of every function we see to GadtConstraint is precisely how it is intended to work. When actually inferring constraints, we need to know whether a symbol is constrainable or not; all type parameters of enclosing functions are intended to be constrainable; it's not possible to tell whether a symbol is a type parameter of an enclosing function after descending into its body; therefore, we need to stick those symbols somewhere when we see them and we stick them into GadtConstraint, which essentially functions like a scope for GADT constraints.

Corrections to the above welcome.