get_impl_paths more exhaustive checks

source/rust_verify/src/fn_call_to_vir.rs

@@ -214,7 +214,8 @@ pub(crate) fn fn_call_to_vir<'tcx>(
                     is_trait_default = true;
                     remove_self_trait_bound = Some((trait_id, &mut self_trait_impl_path));
                 }
-                let impl_paths = get_impl_paths(bctx, did, &inst.args, remove_self_trait_bound);
+                let impl_paths =
+                    get_impl_paths(bctx, did, &inst.args, remove_self_trait_bound, expr.span)?;
                 if tcx.trait_of_item(did).is_some() {
                     if let Some(vir::ast::ImplPath::TraitImplPath(impl_path)) = self_trait_impl_path
                     {
@@ -242,7 +243,7 @@ pub(crate) fn fn_call_to_vir<'tcx>(
     let vir_args = mk_vir_args(bctx, node_substs, f, &args)?;
 
     let typ_args = mk_typ_args(bctx, node_substs, f, expr.span)?;
-    let impl_paths = get_impl_paths(bctx, f, node_substs, None);
+    let impl_paths = get_impl_paths(bctx, f, node_substs, None, expr.span)?;
     let target = CallTarget::Fun(target_kind, name, typ_args, impl_paths, autospec_usage);
     Ok(bctx.spanned_typed_new(expr.span, &expr_typ()?, ExprX::Call(target, Arc::new(vir_args))))
 }
@@ -1426,7 +1427,7 @@ fn verus_item_to_vir<'tcx, 'a>(
             typ_args.swap(0, 1);
             let typ_args = Arc::new(typ_args);
 
-            let impl_paths = get_impl_paths(bctx, f, node_substs, None);
+            let impl_paths = get_impl_paths(bctx, f, node_substs, None, expr.span)?;
 
             return mk_expr(ExprX::Call(
                 CallTarget::BuiltinSpecFun(bsf, typ_args, impl_paths),
@@ -1446,7 +1447,8 @@ fn get_impl_paths<'tcx>(
     f: DefId,
     node_substs: &'tcx rustc_middle::ty::List<rustc_middle::ty::GenericArg<'tcx>>,
     remove_self_trait_bound: Option<(DefId, &mut Option<vir::ast::ImplPath>)>,
-) -> vir::ast::ImplPaths {
+    span: Span,
+) -> Result<vir::ast::ImplPaths, VirErr> {
     if let rustc_middle::ty::FnDef(fid, _fsubsts) = bctx.ctxt.tcx.type_of(f).skip_binder().kind() {
         crate::rust_to_vir_base::get_impl_paths(
             bctx.ctxt.tcx,
@@ -1455,6 +1457,7 @@ fn get_impl_paths<'tcx>(
             *fid,
             node_substs,
             remove_self_trait_bound,
+            span,
         )
     } else {
         panic!("unexpected function {:?}", f)

source/rust_verify/src/rust_to_vir_base.rs

@@ -413,9 +413,17 @@ pub(crate) fn get_impl_paths<'tcx>(
     target_id: DefId,
     node_substs: &'tcx rustc_middle::ty::List<rustc_middle::ty::GenericArg<'tcx>>,
     remove_self_trait_bound: Option<(DefId, &mut Option<vir::ast::ImplPath>)>,
-) -> vir::ast::ImplPaths {
+    span: Span,
+) -> Result<vir::ast::ImplPaths, VirErr> {
     let clauses = instantiate_pred_clauses(tcx, target_id, node_substs);
-    get_impl_paths_for_clauses(tcx, verus_items, param_env_src, clauses, remove_self_trait_bound)
+    get_impl_paths_for_clauses(
+        tcx,
+        verus_items,
+        param_env_src,
+        clauses,
+        remove_self_trait_bound,
+        span,
+    )
 }
 
 pub(crate) fn get_impl_paths_for_clauses<'tcx>(
@@ -424,7 +432,8 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>(
     param_env_src: DefId,
     clauses: Vec<(Option<ClauseFrom<'tcx>>, Clause<'tcx>)>,
     mut remove_self_trait_bound: Option<(DefId, &mut Option<vir::ast::ImplPath>)>,
-) -> vir::ast::ImplPaths {
+    span: Span,
+) -> Result<vir::ast::ImplPaths, VirErr> {
     let mut impl_paths = Vec::new();
     let param_env = tcx.param_env(param_env_src);
 
@@ -465,8 +474,8 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>(
                 let trait_refs = tcx.normalize_erasing_regions(param_env, trait_refs);
                 tcx.codegen_select_candidate((param_env, trait_refs))
             });
-            if let Ok(impl_source) = candidate {
-                if let rustc_middle::traits::ImplSource::UserDefined(u) = impl_source {
+            match candidate {
+                Ok(rustc_middle::traits::ImplSource::UserDefined(u)) => {
                     let impl_path = def_id_to_vir_path(tcx, verus_items, u.impl_def_id);
                     let impl_path = ImplPath::TraitImplPath(impl_path);
                     match (&mut remove_self_trait_bound, inst_bound) {
@@ -487,19 +496,9 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>(
                             predicate_worklist.push(p);
                         }
                     }
-                } else if let rustc_middle::traits::ImplSource::Builtin(
-                    rustc_middle::traits::BuiltinImplSource::Misc,
-                    _,
-                ) = impl_source
-                {
-                    // When the needed trait bound is `FnDef(f) : FnOnce(...)`
-                    // The `impl_source` doesn't have the information we need,
-                    // so we have to special case this here.
-
-                    // REVIEW: need to see if there are other problematic cases here;
-                    // I think codegen_select_candidate lacks some information because
-                    // it's used for codegen
-
+                }
+                Ok(rustc_middle::traits::ImplSource::Param(_)) => {}
+                Ok(rustc_middle::traits::ImplSource::Builtin(_, _)) => {
                     match inst_pred_kind {
                         ClauseKind::Trait(TraitPredicate {
                             trait_ref:
@@ -514,6 +513,7 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>(
                                 || Some(trait_def_id) == tcx.lang_items().fn_mut_trait()
                                 || Some(trait_def_id) == tcx.lang_items().fn_once_trait()
                             {
+                                // Handle the trait bound is `FnDef(f) : FnOnce(...)`
                                 match trait_args.into_type_list(tcx)[0].kind() {
                                     TyKind::FnDef(fn_def_id, fn_node_substs) => {
                                         let fn_path =
@@ -534,15 +534,36 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>(
                                     }
                                     _ => {}
                                 }
+                            } else if Some(trait_def_id) == tcx.lang_items().sized_trait()
+                                || Some(trait_def_id) == tcx.lang_items().tuple_trait()
+                                || Some(trait_def_id) == tcx.lang_items().pointee_trait()
+                                || Some(trait_def_id) == tcx.lang_items().sync_trait()
+                                || matches!(
+                                    verus_items::get_rust_item(tcx, trait_def_id),
+                                    Some(RustItem::Send | RustItem::Thin)
+                                )
+                            {
+                                // Sized, Tuple, Pointee, Thin are all ok to do nothing.
+                                // There can't be user impls of these traits, they can only be built-in.
+
+                                // TODO: Send and Sync needs handling, or a rigorous argument why it's ok to skip;
+                                // See https://github.com/verus-lang/verus/issues/1335
+                            } else {
+                                unsupported_err!(span, "this trait bound: {:?}", trait_refs)
                             }
                         }
-                        _ => {}
+                        _ => {
+                            unsupported_err!(span, "this trait bound: {:?}", trait_refs)
+                        }
                     }
                 }
+                Err(_) => {
+                    // TODO this happens sometimes - why?
+                }
             }
         }
     }
-    Arc::new(impl_paths)
+    Ok(Arc::new(impl_paths))
 }
 
 pub(crate) fn mk_visibility<'tcx>(ctxt: &Context<'tcx>, def_id: DefId) -> vir::ast::Visibility {
@@ -975,7 +996,8 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
                     return Ok((Arc::new(TypX::SpecFn(param_typs, ret_typ)), false));
                 }
                 let typ_args = typ_args.into_iter().map(|(t, _)| t).collect();
-                let impl_paths = get_impl_paths(tcx, verus_items, param_env_src, did, args, None);
+                let impl_paths =
+                    get_impl_paths(tcx, verus_items, param_env_src, did, args, None, span)?;
                 let datatypex =
                     def_id_to_datatype(tcx, verus_items, did, Arc::new(typ_args), impl_paths);
                 (Arc::new(datatypex), false)

source/rust_verify/src/rust_to_vir_expr.rs

@@ -1551,7 +1551,8 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                             bctx.fun_id,
                             vec![(None, clause)],
                             None,
-                        );
+                            expr.span,
+                        )?;
 
                         let typ_args = Arc::new(vec![tup_typ, ret_typ, fun_typ]);
                         (

source/rust_verify/src/rust_to_vir_impl.rs

@@ -83,7 +83,8 @@ fn trait_impl_to_vir<'tcx>(
         trait_did,
         trait_ref.skip_binder().args,
         None,
-    );
+        span,
+    )?;
 
     // If we have `impl X for Z<A, B, C>` then the list of types is [X, A, B, C].
     // We keep this full list, with the first element being the Self type X

source/rust_verify/src/verus_items.rs

@@ -598,6 +598,8 @@ pub(crate) enum RustItem {
     ManuallyDrop,
     PhantomData,
     Destruct,
+    Send,
+    Thin,
 }
 
 pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<RustItem> {
@@ -698,6 +700,12 @@ pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option<RustItem> {
     if rust_path == Some("core::alloc::Allocator") {
         return Some(RustItem::Allocator);
     }
+    if rust_path == Some("core::marker::Send") {
+        return Some(RustItem::Send);
+    }
+    if rust_path == Some("core::ptr::metadata::Thin") {
+        return Some(RustItem::Thin);
+    }
 
     if let Some(rust_path) = rust_path {
         static NUM_RE: std::sync::OnceLock<Regex> = std::sync::OnceLock::new();