GADT reasoning does not work with quotes

[LPTK]

Compiler version

3.1.2

Minimized code

import scala.quoted.*

def test(using Quotes) =
  def foo[T](e: Expr[T]): T = e match { case '{ 2 + 2 } => 4 }

Output

[error] -- [E007] Type Mismatch Error:
[error] 21 |    def foo[T](e: Expr[T]): T = e match { case '{ 2 + 2 } => 4 }
[error]    |                                                             ^
[error]    |                                                     Found:    (4 : Int)
[error]    |                                                     Required: T

Expectation

Should work because we know that Int <: T from this pattern. It's analogous to:

abstract class Expr[+E]
case class Add() extends Expr[Int]

def foo[T](e: Expr[T]): T = e match { case D() => 4 }

which does currently work.

[SethTisue]

@dwijnand is this example helped by your recent PR?

[LPTK]

I just realized that Dotty allows typing 2 + 2 as 4:

scala> 2 + 2 : 4
val res0: Int = 4

So it would actually be unsound to assume T >: Int in the example above.

But the problem in this issue still holds. We still can't type rewritings for things that really are known to return a specific type regardless of their arguments, like example in:

scala> def example(): Int = 0
def example(): Int
                                                                               
scala> def test(using Quotes) =
     |   def foo[T](e: Expr[T]): T = e match { case '{ example() } => 4 }
     | 
-- Error:
2 |  def foo[T](e: Expr[T]): T = e match { case '{ example() } => 4 }
  |                                                               ^
  |                                                       Found:    (4 : Int)
  |                                                       Required: T

[abgruszecki]

Interestingly enough, I think to support this sort of usecase we need to use type members to express appropriate types. Note that ${ example() } can be typed as Expr[X] for any X s.t. Int <: X. If we pretend that Expr is defined as:

class Expr:
  type A

then we can express that the pattern '{ example() } in @LPTK's example matches values of type Expr { type A :> Int }. These types would let us correctly infer that T :> Int.

If Expr is defined as class Expr[A] (which I'm guessing is the case), then we can't express the appropriate pattern type.

[LPTK]

Isn't Dotty already more or less treating type parameters like hidden type members?

[abgruszecki]

Yes, but it's on the "less" end of the scale.

[abgruszecki]

So one important thing: right now, we cannot express a type corresponding to Expr { type A :> Int } with type arguments, since Expr is covariant in A. There were some proposals to allow types like Expr[final Int], which would correspond to Expr { type A = Int } rather than Expr { type A <: Int } (as in, I proposed that myself as a solution for Paolo's unsound covariant inheritance examples), but I don't think anyone considered reversing the direction of the bound so far.