From 273a0468f976b59250b1af11886b95a7cdec54c7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 10 Jun 2024 11:26:27 +0200 Subject: [PATCH] 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); type Synonym = Foo; ``` Thus, if we compute the impl expression for the bound `T: Clone` that appears on the type expression `Foo`, 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 https://github.com/hacspec/hax/issues/708. Fixes #707 --- frontend/exporter/src/state.rs | 7 +++++++ frontend/exporter/src/types/copied.rs | 20 +++++++++++++++++-- .../toolchain__traits into-fstar.snap | 15 ++++++++++++++ tests/traits/src/lib.rs | 6 ++++++ 4 files changed, 46 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 2b70d4df9..094408315 100644 --- 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 index 1f7cdc1fa..de2e481a6 100644 --- 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 = 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 { items: Vec>, }, GlobalAsm(InlineAsm), - TyAlias(Ty, Generics), + 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, + ), OpaqueTy(OpaqueTy), Enum( EnumDef, diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 8047ce566..debc3170e 100644 --- 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 index 9821c42d0..c592d5761 100644 --- 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); + type SynonymA = StructWithGenericBounds; + type SynonymB = StructWithGenericBounds<(T, T)>; +}