diff --git a/crates/flux-infer/src/projections.rs b/crates/flux-infer/src/projections.rs index 0efa6b040d..b24ea27b17 100644 --- a/crates/flux-infer/src/projections.rs +++ b/crates/flux-infer/src/projections.rs @@ -804,6 +804,12 @@ fn normalize_alias_reft<'tcx>( let trait_ref = alias_reft.to_rustc_trait_ref(tcx); let trait_ref = tcx.erase_and_anonymize_regions(trait_ref); let trait_pred = Obligation::new(tcx, ObligationCause::dummy(), param_env, trait_ref); + + let pred: rustc_type_ir::TraitPredicate> = trait_pred.predicate; + if matches!(pred.self_ty().kind(), rustc_middle::ty::Dynamic(_, _)) { + return Ok((false, Expr::alias(alias_reft.clone(), refine_args.clone()))); + } + let impl_source = selcx .select(&trait_pred) .map_err(|e| query_bug!("error selecting {trait_pred:?}: {e:?}"))?; diff --git a/tests/tests/pos/surface/no_panic07.rs b/tests/tests/pos/surface/no_panic07.rs new file mode 100644 index 0000000000..0991e5ba35 --- /dev/null +++ b/tests/tests/pos/surface/no_panic07.rs @@ -0,0 +1,17 @@ +#[flux::assoc(fn blueberry_no_panic() -> bool)] +pub trait MyTrait<'a> { + #[flux::sig(fn(&Self) -> ())] + #[flux::no_panic_if(Self::blueberry_no_panic())] + fn blueberry(&self) { + let x = 3; + } +} + +pub struct MyStruct<'a> { + field: &'a dyn MyTrait<'a>, +} + +#[flux::no_panic_if(MyTrait::blueberry_no_panic())] +fn foo(s: &MyStruct) { + s.field.blueberry(); +}