diff --git a/compiler/src/dotty/tools/dotc/Bench.scala b/compiler/src/dotty/tools/dotc/Bench.scala
index ceb945004844..3d264141eb71 100644
--- a/compiler/src/dotty/tools/dotc/Bench.scala
+++ b/compiler/src/dotty/tools/dotc/Bench.scala
@@ -10,25 +10,28 @@ import scala.annotation.internal.sharable
  *  number of compilers and run each (sequentially) a given number of times
  *  on the same sources.
  */
-object Bench extends Driver {
+object Bench extends Driver:
 
   @sharable private var numRuns = 1
 
   private def ntimes(n: Int)(op: => Reporter): Reporter =
     (0 until n).foldLeft(emptyReporter)((_, _) => op)
 
+  @sharable private var times: Array[Int] = _
+
   override def doCompile(compiler: Compiler, fileNames: List[String])(using Context): Reporter =
-    ntimes(numRuns) {
+    times = new Array[Int](numRuns)
+    var reporter: Reporter = emptyReporter
+    for i <- 0 until numRuns do
       val start = System.nanoTime()
-      val r = super.doCompile(compiler, fileNames)
-      println(s"time elapsed: ${(System.nanoTime - start) / 1000000}ms")
-      if (ctx.settings.Xprompt.value) {
+      reporter = super.doCompile(compiler, fileNames)
+      times(i) = ((System.nanoTime - start) / 1000000).toInt
+      println(s"time elapsed: ${times(i)}ms")
+      if ctx.settings.Xprompt.value then
         print("hit <return> to continue >")
         System.in.read()
         println()
-      }
-      r
-    }
+    reporter
 
   def extractNumArg(args: Array[String], name: String, default: Int = 1): (Int, Array[String]) = {
     val pos = args indexOf name
@@ -36,12 +39,25 @@ object Bench extends Driver {
     else (args(pos + 1).toInt, (args take pos) ++ (args drop (pos + 2)))
   }
 
-  override def process(args: Array[String], rootCtx: Context): Reporter = {
+  def reportTimes() =
+    val best = times.sorted
+    val measured = numRuns / 3
+    val avgBest = best.take(measured).sum / measured
+    val avgLast = times.reverse.take(measured).sum / measured
+    println(s"best out of $numRuns runs: ${best(0)}")
+    println(s"average out of best $measured: $avgBest")
+    println(s"average out of last $measured: $avgLast")
+
+  override def process(args: Array[String], rootCtx: Context): Reporter =
     val (numCompilers, args1) = extractNumArg(args, "#compilers")
     val (numRuns, args2) = extractNumArg(args1, "#runs")
     this.numRuns = numRuns
-    ntimes(numCompilers)(super.process(args2, rootCtx))
-  }
-}
+    var reporter: Reporter = emptyReporter
+    for i <- 0 until numCompilers do
+      reporter = super.process(args2, rootCtx)
+    reportTimes()
+    reporter
+
+end Bench
 
 
diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 6bad889890d4..cbdc40996a91 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -49,6 +49,9 @@ object Config {
    */
   final val checkBackendNames = false
 
+  /** Check that re-used type comparers are in their initialization state */
+  final val checkTypeComparerReset = false
+
   /** Type comparer will fail with an assert if the upper bound
    *  of a constrained parameter becomes Nothing. This should be turned
    *  on only for specific debugging as normally instantiation to Nothing
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 9b1990b981fa..27949f3fb899 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -54,11 +54,18 @@ trait ConstraintHandling {
    */
   protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty
 
+  def checkReset() =
+    assert(addConstraintInvocations == 0)
+    assert(frozenConstraint == false)
+    assert(caseLambda == NoType)
+    assert(homogenizeArgs == false)
+    assert(comparedTypeLambdas == Set.empty)
+
   /** Gives for each instantiated type var that does not yet have its `inst` field
-    *  set, the instance value stored in the constraint. Storing instances in constraints
-    *  is done only in a temporary way for contexts that may be retracted
-    *  without also retracting the type var as a whole.
-    */
+   *  set, the instance value stored in the constraint. Storing instances in constraints
+   *  is done only in a temporary way for contexts that may be retracted
+   *  without also retracting the type var as a whole.
+   */
   def instType(tvar: TypeVar): Type = constraint.entry(tvar.origin) match {
     case _: TypeBounds => NoType
     case tp: TypeParamRef =>
diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index 941078a0d82e..fdba7003a9d1 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -172,17 +172,6 @@ object Contexts {
     protected def searchHistory_= (searchHistory: SearchHistory): Unit = _searchHistory = searchHistory
     final def searchHistory: SearchHistory = _searchHistory
 
-    /** The current type comparer. This ones updates itself automatically for
-     *  each new context.
-     */
-    private var _typeComparer: TypeComparer = _
-    protected def typeComparer_=(typeComparer: TypeComparer): Unit = _typeComparer = typeComparer
-    def typeComparer: TypeComparer = {
-      if (_typeComparer.comparerCtx ne this)
-        _typeComparer = _typeComparer.copyIn(this)
-      _typeComparer
-    }
-
     /** The current source file */
     private var _source: SourceFile = _
     protected def source_=(source: SourceFile): Unit = _source = source
@@ -479,7 +468,6 @@ object Contexts {
       _typeAssigner = origin.typeAssigner
       _gadt = origin.gadt
       _searchHistory = origin.searchHistory
-      _typeComparer = origin.typeComparer
       _source = origin.source
       _moreProperties = origin.moreProperties
       _store = origin.store
@@ -610,7 +598,6 @@ object Contexts {
       util.Stats.record("Context.setSource")
       this.source = source
       this
-    def setTypeComparerFn(tcfn: Context => TypeComparer): this.type = { this.typeComparer = tcfn(this); this }
     private def setMoreProperties(moreProperties: Map[Key[Any], Any]): this.type =
       util.Stats.record("Context.setMoreProperties")
       this.moreProperties = moreProperties
@@ -699,26 +686,57 @@ object Contexts {
     val base = ctx.base
     import base._
     val nestedCtx =
-      if testsInUse < testContexts.size then
-        testContexts(testsInUse).reuseIn(ctx)
+      if exploresInUse < exploreContexts.size then
+        exploreContexts(exploresInUse).reuseIn(ctx)
       else
         val ts = TyperState()
           .setReporter(ExploringReporter())
           .setCommittable(false)
         val c = FreshContext(ctx.base).init(ctx, ctx).setTyperState(ts)
-        testContexts += c
+        exploreContexts += c
         c
-    testsInUse += 1
+    exploresInUse += 1
     val nestedTS = nestedCtx.typerState
     nestedTS.init(ctx.typerState, ctx.typerState.constraint)
     val result =
       try op(using nestedCtx)
       finally
         nestedTS.reporter.asInstanceOf[ExploringReporter].reset()
-        testsInUse -= 1
+        exploresInUse -= 1
     result
   end explore
 
+  /** The type comparer of the kind created by `maker` to be used.
+   *  This is the currently active type comparer CMP if
+   *   - CMP is associated with the current context, and
+   *   - CMP is of the kind created by maker or maker creates a plain type comparer.
+   *  Note: plain TypeComparers always take on the kind of the outer comparer if they are in the same context.
+   *  In other words: tracking or explaining is a sticky property in the same context.
+   */
+  private def comparer(using Context): TypeComparer =
+    val base = ctx.base
+    if base.comparersInUse > 0
+       && (base.comparers(base.comparersInUse - 1).comparerContext eq ctx)
+    then
+      base.comparers(base.comparersInUse - 1).currentInstance
+    else
+      val result =
+        if base.comparersInUse < base.comparers.size then
+          base.comparers(base.comparersInUse)
+        else
+          val result = TypeComparer(ctx)
+          base.comparers += result
+          result
+      base.comparersInUse += 1
+      result.init(ctx)
+      result
+
+  inline def comparing[T](inline op: TypeComparer => T)(using Context): T =
+    val saved = ctx.base.comparersInUse
+    try op(comparer)
+    finally ctx.base.comparersInUse = saved
+  end comparing
+
   /** A class defining the initial context with given context base
    *  and set of possible settings.
    */
@@ -735,7 +753,6 @@ object Contexts {
     store = initialStore
       .updated(settingsStateLoc, settingsGroup.defaultState)
       .updated(notNullInfosLoc, Nil)
-    typeComparer = new TypeComparer(using this)
     searchHistory = new SearchRoot
     gadt = EmptyGadtConstraint
   }
@@ -871,14 +888,18 @@ object Contexts {
 
     protected[dotc] val indentTab: String = "  "
 
-    private[dotc] val testContexts = new mutable.ArrayBuffer[FreshContext]
-    private[dotc] var testsInUse: Int = 0
+    private[Contexts] val exploreContexts = new mutable.ArrayBuffer[FreshContext]
+    private[Contexts] var exploresInUse: Int = 0
+
+    private[Contexts] val comparers = new mutable.ArrayBuffer[TypeComparer]
+    private[Contexts] var comparersInUse: Int = 0
 
     def reset(): Unit = {
       for ((_, set) <- uniqueSets) set.clear()
       errorTypeMsg.clear()
       sources.clear()
       sourceNamed.clear()
+      comparers.clear()  // forces re-evaluation of top and bottom classes in TypeComparer
     }
 
     // Test that access is single threaded
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index bcc5e47fd09e..418d7f3027c9 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1324,7 +1324,7 @@ class Definitions {
   def asContextFunctionType(tp: Type)(using Context): Type =
     tp.stripTypeVar.dealias match {
       case tp1: TypeParamRef if ctx.typerState.constraint.contains(tp1) =>
-        asContextFunctionType(ctx.typeComparer.bounds(tp1).hiBound)
+        asContextFunctionType(TypeComparer.bounds(tp1).hiBound)
       case tp1 =>
         if (isFunctionType(tp1) && tp1.typeSymbol.name.isContextFunction) tp1
         else NoType
diff --git a/compiler/src/dotty/tools/dotc/core/Denotations.scala b/compiler/src/dotty/tools/dotc/core/Denotations.scala
index 4404ae0abf31..2e3bde2ee62c 100644
--- a/compiler/src/dotty/tools/dotc/core/Denotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Denotations.scala
@@ -539,7 +539,7 @@ object Denotations {
       case tp1: MethodType =>
         tp2 match
           case tp2: MethodType
-          if ctx.typeComparer.matchingMethodParams(tp1, tp2)
+          if TypeComparer.matchingMethodParams(tp1, tp2)
              && tp1.isImplicitMethod == tp2.isImplicitMethod
              && tp1.isErasedMethod == tp2.isErasedMethod =>
             val resType = infoMeet(tp1.resType, tp2.resType.subst(tp2, tp1), safeIntersection)
diff --git a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
index d95647593ef7..e33e634c5e9e 100644
--- a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
@@ -220,8 +220,8 @@ final class ProperGadtConstraint private(
   override protected def constraint = myConstraint
   override protected def constraint_=(c: Constraint) = myConstraint = c
 
-  override protected def isSub(tp1: Type, tp2: Type)(using Context): Boolean = ctx.typeComparer.isSubType(tp1, tp2)
-  override protected def isSame(tp1: Type, tp2: Type)(using Context): Boolean = ctx.typeComparer.isSameType(tp1, tp2)
+  override protected def isSub(tp1: Type, tp2: Type)(using Context): Boolean = TypeComparer.isSubType(tp1, tp2)
+  override protected def isSame(tp1: Type, tp2: Type)(using Context): Boolean = TypeComparer.isSameType(tp1, tp2)
 
    override def nonParamBounds(param: TypeParamRef)(using Context): TypeBounds =
      constraint.nonParamBounds(param) match {
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 6b3e570cdc05..951c5e9e15dd 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1991,7 +1991,7 @@ object SymDenotations {
             computeApplied
 
           case tp: TypeParamRef =>  // uncachable, since baseType depends on context bounds
-            recur(ctx.typeComparer.bounds(tp).hi)
+            recur(TypeComparer.bounds(tp).hi)
 
           case tp: TypeProxy =>
             def computeTypeProxy = {
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index aac7562c31d9..333975223168 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -23,16 +23,32 @@ import typer.ProtoTypes.constrained
 import typer.Applications.productSelectorTypes
 import reporting.trace
 import NullOpsDecorator._
+import annotation.constructorOnly
 
 /** Provides methods to compare types.
  */
-class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling with PatternTypeConstrainer {
+class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling, PatternTypeConstrainer {
   import TypeComparer._
+  Stats.record("TypeComparer")
 
-  val state = ctx.typerState
+  private var myContext: Context = initctx
+  def comparerContext: Context = myContext
+
+  protected given [DummySoItsADef] as Context = myContext
+
+  protected var state: TyperState = null
   def constraint: Constraint = state.constraint
   def constraint_=(c: Constraint): Unit = state.constraint = c
 
+  def init(c: Context): Unit =
+    myContext = c
+    state = c.typerState
+    monitored = false
+    GADTused = false
+    recCount = 0
+    needsGc = false
+    if Config.checkTypeComparerReset then checkReset()
+
   private var pendingSubTypes: mutable.Set[(Type, Type)] = null
   private var recCount = 0
   private var monitored = false
@@ -41,6 +57,12 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
 
   private var canCompareAtoms: Boolean = true // used for internal consistency checking
 
+  /** Indicates whether the subtype check used GADT bounds */
+  private var GADTused: Boolean = false
+
+  private var myInstance: TypeComparer = this
+  def currentInstance: TypeComparer = myInstance
+
   /** Is a subtype check in progress? In that case we may not
    *  permanently instantiate type variables, because the corresponding
    *  constraint might still be retracted and the instantiation should
@@ -59,50 +81,24 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
   private var successCount = 0
   private var totalCount = 0
 
-  private var myAnyClass: ClassSymbol = null
-  private var myAnyKindClass: ClassSymbol = null
-  private var myNothingClass: ClassSymbol = null
-  private var myNullClass: ClassSymbol = null
-  private var myObjectClass: ClassSymbol = null
-  private var myAnyType: TypeRef = null
-  private var myAnyKindType: TypeRef = null
-  private var myNothingType: TypeRef = null
-
-  def AnyClass: ClassSymbol = {
-    if (myAnyClass == null) myAnyClass = defn.AnyClass
-    myAnyClass
-  }
-  def AnyKindClass: ClassSymbol = {
-    if (myAnyKindClass == null) myAnyKindClass = defn.AnyKindClass
-    myAnyKindClass
-  }
-  def NothingClass: ClassSymbol = {
-    if (myNothingClass == null) myNothingClass = defn.NothingClass
-    myNothingClass
-  }
-  def NullClass: ClassSymbol = {
-    if (myNullClass == null) myNullClass = defn.NullClass
-    myNullClass
-  }
-  def ObjectClass: ClassSymbol = {
-    if (myObjectClass == null) myObjectClass = defn.ObjectClass
-    myObjectClass
-  }
-  def AnyType: TypeRef = {
-    if (myAnyType == null) myAnyType = AnyClass.typeRef
-    myAnyType
-  }
-  def AnyKindType: TypeRef = {
-    if (myAnyKindType == null) myAnyKindType = AnyKindClass.typeRef
-    myAnyKindType
-  }
-  def NothingType: TypeRef = {
-    if (myNothingType == null) myNothingType = NothingClass.typeRef
-    myNothingType
-  }
-
-  /** Indicates whether a previous subtype check used GADT bounds */
-  var GADTused: Boolean = false
+  protected val AnyClass     = defn.AnyClass
+  protected val AnyKindClass = defn.AnyKindClass
+  protected val NothingClass = defn.NothingClass
+  protected val NullClass    = defn.NullClass
+  protected val ObjectClass  = defn.ObjectClass
+  protected val AnyType      = AnyClass.typeRef
+  protected val AnyKindType  = AnyKindClass.typeRef
+  protected val NothingType  = NothingClass.typeRef
+
+  override def checkReset() =
+    super.checkReset()
+    assert(pendingSubTypes == null || pendingSubTypes.isEmpty)
+    assert(canCompareAtoms == true)
+    assert(successCount == 0)
+    assert(totalCount == 0)
+    assert(approx == FreshApprox)
+    assert(leftRoot == null)
+    assert(frozenGadt == false)
 
   /** Record that GADT bounds of `sym` were used in a subtype check.
    *  But exclude constructor type parameters, as these are aliased
@@ -133,6 +129,12 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
     }
   }
 
+  def testSubType(tp1: Type, tp2: Type): CompareResult =
+    GADTused = false
+    if !topLevelSubType(tp1, tp2) then CompareResult.Fail
+    else if GADTused then CompareResult.OKwithGADTUsed
+    else CompareResult.OK
+
   /** The current approximation state. See `ApproxState`. */
   private var approx: ApproxState = FreshApprox
   protected def approxState: ApproxState = approx
@@ -141,7 +143,7 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
    *  every time we compare components of the previous pair of types.
    *  This type is used for capture conversion in `isSubArgs`.
    */
-  private [this] var leftRoot: Type = _
+  private [this] var leftRoot: Type = null
 
   /** Are we forbidden from recording GADT constraints? */
   private var frozenGadt = false
@@ -200,7 +202,7 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
         //}
         assert(!ctx.settings.YnoDeepSubtypes.value)
         if (Config.traceDeepSubTypeRecursions && !this.isInstanceOf[ExplainingTypeComparer])
-          report.log(TypeComparer.explained(summon[Context].typeComparer.isSubType(tp1, tp2, approx)))
+          report.log(explained(_.isSubType(tp1, tp2, approx)))
       }
       // Eliminate LazyRefs before checking whether we have seen a type before
       val normalize = new TypeMap {
@@ -234,7 +236,7 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
     def firstTry: Boolean = tp2 match {
       case tp2: NamedType =>
         def compareNamed(tp1: Type, tp2: NamedType): Boolean =
-          val ctx = comparerCtx
+          val ctx = comparerContext
           given Context = ctx // optimization for performance
           val info2 = tp2.info
           info2 match
@@ -1187,16 +1189,16 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
     }
 
     // begin recur
-    if (tp2 eq NoType) false
-    else if (tp1 eq tp2) true
-    else {
+    if tp2 eq NoType then false
+    else if tp1 eq tp2 then true
+    else
       val saved = constraint
       val savedSuccessCount = successCount
-      try {
-        recCount = recCount + 1
-        if (recCount >= Config.LogPendingSubTypesThreshold) monitored = true
-        val result = if (monitored) monitoredIsSubType else firstTry
-        recCount = recCount - 1
+      try
+        recCount += 1
+        if recCount >= Config.LogPendingSubTypesThreshold then monitored = true
+        val result = if monitored then monitoredIsSubType else firstTry
+        recCount -= 1
         if !result then
           state.constraint = saved
         else if recCount == 0 && needsGc then
@@ -1204,16 +1206,12 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
           needsGc = false
         if (Stats.monitored) recordStatistics(result, savedSuccessCount)
         result
-      }
-      catch {
-        case NonFatal(ex) =>
-          if (ex.isInstanceOf[AssertionError]) showGoal(tp1, tp2)
-          recCount -= 1
-          state.constraint = saved
-          successCount = savedSuccessCount
-          throw ex
-      }
-    }
+      catch case NonFatal(ex) =>
+        if ex.isInstanceOf[AssertionError] then showGoal(tp1, tp2)
+        recCount -= 1
+        state.constraint = saved
+        successCount = savedSuccessCount
+        throw ex
   }
 
   private def nonExprBaseType(tp: Type, cls: Symbol)(using Context): Type =
@@ -1923,9 +1921,6 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
     }
   }
 
-  /** The greatest lower bound of a list types */
-  final def glb(tps: List[Type]): Type = tps.foldLeft(AnyType: Type)(glb)
-
   def widenInUnions(using Context): Boolean =
     migrateTo3 || ctx.erasedTypes
 
@@ -1960,16 +1955,12 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
         def widen(tp: Type) = if (widenInUnions) tp.widen else tp.widenIfUnstable
         val tp1w = widen(tp1)
         val tp2w = widen(tp2)
-        if ((tp1 ne tp1w) || (tp2 ne tp2w)) lub(tp1w, tp2w)
+        if ((tp1 ne tp1w) || (tp2 ne tp2w)) lub(tp1w, tp2w, canConstrain)
         else orType(tp1w, tp2w) // no need to check subtypes again
       }
       mergedLub(tp1.stripLazyRef, tp2.stripLazyRef)
   }
 
-  /** The least upper bound of a list of types */
-  final def lub(tps: List[Type]): Type =
-    tps.foldLeft(NothingType: Type)(lub(_,_, canConstrain = false))
-
   /** Try to produce joint arguments for a lub `A[T_1, ..., T_n] | A[T_1', ..., T_n']` using
    *  the following strategies:
    *
@@ -2279,9 +2270,6 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
       false
   }
 
-  /** A new type comparer of the same type as this one, using the given context. */
-  def copyIn(ctx: Context): TypeComparer = new TypeComparer(using ctx)
-
   // ----------- Diagnostics --------------------------------------------------
 
   /** A hook for showing subtype traces. Overridden in ExplainingTypeComparer */
@@ -2327,9 +2315,6 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
     }
   }
 
-  /** Returns last check's debug mode, if explicitly enabled. */
-  def lastTrace(): String = ""
-
   /** Does `tycon` have a field with type `tparam`? Special cased for `scala.*:`
    *  as that type is artificially added to tuples. */
   private def typeparamCorrespondsToField(tycon: Type, tparam: TypeParamInfo): Boolean =
@@ -2489,10 +2474,31 @@ class TypeComparer(using val comparerCtx: Context) extends ConstraintHandling wi
         false
     }
   }
+
+  protected def explainingTypeComparer = ExplainingTypeComparer(comparerContext)
+  protected def trackingTypeComparer = TrackingTypeComparer(comparerContext)
+
+  private def inSubComparer[T, Cmp <: TypeComparer](comparer: Cmp)(op: Cmp => T): T =
+    val saved = myInstance
+    myInstance = comparer
+    try op(comparer)
+    finally myInstance = saved
+
+  /** The trace of comparison operations when performing `op` */
+  def explained[T](op: ExplainingTypeComparer => T)(using Context): String =
+    val cmp = explainingTypeComparer
+    inSubComparer(cmp)(op)
+    cmp.lastTrace()
+
+  def tracked[T](op: TrackingTypeComparer => T)(using Context): T =
+    inSubComparer(trackingTypeComparer)(op)
 }
 
 object TypeComparer {
 
+  enum CompareResult:
+    case OK, Fail, OKwithGADTUsed
+
   /** Class for unification variables used in `natValue`. */
   private class AnyConstantType extends UncachedGroundType with ValueType {
     var tpe: Type = NoType
@@ -2532,23 +2538,111 @@ object TypeComparer {
    */
   val FreshApprox: ApproxState = new ApproxState(4)
 
-  /** Show trace of comparison operations when performing `op` */
-  def explaining[T](say: String => Unit)(op: Context ?=> T)(using Context): T = {
-    val nestedCtx = ctx.fresh.setTypeComparerFn(new ExplainingTypeComparer(using _))
-    val res = try { op(using nestedCtx) } finally { say(nestedCtx.typeComparer.lastTrace()) }
-    res
-  }
+  def topLevelSubType(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.topLevelSubType(tp1, tp2))
 
-  /** Like [[explaining]], but returns the trace instead */
-  def explained[T](op: Context ?=> T)(using Context): String = {
-    var trace: String = null
-    try { explaining(trace = _)(op) } catch { case ex: Throwable => ex.printStackTrace }
-    trace
-  }
+  def isSubType(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.isSubType(tp1, tp2))
+
+  def isSameType(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.isSameType(tp1, tp2))
+
+  def isSubTypeWhenFrozen(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.isSubTypeWhenFrozen(tp1, tp2))
+
+  def testSubType(tp1: Type, tp2: Type)(using Context): CompareResult =
+    comparing(_.testSubType(tp1, tp2))
+
+  def isSameTypeWhenFrozen(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.isSameTypeWhenFrozen(tp1, tp2))
+
+  def isSameRef(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.isSameRef(tp1, tp2))
+
+  def matchesType(tp1: Type, tp2: Type, relaxed: Boolean)(using Context): Boolean =
+    comparing(_.matchesType(tp1, tp2, relaxed))
+
+  def matchingMethodParams(tp1: MethodType, tp2: MethodType)(using Context): Boolean =
+    comparing(_.matchingMethodParams(tp1, tp2))
+
+  def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false)(using Context): Type =
+    comparing(_.lub(tp1, tp2, canConstrain))
+
+  /** The least upper bound of a list of types */
+  final def lub(tps: List[Type])(using Context): Type =
+    tps.foldLeft(defn.NothingType: Type)(lub(_,_))
+
+  def lubArgs(args1: List[Type], args2: List[Type], tparams: List[TypeParamInfo], canConstrain: Boolean = false)(using Context): List[Type] =
+    comparing(_.lubArgs(args1, args2, tparams, canConstrain))
+
+  def glb(tp1: Type, tp2: Type)(using Context): Type =
+    comparing(_.glb(tp1, tp2))
+
+  /** The greatest lower bound of a list types */
+  def glb(tps: List[Type])(using Context): Type =
+    tps.foldLeft(defn.AnyType: Type)(glb)
+
+  def orType(using Context)(tp1: Type, tp2: Type, isErased: Boolean = ctx.erasedTypes): Type =
+    comparing(_.orType(tp1, tp2, isErased))
+
+  def andType(using Context)(tp1: Type, tp2: Type, isErased: Boolean = ctx.erasedTypes): Type =
+    comparing(_.andType(tp1, tp2, isErased))
+
+  def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean =
+    comparing(_.provablyDisjoint(tp1, tp2))
+
+  def liftIfHK(tp1: Type, tp2: Type,
+      op: (Type, Type) => Type, original: (Type, Type) => Type,
+      combineVariance: (Variance, Variance) => Variance)(using Context): Type =
+    comparing(_.liftIfHK(tp1, tp2, op, original, combineVariance))
+
+  def constValue(tp: Type)(using Context): Option[Constant] =
+    comparing(_.constValue(tp))
+
+  def subtypeCheckInProgress(using Context): Boolean =
+    comparing(_.subtypeCheckInProgress)
+
+  def instType(tvar: TypeVar)(using Context): Type =
+    comparing(_.instType(tvar))
+
+  def instanceType(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
+    comparing(_.instanceType(param, fromBelow))
+
+  def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
+    comparing(_.approximation(param, fromBelow))
+
+  def bounds(param: TypeParamRef)(using Context): TypeBounds =
+    comparing(_.bounds(param))
+
+  def fullBounds(param: TypeParamRef)(using Context): TypeBounds =
+    comparing(_.fullBounds(param))
+
+  def fullLowerBound(param: TypeParamRef)(using Context): Type =
+    comparing(_.fullLowerBound(param))
+
+  def fullUpperBound(param: TypeParamRef)(using Context): Type =
+    comparing(_.fullUpperBound(param))
+
+  def addToConstraint(tl: TypeLambda, tvars: List[TypeVar])(using Context): Boolean =
+    comparing(_.addToConstraint(tl, tvars))
+
+  def widenInferred(inst: Type, bound: Type)(using Context): Type =
+    comparing(_.widenInferred(inst, bound))
+
+  def constrainPatternType(pat: Type, scrut: Type)(using Context): Boolean =
+    comparing(_.constrainPatternType(pat, scrut))
+
+  def explained[T](op: ExplainingTypeComparer => T)(using Context): String =
+    comparing(_.explained(op))
+
+  def tracked[T](op: TrackingTypeComparer => T)(using Context): T =
+    comparing(_.tracked(op))
 }
 
-class TrackingTypeComparer(using Context) extends TypeComparer {
-  import state.constraint
+class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
+  init(initctx)
+
+  override def trackingTypeComparer = this
 
   val footprint: mutable.Set[Type] = mutable.Set[Type]()
 
@@ -2695,9 +2789,13 @@ class TrackingTypeComparer(using Context) extends TypeComparer {
 }
 
 /** A type comparer that can record traces of subtype operations */
-class ExplainingTypeComparer(using Context) extends TypeComparer {
+class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   import TypeComparer._
 
+  init(initctx)
+
+  override def explainingTypeComparer = this
+
   private var indent = 0
   private val b = new StringBuilder
 
@@ -2748,7 +2846,5 @@ class ExplainingTypeComparer(using Context) extends TypeComparer {
       super.addConstraint(param, bound, fromBelow)
     }
 
-  override def copyIn(using Context): ExplainingTypeComparer = new ExplainingTypeComparer
-
-  override def lastTrace(): String = "Subtype trace:" + { try b.toString finally b.clear() }
+  def lastTrace(): String = "Subtype trace:" + { try b.toString finally b.clear() }
 }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index ecc5b14a2536..64f97f8a7c1f 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -468,7 +468,7 @@ class TypeErasure(isJava: Boolean, semiEraseVCs: Boolean, isConstructor: Boolean
     case AndType(tp1, tp2) =>
       erasedGlb(this(tp1), this(tp2), isJava)
     case OrType(tp1, tp2) =>
-      ctx.typeComparer.orType(this(tp1), this(tp2), isErased = true)
+      TypeComparer.orType(this(tp1), this(tp2), isErased = true)
     case tp: MethodType =>
       def paramErasure(tpToErase: Type) =
         erasureFn(tp.isJavaMethod, semiEraseVCs, isConstructor, wildcardOK)(tpToErase)
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index c15af0461811..318e4419e295 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -216,7 +216,7 @@ object TypeOps:
             case AppliedType(tycon2, args2) =>
               tp1.derivedAppliedType(
                 mergeRefinedOrApplied(tycon1, tycon2),
-                ctx.typeComparer.lubArgs(args1, args2, tycon1.typeParams))
+                TypeComparer.lubArgs(args1, args2, tycon1.typeParams))
             case _ => fallback
           }
         case tp1 @ TypeRef(pre1, _) =>
@@ -334,7 +334,7 @@ object TypeOps:
    */
   def classBound(info: ClassInfo)(using Context): Type = {
     val cls = info.cls
-    val parentType = info.parents.reduceLeft(ctx.typeComparer.andType(_, _))
+    val parentType = info.parents.reduceLeft(TypeComparer.andType(_, _))
 
     def addRefinement(parent: Type, decl: Symbol) = {
       val inherited =
@@ -420,8 +420,8 @@ object TypeOps:
         case tp: SkolemType if partsToAvoid(mutable.Set.empty, tp.info).nonEmpty =>
           range(defn.NothingType, apply(tp.info))
         case tp: TypeVar if mapCtx.typerState.constraint.contains(tp) =>
-          val lo = mapCtx.typeComparer.instanceType(
-            tp.origin, fromBelow = variance > 0 || variance == 0 && tp.hasLowerBound)
+          val lo = TypeComparer.instanceType(
+            tp.origin, fromBelow = variance > 0 || variance == 0 && tp.hasLowerBound)(using mapCtx)
           val lo1 = apply(lo)
           if (lo1 ne lo) lo1 else tp
         case _ =>
diff --git a/compiler/src/dotty/tools/dotc/core/TyperState.scala b/compiler/src/dotty/tools/dotc/core/TyperState.scala
index ccb1cfd29648..a1fba01be312 100644
--- a/compiler/src/dotty/tools/dotc/core/TyperState.scala
+++ b/compiler/src/dotty/tools/dotc/core/TyperState.scala
@@ -141,7 +141,7 @@ class TyperState() {
     val toCollect = new mutable.ListBuffer[TypeLambda]
     constraint foreachTypeVar { tvar =>
       if (!tvar.inst.exists) {
-        val inst = ctx.typeComparer.instType(tvar)
+        val inst = TypeComparer.instType(tvar)
         if (inst.exists && (tvar.owningState.get eq this)) {
           tvar.inst = inst
           val lam = tvar.origin.binder
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 67b2f2eb00a3..df248eb2987e 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -915,13 +915,13 @@ object Types {
     /** Is this type a subtype of that type? */
     final def <:<(that: Type)(using Context): Boolean = {
       record("<:<")
-      ctx.typeComparer.topLevelSubType(this, that)
+      TypeComparer.topLevelSubType(this, that)
     }
 
     /** Is this type a subtype of that type? */
     final def frozen_<:<(that: Type)(using Context): Boolean = {
       record("frozen_<:<")
-      ctx.typeComparer.isSubTypeWhenFrozen(this, that)
+      TypeComparer.isSubTypeWhenFrozen(this, that)
     }
 
     /** Is this type the same as that type?
@@ -929,11 +929,11 @@ object Types {
      */
     final def =:=(that: Type)(using Context): Boolean = {
       record("=:=")
-      ctx.typeComparer.isSameType(this, that)
+      TypeComparer.isSameType(this, that)
     }
 
     final def frozen_=:=(that: Type)(using Context): Boolean =
-      ctx.typeComparer.isSameTypeWhenFrozen(this, that)
+      TypeComparer.isSameTypeWhenFrozen(this, that)
 
     /** Is this type a primitive value type which can be widened to the primitive value type `that`? */
     def isValueSubType(that: Type)(using Context): Boolean = widen match {
@@ -988,7 +988,7 @@ object Types {
      */
     def matches(that: Type)(using Context): Boolean = {
       record("matches")
-      ctx.typeComparer.matchesType(this, that, relaxed = !ctx.phase.erasedTypes)
+      TypeComparer.matchesType(this, that, relaxed = !ctx.phase.erasedTypes)
     }
 
     /** This is the same as `matches` except that it also matches => T with T and
@@ -1012,7 +1012,7 @@ object Types {
 
     def & (that: Type)(using Context): Type = {
       record("&")
-      ctx.typeComparer.glb(this, that)
+      TypeComparer.glb(this, that)
     }
 
     /** Safer version of `&`.
@@ -1046,7 +1046,7 @@ object Types {
 
     def | (that: Type)(using Context): Type = {
       record("|")
-      ctx.typeComparer.lub(this, that)
+      TypeComparer.lub(this, that)
     }
 
 // ----- Unwrapping types -----------------------------------------------
@@ -1156,7 +1156,7 @@ object Types {
 
     def widenUnionWithoutNull(using Context): Type = widen match {
       case tp @ OrType(lhs, rhs) =>
-        ctx.typeComparer.lub(lhs.widenUnionWithoutNull, rhs.widenUnionWithoutNull, canConstrain = true) match {
+        TypeComparer.lub(lhs.widenUnionWithoutNull, rhs.widenUnionWithoutNull, canConstrain = true) match {
           case union: OrType => union.join
           case res => res
         }
@@ -2948,7 +2948,7 @@ object Types {
 
     /** Like `make`, but also supports higher-kinded types as argument */
     def makeHk(tp1: Type, tp2: Type)(using Context): Type =
-      ctx.typeComparer.liftIfHK(tp1, tp2, AndType.make(_, _, checkValid = false), makeHk, _ | _)
+      TypeComparer.liftIfHK(tp1, tp2, AndType.make(_, _, checkValid = false), makeHk, _ | _)
   }
 
   abstract case class OrType(tp1: Type, tp2: Type) extends AndOrType {
@@ -3038,7 +3038,7 @@ object Types {
 
     /** Like `make`, but also supports higher-kinded types as argument */
     def makeHk(tp1: Type, tp2: Type)(using Context): Type =
-      ctx.typeComparer.liftIfHK(tp1, tp2, OrType(_, _), makeHk, _ & _)
+      TypeComparer.liftIfHK(tp1, tp2, OrType(_, _), makeHk, _ & _)
   }
 
   /** An extractor object to pattern match against a nullable union.
@@ -4184,7 +4184,7 @@ object Types {
      *  uninstantiated
      */
     def instanceOpt(using Context): Type =
-      if (inst.exists) inst else ctx.typeComparer.instType(this)
+      if (inst.exists) inst else TypeComparer.instType(this)
 
     /** Is the variable already instantiated? */
     def isInstantiated(using Context): Boolean = instanceOpt.exists
@@ -4208,7 +4208,7 @@ object Types {
         val atp = TypeOps.avoid(tp, problems.toList)
         def msg = i"Inaccessible variables captured in instantation of type variable $this.\n$tp was fixed to $atp"
         typr.println(msg)
-        val bound = ctx.typeComparer.fullUpperBound(origin)
+        val bound = TypeComparer.fullUpperBound(origin)
         if !(atp <:< bound) then
           throw new TypeError(s"$msg,\nbut the latter type does not conform to the upper bound $bound")
         atp
@@ -4223,7 +4223,7 @@ object Types {
     def instantiateWith(tp: Type)(using Context): Type = {
       assert(tp ne this, s"self instantiation of ${tp.show}, constraint = ${ctx.typerState.constraint.show}")
       typr.println(s"instantiating ${this.show} with ${tp.show}")
-      if ((ctx.typerState eq owningState.get) && !ctx.typeComparer.subtypeCheckInProgress)
+      if ((ctx.typerState eq owningState.get) && !TypeComparer.subtypeCheckInProgress)
         inst = tp
       ctx.typerState.constraint = ctx.typerState.constraint.replace(origin, tp)
       tp
@@ -4237,7 +4237,7 @@ object Types {
      *  is also a singleton type.
      */
     def instantiate(fromBelow: Boolean)(using Context): Type =
-      instantiateWith(avoidCaptures(ctx.typeComparer.instanceType(origin, fromBelow)))
+      instantiateWith(avoidCaptures(TypeComparer.instanceType(origin, fromBelow)))
 
     /** For uninstantiated type variables: Is the lower bound different from Nothing? */
     def hasLowerBound(using Context): Boolean =
@@ -4304,13 +4304,11 @@ object Types {
     override def tryNormalize(using Context): Type = reduced.normalized
 
     def reduced(using Context): Type = {
-      val trackingCtx = ctx.fresh.setTypeComparerFn(new TrackingTypeComparer(using _))
-      val typeComparer = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
 
       def contextInfo(tp: Type): Type = tp match {
         case tp: TypeParamRef =>
           val constraint = ctx.typerState.constraint
-          if (constraint.entry(tp).exists) ctx.typeComparer.fullBounds(tp)
+          if (constraint.entry(tp).exists) TypeComparer.fullBounds(tp)
           else NoType
         case tp: TypeRef =>
           val bounds = ctx.gadt.fullBounds(tp.symbol)
@@ -4319,12 +4317,11 @@ object Types {
           tp.underlying
       }
 
-      def updateReductionContext(): Unit = {
+      def updateReductionContext(footprint: collection.Set[Type]): Unit =
         reductionContext = new mutable.HashMap
-        for (tp <- typeComparer.footprint)
+        for (tp <- footprint)
           reductionContext(tp) = contextInfo(tp)
-        typr.println(i"footprint for $this $hashCode: ${typeComparer.footprint.toList.map(x => (x, contextInfo(x)))}%, %")
-      }
+        typr.println(i"footprint for $this $hashCode: ${footprint.toList.map(x => (x, contextInfo(x)))}%, %")
 
       def isUpToDate: Boolean =
         reductionContext.keysIterator.forall { tp =>
@@ -4337,14 +4334,13 @@ object Types {
         if (myReduced != null) record("MatchType.reduce cache miss")
         myReduced =
           trace(i"reduce match type $this $hashCode", typr, show = true) {
-            try
-              typeComparer.matchCases(scrutinee.normalized, cases)(using trackingCtx)
-            catch {
-              case ex: Throwable =>
+            def matchCases(cmp: TrackingTypeComparer): Type =
+              try cmp.matchCases(scrutinee.normalized, cases)
+              catch case ex: Throwable =>
                 handleRecursive("reduce type ", i"$scrutinee match ...", ex)
-            }
+              finally updateReductionContext(cmp.footprint)
+            TypeComparer.tracked(matchCases)
           }
-        updateReductionContext()
       }
       myReduced
     }
@@ -5553,7 +5549,7 @@ object Types {
           case tp: TypeRef if tp.info.isTypeAlias =>
             apply(n, tp.superType)
           case tp: TypeParamRef =>
-            apply(n, ctx.typeComparer.bounds(tp))
+            apply(n, TypeComparer.bounds(tp))
           case _ =>
             foldOver(n, tp)
         }
@@ -5581,7 +5577,7 @@ object Types {
             val tsym = if (tp.termSymbol.is(Param)) tp.underlying.typeSymbol else tp.termSymbol
             foldOver(cs + tsym, tp)
           case tp: TypeParamRef =>
-            apply(cs, ctx.typeComparer.bounds(tp))
+            apply(cs, TypeComparer.bounds(tp))
           case other =>
             foldOver(cs, tp)
         }
diff --git a/compiler/src/dotty/tools/dotc/printing/Formatting.scala b/compiler/src/dotty/tools/dotc/printing/Formatting.scala
index b4a2af039b5c..be25469c549d 100644
--- a/compiler/src/dotty/tools/dotc/printing/Formatting.scala
+++ b/compiler/src/dotty/tools/dotc/printing/Formatting.scala
@@ -199,7 +199,7 @@ object Formatting {
 
     entry match {
       case param: TypeParamRef =>
-        s"is a type variable${addendum("constraint", ctx.typeComparer.bounds(param))}"
+        s"is a type variable${addendum("constraint", TypeComparer.bounds(param))}"
       case param: TermParamRef =>
         s"is a reference to a value parameter"
       case sym: Symbol =>
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 8b41983bad27..84d422c99207 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -216,7 +216,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
           val constr = ctx.typerState.constraint
           val bounds =
             if constr.contains(tp) then
-              withMode(Mode.Printing)(ctx.typeComparer.fullBounds(tp.origin))
+              withMode(Mode.Printing)(TypeComparer.fullBounds(tp.origin))
             else
               TypeBounds.empty
           if (bounds.isTypeAlias) toText(bounds.lo) ~ (Str("^") provided printDebug)
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index d875a930b063..ab389eebc33c 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -248,8 +248,8 @@ import ast.tpd
         case tp: TypeParamRef =>
           constraint.entry(tp) match
             case bounds: TypeBounds =>
-              if variance < 0 then apply(mapCtx.typeComparer.fullUpperBound(tp))
-              else if variance > 0 then apply(mapCtx.typeComparer.fullLowerBound(tp))
+              if variance < 0 then apply(TypeComparer.fullUpperBound(tp))
+              else if variance > 0 then apply(TypeComparer.fullLowerBound(tp))
               else tp
             case NoType => tp
             case instType => apply(instType)
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index ed1232c0e213..334161f582ed 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -341,7 +341,7 @@ class TreeChecker extends Phase with SymTransformer {
                |Original tree : ${tree.show}
                |After checking: ${tree1.show}
                |Why different :
-             """.stripMargin + core.TypeComparer.explained(tp1 <:< tp2)
+             """.stripMargin + core.TypeComparer.explained(_.isSubType(tp1, tp2))
           if (tree.hasType) // it might not be typed because Typer sometimes constructs new untyped trees and resubmits them to typedUnadapted
             assert(isSubType(tree1.tpe, tree.typeOpt), divergenceMsg(tree1.tpe, tree.typeOpt))
           tree1
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index bc4c066fb065..d5c0df04c778 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -120,7 +120,7 @@ object TypeTestsCasts {
 
       val res = P1 <:< P
 
-      debug.println(TypeComparer.explained(P1 <:< P))
+      debug.println(TypeComparer.explained(_.isSubType(P1, P)))
 
       debug.println("P1 : " + P1.show)
       debug.println("P1 <:< P = " + res)
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 4de45c371047..c292a79b9cae 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -345,7 +345,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
       Empty
     }
     else {
-      val res = ctx.typeComparer.provablyDisjoint(tp1, tp2)
+      val res = TypeComparer.provablyDisjoint(tp1, tp2)
 
       if (res) Empty
       else if (tp1.isSingleton) Typ(tp1, true)
@@ -499,7 +499,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
 
   /** Is `tp1` a subtype of `tp2`?  */
   def isSubType(tp1: Type, tp2: Type): Boolean = {
-    debug.println(TypeComparer.explained(tp1 <:< tp2))
+    debug.println(TypeComparer.explained(_.isSubType(tp1, tp2)))
     val res = if (ctx.explicitNulls) {
       tp1 <:< tp2
     } else {
@@ -612,7 +612,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
 
           def inhabited(tp: Type): Boolean =
             tp.dealias match {
-              case AndType(tp1, tp2) => !ctx.typeComparer.provablyDisjoint(tp1, tp2)
+              case AndType(tp1, tp2) => !TypeComparer.provablyDisjoint(tp1, tp2)
               case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2)
               case tp: RefinedType => inhabited(tp.parent)
               case tp: TypeRef => inhabited(tp.prefix)
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 38f5dbaf4e00..daf6dc58c1b9 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1242,7 +1242,7 @@ trait Applications extends Compatibility {
             // 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.
-            withMode(Mode.GadtConstraintInference)(ctx.typeComparer.constrainPatternType(unapplyArgType, selType))
+            withMode(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}")
diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
index 0026cf005fe5..03c5b4dd32cf 100644
--- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -122,7 +122,7 @@ object ErrorReporting {
       else if (ctx.settings.explainTypes.value)
         i"""
            |${ctx.typerState.constraint}
-           |${TypeComparer.explained(found <:< expected)}"""
+           |${TypeComparer.explained(_.isSubType(found, expected))}"""
       else
         ""
     }
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index 607e891852d5..cba3af104944 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -443,7 +443,7 @@ object Implicits:
             case t: TypeParamRef =>
               constraint.entry(t) match {
                 case NoType => t
-                case bounds: TypeBounds => mapCtx.typeComparer.fullBounds(t)
+                case bounds: TypeBounds => TypeComparer.fullBounds(t)
                 case t1 => t1
               }
             case t: TypeVar =>
@@ -760,7 +760,7 @@ trait Implicits:
         case ex: AssertionError =>
           implicits.println(s"view $from ==> $to")
           implicits.println(ctx.typerState.constraint.show)
-          implicits.println(TypeComparer.explained(from.tpe <:< to))
+          implicits.println(TypeComparer.explained(_.isSubType(from.tpe, to)))
           throw ex
       }
     }
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index e11c14363c3f..39cc1ffa10ac 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -69,7 +69,7 @@ object Inferencing {
       def apply(tvars: Set[TypeVar], tp: Type) = tp match {
         case tp: TypeVar
         if !tp.isInstantiated &&
-            accCtx.typeComparer.bounds(tp.origin)
+            TypeComparer.bounds(tp.origin)
               .namedPartsWith(ref => params.contains(ref.symbol))
               .nonEmpty =>
           tvars + tp
@@ -242,7 +242,7 @@ object Inferencing {
             constraint.entry(param) match {
               case TypeBounds(lo, hi)
               if (hi frozen_<:< lo) =>
-                val inst = accCtx.typeComparer.approximation(param, fromBelow = true)
+                val inst = TypeComparer.approximation(param, fromBelow = true)
                 typr.println(i"replace singleton $param := $inst")
                 accCtx.typerState.constraint = constraint.replace(param, inst)
               case _ =>
@@ -319,9 +319,9 @@ object Inferencing {
    *            0 if unconstrained, or constraint is from below and above.
    */
   private def instDirection(param: TypeParamRef)(using Context): Int = {
-    val constrained = ctx.typeComparer.fullBounds(param)
+    val constrained = TypeComparer.fullBounds(param)
     val original = param.binder.paramInfos(param.paramNum)
-    val cmp = ctx.typeComparer
+    val cmp = TypeComparer
     val approxBelow =
       if (!cmp.isSubTypeWhenFrozen(constrained.lo, original.lo)) 1 else 0
     val approxAbove =
@@ -355,7 +355,7 @@ object Inferencing {
       if (v == 1) tvar.instantiate(fromBelow = false)
       else if (v == -1) tvar.instantiate(fromBelow = true)
       else {
-        val bounds = ctx.typeComparer.fullBounds(tvar.origin)
+        val bounds = TypeComparer.fullBounds(tvar.origin)
         if (bounds.hi <:< bounds.lo || bounds.hi.classSymbol.is(Final) || fromScala2x)
           tvar.instantiate(fromBelow = false)
         else {
diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
index e05bc4cd8421..9af8f9ac06c9 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
@@ -611,7 +611,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(using Context) {
     tree.changeOwner(originalOwner, ctx.owner)
 
   def tryConstValue: Tree =
-    ctx.typeComparer.constValue(callTypeArgs.head.tpe) match {
+    TypeComparer.constValue(callTypeArgs.head.tpe) match {
       case Some(c) => Literal(c).withSpan(call.span)
       case _ => EmptyTree
     }
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index 0366636ec43d..798e132626bf 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1343,7 +1343,7 @@ class Namer { typer: Typer =>
       def widenRhs(tp: Type): Type =
         tp.widenTermRefExpr.simplified match
           case ctp: ConstantType if isInlineVal => ctp
-          case tp => ctx.typeComparer.widenInferred(tp, rhsProto)
+          case tp => TypeComparer.widenInferred(tp, rhsProto)
 
       // Replace aliases to Unit by Unit itself. If we leave the alias in
       // it would be erased to BoxedUnit.
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index 2cb455ad8e2d..6920d972b387 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -512,7 +512,7 @@ object ProtoTypes {
 
     val added = state.constraint.ensureFresh(tl)
     val tvars = if (addTypeVars) newTypeVars(added) else Nil
-    ctx.typeComparer.addToConstraint(added, tvars.tpes.asInstanceOf[List[TypeVar]])
+    TypeComparer.addToConstraint(added, tvars.tpes.asInstanceOf[List[TypeVar]])
     (added, tvars)
   }
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Synthesizer.scala b/compiler/src/dotty/tools/dotc/typer/Synthesizer.scala
index d6c47380e438..bb34a230bf49 100644
--- a/compiler/src/dotty/tools/dotc/typer/Synthesizer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Synthesizer.scala
@@ -307,7 +307,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
                   val tparams = poly.paramRefs
                   val variances = caseClass.typeParams.map(_.paramVarianceSign)
                   val instanceTypes = tparams.lazyZip(variances).map((tparam, variance) =>
-                    ctx.typeComparer.instanceType(tparam, fromBelow = variance < 0))
+                    TypeComparer.instanceType(tparam, fromBelow = variance < 0))
                   resType.substParams(poly, instanceTypes)
                 instantiate(using ctx.fresh.setExploreTyperState().setOwner(caseClass))
               case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 28b3ddeb2fbf..402d8b567d22 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -413,7 +413,7 @@ trait TypeAssigner {
   }
 
   def assignType(tree: untpd.Match, scrutinee: Tree, cases: List[CaseDef])(using Context): Match =
-    tree.withType(ctx.typeComparer.lub(cases.tpes))
+    tree.withType(TypeComparer.lub(cases.tpes))
 
   def assignType(tree: untpd.Labeled)(using Context): Labeled =
     tree.withType(tree.bind.symbol.info)
@@ -426,7 +426,7 @@ trait TypeAssigner {
 
   def assignType(tree: untpd.Try, expr: Tree, cases: List[CaseDef])(using Context): Try =
     if (cases.isEmpty) tree.withType(expr.tpe)
-    else tree.withType(ctx.typeComparer.lub(expr.tpe :: cases.tpes))
+    else tree.withType(TypeComparer.lub(expr.tpe :: cases.tpes))
 
   def assignType(tree: untpd.SeqLiteral, elems: List[Tree], elemtpt: Tree)(using Context): SeqLiteral = {
     val ownType = tree match {
@@ -487,7 +487,7 @@ trait TypeAssigner {
     tree.withType(NamedType(NoPrefix, sym))
 
   def assignType(tree: untpd.Alternative, trees: List[Tree])(using Context): Alternative =
-    tree.withType(ctx.typeComparer.lub(trees.tpes))
+    tree.withType(TypeComparer.lub(trees.tpes))
 
   def assignType(tree: untpd.UnApply, proto: Type)(using Context): UnApply =
     tree.withType(proto)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 6d074f5a2664..84938132bd49 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -26,6 +26,7 @@ import ErrorReporting._
 import Checking._
 import Inferencing._
 import EtaExpansion.etaExpand
+import TypeComparer.CompareResult
 import util.Spans._
 import util.common._
 import util.{Property, SimpleIdentityMap, SrcPos}
@@ -167,7 +168,7 @@ class Typer extends Namer
        *                   the previous (inner) definition. This models what scalac does.
        */
       def checkNewOrShadowed(found: Type, newPrec: BindingPrec, scala2pkg: Boolean = false)(using Context): Type =
-        if !previous.exists || ctx.typeComparer.isSameRef(previous, found) then
+        if !previous.exists || TypeComparer.isSameRef(previous, found) then
            found
         else if (prevCtx.scope eq ctx.scope)
                 && (newPrec == Definition || newPrec == NamedImport && prevPrec == WildImport)
@@ -767,7 +768,9 @@ class Typer extends Namer
       def handlePattern: Tree = {
         val tpt1 = typedTpt
         if (!ctx.isAfterTyper && pt != defn.ImplicitScrutineeTypeRef)
-          withMode(Mode.GadtConstraintInference)(ctx.typeComparer.constrainPatternType(tpt1.tpe, pt))
+          withMode(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)
       }
@@ -1615,7 +1618,7 @@ class Typer extends Namer
         else if (tree.elems.isEmpty && tree.isInstanceOf[Trees.JavaSeqLiteral[?]])
           defn.ObjectType // generic empty Java varargs are of type Object[]
         else
-          ctx.typeComparer.lub(elems1.tpes)
+          TypeComparer.lub(elems1.tpes)
       val elemtpt1 = typed(tree.elemtpt, elemtptType)
       assign(elems1, elemtpt1)
     }
@@ -2194,7 +2197,7 @@ class Typer extends Namer
       case _ =>
         val pcls = parents.foldLeft(defn.ObjectClass)(improve)
         typr.println(i"ensure first is class $parents%, % --> ${parents map (_ baseType pcls)}%, %")
-        val first = ctx.typeComparer.glb(defn.ObjectType :: parents.map(_.baseType(pcls)))
+        val first = TypeComparer.glb(defn.ObjectType :: parents.map(_.baseType(pcls)))
         checkFeasibleParent(first, ctx.source.atSpan(span), em" in inferred superclass $first") :: parents
     }
   }
@@ -2383,7 +2386,7 @@ class Typer extends Namer
         if (ctx.mode.is(Mode.Pattern)) app1
         else {
           val elemTpes = elems.lazyZip(pts).map((elem, pt) =>
-            ctx.typeComparer.widenInferred(elem.tpe, pt))
+            TypeComparer.widenInferred(elem.tpe, pt))
           val resTpe = TypeOps.nestedPairs(elemTpes)
           app1.cast(resTpe)
         }
@@ -3227,7 +3230,6 @@ class Typer extends Namer
     }
 
     def adaptNoArgsOther(wtp: Type): Tree = {
-      ctx.typeComparer.GADTused = false
       if (isContextFunctionRef(wtp) &&
           !untpd.isContextualClosure(tree) &&
           !isApplyProto(pt) &&
@@ -3282,23 +3284,22 @@ class Typer extends Namer
               |To turn this error into a warning, pass -Xignore-scala2-macros to the compiler""".stripMargin, tree.srcPos.startPos)
           tree
         }
-      else if (tree.tpe.widenExpr <:< pt) {
-        if (ctx.typeComparer.GADTused && pt.isValueType)
+      else TypeComparer.testSubType(tree.tpe.widenExpr, pt) match
+        case CompareResult.Fail =>
+          wtp match
+            case wtp: MethodType => missingArgs(wtp)
+            case _ =>
+              typr.println(i"adapt to subtype ${tree.tpe} !<:< $pt")
+              //typr.println(TypeComparer.explained(tree.tpe <:< pt))
+              adaptToSubType(wtp)
+        case CompareResult.OKwithGADTUsed if pt.isValueType =>
           // Insert an explicit cast, so that -Ycheck in later phases succeeds.
           // I suspect, but am not 100% sure that this might affect inferred types,
           // if the expected type is a supertype of the GADT bound. It would be good to come
           // up with a test case for this.
           tree.cast(pt)
-        else
-          tree
-      }
-      else wtp match {
-        case wtp: MethodType => missingArgs(wtp)
         case _ =>
-          typr.println(i"adapt to subtype ${tree.tpe} !<:< $pt")
-          //typr.println(TypeComparer.explained(tree.tpe <:< pt))
-          adaptToSubType(wtp)
-      }
+          tree
     }
 
     // Follow proxies and approximate type paramrefs by their upper bound
@@ -3307,7 +3308,7 @@ class Typer extends Namer
     def underlyingApplied(tp: Type): Type = tp.stripTypeVar match {
       case tp: RefinedType => tp
       case tp: AppliedType => tp
-      case tp: TypeParamRef => underlyingApplied(ctx.typeComparer.bounds(tp).hi)
+      case tp: TypeParamRef => underlyingApplied(TypeComparer.bounds(tp).hi)
       case tp: TypeProxy => underlyingApplied(tp.superType)
       case _ => tp
     }
@@ -3615,9 +3616,11 @@ class Typer extends Namer
   protected def checkEqualityEvidence(tree: tpd.Tree, pt: Type)(using Context) : Unit =
     tree match {
       case _: RefTree | _: Literal
-        if !isVarPattern(tree) &&
-           !(pt <:< tree.tpe) &&
-           !withMode(Mode.GadtConstraintInference)(ctx.typeComparer.constrainPatternType(tree.tpe, pt)) =>
+      if !isVarPattern(tree)
+         && !(pt <:< tree.tpe)
+         && !withMode(Mode.GadtConstraintInference) {
+              TypeComparer.constrainPatternType(tree.tpe, pt)
+            } =>
         val cmp =
           untpd.Apply(
             untpd.Select(untpd.TypedSplice(tree), nme.EQ),
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index 7b3fd7c6f04a..610467f705cf 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -153,7 +153,6 @@ class CompilationTests extends ParallelTesting {
       compileFile("tests/neg-custom-args/conditionalWarnings.scala", allowDeepSubtypes.and("-deprecation").and("-Xfatal-warnings")),
       compileFilesInDir("tests/neg-custom-args/isInstanceOf", allowDeepSubtypes and "-Xfatal-warnings"),
       compileFile("tests/neg-custom-args/i3627.scala", allowDeepSubtypes),
-      compileFile("tests/neg-custom-args/matchtype-loop.scala", allowDeepSubtypes),
       compileFile("tests/neg-custom-args/sourcepath/outer/nested/Test1.scala", defaultOptions.and("-sourcepath", "tests/neg-custom-args/sourcepath")),
       compileDir("tests/neg-custom-args/sourcepath2/hi", defaultOptions.and("-sourcepath", "tests/neg-custom-args/sourcepath2", "-Xfatal-warnings")),
       compileList("duplicate source", List(
diff --git a/tests/neg/matchtype-loop2.scala b/tests/neg-custom-args/allow-deep-subtypes/matchtype-loop2.scala
similarity index 60%
rename from tests/neg/matchtype-loop2.scala
rename to tests/neg-custom-args/allow-deep-subtypes/matchtype-loop2.scala
index 4ea55fc2928f..3a97d54a2820 100644
--- a/tests/neg/matchtype-loop2.scala
+++ b/tests/neg-custom-args/allow-deep-subtypes/matchtype-loop2.scala
@@ -2,7 +2,8 @@ object Test {
   type L[X] = X match {
     case Int => L[X]
   }
-  type LL[X] = X match {   // error: recursion limit exceeded
+  type LL[X] = X match {
     case Int => LL[LL[X]]
   }
+  val x: LL[Int] = 2   // error
 }