Merge pull request #1008 from Nadrieril/resolve-impl-trait

Support `impl Trait` in trait resolution
hacspec · Oct 16, 2024 · 21672cd · 21672cd
2 parents 69d97ef + 1b45ce1
commit 21672cd
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 1 deletion.
diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs
@@ -164,7 +164,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
     pub fn new_for_owner(tcx: TyCtxt<'tcx>, owner_id: DefId) -> Self {
         let mut out = Self {
             tcx,
-            param_env: tcx.param_env(owner_id),
+            param_env: tcx.param_env(owner_id).with_reveal_all_normalized(tcx),
             candidates: Default::default(),
         };
         out.extend(

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -602,6 +602,15 @@ let iter_option (#v_T: Type0) (x: Core.Option.t_Option v_T) : Core.Option.t_Into
     #FStar.Tactics.Typeclasses.solve
     (Core.Option.impl__as_ref #v_T x <: Core.Option.t_Option v_T)
 
+let use_impl_trait (_: Prims.unit) : Prims.unit =
+  let iter:_ = iter_option #bool (Core.Option.Option_Some false <: Core.Option.t_Option bool) in
+  let tmp0, out:(_ & Core.Option.t_Option bool) =
+    Core.Iter.Traits.Iterator.f_next #_ #FStar.Tactics.Typeclasses.solve iter
+  in
+  let iter:_ = tmp0 in
+  let _:Core.Option.t_Option bool = out in
+  ()
+
 class t_Foo (v_Self: Type0) = {
   f_AssocType:Type0;
   f_AssocType_15525962639250476383:t_SuperTrait f_AssocType;

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -83,6 +83,12 @@ fn iter_option<'a, T>(x: &'a Option<T>) -> impl Iterator<Item = &'a T> {
     x.as_ref().into_iter()
 }
 
+// Issue #684
+fn use_impl_trait() {
+    let mut iter = iter_option(&Some(false));
+    let _ = iter.next();
+}
+
 mod for_clauses {
     trait Foo<T> {
         fn to_t(&self) -> T;