From 3c126b2fc910608ffd781166381d1658080f1d49 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Wed, 30 Sep 2020 00:09:27 -0400 Subject: [PATCH 1/2] Permit fundamental types w/ multiple parameters --- chalk-integration/src/lowering.rs | 2 +- chalk-solve/src/clauses/program_clauses.rs | 38 +++++------- tests/lowering/mod.rs | 14 ----- tests/test/coherence.rs | 71 ++++++++++++++++++++++ 4 files changed, 88 insertions(+), 37 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 324c25f68f9..aeef609021b 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -274,7 +274,7 @@ impl LowerWithEnv for (&AdtDefn, chalk_ir::AdtId) { fn lower(&self, env: &Env) -> LowerResult { let (adt_defn, adt_id) = self; - if adt_defn.flags.fundamental && adt_defn.all_parameters().len() != 1 { + if adt_defn.flags.fundamental && adt_defn.all_parameters().len() < 1 { Err(RustIrError::InvalidFundamentalTypesParameters( adt_defn.name.clone(), ))?; diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 2f9ed502c46..7831285a693 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -402,28 +402,17 @@ impl ToProgramClauses for AdtDatum { ($goal:ident) => { // Fundamental types must always have at least one // type parameter for this rule to make any - // sense. We currently do not have have any - // fundamental types with more than one type - // parameter, nor do we know what the behaviour - // for that should be. Thus, we are asserting here - // that there is only a single type parameter - // until the day when someone makes a decision - // about how that should behave. - assert_eq!( - self_appl_ty.len_type_parameters(interner), - 1, - "Only fundamental types with a single parameter are supported" - ); - - builder.push_clause( - DomainGoal::$goal(self_ty.clone()), - Some(DomainGoal::$goal( - // This unwrap is safe because we asserted - // above for the presence of a type - // parameter - self_appl_ty.first_type_parameter(interner).unwrap(), - )), + // sense. + assert!( + self_appl_ty.len_type_parameters(interner) >= 1, + "Only fundamental types with type parameter are supported" ); + for type_param in self_appl_ty.type_parameters(interner) { + builder.push_clause( + DomainGoal::$goal(self_ty.clone()), + Some(DomainGoal::$goal(type_param)), + ); + } }; } @@ -437,7 +426,12 @@ impl ToProgramClauses for AdtDatum { // `#[fundamental]`, it satisfies IsLocal if and only // if its parameters satisfy IsLocal fundamental_rule!(IsLocal); - fundamental_rule!(IsUpstream); + builder.push_clause( + DomainGoal::IsUpstream(self_ty.clone()), + self_appl_ty + .type_parameters(interner) + .map(|type_param| DomainGoal::IsUpstream(type_param)), + ); } else { // The type is just upstream and not fundamental builder.push_fact(DomainGoal::IsUpstream(self_ty.clone())); diff --git a/tests/lowering/mod.rs b/tests/lowering/mod.rs index 6f7e3129c71..bdcc417c8a6 100644 --- a/tests/lowering/mod.rs +++ b/tests/lowering/mod.rs @@ -454,20 +454,6 @@ fn upstream_items() { } } -#[test] -fn fundamental_multiple_type_parameters() { - lowering_error! { - program { - #[fundamental] - struct Boxes { } - } - - error_msg { - "only a single parameter supported for fundamental type `Boxes`" - } - } -} - #[test] fn tuples() { lowering_success! { diff --git a/tests/test/coherence.rs b/tests/test/coherence.rs index 77c9b9eb454..ba431e7be3f 100644 --- a/tests/test/coherence.rs +++ b/tests/test/coherence.rs @@ -516,3 +516,74 @@ fn orphan_check() { } } } + +#[test] +fn fundamental_type_multiple_parameters() { + // Test that implementing a local trait on a fundamental + // type with multiple parameters is allowed + lowering_success! { + program { + #[upstream] + #[fundamental] + struct Box { } + + trait Local { } + + impl Local for Box { } + } + } + + // Test that implementing a remote trait on a fundamental + // type with multiple parameters is rejected + lowering_error! { + program { + #[upstream] + #[fundamental] + struct Box { } + + #[upstream] + trait Remote { } + + impl Remote for Box { } + } error_msg { + "impl for trait `Remote` violates the orphan rules" + } + } + + // Test that implementing a remote trait on a fundamental type + // with one local type parameter is allowed + lowering_success! { + program { + #[upstream] + #[fundamental] + struct Box { } + + struct Local { } + + #[upstream] + trait Remote { } + + impl Remote for Box { } + } + } + + // Test that implementing a remote trait on a fundamental type + // with one concrete remote type parameter is rejected + lowering_error! { + program { + #[upstream] + #[fundamental] + struct Box { } + + #[upstream] + struct Up { } + + #[upstream] + trait Remote { } + + impl Remote for Box { } + } error_msg { + "impl for trait `Remote` violates the orphan rules" + } + } +} From 2ee1c9d18511683857a9667788595e2116b0e5e6 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Wed, 30 Sep 2020 12:24:41 -0400 Subject: [PATCH 2/2] Address comments / clarify docs --- chalk-solve/src/clauses/program_clauses.rs | 49 ++++++++++------------ 1 file changed, 22 insertions(+), 27 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 7831285a693..bd05f4e1005 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -361,18 +361,20 @@ impl ToProgramClauses for AdtDatum { /// ```notrust /// #[upstream] /// #[fundamental] - /// struct Box {} + /// struct Box {} /// ``` /// /// We generate the following clauses: /// /// ```notrust - /// forall { IsLocal(Box) :- IsLocal(T). } + /// forall { IsLocal(Box) :- IsLocal(T). } + /// forall { IsLocal(Box) :- IsLocal(U). } /// - /// forall { IsUpstream(Box) :- IsUpstream(T). } + /// forall { IsUpstream(Box) :- IsUpstream(T), IsUpstream(U). } /// /// // Generated for both upstream and local fundamental types - /// forall { DownstreamType(Box) :- DownstreamType(T). } + /// forall { DownstreamType(Box) :- DownstreamType(T). } + /// forall { DownstreamType(Box) :- DownstreamType(U). } /// ``` /// #[instrument(level = "debug", skip(builder))] @@ -395,27 +397,6 @@ impl ToProgramClauses for AdtDatum { let self_appl_ty = application_ty(builder, id); let self_ty = self_appl_ty.clone().intern(interner); - // Fundamental types often have rules in the form of: - // Goal(FundamentalType) :- Goal(T) - // This macro makes creating that kind of clause easy - macro_rules! fundamental_rule { - ($goal:ident) => { - // Fundamental types must always have at least one - // type parameter for this rule to make any - // sense. - assert!( - self_appl_ty.len_type_parameters(interner) >= 1, - "Only fundamental types with type parameter are supported" - ); - for type_param in self_appl_ty.type_parameters(interner) { - builder.push_clause( - DomainGoal::$goal(self_ty.clone()), - Some(DomainGoal::$goal(type_param)), - ); - } - }; - } - // Types that are not marked `#[upstream]` satisfy IsLocal(TypeName) if !self.flags.upstream { // `IsLocalTy(Ty)` depends *only* on whether the type @@ -425,7 +406,12 @@ impl ToProgramClauses for AdtDatum { // If a type is `#[upstream]`, but is also // `#[fundamental]`, it satisfies IsLocal if and only // if its parameters satisfy IsLocal - fundamental_rule!(IsLocal); + for type_param in self_appl_ty.type_parameters(interner) { + builder.push_clause( + DomainGoal::IsLocal(self_ty.clone()), + Some(DomainGoal::IsLocal(type_param)), + ); + } builder.push_clause( DomainGoal::IsUpstream(self_ty.clone()), self_appl_ty @@ -438,7 +424,16 @@ impl ToProgramClauses for AdtDatum { } if self.flags.fundamental { - fundamental_rule!(DownstreamType); + assert!( + self_appl_ty.len_type_parameters(interner) >= 1, + "Only fundamental types with type parameters are supported" + ); + for type_param in self_appl_ty.type_parameters(interner) { + builder.push_clause( + DomainGoal::DownstreamType(self_ty.clone()), + Some(DomainGoal::DownstreamType(type_param)), + ); + } } }); }