A few more tests for the interaction between sealed and #513

src/test/java/org/checkerframework/specimin/NonExtendableCastOperandSealedTest.java

@@ -0,0 +1,20 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.jupiter.api.Test;
+
+/**
+ * The sealed counterpart of {@link NonExtendableCastOperandPrimitiveTest}. The cast's operand has
+ * type {@code SealedBase}, which permits only {@code Known} (JLS 8.1.1.2), so the synthetic {@code
+ * Baz} cannot be made a subtype of it and the return type falls back instead. Without that, the
+ * output declares {@code Baz extends SealedBase}, which does not compile.
+ */
+public class NonExtendableCastOperandSealedTest {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "nonextendablecastoperandsealed",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#target(Foo)"});
+  }
+}

src/test/java/org/checkerframework/specimin/NonExtendableTargetSealedTest.java

@@ -0,0 +1,26 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.jupiter.api.Test;
+
+/**
+ * A sealed class as an assignment target. Only the classes named in {@code SealedBase}'s {@code
+ * permits} clause may extend it (JLS 8.1.1.2), and a placeholder Specimin invents is never one of
+ * them, so the return type of {@code get} cannot be made to fit this assignment and falls back to
+ * an unconstrained type variable. Without that, the output declares {@code GetReturnType extends
+ * SealedBase}, which does not compile because {@code GetReturnType} is not permitted.
+ *
+ * <p>The cast on the second line is what makes the sealed classification the deciding factor rather
+ * than incidental. It keeps the placeholder return type alive until the assignment is examined; if
+ * the assignment instead saw a return type that already existed, the repair for a conflict that no
+ * supertype can fix would handle this program without consulting sealedness at all.
+ */
+public class NonExtendableTargetSealedTest {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "nonextendabletargetsealed",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#target(Foo)"});
+  }
+}

src/test/java/org/checkerframework/specimin/SealedPermitsGeneratedSubtypeTest.java

@@ -0,0 +1,30 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.jupiter.api.Test;
+
+/**
+ * The one case in which a sealed class does take a synthetic subtype: its own {@code permits}
+ * clause names a type Specimin has to generate. {@code Baz} must then be declared {@code extends
+ * SealedBase}, because a permitted class is required to be a direct subclass, and it must be
+ * declared {@code non-sealed} so that it can be extended in turn.
+ *
+ * <p>Treating sealed types as unextendable therefore must not be read as "no synthetic type may
+ * name this as a supertype". It is the {@code permits} clause that establishes this relationship,
+ * where it is processed; {@link NonExtendableCastOperandSealedTest} is what asks for it from the
+ * outside, and is refused. This fixture guards the boundary between those two.
+ *
+ * <p>The cast that appears here is precisely such an outside request, and its being refused is
+ * visible in the output: {@code get}'s return type falls back rather than {@code Baz} acquiring
+ * {@code SealedBase} a second time. When the cast did impose it, the two routes disagreed about
+ * what kind of supertype it was and the output said {@code implements} for a class.
+ */
+public class SealedPermitsGeneratedSubtypeTest {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "sealedpermitsgeneratedsubtype",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#target(Foo)"});
+  }
+}

src/test/resources/nonextendablecastoperandsealed/expected/com/example/Known.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public final class Known extends SealedBase {}

src/test/resources/nonextendablecastoperandsealed/expected/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Known {}

src/test/resources/nonextendablecastoperandsealed/expected/com/example/Simple.java

@@ -0,0 +1,13 @@
+package com.example;
+
+import org.example.Baz;
+import org.example.Foo;
+
+public class Simple {
+
+  public void target(Foo f) {
+    Baz b = (Baz) f.get();
+    SealedBase s = f.get();
+    System.out.println(b + "" + s);
+  }
+}

src/test/resources/nonextendablecastoperandsealed/expected/org/example/Baz.java

@@ -0,0 +1,3 @@
+package org.example;
+public class Baz {
+}

src/test/resources/nonextendablecastoperandsealed/expected/org/example/Foo.java

@@ -0,0 +1,7 @@
+package org.example;
+public class Foo {
+
+    public <T> T get() {
+        throw new java.lang.Error();
+    }
+}

src/test/resources/nonextendablecastoperandsealed/input/com/example/Known.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public final class Known extends SealedBase {}

src/test/resources/nonextendablecastoperandsealed/input/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Known {}

src/test/resources/nonextendablecastoperandsealed/input/com/example/Simple.java

@@ -0,0 +1,12 @@
+package com.example;
+
+import org.example.Baz;
+import org.example.Foo;
+
+public class Simple {
+  public void target(Foo f) {
+    Baz b = (Baz) f.get();
+    SealedBase s = f.get();
+    System.out.println(b + "" + s);
+  }
+}

src/test/resources/nonextendabletargetsealed/expected/com/example/Known.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public final class Known extends SealedBase {}

src/test/resources/nonextendabletargetsealed/expected/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Known {}

src/test/resources/nonextendabletargetsealed/expected/com/example/Simple.java

@@ -0,0 +1,13 @@
+package com.example;
+
+import org.example.Baz;
+import org.example.Foo;
+
+public class Simple {
+
+  public void target(Foo f) {
+    SealedBase s = f.get();
+    Baz b = (Baz) f.get();
+    System.out.println(b + "" + s);
+  }
+}

src/test/resources/nonextendabletargetsealed/expected/org/example/Baz.java

@@ -0,0 +1,3 @@
+package org.example;
+public class Baz extends org.example.GetReturnType  {
+}

src/test/resources/nonextendabletargetsealed/expected/org/example/Foo.java

@@ -0,0 +1,7 @@
+package org.example;
+public class Foo {
+
+    public <T> T get() {
+        throw new java.lang.Error();
+    }
+}

src/test/resources/nonextendabletargetsealed/expected/org/example/GetReturnType.java

@@ -0,0 +1,3 @@
+package org.example;
+public class GetReturnType {
+}

src/test/resources/nonextendabletargetsealed/input/com/example/Known.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public final class Known extends SealedBase {}

src/test/resources/nonextendabletargetsealed/input/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Known {}

src/test/resources/nonextendabletargetsealed/input/com/example/Simple.java

@@ -0,0 +1,12 @@
+package com.example;
+
+import org.example.Baz;
+import org.example.Foo;
+
+public class Simple {
+  public void target(Foo f) {
+    SealedBase s = f.get();
+    Baz b = (Baz) f.get();
+    System.out.println(b + "" + s);
+  }
+}

src/test/resources/sealedpermitsgeneratedsubtype/expected/com/example/Baz.java

@@ -0,0 +1,3 @@
+package com.example;
+public non-sealed class Baz extends com.example.SealedBase  {
+}

src/test/resources/sealedpermitsgeneratedsubtype/expected/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Baz {}

src/test/resources/sealedpermitsgeneratedsubtype/expected/com/example/Simple.java

@@ -0,0 +1,12 @@
+package com.example;
+
+import org.example.Foo;
+
+public class Simple {
+
+  public void target(Foo f) {
+    Baz b = (Baz) f.get();
+    SealedBase s = f.get();
+    System.out.println(b + "" + s);
+  }
+}

src/test/resources/sealedpermitsgeneratedsubtype/expected/org/example/Foo.java

@@ -0,0 +1,7 @@
+package org.example;
+public class Foo {
+
+    public <T> T get() {
+        throw new java.lang.Error();
+    }
+}

src/test/resources/sealedpermitsgeneratedsubtype/input/com/example/SealedBase.java

@@ -0,0 +1,3 @@
+package com.example;
+
+public sealed class SealedBase permits Baz {}

src/test/resources/sealedpermitsgeneratedsubtype/input/com/example/Simple.java

@@ -0,0 +1,11 @@
+package com.example;
+
+import org.example.Foo;
+
+public class Simple {
+  public void target(Foo f) {
+    Baz b = (Baz) f.get();
+    SealedBase s = f.get();
+    System.out.println(b + "" + s);
+  }
+}