From f23ec80aab3b859aff2d9b5b8ce521a493a18fa7 Mon Sep 17 00:00:00 2001
From: Chris Povirk <cpovirk@google.com>
Date: Tue, 8 Mar 2022 16:10:28 -0500
Subject: [PATCH] Implement subtyping for type variables created by capture
 conversion of `? super` wildcards.

- For the code in `isNullnessSubtype`, see
  ["`F` is a type-variable usage that meets _both_ of the following conditions...."](https://jspecify.dev/spec#:~:text=F%20is%20a%20type%2Dvariable%20usage%20that%20meets%20both%20of%20the%20following%20conditions%3A)
- For the code in `isNullInclusiveUnderEveryParameterization`, see
  ["It is a type variable that meets _both_ of the following conditions...."](https://jspecify.dev/spec#:~:text=It%20is%20a%20type%20variable%20that%20meets%20both%20of%20the%20following%20conditions%3A)

This code will never (or
[perhaps only _almost_ never](https://github.com/jspecify/nullness-checker-for-checker-framework/commit/e80571b1d612f2476f89b401fcd6100169c3f7c5))
run under the current version of the checker, but it will become
necessary when we merge the upstream implementation of capture
conversion.
---
 .../NullSpecAnnotatedTypeFactory.java         | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java b/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java
index b9fc1df..393c683 100644
--- a/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java
+++ b/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java
@@ -30,6 +30,7 @@
 import static javax.lang.model.element.ElementKind.ENUM_CONSTANT;
 import static javax.lang.model.type.TypeKind.ARRAY;
 import static javax.lang.model.type.TypeKind.DECLARED;
+import static javax.lang.model.type.TypeKind.TYPEVAR;
 import static javax.lang.model.type.TypeKind.WILDCARD;
 import static org.checkerframework.framework.qual.TypeUseLocation.CONSTRUCTOR_RESULT;
 import static org.checkerframework.framework.qual.TypeUseLocation.EXCEPTION_PARAMETER;
@@ -444,6 +445,11 @@ private boolean isNullnessSubtype(AnnotatedTypeMirror subtype, AnnotatedTypeMirr
          */
         return true;
       }
+      if (supertype.getKind() == TYPEVAR
+          && !supertype.hasAnnotation(minusNull)
+          && isNullnessSubtype(subtype, ((AnnotatedTypeVariable) supertype).getLowerBound())) {
+        return true;
+      }
       return isNullInclusiveUnderEveryParameterization(supertype)
           || isNullExclusiveUnderEveryParameterization(subtype)
           || (nullnessEstablishingPathExists(subtype, supertype)
@@ -452,6 +458,14 @@ private boolean isNullnessSubtype(AnnotatedTypeMirror subtype, AnnotatedTypeMirr
   }
 
   boolean isNullInclusiveUnderEveryParameterization(AnnotatedTypeMirror type) {
+    // We put the third case from the spec first because it's a mouthful.
+    // (As discussed in the spec, we probably don't strictly need this case at all....)
+    if (type.getKind() == TYPEVAR
+        && !type.hasAnnotation(minusNull)
+        && isNullInclusiveUnderEveryParameterization(
+            ((AnnotatedTypeVariable) type).getLowerBound())) {
+      return true;
+    }
     /*
      * Our draft subtyping rules specify a special case for intersection types. However, those rules
      * make sense only because the rules also specify that an intersection type never has an
@@ -562,11 +576,6 @@ private boolean nullnessEstablishingPathExists(
         return true;
       }
     }
-    /*
-     * We don't need to handle the "lower-bound rule" here: The Checker Framework doesn't perform
-     * wildcard capture conversion. (Hmm, but it might see post-capture-conversion types in some
-     * cases....) It compares "? super Foo" against "Bar" by more directly comparing Foo and Bar.
-     */
     return false;
   }