Refactor Mode.GADTFlexible and TypeComparer.frozenGadt

Author: abgruszecki

compiler/src/dotty/tools/dotc/core/Mode.scala

@@ -49,8 +49,11 @@ object Mode {
   /** We are in a pattern alternative */
   val InPatternAlternative: Mode = newMode(7, "InPatternAlternative")
 
-  /** Infer GADT constraints during type comparisons `A <:< B` */
-  val GADTflexible: Mode = newMode(8, "GADTflexible")
+  /** Make subtyping checks instead infer constraints necessarily following from given subtyping relation.
+   *
+   *  This enables changing [[GadtConstraint]] and alters how [[TypeComparer]] approximates constraints.
+   */
+  val GadtConstraintInference: Mode = newMode(8, "GadtConstraintInference")
 
   /** Assume -language:strictEquality */
   val StrictEquality: Mode = newMode(9, "StrictEquality")

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -141,7 +141,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private [this] var leftRoot: Type = _
 
-  /** Are we forbidden from recording GADT constraints? */
+  /** Are we forbidden from recording GADT constraints?
+   *
+   *  This flag is set when we're already in [[Mode.GadtConstraintInference]],
+   *  to signify that we temporarily cannot record any GADT constraints.
+   */
   private[this] var frozenGadt = false
 
   protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
@@ -846,7 +850,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                   isSubType(tycon1.prefix, tycon2.prefix) && {
                     // check both tycons to deal with the case when they are equal b/c of GADT constraint
                     val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass
-                    isSubArgs(args1, args2, tp1, tparams, inferGadtBounds = tyconIsInjective)
+                    def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
+                    // we only record GADT constraints if tycon is guaranteed to be injective
+                    if (tyconIsInjective) checkSubArgs()
+                    else {
+                      val savedFrozenGadt = frozenGadt
+                      frozenGadt = true
+                      try checkSubArgs() finally frozenGadt = savedFrozenGadt
+                    }
                   }
                   if (res && touchedGADTs) GADTused = true
                   res
@@ -1103,7 +1114,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @param  tp1       The applied type containing `args1`
    *  @param  tparams2  The type parameters of the type constructor applied to `args2`
    */
-  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo], inferGadtBounds: Boolean = false): Boolean = {
+  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {
     /** The bounds of parameter `tparam`, where all references to type paramneters
      *  are replaced by corresponding arguments (or their approximations in the case of
      *  wildcard arguments).
@@ -1167,17 +1178,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               case arg1: TypeBounds =>
                 compareCaptured(arg1, arg2)
               case _ =>
-                def isSub(tp: Type, pt: Type): Boolean = {
-                  if (inferGadtBounds) isSubType(tp, pt)
-                  else {
-                    val savedFrozenGadt = frozenGadt
-                    frozenGadt = true
-                    try isSubType(tp, pt) finally frozenGadt = savedFrozenGadt
-                  }
-                }
-
-                (v > 0 || isSub(arg2, arg1)) &&
-                (v < 0 || isSub(arg1, arg2))
+                (v > 0 || isSubType(arg2, arg1)) &&
+                (v < 0 || isSubType(arg1, arg2))
             }
         }
 
@@ -1243,7 +1245,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @see [[necessaryEither]] for the GADTFlexible case
    */
   protected def either(op1: => Boolean, op2: => Boolean): Boolean =
-    if (ctx.mode.is(Mode.GADTflexible)) necessaryEither(op1, op2) else sufficientEither(op1, op2)
+    if (ctx.mode.is(Mode.GadtConstraintInference)) necessaryEither(op1, op2) else sufficientEither(op1, op2)
 
   /** Returns true iff the result of evaluating either `op1` or `op2` is true,
    *  trying at the same time to keep the constraint as wide as possible.
@@ -1491,7 +1493,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private def narrowGADTBounds(tr: NamedType, bound: Type, approx: ApproxState, isUpper: Boolean): Boolean = {
     val boundImprecise = approx.high || approx.low
-    ctx.mode.is(Mode.GADTflexible) && !frozenGadt && !frozenConstraint && !boundImprecise && {
+    ctx.mode.is(Mode.GadtConstraintInference) && !frozenGadt && !frozenConstraint && !boundImprecise && {
       val tparam = tr.symbol
       gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
       if (bound.isRef(tparam)) false

compiler/src/dotty/tools/dotc/typer/Applications.scala

@@ -1098,7 +1098,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
             // We ignore whether constraining the pattern succeeded.
             // Constraining only fails if the pattern cannot possibly match,
             // but useless pattern checks detect more such cases, so we simply rely on them instead.
-            ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(unapplyArgType, selType)
+            ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(unapplyArgType, selType)
             val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
             if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)
             unapp.println(i"case 2 $unapplyArgType ${ctx.typerState.constraint}")

compiler/src/dotty/tools/dotc/typer/Inliner.scala

@@ -916,7 +916,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) {
           }
 
         if (!isImplicit) caseBindingMap += ((NoSymbol, scrutineeBinding))
-        val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GADTflexible)
+        val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GadtConstraintInference)
         if (reducePattern(caseBindingMap, scrutineeSym.termRef, cdef.pat)(gadtCtx)) {
           val (caseBindings, from, to) = substBindings(caseBindingMap.toList, mutable.ListBuffer(), Nil, Nil)
           val guardOK = cdef.guard.isEmpty || {

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -607,7 +607,7 @@ class Typer extends Namer
       def handlePattern: Tree = {
         val tpt1 = typedTpt
         if (!ctx.isAfterTyper && pt != defn.ImplicitScrutineeTypeRef)
-          ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tpt1.tpe, pt)
+          ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tpt1.tpe, pt)
         // special case for an abstract type that comes with a class tag
         tryWithClassTag(ascription(tpt1, isWildcard = true), pt)
       }
@@ -3153,7 +3153,7 @@ class Typer extends Namer
       case _: RefTree | _: Literal
         if !isVarPattern(tree) &&
            !(pt <:< tree.tpe) &&
-           !ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tree.tpe, pt) =>
+           !ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tree.tpe, pt) =>
         val cmp =
           untpd.Apply(
             untpd.Select(untpd.TypedSplice(tree), nme.EQ),