Unsound use of metaprogramming quotes: future-stage type evidence shouldn't be usable in the current stage

[LPTK]

While reviewing my thesis, Oleg Kiselyov pointed out a subtlety in the interaction of GADTs with staging in MetaOCaml: GADT constraints should be marked by stage to prevent the use of future-stage constraints in the current stage, which would be unsound. He gave the following example, which is a test in the MetaOCaml distribution:

type _ t = T : string t
let f : type a. a t option code -> a -> unit code =
  fun c x -> .< match .~c with
  | None -> ()
  | Some T -> .~(print_endline x; .<()>.) >.
let _ = f .< None >. 0

(As an answer to the problem, MetaOCaml rejects pattern-matches of GADTs within quotes, so that does not compile.)

Sure enough, we can reproduce something similar in Scala, without even having to use a GADT, since Scala has first-class support for subtype evidence:

scala> import scala.quoted.staging._

scala> given Toolbox = Toolbox.make(getClass.getClassLoader)
def given_Toolbox: quoted.staging.Toolbox

scala> trait T { type A >: Any <: Nothing }
// defined trait T

scala> withQuoteContext { '{ (x: T) => ${ 42: x.A } } }
    java.lang.ClassCastException: java.base/java.lang.Integer cannot be cast to scala.runtime.Nothing$

[abgruszecki]

Note that we (I think) can recreate the same issue with pattern-matching on GADTs. Since:

MetaOCaml rejects pattern-matches of GADTs within quotes, so that does not compile.

we could just not infer any GADT constraints when pattern matching inside quotes. Major upside is that this is trivial to implement.

(This doesn't do anything about the specific issue above, though)

[LPTK]

@AleksanderBG, yes, unsurprisingly we can reproduce the issue with GADTs too:

scala> enum Foo[A] { case Bar extends Foo[String] }
// defined class Foo

scala> import quoted._

scala> def foo[A: Type](using QuoteContext) = (a: A) => '{
     |   (x: Foo[A]) => x match { case Foo.Bar => ${ print(a: String); '{} } } }

scala> withQuoteContext { foo[Int].apply(42) }
    java.lang.ClassCastException: java.base/java.lang.Integer cannot be cast to java.base/java.lang.String