diff --git a/pyrefly/lib/alt/narrow.rs b/pyrefly/lib/alt/narrow.rs
index 453c0ea7b8..f1cb546334 100644
--- a/pyrefly/lib/alt/narrow.rs
+++ b/pyrefly/lib/alt/narrow.rs
@@ -1768,6 +1768,10 @@ impl<'ctx, 'answer, Ans: LookupAnswer> AnswersSolver<'ctx, 'answer, Ans> {
                             // too conservative and prone to false positives, see
                             // https://github.com/facebook/pyrefly/issues/911
                             self.heap.mk_callable_ellipsis(self.heap.mk_any_implicit())
+                        } else if let Some(q) = self.solver().partial_quantified(&t) {
+                            // An uninferred TypeVar provides its upper bound as positive evidence.
+                            // Do not infer it from the subject during the intersection check.
+                            q.upper_bound(self.stdlib, self.heap)
                         } else {
                             *t
                         };
@@ -1795,6 +1799,11 @@ impl<'ctx, 'answer, Ans: LookupAnswer> AnswersSolver<'ctx, 'answer, Ans> {
                         )
                         .ty;
                     if let Type::TypeIs(t) = ret {
+                        if self.solver().partial_quantified(&t).is_some() {
+                            // The unknown type may be narrower than its bound, so a failed
+                            // check cannot exclude every value assignable to that bound.
+                            return ty.clone();
+                        }
                         return self.subtract(ty, &t);
                     }
                 }
diff --git a/pyrefly/lib/solver/solver.rs b/pyrefly/lib/solver/solver.rs
index ab6f15cbf4..3f0e8ed140 100644
--- a/pyrefly/lib/solver/solver.rs
+++ b/pyrefly/lib/solver/solver.rs
@@ -826,6 +826,17 @@ impl Solver {
         }
     }
 
+    /// Return the type parameter for a variable awaiting first-use inference.
+    pub fn partial_quantified(&self, ty: &Type) -> Option<Quantified> {
+        if let Type::Var(v) = ty {
+            let variables = self.variables.lock();
+            if let Variable::PartialQuantified(q) = &*variables.get(*v) {
+                return Some(q.clone());
+            }
+        }
+        None
+    }
+
     /// Only an unsolved quantified var can hold what a branch implies, since finishing the call
     /// is what turns those into answers.
     pub(crate) fn var_is_quantified(&self, var: Var) -> bool {
diff --git a/pyrefly/lib/test/narrow.rs b/pyrefly/lib/test/narrow.rs
index bb7c5a984f..7043b12e7f 100644
--- a/pyrefly/lib/test/narrow.rs
+++ b/pyrefly/lib/test/narrow.rs
@@ -1605,6 +1605,80 @@ def f(x: Cat | Dog):
     "#,
 );
 
+testcase!(
+    test_typeis_free_typevar_bound,
+    r#"
+from typing import TypeIs, TypeVar, assert_type
+
+T = TypeVar("T", bound=int)
+
+def is_t(x: object) -> TypeIs[T]: ...
+
+def caller(x: int | str | None) -> None:
+    if is_t(x):
+        assert_type(x, int)
+    else:
+        assert_type(x, int | str | None)
+
+def caller_object(x: object) -> None:
+    if is_t(x):
+        assert_type(x, int)
+
+def caller_subtype(x: bool | str) -> None:
+    if is_t(x):
+        assert_type(x, bool)
+    else:
+        assert_type(x, bool | str)
+    "#,
+);
+
+testcase!(
+    test_typeis_free_typevar_restrictions,
+    r#"
+from typing import TypeIs, assert_type
+
+def is_bounded[T: int](x: object) -> TypeIs[T]: ...
+def is_constrained[T: (int, str)](x: object) -> TypeIs[T]: ...
+def is_unbounded[T](x: object) -> TypeIs[T]: ...
+def is_defaulted[T: int = bool](x: object) -> TypeIs[T]: ...
+
+def caller(x: int | str | None) -> None:
+    if is_bounded(x):
+        assert_type(x, int)
+    if is_constrained(x):
+        assert_type(x, int | str)
+    else:
+        assert_type(x, int | str | None)
+    if is_unbounded(x):
+        assert_type(x, int | str | None)
+    else:
+        assert_type(x, int | str | None)
+    if is_defaulted(x):
+        assert_type(x, bool)
+    else:
+        assert_type(x, int | str | None)
+    "#,
+);
+
+testcase!(
+    test_typeis_inferred_typevar_bound,
+    r#"
+from typing import TypeIs, assert_type
+
+def is_t[T: int](x: object, target: type[T]) -> TypeIs[T]: ...
+
+def caller(x: bool | str) -> None:
+    if is_t(x, bool):
+        assert_type(x, bool)
+    else:
+        assert_type(x, str)
+
+def caller_generic[T: int](x: object, target: type[T]) -> None:
+    if is_t(x, target):
+        assert_type(x, T)
+    "#,
+);
+
 testcase!(
     test_typeis_union,
     r#"