From 4eae5c69631882517b81926d98c3dd469f7d7b7f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 15 May 2024 11:30:09 +0200 Subject: [PATCH] Skip inner obligations of `ImplSource::Builtin` As they can lead to infinite recursion. --- frontend/exporter/src/traits.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 8492ce736..6bb47923d 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -384,10 +384,14 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { ImplSource::Object(data) => { ImplExprAtom::Dyn.with_args(impl_exprs(s, &data.nested), trait_ref) } - ImplSource::Builtin(nested) => ImplExprAtom::Builtin { + // We ignore the contained obligations here. For example for `(): Send`, the + // obligations contained would be `[(): Send]`, which leads to an infinite loop. There + // might be important obligation shere inother cases; we'll have to see if that comes + // up. + ImplSource::Builtin(_ignored) => ImplExprAtom::Builtin { r#trait: self.skip_binder().sinto(s), } - .with_args(impl_exprs(s, &nested), trait_ref), + .with_args(vec![], trait_ref), x => ImplExprAtom::Todo(format!( "ImplExprAtom::Todo(see https://github.com/hacspec/hax/issues/381) {:#?}\n\n{:#?}", x, self