fix(exporter): disable impl expr resolution under type aliases

This commits disables trait resolution in the context of a type alias definition. Rust doesn't enforce bounds on generic parameters in type aliases, so it is legal to write: ```rust struct Foo<T: Clone>(T); type Synonym<T> = Foo<T>; ``` Thus, if we compute the impl expression for the bound `T: Clone` that appears on the type expression `Foo<T>`, Rustc's trait selection fails: in the context of `Synonym`, `T` indeed doesn't implement `Clone`, _a priori_. This is raising an issue about backends: translating such type synonym with "missing" bounds will fail. See #708. Fixes #707
cryspen · Jun 24, 2024 · 273a046 · 273a046
1 parent f4fd720
commit 273a046
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 2 deletions.
diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs
@@ -131,6 +131,12 @@ mod types {
             >,
         >,
         pub tcx: rustc_middle::ty::TyCtxt<'tcx>,
+        /// Rust doesn't enforce bounds on generic parameters in type
+        /// aliases. Thus, when translating type aliases, we need to
+        /// disable the resolution of implementation expressions. For
+        /// more details, please see
+        /// https://github.com/hacspec/hax/issues/707.
+        pub ty_alias_mode: bool,
     }
 
     impl<'tcx> Base<'tcx> {
@@ -149,6 +155,7 @@ mod types {
                 local_ctx: Rc::new(RefCell::new(LocalContextS::new())),
                 exported_spans: Rc::new(RefCell::new(HashSet::new())),
                 exported_def_ids: Rc::new(RefCell::new(HashSet::new())),
+                ty_alias_mode: false,
             }
         }
     }

diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
@@ -1627,7 +1627,11 @@ pub enum Ty {
         rustc_middle::ty::TyKind::Adt(adt_def, generics) => {
             let def_id = adt_def.did().sinto(state);
             let generic_args: Vec<GenericArg> = generics.sinto(state);
-            let trait_refs = solve_item_traits(state, state.param_env(), adt_def.did(), generics, None);
+            let trait_refs = if state.base().ty_alias_mode {
+                vec![]
+            } else {
+                solve_item_traits(state, state.param_env(), adt_def.did(), generics, None)
+            };
             Ty::Adt { def_id, generic_args, trait_refs }
         },
     )]
@@ -3003,7 +3007,19 @@ pub enum ItemKind<Body: IsBody> {
         items: Vec<ForeignItem<Body>>,
     },
     GlobalAsm(InlineAsm),
-    TyAlias(Ty, Generics<Body>),
+    TyAlias(
+        #[map({
+            let s = &State {
+                thir: s.clone(),
+                owner_id: s.owner_id(),
+                base: Base {ty_alias_mode: true, ..s.base()},
+                mir: (),
+            };
+            x.sinto(s)
+        })]
+        Ty,
+        Generics<Body>,
+    ),
     OpaqueTy(OpaqueTy<Body>),
     Enum(
         EnumDef<Body>,

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -173,6 +173,21 @@ let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyTy
   Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType
     x
 '''
+"Traits.Type_alias_bounds_issue_707_.fst" = '''
+module Traits.Type_alias_bounds_issue_707_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} =
+  | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T
+
+unfold
+let t_SynonymA (#v_T: Type0) = t_StructWithGenericBounds v_T
+
+unfold
+let t_SynonymB (#v_T: Type0) = t_StructWithGenericBounds (v_T & v_T)
+'''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''
 module Traits.Unconstrainted_types_issue_677_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -163,3 +163,9 @@ mod implicit_dependencies_issue_667 {
         }
     }
 }
+
+mod type_alias_bounds_issue_707 {
+    struct StructWithGenericBounds<T: Clone>(T);
+    type SynonymA<T> = StructWithGenericBounds<T>;
+    type SynonymB<T> = StructWithGenericBounds<(T, T)>;
+}