Merge pull request #672 from Nadrieril/fix-divergence-on-send-bound

Skip inner obligations of `ImplSource::Builtin`

frontend/exporter/src/traits.rs

@@ -377,10 +377,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