From ad9d792929fdb454775a8415c4c0f6b420de11bd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 13 Oct 2026 21:48:51 +0000
Subject: [PATCH] Type a trait method call by the resolved impl method's type

A call to a trait method with a default body was typed by the trait
method's type, which is inferred from the default body, even when it
resolved to an override annotated with its own spec. The override is
checked only against that spec, so callers assumed a postcondition
nobody proved. Use the resolved impl method's type when there is one;
an unannotated override's type is the trait method's type anyway.

Fixes #337

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01SHVtHJd3xtzyFQiUiyqD3m
---
 src/analyze/basic_block.rs                    |  7 +++++--
 .../fail/trait_default_override_callable.rs   | 21 +++++++++++++++++++
 .../pass/trait_default_override_callable.rs   | 21 +++++++++++++++++++
 3 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 tests/ui/fail/trait_default_override_callable.rs
 create mode 100644 tests/ui/pass/trait_default_override_callable.rs

diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 97cc7f89..cf0654e9 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -1067,9 +1067,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     ) -> rty::Type<rty::Closed> {
         if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args) {
             let (impl_def_id, impl_args) = self.resolve_fn_def(def_id, args);
-            // otherwise nothing asks for a deferred impl method's type and its body goes unchecked
+            // an impl method annotated with its own spec is checked against that spec, not
+            // against the trait method's type, so the call must assume the impl's type
             if impl_def_id != def_id {
-                let _ = self.ctx.def_ty_with_args(impl_def_id, impl_args);
+                if let Some(impl_ty) = self.ctx.def_ty_with_args(impl_def_id, impl_args) {
+                    return impl_ty.ty;
+                }
             }
             return def_ty.ty;
         }
diff --git a/tests/ui/fail/trait_default_override_callable.rs b/tests/ui/fail/trait_default_override_callable.rs
new file mode 100644
index 00000000..bb62b96a
--- /dev/null
+++ b/tests/ui/fail/trait_default_override_callable.rs
@@ -0,0 +1,21 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+trait Tr {
+    fn m(&self) -> i64 {
+        2
+    }
+}
+
+struct A;
+
+impl Tr for A {
+    #[thrust::callable]
+    fn m(&self) -> i64 {
+        1
+    }
+}
+
+fn main() {
+    assert!(A.m() == 2);
+}
diff --git a/tests/ui/pass/trait_default_override_callable.rs b/tests/ui/pass/trait_default_override_callable.rs
new file mode 100644
index 00000000..4d927b5b
--- /dev/null
+++ b/tests/ui/pass/trait_default_override_callable.rs
@@ -0,0 +1,21 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+trait Tr {
+    fn m(&self) -> i64 {
+        2
+    }
+}
+
+struct A;
+
+impl Tr for A {
+    #[thrust::callable]
+    fn m(&self) -> i64 {
+        1
+    }
+}
+
+fn main() {
+    let _ = A.m();
+}