Skip to content

Commit 3a3c439

Browse files
authored
Merge pull request #145 from scalexm/quantified-inline-bound
Add support for quantified bounds on GATs
2 parents c80a5ee + ddaafd3 commit 3a3c439

File tree

9 files changed

+167
-27
lines changed

9 files changed

+167
-27
lines changed

chalk-parse/src/ast.rs

+7-1
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ pub struct TraitFlags {
6262
pub struct AssocTyDefn {
6363
pub name: Identifier,
6464
pub parameter_kinds: Vec<ParameterKind>,
65-
pub bounds: Vec<InlineBound>,
65+
pub bounds: Vec<QuantifiedInlineBound>,
6666
pub where_clauses: Vec<QuantifiedWhereClause>,
6767
}
6868

@@ -85,6 +85,12 @@ pub enum InlineBound {
8585
ProjectionEqBound(ProjectionEqBound),
8686
}
8787

88+
#[derive(Clone, PartialEq, Eq, Debug)]
89+
pub struct QuantifiedInlineBound {
90+
pub parameter_kinds: Vec<ParameterKind>,
91+
pub bound: InlineBound,
92+
}
93+
8894
#[derive(Clone, PartialEq, Eq, Debug)]
8995
/// Represents a trait bound on e.g. a type or type parameter.
9096
/// Does not know anything about what it's binding.

chalk-parse/src/parser.lalrpop

+13-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ TraitDefn: TraitDefn = {
7474
};
7575

7676
AssocTyDefn: AssocTyDefn = {
77-
"type" <name:Id> <p:Angle<ParameterKind>> <b:(":" <Plus<InlineBound>>)?>
77+
"type" <name:Id> <p:Angle<ParameterKind>> <b:(":" <Plus<QuantifiedInlineBound>>)?>
7878
<w:QuantifiedWhereClauses> ";" =>
7979
{
8080
AssocTyDefn {
@@ -114,6 +114,18 @@ ProjectionEqBound: ProjectionEqBound = {
114114
}
115115
};
116116

117+
QuantifiedInlineBound: QuantifiedInlineBound = {
118+
<b:InlineBound> => QuantifiedInlineBound {
119+
parameter_kinds: vec![],
120+
bound: b,
121+
},
122+
123+
"forall" "<" <pk:Comma<ParameterKind>> ">" <b:InlineBound> => QuantifiedInlineBound {
124+
parameter_kinds: pk,
125+
bound: b,
126+
},
127+
};
128+
117129
Impl: Impl = {
118130
<external:ExternalKeyword?> "impl" <p:Angle<ParameterKind>> <mark:"!"?> <t:Id> <a:Angle<Parameter>> "for" <s:Ty>
119131
<w:QuantifiedWhereClauses> "{" <assoc:AssocTyValue*> "}" =>

src/ir.rs

+20-6
Original file line numberDiff line numberDiff line change
@@ -282,19 +282,34 @@ pub enum InlineBound {
282282
ProjectionEqBound(ProjectionEqBound),
283283
}
284284

285+
pub type QuantifiedInlineBound = Binders<InlineBound>;
286+
285287
impl InlineBound {
286288
/// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`].
287289
///
288290
/// Because an `InlineBound` does not know anything about what it's binding,
289291
/// you must provide that type as `self_ty`.
290-
crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
292+
fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
291293
match self {
292294
InlineBound::TraitBound(b) => b.into_where_clauses(self_ty),
293295
InlineBound::ProjectionEqBound(b) => b.into_where_clauses(self_ty),
294296
}
295297
}
296298
}
297299

300+
impl QuantifiedInlineBound {
301+
crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<QuantifiedWhereClause> {
302+
let self_ty = self_ty.up_shift(self.binders.len());
303+
self.value.into_where_clauses(self_ty).into_iter().map(|wc| {
304+
Binders {
305+
binders: self.binders.clone(),
306+
value: wc,
307+
}
308+
}).collect()
309+
}
310+
}
311+
312+
298313
/// Represents a trait bound on e.g. a type or type parameter.
299314
/// Does not know anything about what it's binding.
300315
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -304,7 +319,7 @@ pub struct TraitBound {
304319
}
305320

306321
impl TraitBound {
307-
crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
322+
fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
308323
let trait_ref = self.as_trait_ref(self_ty);
309324
vec![WhereClause::Implemented(trait_ref)]
310325
}
@@ -317,7 +332,6 @@ impl TraitBound {
317332
}
318333
}
319334
}
320-
321335
/// Represents a projection equality bound on e.g. a type or type parameter.
322336
/// Does not know anything about what it's binding.
323337
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -330,7 +344,7 @@ pub struct ProjectionEqBound {
330344
}
331345

332346
impl ProjectionEqBound {
333-
crate fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
347+
fn into_where_clauses(&self, self_ty: Ty) -> Vec<WhereClause> {
334348
let trait_ref = self.trait_bound.as_trait_ref(self_ty);
335349

336350
let mut parameters = self.parameters.clone();
@@ -368,7 +382,7 @@ pub struct AssociatedTyDatum {
368382
///
369383
/// These must be proven by the implementer, for all possible parameters that
370384
/// would result in a well-formed projection.
371-
crate bounds: Vec<InlineBound>,
385+
crate bounds: Vec<QuantifiedInlineBound>,
372386

373387
/// Where clauses that must hold for the projection to be well-formed.
374388
crate where_clauses: Vec<QuantifiedWhereClause>,
@@ -380,7 +394,7 @@ impl AssociatedTyDatum {
380394
/// ```notrust
381395
/// Implemented(<?0 as Foo>::Item<?1>: Sized)
382396
/// ```
383-
crate fn bounds_on_self(&self) -> Vec<WhereClause> {
397+
crate fn bounds_on_self(&self) -> Vec<QuantifiedWhereClause> {
384398
let parameters = self.parameter_kinds
385399
.anonymize()
386400
.iter()

src/ir/lowering.rs

+21-13
Original file line numberDiff line numberDiff line change
@@ -415,17 +415,11 @@ impl LowerWhereClauses for Impl {
415415
}
416416
}
417417

418-
trait LowerWhereClauseVec<T> {
419-
fn lower(&self, env: &Env) -> Result<Vec<T>>;
418+
trait LowerWhereClauseVec {
419+
fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedWhereClause>>;
420420
}
421421

422-
impl LowerWhereClauseVec<ir::WhereClause> for [WhereClause] {
423-
fn lower(&self, env: &Env) -> Result<Vec<ir::WhereClause>> {
424-
self.iter().flat_map(|wc| wc.lower(env).apply_result()).collect()
425-
}
426-
}
427-
428-
impl LowerWhereClauseVec<ir::QuantifiedWhereClause> for [QuantifiedWhereClause] {
422+
impl LowerWhereClauseVec for [QuantifiedWhereClause] {
429423
fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedWhereClause>> {
430424
self.iter()
431425
.flat_map(|wc| match wc.lower(env) {
@@ -724,12 +718,26 @@ impl LowerInlineBound for InlineBound {
724718
}
725719
}
726720

727-
trait LowerInlineBounds {
728-
fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>>;
721+
trait LowerQuantifiedInlineBound {
722+
fn lower(&self, env: &Env) -> Result<ir::QuantifiedInlineBound>;
723+
}
724+
725+
impl LowerQuantifiedInlineBound for QuantifiedInlineBound {
726+
fn lower(&self, env: &Env) -> Result<ir::QuantifiedInlineBound> {
727+
let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower());
728+
let binders = env.in_binders(parameter_kinds, |env| {
729+
Ok(self.bound.lower(env)?)
730+
})?;
731+
Ok(binders)
732+
}
733+
}
734+
735+
trait LowerQuantifiedInlineBoundVec {
736+
fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedInlineBound>>;
729737
}
730738

731-
impl LowerInlineBounds for Vec<InlineBound> {
732-
fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>> {
739+
impl LowerQuantifiedInlineBoundVec for [QuantifiedInlineBound] {
740+
fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedInlineBound>> {
733741
self.iter()
734742
.map(|b| b.lower(env))
735743
.collect()

src/ir/lowering/test.rs

+28
Original file line numberDiff line numberDiff line change
@@ -355,6 +355,21 @@ fn gat_parse() {
355355
}
356356
}
357357

358+
#[test]
359+
fn gat_higher_ranked_bound() {
360+
lowering_success! {
361+
program {
362+
trait Fn<T> {}
363+
trait Ref<'a, T> {}
364+
trait Sized {}
365+
366+
trait Foo {
367+
type Item<T>: forall<'a> Fn<Ref<'a, T>> + Sized;
368+
}
369+
}
370+
}
371+
}
372+
358373
#[test]
359374
fn duplicate_parameters() {
360375
lowering_error! {
@@ -389,6 +404,19 @@ fn duplicate_parameters() {
389404
"duplicate or shadowed parameters"
390405
}
391406
}
407+
408+
lowering_error! {
409+
program {
410+
trait Fn<T> {}
411+
trait Ref<'a, T> {}
412+
413+
trait Foo<'a> {
414+
type Item<T>: forall<'a> Fn<Ref<'a, T>>;
415+
}
416+
} error_msg {
417+
"duplicate or shadowed parameters"
418+
}
419+
}
392420
}
393421

394422
#[test]

src/rules.rs

+5-3
Original file line numberDiff line numberDiff line change
@@ -717,12 +717,14 @@ impl AssociatedTyDatum {
717717
// FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
718718
// }
719719
clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
720+
// Same as above in case of higher-ranked inline bounds.
721+
let shift = bound.binders.len();
720722
Binders {
721-
binders: binders.clone(),
723+
binders: bound.binders.iter().chain(binders.iter()).cloned().collect(),
722724
value: ProgramClauseImplication {
723-
consequence: bound.into_from_env_goal(),
725+
consequence: bound.value.clone().into_from_env_goal(),
724726
conditions: vec![
725-
FromEnv::Trait(trait_ref.clone()).cast()
727+
FromEnv::Trait(trait_ref.clone()).up_shift(shift).cast()
726728
],
727729
}
728730
}.cast()

src/rules/wf.rs

+5-3
Original file line numberDiff line numberDiff line change
@@ -216,7 +216,8 @@ impl WfSolver {
216216

217217
let wf_goals =
218218
input_types.into_iter()
219-
.map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)));
219+
.map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)))
220+
.casted();
220221

221222
let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len());
222223

@@ -233,9 +234,10 @@ impl WfSolver {
233234
bounds.iter()
234235
.map(|b| Subst::apply(&all_parameters, b))
235236
.flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone()))
236-
.map(|g| g.into_well_formed_goal());
237+
.map(|wc| wc.map(|bound| bound.into_well_formed_goal()))
238+
.casted();
237239

238-
let goals = wf_goals.chain(bound_goals).casted();
240+
let goals = wf_goals.chain(bound_goals);
239241
let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) {
240242
Some(goal) => goal,
241243
None => return None,

src/rules/wf/test.rs

+44
Original file line numberDiff line numberDiff line change
@@ -519,3 +519,47 @@ fn higher_ranked_cyclic_requirements() {
519519
}
520520
}
521521
}
522+
523+
#[test]
524+
fn higher_ranked_inline_bound_on_gat() {
525+
lowering_success! {
526+
program {
527+
trait Fn<T> { }
528+
struct Ref<'a, T> { }
529+
struct i32 {}
530+
531+
struct fn<T> { }
532+
533+
impl<'a, T> Fn<Ref<'a, T>> for for<'b> fn<Ref<'b, T>> { }
534+
535+
trait Bar {
536+
type Item<T>: forall<'a> Fn<Ref<'a, T>>;
537+
}
538+
539+
impl Bar for i32 {
540+
type Item<T> = for<'a> fn<Ref<'a, T>>;
541+
}
542+
}
543+
}
544+
545+
lowering_error! {
546+
program {
547+
trait Fn<T, U> { }
548+
struct i32 {}
549+
550+
struct fn<T, U> { }
551+
552+
impl<T, U> Fn<T, U> for fn<T, U> { }
553+
554+
trait Bar {
555+
type Item<T>: forall<U> Fn<T, U>;
556+
}
557+
558+
impl Bar for i32 {
559+
type Item<T> = fn<T, i32>;
560+
}
561+
} error_msg {
562+
"trait impl for \"Bar\" does not meet well-formedness requirements"
563+
}
564+
}
565+
}

src/solve/test.rs

+24
Original file line numberDiff line numberDiff line change
@@ -798,6 +798,30 @@ fn gat_implied_bounds() {
798798
"No possible solution"
799799
}
800800
}
801+
802+
test! {
803+
program {
804+
trait Fn<T> { }
805+
struct Ref<'a, T> { }
806+
trait Sized { }
807+
808+
trait Foo {
809+
type Item<T>: forall<'a> Fn<Ref<'a, T>> + Sized;
810+
}
811+
}
812+
813+
goal {
814+
forall<Type> {
815+
if (Type: Foo) {
816+
forall<'a, T> {
817+
<Type as Foo>::Item<T>: Fn<Ref<'a, T>>
818+
}
819+
}
820+
}
821+
} yields {
822+
"Unique"
823+
}
824+
}
801825
}
802826

803827
#[test]

0 commit comments

Comments
 (0)