From 4cc6ff1e88b9db432aa1c06b1b0f056f254fddb8 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Fri, 17 Jul 2026 15:17:07 -0400 Subject: [PATCH 1/2] Test capture glb with a non-top type-parameter bound framework/tests/h1h2checker/WildcardBounds.java notes it only exercises wildcard capture against a top type-parameter bound ("We could add an OuterS1 to also test with a non-top upper bound."), for which the glb of the wildcard's extends bound and the parameter bound trivially equals the wildcard's bound. Add a nontopdefault test capturing Foo where Foo and the wildcard's extends bound (the @NTDMiddle type-use default, or an explicit qualifier) is strictly more precise than the @NTDTop parameter bound. This confirms the captured type variable's upper bound is the greatest lower bound (@NTDMiddle), not the parameter bound wholesale, and that the result varies with the wildcard's extends bound (an explicit @NTDTop bound is not assignable to @NTDMiddle). This is the CF-level reduction for cf-tasks/task-3; see cf-tasks/task-3-findings.md. Capture conversion computes the glb correctly in stock CF, so no framework change is warranted. Co-Authored-By: Claude Fable 5 --- .../CaptureGlbWildcardBound.java | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 framework/tests/nontopdefault/CaptureGlbWildcardBound.java diff --git a/framework/tests/nontopdefault/CaptureGlbWildcardBound.java b/framework/tests/nontopdefault/CaptureGlbWildcardBound.java new file mode 100644 index 000000000000..b6b8af95ef84 --- /dev/null +++ b/framework/tests/nontopdefault/CaptureGlbWildcardBound.java @@ -0,0 +1,41 @@ +import org.checkerframework.framework.testchecker.nontopdefault.qual.NTDMiddle; +import org.checkerframework.framework.testchecker.nontopdefault.qual.NTDTop; + +// Capture conversion of Foo where Foo must give the +// captured type variable an upper bound equal to the glb of the wildcard's extends bound and the +// type parameter's bound -- not the type parameter's bound wholesale. Here the wildcard's extends +// bound (the type-use default @NTDMiddle, or an explicit qualifier) is more precise than the +// @NTDTop parameter bound, so the glb is the wildcard's qualifier. +// +// This fills the coverage gap noted in framework/tests/h1h2checker/WildcardBounds.java ("We could +// add an OuterS1 to also test with a non-top upper bound."): the existing wildcard-capture tests +// use a top parameter bound, for which the glb trivially equals the wildcard's bound. See also +// cf-tasks/task-3-findings.md. +@SuppressWarnings("inconsistent.constructor.type") // not the point of this test +class CaptureGlbWildcardBound { + interface Bar {} + + interface Foo { + T get(); + } + + // Implicit wildcard extends bound: Bar defaults to the type-use default @NTDMiddle, which is + // below the @NTDTop parameter bound. glb(@NTDMiddle Bar, @NTDTop Object) == @NTDMiddle Bar, so + // x.get() is @NTDMiddle. + void implicitBound(Foo x) { + @NTDMiddle Object m = x.get(); + } + + // Explicit @NTDMiddle wildcard extends bound: same glb, @NTDMiddle. + void explicitMiddleBound(Foo x) { + @NTDMiddle Object m = x.get(); + } + + // Discriminating control: an explicit @NTDTop wildcard extends bound equals the parameter + // bound, so the glb is @NTDTop, which is not assignable to @NTDMiddle. This confirms the glb + // machinery actually varies with the wildcard's extends bound. + void explicitTopBound(Foo x) { + // :: error: (assignment.type.incompatible) + @NTDMiddle Object m = x.get(); + } +} From 74ac01663514c5b59fea2bdf70365cd0612df872 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Sun, 19 Jul 2026 05:05:19 -0400 Subject: [PATCH 2/2] Extend capture-glb test with non-top parameter-bound cases Round-2 reconciliation (cf-tasks2/task-1-findings.md) re-verified with instrumentation that AnnotatedTypeFactory.applyCaptureConversion computes the correct qualifier glb for every JSpecify capture-glb record, including the conformance Basic.java:49 expression-type case: the observed capture upper bound carries the glb of the wildcard's extends bound and the substituted parameter bound. The remaining reference-checker mismatches are downstream (substituteTypeVariable overwriting a correct capture, and a capture-id formatting difference), not capture-side in CF. Add cases where the type parameter bound is itself non-top (@NTDMiddle) so the glb is taken from the parameter side too: a @NTDTop wildcard bound is pulled down to @NTDMiddle. Together with the existing @NTDTop-parameter-bound cases this exercises the glb from both the wildcard and the parameter side. Co-Authored-By: Claude Fable 5 --- .../CaptureGlbWildcardBound.java | 37 +++++++++++++++---- 1 file changed, 30 insertions(+), 7 deletions(-) diff --git a/framework/tests/nontopdefault/CaptureGlbWildcardBound.java b/framework/tests/nontopdefault/CaptureGlbWildcardBound.java index b6b8af95ef84..e3372e8d91ae 100644 --- a/framework/tests/nontopdefault/CaptureGlbWildcardBound.java +++ b/framework/tests/nontopdefault/CaptureGlbWildcardBound.java @@ -1,16 +1,22 @@ import org.checkerframework.framework.testchecker.nontopdefault.qual.NTDMiddle; import org.checkerframework.framework.testchecker.nontopdefault.qual.NTDTop; -// Capture conversion of Foo where Foo must give the -// captured type variable an upper bound equal to the glb of the wildcard's extends bound and the -// type parameter's bound -- not the type parameter's bound wholesale. Here the wildcard's extends -// bound (the type-use default @NTDMiddle, or an explicit qualifier) is more precise than the -// @NTDTop parameter bound, so the glb is the wildcard's qualifier. +// Capture conversion of Foo where Foo must give the captured +// type variable an upper bound equal to the glb of the wildcard's extends bound and the +// (substituted) type parameter bound -- not either bound wholesale. This mirrors JSpecify's +// spec-grounded capture rule (JLS 5.1.10 glb) with the qualifier lattice +// @NTDBottom <: @NTDMiddle <: @NTDTop, whose non-top type-use default @NTDMiddle plays the role of +// JSpecify's "unspecified". // // This fills the coverage gap noted in framework/tests/h1h2checker/WildcardBounds.java ("We could // add an OuterS1 to also test with a non-top upper bound."): the existing wildcard-capture tests -// use a top parameter bound, for which the glb trivially equals the wildcard's bound. See also -// cf-tasks/task-3-findings.md. +// use a top parameter bound, for which the glb trivially equals the wildcard's bound. +// +// Round-2 note: an investigation of the JSpecify capture-glb records (cf-tasks2/task-1-findings.md) +// confirmed with instrumentation that AnnotatedTypeFactory.applyCaptureConversion already computes +// the correct qualifier glb in every observed case; the remaining reference-checker mismatches are +// downstream (substituteTypeVariable and a capture-id formatting difference), not capture-side. +// This test locks in the CF behavior that investigation verified correct. @SuppressWarnings("inconsistent.constructor.type") // not the point of this test class CaptureGlbWildcardBound { interface Bar {} @@ -19,6 +25,10 @@ interface Foo { T get(); } + interface FooMid { + T get(); + } + // Implicit wildcard extends bound: Bar defaults to the type-use default @NTDMiddle, which is // below the @NTDTop parameter bound. glb(@NTDMiddle Bar, @NTDTop Object) == @NTDMiddle Bar, so // x.get() is @NTDMiddle. @@ -38,4 +48,17 @@ void explicitTopBound(Foo x) { // :: error: (assignment.type.incompatible) @NTDMiddle Object m = x.get(); } + + // The parameter bound constrains a less-precise wildcard bound: with a @NTDMiddle parameter + // bound, a @NTDTop wildcard extends bound is pulled down by the glb to @NTDMiddle, so x.get() + // is @NTDMiddle (not the wildcard's @NTDTop). A no-error assertion here holds only if the glb + // is taken from both sides. + void midParamTopWildcard(FooMid x) { + @NTDMiddle Object m = x.get(); + } + + // Both sides @NTDMiddle (the implicit default): glb is @NTDMiddle. + void midParamImplicit(FooMid x) { + @NTDMiddle Object m = x.get(); + } }