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