Open existential scopes only for (x: T) => U functions

odersky · odersky · commit 30971b574332 · 2025-03-14T08:55:22.000+01:00
Parametric functions `A -&gt; B` or `A =&gt; B` do not open an existential scope
anymore. Hence, a function of the form
```scala
  def f(x: A =&gt; B^)
```
is capture polymorphic in both the function effect and the function result effect.
On the other hand,
```scala
  def f(x: (y: A) =&gt; B^)
```
would be a function that can be passed only arguments that return a fresh result on each call.
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -540,11 +540,13 @@ extension (tp: Type)
           case t @ AnnotatedType(parent, ann) =>
             // Don't map annotations, which includes capture sets
             t.derivedAnnotatedType(this(parent), ann)
-          case t @ FunctionOrMethod(args, res)
-          if args.forall(_.isAlwaysPure) =>
-            // Also map existentials in results to reach capabilities if all
-            // preceding arguments are known to be always pure
-            t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
+          case t @ FunctionOrMethod(args, res) =>
+            if args.forall(_.isAlwaysPure) then
+              // Also map existentials in results to reach capabilities if all
+              // preceding arguments are known to be always pure
+              t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
+            else
+              t
           case _ =>
             mapOver(t)
     end narrowCaps
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -252,18 +252,23 @@ trait CaptureRef extends TypeProxy, ValueType:
    *                       fail a comparison.
    */
   def maxSubsumes(y: CaptureRef, canAddHidden: Boolean)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
+    def yIsExistential = y.stripReadOnly match
+      case Existential.Vble(_) =>
+        capt.println(i"failed existential $this >: $y")
+        true
+      case _ => false
     (this eq y)
     || this.match
       case Fresh(hidden) =>
         vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
-        || !y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
+        || !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
       case Existential.Vble(binder) =>
         y.stripReadOnly match
           case Existential.Vble(binder1) => binder1.hasSuffix(binder)
             .showing(i"cmp existential $binder maxSubsumes $binder1 = $result", capt)
           case _ => true
       case _ =>
-        this.isCap && canAddHidden && vs != VarState.HardSeparate
+        this.isCap /*&& !yIsExistential*/ && canAddHidden && vs != VarState.HardSeparate
         || y.match
             case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
             case _ => false
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1260,7 +1260,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       if isCompatible(actualBoxed, expected1) then
         if debugSuccesses then tree match
             case Ident(_) =>
-              println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
+              println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}")
             case _ =>
         actualBoxed
       else
diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
@@ -281,7 +281,8 @@ object Existential:
             seen.getOrElseUpdate(t, Vble(mt))
           else
             if variance == 0 then
-              fail(em"""$tp captures the root capability `cap` in invariant position""")
+              fail(em"""$tp captures the root capability `cap` in invariant position.
+                       |This capability cannot be converted to an existential in the result type of a function.""")
             // we accept variance < 0, and leave the cap as it is
             super.mapOver(t)
         case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction =>
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -403,7 +403,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           && (!sym.isConstructor || (t ne tp.finalResultType))
             // Don't add ^ to result types of class constructors deriving from Capability
         then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
-        else normalizeCaptures(normalizeFunctions(mapFollowingAliases(t), t))
+        else normalizeCaptures(mapFollowingAliases(t))
 
       def innerApply(t: Type) =
         t match
@@ -438,9 +438,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               keptFunAliases = true
               mapOver(t)
             else
-              // In the second pass, map the alias and make sure it has the form
-              // of a dependent function.
-              normalizeFunctions(apply(t.dealias), t, expandAlways = true)
+              // In the second pass, map the alias
+              apply(t.dealias)
           case t =>
             defaultApply(t)
     end toCapturing
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -321,10 +321,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 // This is safe because X$ self-type is X.type
                 sym1 = sym1.companionModule
               if (sym1 ne NoSymbol) && (sym1 eq sym2) then
-                ctx.erasedTypes ||
-                sym1.isStaticOwner ||
-                isSubPrefix(tp1.prefix, tp2.prefix) ||
-                thirdTryNamed(tp2)
+                ctx.erasedTypes
+                || sym1.isStaticOwner
+                || isSubPrefix(tp1.prefix, tp2.prefix)
+                || thirdTryNamed(tp2)
               else
                 (tp1.name eq tp2.name)
                 && !sym1.is(Private)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1124,7 +1124,7 @@ object Types extends TypeUtils {
       TypeComparer.topLevelSubType(this, that)
     }
 
-    /** Is this type a subtype of that type? */
+    /** Is this type a subtype of that type without adding to the constraint? */
     final def frozen_<:<(that: Type)(using Context): Boolean = {
       record("frozen_<:<")
       TypeComparer.isSubTypeWhenFrozen(this, that)
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -260,7 +260,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
           def isUniversal =
             refs.elems.size == 1
             && (refs.isUniversal
-                || !printDebug && !showUniqueIds && refs.elems.nth(0).match
+                || !printDebug && !printFresh && !showUniqueIds && refs.elems.nth(0).match
                       case Existential.Vble(binder) =>
                         CCState.openExistentialScopes match
                           case b :: _ => binder eq b
@@ -459,7 +459,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
         val vbleText: Text = CCState.openExistentialScopes.indexOf(binder) match
           case -1 =>
             "<cap of " ~ toText(binder) ~ ">"
-          case n => "outer_" * n ++ "cap"
+          case n => "outer_" * n ++ (if printFresh then "localcap" else "cap")
         vbleText ~ hashStr(binder)
       case Fresh(hidden) =>
         val idStr = if showUniqueIds then s"#${hidden.id}" else ""
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -190,8 +190,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         val capturesRoot = refs == rootSetText
         if cc.isCaptureCheckingOrSetup
             && tp.allParamNamesSynthetic && !tp.looksDependent
-            && !showUniqueIds && !printDebug
-        then
+            && !showUniqueIds && !printDebug && !printFresh
+          then
           // cc.Setup converts all functions to dependent functions. Undo that when printing.
           toTextFunction(tp.paramInfos, tp.resType, tp, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
         else
diff --git a/tests/neg-custom-args/captures/boundschecks3.check b/tests/neg-custom-args/captures/boundschecks3.check
@@ -1,4 +1,24 @@
--- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
-11 |  val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
-   |           ^^^^^^
-   |           test.C[box test.Tree^] captures the root capability `cap` in invariant position
+-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:9:11 ---------------------------------
+9 |  val foo: C[Tree^] = ??? // error
+  |           ^
+  |    Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:10:11 --------------------------------
+10 |  type T = C[Tree^] // error
+   |           ^
+   |  Type argument box test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[box test.Tree^]
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:11:11 --------------------------------
+11 |  val bar: T -> T = ??? // error
+   |           ^
+   |Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> test.C[box test.Tree^]
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:12:11 --------------------------------
+12 |  val baz: C[Tree^] -> Unit = ??? // error
+   |           ^
+   |Type argument box test.Tree^ does not conform to upper bound test.Tree in subpart test.C[box test.Tree^] of inferred type test.C[box test.Tree^] -> Unit
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/boundschecks3.scala b/tests/neg-custom-args/captures/boundschecks3.scala
@@ -6,8 +6,8 @@ object test {
 
   class C[X <: Tree](x: X)
 
-  val foo: C[Tree^] = ??? // hidden error
-  type T = C[Tree^] // hidden error
-  val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
-  val baz: C[Tree^] -> Unit = ??? // hidden error
+  val foo: C[Tree^] = ??? // error
+  type T = C[Tree^] // error
+  val bar: T -> T = ??? // error
+  val baz: C[Tree^] -> Unit = ??? // error
 }
diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check
@@ -1,7 +1,20 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 --------------------
 8 |  val y: A -> Fun[B^] = x // error
   |                        ^
-  |                        Found:    (x : A -> A -> B^)
-  |                        Required: A -> A -> B^{outer_cap}
+  |                        Found:    (x : A -> (x²: A) -> B^{localcap})
+  |                        Required: A -> A -> B^{fresh}
+  |
+  |                        where:    x  is a value in method test
+  |                                  x² is a reference to a value parameter
   |
   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
+13 |  val y: Fun[B^] = x // error
+   |                   ^
+   |                   Found:    (x : (x²: A) -> B^{localcap})
+   |                   Required: A -> B^{fresh}
+   |
+   |                   where:    x  is a value in method test2
+   |                             x² is a reference to a value parameter
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.scala b/tests/neg-custom-args/captures/cc-existential-conformance.scala
@@ -4,11 +4,11 @@ class B
 type Fun[T] = A -> T
 
 def test() =
-  val x: A -> A -> B^ = ???
+  val x: A -> (x: A) -> B^ = ???
   val y: A -> Fun[B^] = x // error
   val z: A -> A -> B^ = y // ok
 
 def test2() =
-  val x: A -> B^ = ???
-  val y: Fun[B^] = x // should be error
+  val x: (x: A) -> B^ = ???
+  val y: Fun[B^] = x // error
   val z: A -> B^ = y // ok
diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check
@@ -1,15 +1,15 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:19:4 ----------------------------------
 19 |    op // error
    |    ^^
-   |    Found:    (xs: List[(X, box () ->{io} Unit)]) ->{op} List[box () ->{xs*} Unit]
+   |    Found:    (op : (xs: List[(X, box () ->{io} Unit)]) => List[box () ->{xs*} Unit])
    |    Required: (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit]
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:26:60 ---------------------------------
 26 |  val b: (xs: List[() ->{io} Unit]) => List[() ->{} Unit] = a // error
    |                                                            ^
-   |                                        Found:    (xs: List[box () ->{io} Unit]) ->{a} List[box () ->{xs*} Unit]
-   |                                        Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
+   |                                     Found:    (a : (xs: List[box () ->{io} Unit]) => List[box () ->{xs*} Unit])
+   |                                     Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/depfun-reach.scala:18:17 ------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check
@@ -1,88 +1,89 @@
--- Error: tests/neg-custom-args/captures/existential-mapping.scala:44:13 -----------------------------------------------
-44 |  val z1: A^ => Array[C^] = ??? // error
-   |          ^^^^^^^^^^^^^^^
-   |          Array[box C^] captures the root capability `cap` in invariant position
+-- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 -----------------------------------------------
+46 |  val z2: (x: A^) => Array[C^] = ??? // error
+   |          ^^^^^^^^^^^^^^^^^^^^
+   |          Array[box C^] captures the root capability `cap` in invariant position.
+   |          This capability cannot be converted to an existential in the result type of a function.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
 9 |  val _:  (x: C^) -> C = x1 // error
   |                         ^^
-  |                         Found:    (x1 : (x: C^) -> C^)
+  |                         Found:    (x1 : (x: C^) -> C^{localcap})
   |                         Required: (x: C^) -> C
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 --------------------------
 12 |  val _:  C^ -> C = x2 // error
    |                    ^^
-   |                    Found:    (x2 : C^ -> C^)
+   |                    Found:    (x2 : C^ -> C^{fresh})
    |                    Required: C^ -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 --------------------------
 15 |  val _: A^ -> (x: C^) -> C = x3 // error
    |                              ^^
-   |                              Found:    (x3 : A^ -> (x: C^) -> C^)
+   |                              Found:    (x3 : A^ -> (x: C^) -> C^{localcap})
    |                              Required: A^ -> (x: C^) -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 --------------------------
 18 |  val _: A^ -> C^ -> C = x4 // error
    |                         ^^
-   |                         Found:    (x4 : A^ -> C^ -> C^)
+   |                         Found:    (x4 : A^ -> C^ -> C^{fresh})
    |                         Required: A^ -> C^ -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
 21 |  val _: A^ -> (x: C^) -> C = x5 // error
    |                              ^^
-   |                              Found:    (x5 : A^ -> (x: C^) -> C^)
+   |                              Found:    (x5 : A^ -> (x: C^) -> C^{localcap})
    |                              Required: A^ -> (x: C^) -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
 24 |  val _: A^ -> (x: C^) => C = x6 // error
    |                              ^^
-   |                              Found:    (x6 : A^ -> (x: C^) => C^)
-   |                              Required: A^ -> (x: C^) => C
+   |                              Found:    (x6 : A^ -> (x: C^) ->{fresh} C^{localcap})
+   |                              Required: A^ -> (x: C^) ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
 27 |  val _:  (x: C^) => C = y1 // error
    |                         ^^
-   |                         Found:    (y1 : (x: C^) ->{fresh} C^)
+   |                         Found:    (y1 : (x: C^) ->{fresh} C^{localcap})
    |                         Required: (x: C^) ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
 30 |  val _:  C^ => C = y2 // error
    |                    ^^
-   |                    Found:    (y2 : C^ ->{fresh} C^)
+   |                    Found:    (y2 : C^ ->{fresh} C^{fresh})
    |                    Required: C^ ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
 33 |  val _: A^ => (x: C^) => C = y3 // error
    |                              ^^
-   |                              Found:    (y3 : A^ ->{fresh} (x: C^) => C^)
-   |                              Required: A^ ->{fresh} (x: C^) => C
+   |                              Found:    (y3 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
+   |                              Required: A^ ->{fresh} (x: C^) ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
 36 |  val _: A^ => C^ => C = y4 // error
    |                         ^^
-   |                         Found:    (y4 : A^ ->{fresh} C^ => C^)
-   |                         Required: A^ ->{fresh} C^ => C
+   |                         Found:    (y4 : A^ ->{fresh} C^ ->{fresh} C^{fresh})
+   |                         Required: A^ ->{fresh} C^ ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
 39 |  val _: A^ => (x: C^) -> C = y5 // error
    |                              ^^
-   |                              Found:    (y5 : A^ ->{fresh} (x: C^) -> C^)
+   |                              Found:    (y5 : A^ ->{fresh} (x: C^) -> C^{localcap})
    |                              Required: A^ ->{fresh} (x: C^) -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
 42 |  val _: A^ => (x: C^) => C = y6 // error
    |                              ^^
-   |                              Found:    (y6 : A^ ->{fresh} (x: C^) => C^)
-   |                              Required: A^ ->{fresh} (x: C^) => C
+   |                              Found:    (y6 : A^ ->{fresh} (x: C^) ->{fresh} C^{localcap})
+   |                              Required: A^ ->{fresh} (x: C^) ->{fresh} C
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/existential-mapping.scala b/tests/neg-custom-args/captures/existential-mapping.scala
@@ -41,6 +41,7 @@ def Test =
   val y6: A^ => IFun[C^] = ???
   val _: A^ => (x: C^) => C = y6 // error
 
-  val z1: A^ => Array[C^] = ??? // error
+  val z1: A^ => Array[C^] = ??? // ok
 
+  val z2: (x: A^) => Array[C^] = ??? // error
 
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
@@ -8,7 +8,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
 15 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |            Found:    (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |            Found:    (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{localcap.rd, _$1}
    |            Required: (_$1: box File^{files*}) ->{fresh} box Logger{val f: File^?}^?
    |
    |            Note that reference <cap of (f: box F^{files*.rd}): box Logger{val f: File^?}^?>.rd
diff --git a/tests/neg-custom-args/captures/leaked-curried.check b/tests/neg-custom-args/captures/leaked-curried.check
diff --git a/tests/neg-custom-args/captures/leaked-curried.scala b/tests/neg-custom-args/captures/leaked-curried.scala
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check
diff --git a/tests/neg-custom-args/captures/sep-use2.scala b/tests/neg-custom-args/captures/sep-use2.scala
diff --git a/tests/pos-custom-args/captures/list-encoding.scala b/tests/pos-custom-args/captures/list-encoding.scala
diff --git a/tests/pos-custom-args/captures/skolems2.scala b/tests/pos-custom-args/captures/skolems2.scala

Original file line number	Diff line number	Diff line change
`@@ -1124,7 +1124,7 @@ object Types extends TypeUtils {`
`1124`	`1124`	`TypeComparer.topLevelSubType(this, that)`
`1125`	`1125`	`}`
`1126`	`1126`
`1127`		`- /** Is this type a subtype of that type? */`
	`1127`	`+ /** Is this type a subtype of that type without adding to the constraint? */`
`1128`	`1128`	`final def frozen_<:<(that: Type)(using Context): Boolean = {`
`1129`	`1129`	`record("frozen_<:<")`
`1130`	`1130`	`TypeComparer.isSubTypeWhenFrozen(this, that)`