Support more features

engine/lib/import_thir.ml

@@ -1019,7 +1019,7 @@ end) : EXPR = struct
         let impl = c_impl_expr span impl_expr in
         let item = Concrete_ident.of_def_id (AssociatedItem Type) def_id in
         TAssociatedType { impl; item }
-    | Alias { kind = Opaque; def_id; _ } ->
+    | Alias { kind = Opaque _; def_id; _ } ->
         TOpaque (Concrete_ident.of_def_id Type def_id)
     | Alias { kind = Inherent; _ } ->
         assertion_failure [ span ] "Ty::Alias with AliasTyKind::Inherent"

frontend/exporter/src/constant_utils.rs

@@ -581,27 +581,43 @@ mod rustc {
             .s_unwrap(s);
 
         // Iterate over the fields, which should be values
-        assert!(dc.variant.is_none());
-
-        // The type should be tuple
-        let hax_ty: Ty = ty.sinto(s);
-        match hax_ty.kind() {
-            TyKind::Tuple(_) => (),
-            _ => {
-                fatal!(s[span], "Expected the type to be tuple: {:?}", val)
-            }
-        };
-
         // Below: we are mutually recursive with [const_value_to_constant_expr],
         // which takes a [Const] as input, but it should be
         // ok because we call it on a strictly smaller value.
-        let fields: Vec<ConstantExpr> = dc
+        let fields = dc
             .fields
             .iter()
             .copied()
-            .map(|(val, ty)| const_value_to_constant_expr(s, ty, val, span))
-            .collect();
-        (ConstantExprKind::Tuple { fields }).decorate(hax_ty, span.sinto(s))
+            .map(|(val, ty)| const_value_to_constant_expr(s, ty, val, span));
+
+        // The type should be tuple
+        let hax_ty: Ty = ty.sinto(s);
+        match ty.kind() {
+            ty::TyKind::Tuple(_) => {
+                assert!(dc.variant.is_none());
+                let fields = fields.collect();
+                ConstantExprKind::Tuple { fields }
+            }
+            ty::TyKind::Adt(adt_def, ..) => {
+                let variant = dc.variant.unwrap_or(rustc_target::abi::FIRST_VARIANT);
+                let variants_info = get_variant_information(adt_def, variant, s);
+                let fields = fields
+                    .zip(&adt_def.variant(variant).fields)
+                    .map(|(value, field)| ConstantFieldExpr {
+                        field: field.did.sinto(s),
+                        value,
+                    })
+                    .collect();
+                ConstantExprKind::Adt {
+                    info: variants_info,
+                    fields,
+                }
+            }
+            _ => {
+                fatal!(s[span], "Expected the type to be tuple or adt: {:?}", val)
+            }
+        }
+        .decorate(hax_ty, span.sinto(s))
     }
 
     pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
@@ -633,26 +649,30 @@ mod rustc {
             ConstValue::ZeroSized { .. } => {
                 // Should be unit
                 let hty: Ty = ty.sinto(s);
-                let cv = match hty.kind() {
-                    TyKind::Tuple(tys) if tys.is_empty() => {
+                let cv = match ty.kind() {
+                    ty::TyKind::Tuple(tys) if tys.is_empty() => {
                         ConstantExprKind::Tuple { fields: Vec::new() }
                     }
-                    TyKind::Arrow(_) => match ty.kind() {
-                        rustc_middle::ty::TyKind::FnDef(def_id, args) => {
-                            let (def_id, generics, generics_impls, method_impl) =
-                                get_function_from_def_id_and_generics(s, *def_id, args);
-
-                            ConstantExprKind::FnPtr {
-                                def_id,
-                                generics,
-                                generics_impls,
-                                method_impl,
-                            }
+                    ty::TyKind::FnDef(def_id, args) => {
+                        let (def_id, generics, generics_impls, method_impl) =
+                            get_function_from_def_id_and_generics(s, *def_id, args);
+
+                        ConstantExprKind::FnPtr {
+                            def_id,
+                            generics,
+                            generics_impls,
+                            method_impl,
                         }
-                        kind => {
-                            fatal!(s[span], "Unexpected:"; {kind})
+                    }
+                    ty::TyKind::Adt(adt_def, ..) => {
+                        assert_eq!(adt_def.variants().len(), 1);
+                        let variant = rustc_target::abi::FIRST_VARIANT;
+                        let variants_info = get_variant_information(adt_def, variant, s);
+                        ConstantExprKind::Adt {
+                            info: variants_info,
+                            fields: vec![],
                         }
-                    },
+                    }
                     _ => {
                         fatal!(
                             s[span],

frontend/exporter/src/traits.rs

@@ -17,17 +17,29 @@ pub use resolution::PredicateSearcher;
 pub enum ImplExprPathChunk {
     AssocItem {
         item: AssocItem,
+        /// The arguments provided to the item (for GATs).
+        generic_args: Vec<GenericArg>,
+        /// The impl exprs that must be satisfied to apply the given arguments to the item. E.g.
+        /// `T: Clone` in the following example:
+        /// ```ignore
+        /// trait Foo {
+        ///     type Type<T: Clone>: Debug;
+        /// }
+        /// ```
+        impl_exprs: Vec<ImplExpr>,
+        /// The implemented predicate.
         predicate: Binder<TraitPredicate>,
         #[value(<_ as SInto<_, Clause>>::sinto(predicate, s).id)]
         predicate_id: PredicateId,
-        /// The nth predicate returned by `tcx.item_bounds`.
+        /// The index of this predicate in the list returned by `tcx.item_bounds`.
         index: usize,
     },
     Parent {
+        /// The implemented predicate.
         predicate: Binder<TraitPredicate>,
         #[value(<_ as SInto<_, Clause>>::sinto(predicate, s).id)]
         predicate_id: PredicateId,
-        /// The nth predicate returned by `tcx.predicates_of`.
+        /// The index of this predicate in the list returned by `tcx.predicates_of`.
         index: usize,
     },
 }

frontend/exporter/src/traits/resolution.rs

@@ -14,13 +14,25 @@ use crate::traits::utils::erase_and_norm;
 pub enum PathChunk<'tcx> {
     AssocItem {
         item: AssocItem,
+        /// The arguments provided to the item (for GATs).
+        generic_args: &'tcx [GenericArg<'tcx>],
+        /// The impl exprs that must be satisfied to apply the given arguments to the item. E.g.
+        /// `T: Clone` in the following example:
+        /// ```ignore
+        /// trait Foo {
+        ///     type Type<T: Clone>: Debug;
+        /// }
+        /// ```
+        impl_exprs: Vec<ImplExpr<'tcx>>,
+        /// The implemented predicate.
         predicate: PolyTraitPredicate<'tcx>,
-        /// The nth predicate returned by `tcx.item_bounds`.
+        /// The index of this predicate in the list returned by `tcx.item_bounds`.
         index: usize,
     },
     Parent {
+        /// The implemented predicate.
         predicate: PolyTraitPredicate<'tcx>,
-        /// The nth predicate returned by `tcx.predicates_of`.
+        /// The index of this predicate in the list returned by `tcx.predicates_of`.
         index: usize,
     },
 }
@@ -213,20 +225,27 @@ impl<'tcx> PredicateSearcher<'tcx> {
     }
 
     /// If the type is a trait associated type, we add any relevant bounds to our context.
-    fn add_associated_type_refs(&mut self, ty: Binder<'tcx, Ty<'tcx>>) {
+    fn add_associated_type_refs(
+        &mut self,
+        ty: Binder<'tcx, Ty<'tcx>>,
+        // Call back into hax-related code to display a nice warning.
+        warn: &impl Fn(&str),
+    ) -> Result<(), String> {
         let tcx = self.tcx;
         // Note: We skip a binder but rebind it just after.
         let TyKind::Alias(AliasTyKind::Projection, alias_ty) = ty.skip_binder().kind() else {
-            return;
+            return Ok(());
         };
-        let trait_ref = ty.rebind(alias_ty.trait_ref(tcx)).upcast(tcx);
+        let (trait_ref, item_args) = alias_ty.trait_ref_and_own_args(tcx);
+        let trait_ref = ty.rebind(trait_ref).upcast(tcx);
 
         // The predicate we're looking for is is `<T as Trait>::Type: OtherTrait`. We look up `T as
         // Trait` in the current context and add all the bounds on `Trait::Type` to our context.
-        let Some(trait_candidate) = self.lookup(trait_ref) else {
-            return;
+        let Some(trait_candidate) = self.resolve_local(trait_ref, warn)? else {
+            return Ok(());
         };
 
+        // The bounds that the associated type must validate.
         let item_bounds = tcx
             // TODO: `item_bounds` can contain parent traits, we don't want them
             .item_bounds(alias_ty.def_id)
@@ -235,6 +254,16 @@ impl<'tcx> PredicateSearcher<'tcx> {
             .filter_map(|pred| pred.as_trait_clause())
             .enumerate();
 
+        // Resolve predicates required to mention the item.
+        let nested_impl_exprs: Vec<_> = tcx
+            .predicates_defined_on(alias_ty.def_id)
+            .predicates
+            .iter()
+            .filter_map(|(clause, _span)| clause.as_trait_clause())
+            .map(|trait_pred| trait_pred.map_bound(|p| p.trait_ref))
+            .map(|trait_ref| self.resolve(&trait_ref, warn))
+            .collect::<Result<_, _>>()?;
+
         // Add all the bounds on the corresponding associated item.
         self.extend(item_bounds.map(|(index, pred)| {
             let mut candidate = Candidate {
@@ -244,26 +273,35 @@ impl<'tcx> PredicateSearcher<'tcx> {
             };
             candidate.path.push(PathChunk::AssocItem {
                 item: tcx.associated_item(alias_ty.def_id),
+                generic_args: item_args,
+                impl_exprs: nested_impl_exprs.clone(),
                 predicate: pred,
                 index,
             });
             candidate
         }));
+
+        Ok(())
     }
 
-    /// Lookup a predicate in this set. If the predicate applies to an associated type, we
-    /// add the relevant implied associated type bounds to the set as well.
-    fn lookup(&mut self, target: PolyTraitPredicate<'tcx>) -> Option<Candidate<'tcx>> {
+    /// Resolve a local clause by looking it up in this set. If the predicate applies to an
+    /// associated type, we add the relevant implied associated type bounds to the set as well.
+    fn resolve_local(
+        &mut self,
+        target: PolyTraitPredicate<'tcx>,
+        // Call back into hax-related code to display a nice warning.
+        warn: &impl Fn(&str),
+    ) -> Result<Option<Candidate<'tcx>>, String> {
         tracing::trace!("Looking for {target:?}");
 
         // Look up the predicate
         let ret = self.candidates.get(&target).cloned();
         if ret.is_some() {
-            return ret;
+            return Ok(ret);
         }
 
         // Add clauses related to associated type in the `Self` type of the predicate.
-        self.add_associated_type_refs(target.self_ty());
+        self.add_associated_type_refs(target.self_ty(), warn)?;
 
         let ret = self.candidates.get(&target).cloned();
         if ret.is_none() {
@@ -275,7 +313,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
                     .join("")
             );
         }
-        ret
+        Ok(ret)
     }
 
     /// Resolve the given trait reference in the local context.
@@ -304,7 +342,9 @@ impl<'tcx> PredicateSearcher<'tcx> {
                 def_id: impl_def_id,
                 generics,
             },
-            Ok(ImplSource::Param(_)) => match self.lookup(erased_tref.upcast(self.tcx)) {
+            Ok(ImplSource::Param(_)) => match self
+                .resolve_local(erased_tref.upcast(self.tcx), warn)?
+            {
                 Some(candidate) => {
                     let path = candidate.path;
                     let r#trait = candidate.origin.clause.to_poly_trait_ref();
@@ -338,27 +378,28 @@ impl<'tcx> PredicateSearcher<'tcx> {
 
         let nested = match &impl_source {
             Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { nested, .. })) => {
-                nested.as_slice()
+                // The nested obligations of depth 1 correspond (we hope) to the predicates on the
+                // relevant impl that need to be satisfied.
+                nested
+                    .iter()
+                    .filter(|obligation| obligation.recursion_depth == 1)
+                    .filter_map(|obligation| {
+                        obligation.predicate.as_trait_clause().map(|trait_ref| {
+                            self.resolve(&trait_ref.map_bound(|p| p.trait_ref), warn)
+                        })
+                    })
+                    .collect::<Result<_, _>>()?
             }
-            Ok(ImplSource::Param(nested)) => nested.as_slice(),
+            // Nested obligations can happen e.g. for GATs. We ignore these as we resolve local
+            // clauses ourselves.
+            Ok(ImplSource::Param(_)) => vec![],
             // 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 obligations here in other cases; we'll have to see if that comes
             // up.
-            Ok(ImplSource::Builtin(_, _ignored)) => &[],
-            Err(_) => &[],
+            Ok(ImplSource::Builtin(..)) => vec![],
+            Err(_) => vec![],
         };
-        let nested = nested
-            .iter()
-            // Only keep depth-1 obligations to avoid duplicate impl exprs.
-            .filter(|obligation| obligation.recursion_depth == 1)
-            .filter_map(|obligation| {
-                obligation
-                    .predicate
-                    .as_trait_clause()
-                    .map(|trait_ref| self.resolve(&trait_ref.map_bound(|p| p.trait_ref), warn))
-            })
-            .collect::<Result<_, _>>()?;
 
         Ok(ImplExpr {
             r#impl: atom,

frontend/exporter/src/types/copied.rs

@@ -1766,7 +1766,10 @@ pub enum AliasKind {
     /// An associated type in an inherent impl.
     Inherent,
     /// An `impl Trait` opaque type.
-    Opaque,
+    Opaque {
+        /// The real type hidden inside this opaque type.
+        hidden_ty: Ty,
+    },
     /// A type alias that references opaque types. Likely to always be normalized away.
     Weak,
 }
@@ -1778,11 +1781,11 @@ impl Alias {
         s: &S,
         alias_kind: &rustc_type_ir::AliasTyKind,
         alias_ty: &rustc_middle::ty::AliasTy<'tcx>,
-    ) -> Self {
+    ) -> TyKind {
+        let tcx = s.base().tcx;
         use rustc_type_ir::AliasTyKind as RustAliasKind;
         let kind = match alias_kind {
             RustAliasKind::Projection => {
-                let tcx = s.base().tcx;
                 let trait_ref = alias_ty.trait_ref(tcx);
                 // In a case like:
                 // ```
@@ -1803,14 +1806,20 @@ impl Alias {
                 }
             }
             RustAliasKind::Inherent => AliasKind::Inherent,
-            RustAliasKind::Opaque => AliasKind::Opaque,
+            RustAliasKind::Opaque => {
+                // Reveal the underlying `impl Trait` type.
+                let ty = tcx.type_of(alias_ty.def_id).instantiate(tcx, alias_ty.args);
+                AliasKind::Opaque {
+                    hidden_ty: ty.sinto(s),
+                }
+            }
             RustAliasKind::Weak => AliasKind::Weak,
         };
-        Alias {
+        TyKind::Alias(Alias {
             kind,
             args: alias_ty.args.sinto(s),
             def_id: alias_ty.def_id.sinto(s),
-        }
+        })
     }
 }
 
@@ -1903,7 +1912,7 @@ pub enum TyKind {
     Tuple(Vec<Ty>),
     #[custom_arm(
         rustc_middle::ty::TyKind::Alias(alias_kind, alias_ty) => {
-            TyKind::Alias(Alias::from(state, alias_kind, alias_ty))
+            Alias::from(state, alias_kind, alias_ty)
         },
     )]
     Alias(Alias),