GADT constraints not propagated correctly

[pjmc-oliveira]

Compiler version

(scalac -version)
Scala compiler version 3.3.0 -- Copyright 2002-2023, LAMP/EPFL

Minimized code

sealed trait PTwo

sealed trait Foo[+A]
case class One(unit: Unit) extends Foo[Nothing]
case class Two(unit: Unit) extends Foo[PTwo]

sealed trait FooK[+A]
case class OneK(unit: Unit) extends FooK[Nothing]
case class TwoK(unit: Unit) extends FooK[PTwo]


def foo[A](x: Foo[A], fun: FooK[A] => Unit): Unit =
  if x.isInstanceOf[One] then
    ???
  else x.asInstanceOf[Two] match {
    case Two(unit) =>
      val twoK = fun(TwoK(unit))
      ???
  }

Output

-- [E007] Type Mismatch Error: src/main/scala/main.scala:18:25 -----------------
17 |      val twoK = fun(TwoK(unit))
   |                     ^^^^^^^^^^
   |                     Found:    TwoK
   |                     Required: FooK[A]
   |----------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: TwoK.apply(unit)
   | I tried to show that
   |   TwoK
   | conforms to
   |   FooK[A]
   | but the comparison trace ended with `false`:
   |
   |   ==> TwoK  <:  FooK[A]
   |     ==> FooK[PTwo]  <:  FooK[A] (left is approximated)
   |       ==> PTwo  <:  A
   |         ==> PTwo  <:  Nothing in frozen constraint
   |         <== PTwo  <:  Nothing in frozen constraint = false
   |       <== PTwo  <:  A = false
   |     <== FooK[PTwo]  <:  FooK[A] (left is approximated) = false
   |   <== TwoK  <:  FooK[A] = false
   |
   | The tests were made under the empty constraint
    ----------------------------------------------------------------------------
1 error found

Expectation

• Expected code to compile
• Note that if we change the asInstanceOf cast from Two to Foo[A] & (Two | One) the code will compile. But if it's Two | One or Foo[A] & Two it does not compile.
• Looking at Dotty in typer > Applications.scala > typedUnApply it only seems to add the GADT constraint mode (withMode(Mode.GadtConstraintInference)(TypeComparer.constrainPatternType(unapplyArgType, selType))) if the selector type is a subtype of the unapply arg type. Adding the GADT constraints to both sides of the seems to fix this type error, but I'm not sure if it would create any unsoundness issues.

[dwijnand]

There's no chance of making x.asInstanceOf[Two] infer anything against A. But perhaps one could add constrainPatternType to other branch in typedUnApply such that x.asInstanceOf[Foo[A] & Two] would type-check. But is it even worth it when the more natural:

def foo[A](x: Foo[A], fun: FooK[A] => Unit): Unit = x match
  case One(_) =>
  case x @ Two(_) => x match
    case Two(unit) =>
      val twoK = fun(TwoK(unit))

works today?

[odersky]

I don't think we want to mix isInstanceOf and GADT reasoning. That would set false expectations.

[som-snytt]

If asInstanceOf tells the compiler, "I don't need your help", then it's in bad faith to ask it for help anyway.

[dwijnand]

You have the same problem with

def foo[A](x: Foo[A] & Two, fun: FooK[A] => Unit): Unit = x match
  case Two(unit) =>
    val twoK = fun(TwoK(unit))

But that's just a complicated way of writing

def foo(x: Two, fun: FooK[PTwo] => Unit): Unit = x match
  case Two(unit) =>
    val twoK = fun(TwoK(unit))

[olhotak]

The asInstanceOf is a red herring as @dwijnand points out.

The real issue is that when the compiler already know that the scrutinee is a Two, it doesn't do GADT inference on its superclass Foo[A].

If you add Foo[A] in an intersection, then sometimes it does. Foo[A] & (One|Two) will do the GADT inference. But Foo[A] & Two will simplify to just Two and the GADT inference goes away again. It's unpredictable.

Our more general motivation here is an attempt to improve type inference for match cases. If you have an enum or sealed hierarchy with three cases One, Two, Three, we're experimenting with mechanisms that would infer the type Three for c in the following:

x match {
  case a: One => ???
  case b: Two => ???
  case c => ???
}

But we've observed that sometimes knowing a more precise type for the scrutinee reduces the precision of GADT inference.

[olhotak]

To propose something concrete, could GADT inference be done with all supeclasses of the type of the scrutinee? That is, if we know the scrutinee is a Two, could we also do GADT inference on its superclass Foo?

[dwijnand]

I don't see the problem with doing in in both cases. But it would also be nice to have a test case that's less contrived and doesn't already work.