From f4742809abc501a934610bbb0cad1488400bceca Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 14 Jan 2020 20:45:28 +0100 Subject: [PATCH 01/42] Make AliasTy an enum of Projection, ImplTrait and TypeAlias --- chalk-integration/src/lowering.rs | 4 +- chalk-integration/src/program.rs | 17 +++- chalk-ir/src/debug.rs | 37 +++++++++ chalk-ir/src/interner.rs | 22 +++++- chalk-ir/src/lib.rs | 23 ++++-- chalk-ir/src/macros.rs | 2 +- chalk-ir/src/tls.rs | 10 ++- chalk-ir/src/zip.rs | 9 ++- chalk-rust-ir/src/lib.rs | 12 +-- chalk-solve/src/clauses.rs | 90 +++++++++++++--------- chalk-solve/src/clauses/env_elaborator.rs | 9 +-- chalk-solve/src/clauses/program_clauses.rs | 17 ++-- chalk-solve/src/solve/slg.rs | 19 +++-- chalk-solve/src/solve/slg/aggregate.rs | 27 ++++--- chalk-solve/src/split.rs | 23 +++--- chalk-solve/src/wf.rs | 10 ++- 16 files changed, 225 insertions(+), 106 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 1d79771e975..f8001746d01 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -960,10 +960,10 @@ impl LowerAliasTy for AliasTy { args.extend(trait_substitution.iter(interner).cloned()); - Ok(chalk_ir::AliasTy { + Ok(chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { associated_ty_id: lookup.id, substitution: chalk_ir::Substitution::from(interner, args), - }) + })) } } diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 711ecee83e4..2d8bd4b6d02 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr; use chalk_ir::tls; use chalk_ir::{ debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime, - Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution, - TraitId, Ty, TypeName, + Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, StructId, + Substitution, TraitId, Ty, TypeName, }; use chalk_rust_ir::{ AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum, @@ -114,7 +114,18 @@ impl tls::DebugContext for Program { alias_ty: &AliasTy, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { - let (associated_ty_data, trait_params, other_params) = self.split_projection(alias_ty); + match alias_ty { + AliasTy::Projection(proj) => self.debug_projection_ty(proj, fmt), + _ => todo!(), + } + } + + fn debug_projection_ty( + &self, + projection_ty: &ProjectionTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error> { + let (associated_ty_data, trait_params, other_params) = self.split_projection(projection_ty); write!( fmt, "<{:?} as {:?}{:?}>::{}{:?}", diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index de7cf4ba83b..b7d805d39cd 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -96,6 +96,14 @@ impl Debug for QuantifiedWhereClauses { } } +impl Debug for ProjectionTy { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { + I::debug_projection_ty(self, fmt).unwrap_or_else(|| { + unimplemented!("cannot format ProjectionTy without setting Program in tls") + }) + } +} + impl Display for Substitution { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { I::debug_substitution(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned)) @@ -428,6 +436,35 @@ impl<'me, I: Interner> SeparatorTraitRef<'me, I> { } } +pub struct ProjectionTyDebug<'a, I: Interner> { + projection_ty: &'a ProjectionTy, + interner: &'a I, +} + +impl<'a, I: Interner> Debug for ProjectionTyDebug<'a, I> { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { + let ProjectionTyDebug { + projection_ty, + interner, + } = self; + write!( + fmt, + "({:?}){:?}", + projection_ty.associated_ty_id, + projection_ty.substitution.with_angle(interner) + ) + } +} + +impl ProjectionTy { + pub fn debug<'a>(&'a self, interner: &'a I) -> ProjectionTyDebug<'a, I> { + ProjectionTyDebug { + projection_ty: self, + interner, + } + } +} + pub struct Angle<'a, T>(pub &'a [T]); impl<'a, T: Debug> Debug for Angle<'a, T> { diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs index 305f6991f66..549bc43d075 100644 --- a/chalk-ir/src/interner.rs +++ b/chalk-ir/src/interner.rs @@ -12,6 +12,7 @@ use crate::ProgramClause; use crate::ProgramClauseData; use crate::ProgramClauseImplication; use crate::ProgramClauses; +use crate::ProjectionTy; use crate::QuantifiedWhereClause; use crate::QuantifiedWhereClauses; use crate::SeparatorTraitRef; @@ -115,7 +116,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { /// converted back to its underlying data via `program_clause_data`. type InternedProgramClause: Debug + Clone + Eq + Hash; - /// "Interned" representation of a list of quantified where clauses. + /// "Interned" representation of a list of quantified where clauses. /// In normal user code, `Self::InternedQuantifiedWhereClauses` is not referenced. /// Instead, we refer to `QuantifiedWhereClauses`, which wraps this type. /// @@ -182,6 +183,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } + /// Prints the debug representation of a ProjectionTy. To get good + /// results, this requires inspecting TLS, and is difficult to + /// code without reference to a specific interner (and hence + /// fully known types). + /// + /// Returns `None` to fallback to the default debug output (e.g., + /// if no info about current program is available from TLS). + fn debug_projection_ty( + projection_ty: &ProjectionTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Option; + /// Prints the debug representation of an type. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific interner (and hence @@ -542,6 +555,13 @@ mod default { tls::with_current_program(|prog| Some(prog?.debug_alias(alias, fmt))) } + fn debug_projection_ty( + proj: &ProjectionTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Option { + tls::with_current_program(|prog| Some(prog?.debug_projection_ty(proj, fmt))) + } + fn debug_ty(ty: &Ty, fmt: &mut fmt::Formatter<'_>) -> Option { tls::with_current_program(|prog| Some(prog?.debug_ty(ty, fmt))) } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 0823f8d177e..ad325a0aae9 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -838,7 +838,14 @@ impl ParameterData { } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] -pub struct AliasTy { +pub enum AliasTy { + Projection(ProjectionTy), + ImplTrait(()), + TypeAlias(()), +} + +#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] +pub struct ProjectionTy { pub associated_ty_id: AssocTypeId, pub substitution: Substitution, } @@ -849,11 +856,15 @@ impl AliasTy { } pub fn self_type_parameter(&self, interner: &I) -> Ty { - self.substitution - .iter(interner) - .find_map(move |p| p.ty(interner)) - .unwrap() - .clone() + match self { + AliasTy::Projection(projection_ty) => projection_ty + .substitution + .iter(interner) + .find_map(move |p| p.ty(interner)) + .unwrap() + .clone(), + _ => todo!(), + } } } diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index 1d34e4eec81..3c31150a2d4 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -24,7 +24,7 @@ macro_rules! ty { }; (alias (item $n:tt) $($arg:tt)*) => { - $crate::TyData::Alias(AliasTy { + chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { associated_ty_id: AssocTypeId(chalk_ir::interner::RawId { index: $n }), substitution: $crate::Substitution::from(&chalk_ir::interner::ChalkIr, vec![$(arg!($arg)),*] as Vec<$crate::Parameter<_>>), }).intern(&chalk_ir::interner::ChalkIr) diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs index 7344e8b8261..4a915a5a808 100644 --- a/chalk-ir/src/tls.rs +++ b/chalk-ir/src/tls.rs @@ -1,8 +1,8 @@ use crate::interner::ChalkIr; use crate::{ debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime, - Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, QuantifiedWhereClauses, - StructId, Substitution, TraitId, Ty, + Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, + QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, }; use std::cell::RefCell; use std::fmt; @@ -37,6 +37,12 @@ pub trait DebugContext { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; + fn debug_projection_ty( + &self, + proj: &ProjectionTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error>; + fn debug_ty(&self, ty: &Ty, fmt: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error>; fn debug_lifetime( diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 956d0b0a0a0..1124f0c205d 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -234,10 +234,6 @@ struct_zip!(impl[ }); struct_zip!(impl[I: Interner] Zip for ApplicationTy { name, substitution }); struct_zip!(impl[I: Interner] Zip for DynTy { bounds }); -struct_zip!(impl[I: Interner] Zip for AliasTy { - associated_ty_id, - substitution, -}); struct_zip!(impl[I: Interner] Zip for Normalize { alias, ty }); struct_zip!(impl[I: Interner] Zip for AliasEq { alias, ty }); struct_zip!(impl[I: Interner] Zip for EqGoal { a, b }); @@ -246,6 +242,10 @@ struct_zip!(impl[I: Interner] Zip for ProgramClauseImplication { conditions, priority, }); +struct_zip!(impl[I: Interner] Zip for ProjectionTy { + associated_ty_id, + substitution +}); impl Zip for Environment { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> @@ -339,6 +339,7 @@ enum_zip!(impl for DomainGoal { DownstreamType }); enum_zip!(impl for ProgramClauseData { Implies, ForAll }); +enum_zip!(impl for AliasTy { Projection, ImplTrait, TypeAlias }); impl Zip for Substitution { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index ee4e30268c9..1b498f49a8f 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -10,8 +10,8 @@ use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, - Parameter, ParameterKind, QuantifiedWhereClause, StructId, Substitution, TraitId, TraitRef, Ty, - TyData, TypeName, WhereClause, + Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, TraitId, + TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -307,10 +307,10 @@ impl AliasEqBound { vec![ WhereClause::Implemented(trait_ref), WhereClause::AliasEq(AliasEq { - alias: AliasTy { + alias: AliasTy::Projection(ProjectionTy { associated_ty_id: self.associated_ty_id, substitution, - }, + }), ty: self.value.clone(), }), ] @@ -433,10 +433,10 @@ impl AssociatedTyDatum { ); // The self type will be `>::Item` etc - let self_ty = TyData::Alias(AliasTy { + let self_ty = TyData::Alias(AliasTy::Projection(ProjectionTy { associated_ty_id: self.id, substitution, - }) + })) .intern(interner); // Now use that as the self type for the bounds, transforming diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index d1b13b86596..d5afdb85b5d 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -268,10 +268,12 @@ fn program_clauses_that_could_match( ); } } - DomainGoal::Holds(WhereClause::AliasEq(alias_predicate)) => { - db.associated_ty_data(alias_predicate.alias.associated_ty_id) - .to_program_clauses(builder); - } + DomainGoal::Holds(WhereClause::AliasEq(alias_predicate)) => match &alias_predicate.alias { + AliasTy::Projection(proj) => db + .associated_ty_data(proj.associated_ty_id) + .to_program_clauses(builder), + _ => todo!(), + }, DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { db.trait_datum(trait_predicate.trait_id) .to_program_clauses(builder); @@ -283,39 +285,42 @@ fn program_clauses_that_could_match( match_ty(builder, environment, ty)? } DomainGoal::FromEnv(_) => (), // Computed in the environment - DomainGoal::Normalize(Normalize { alias, ty: _ }) => { - // Normalize goals derive from `AssociatedTyValue` datums, - // which are found in impls. That is, if we are - // normalizing (e.g.) `::Item>`, then - // search for impls of iterator and, within those impls, - // for associated type values: - // - // ```ignore - // impl Iterator for Foo { - // type Item = Bar; // <-- associated type value - // } - // ``` - let associated_ty_datum = db.associated_ty_data(alias.associated_ty_id); - let trait_id = associated_ty_datum.trait_id; - let trait_parameters = db.trait_parameters_from_projection(alias); - - let trait_datum = db.trait_datum(trait_id); + DomainGoal::Normalize(Normalize { alias, ty: _ }) => match alias { + AliasTy::Projection(proj) => { + // Normalize goals derive from `AssociatedTyValue` datums, + // which are found in impls. That is, if we are + // normalizing (e.g.) `::Item>`, then + // search for impls of iterator and, within those impls, + // for associated type values: + // + // ```ignore + // impl Iterator for Foo { + // type Item = Bar; // <-- associated type value + // } + // ``` + let associated_ty_datum = db.associated_ty_data(proj.associated_ty_id); + let trait_id = associated_ty_datum.trait_id; + let trait_parameters = db.trait_parameters_from_projection(proj); + + let trait_datum = db.trait_datum(trait_id); + + // Flounder if the self-type is unknown and the trait is non-enumerable. + // + // e.g., Normalize(::Item = u32) + if (alias.self_type_parameter(interner).is_var(interner)) + && trait_datum.is_non_enumerable_trait() + { + return Err(Floundered); + } - // Flounder if the self-type is unknown and the trait is non-enumerable. - // - // e.g., Normalize(::Item = u32) - if (alias.self_type_parameter(interner).is_var(interner)) - && trait_datum.is_non_enumerable_trait() - { - return Err(Floundered); + push_program_clauses_for_associated_type_values_in_impls_of( + builder, + trait_id, + trait_parameters, + ); } - - push_program_clauses_for_associated_type_values_in_impls_of( - builder, - trait_id, - trait_parameters, - ); - } + _ => todo!(), + }, DomainGoal::LocalImplAllowed(trait_ref) => db .trait_datum(trait_ref.trait_id) .to_program_clauses(builder), @@ -390,10 +395,11 @@ fn match_ty( TyData::Placeholder(_) => { builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone()))); } - TyData::Alias(alias_ty) => builder + TyData::Alias(AliasTy::Projection(proj)) => builder .db - .associated_ty_data(alias_ty.associated_ty_id) + .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), + TyData::Alias(_) => todo!(), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); quantified_ty @@ -419,6 +425,16 @@ fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeNa } } +fn match_alias_ty(builder: &mut ClauseBuilder<'_, I>, alias: &AliasTy) { + match alias { + AliasTy::Projection(projection_ty) => builder + .db + .associated_ty_data(projection_ty.associated_ty_id) + .to_program_clauses(builder), + _ => (), + } +} + fn match_struct(builder: &mut ClauseBuilder<'_, I>, struct_id: StructId) { builder .db diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs index e6cf1cb6bf7..f0885ad6610 100644 --- a/chalk-solve/src/clauses/env_elaborator.rs +++ b/chalk-solve/src/clauses/env_elaborator.rs @@ -1,6 +1,6 @@ use super::program_clauses::ToProgramClauses; use crate::clauses::builder::ClauseBuilder; -use crate::clauses::match_type_name; +use crate::clauses::{match_alias_ty, match_type_name}; use crate::DomainGoal; use crate::FromEnv; use crate::ProgramClause; @@ -63,14 +63,9 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> { TyData::Apply(application_ty) => { match_type_name(&mut self.builder, application_ty.name) } + TyData::Alias(alias_ty) => match_alias_ty(&mut self.builder, alias_ty), TyData::Placeholder(_) => {} - TyData::Alias(alias_ty) => { - self.db - .associated_ty_data(alias_ty.associated_ty_id) - .to_program_clauses(&mut self.builder); - } - // FIXME(#203) -- We haven't fully figured out the implied // bounds story around `dyn Trait` types. TyData::Dyn(_) => (), diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index b76c2da2d8c..61771144d1e 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -109,7 +109,7 @@ impl ToProgramClauses for AssociatedTyValue { // ``` builder.push_clause( Normalize { - alias: projection.clone(), + alias: AliasTy::Projection(projection.clone()), ty: assoc_ty_value.ty, }, impl_where_clauses.chain(assoc_ty_where_clauses), @@ -584,14 +584,14 @@ impl ToProgramClauses for AssociatedTyDatum { builder.push_binders(&binders, |builder, (where_clauses, bounds)| { let substitution = builder.substitution_in_scope(); - let alias = AliasTy { + let projection = ProjectionTy { associated_ty_id: self.id, substitution: substitution.clone(), }; - let projection_ty = alias.clone().intern(interner); + let projection_ty = AliasTy::Projection(projection.clone()).intern(interner); // Retrieve the trait ref embedding the associated type - let trait_ref = builder.db.trait_ref_from_projection(&alias); + let trait_ref = builder.db.trait_ref_from_projection(&projection); // Construct an application from the projection. So if we have `::Item`, // we would produce `(Iterator::Item)`. @@ -602,7 +602,7 @@ impl ToProgramClauses for AssociatedTyDatum { .intern(interner); let alias_eq = AliasEq { - alias: alias.clone(), + alias: AliasTy::Projection(projection.clone()), ty: app_ty.clone(), }; @@ -675,12 +675,15 @@ impl ToProgramClauses for AssociatedTyDatum { builder.push_bound_ty(|builder, ty| { // `Normalize(::Assoc -> U)` let normalize = Normalize { - alias: alias.clone(), + alias: AliasTy::Projection(projection.clone()), ty: ty.clone(), }; // `AliasEq(::Assoc = U)` - let alias_eq = AliasEq { alias, ty }; + let alias_eq = AliasEq { + alias: AliasTy::Projection(projection), + ty, + }; // Projection equality rule from above. // diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index c23eea490e3..aea1849e105 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -508,9 +508,12 @@ impl MayInvalidate<'_, I> { self.aggregate_placeholder_tys(p1, p2) } - (TyData::Alias(alias1), TyData::Alias(alias2)) => { - self.aggregate_alias_tys(alias1, alias2) - } + ( + TyData::Alias(AliasTy::Projection(proj1)), + TyData::Alias(AliasTy::Projection(proj2)), + ) => self.aggregate_projection_tys(proj1, proj2), + + (TyData::Alias(_), TyData::Alias(_)) => todo!(), // For everything else, be conservative here and just say we may invalidate. (TyData::Function(_), _) @@ -555,12 +558,16 @@ impl MayInvalidate<'_, I> { new != current } - fn aggregate_alias_tys(&mut self, new: &AliasTy, current: &AliasTy) -> bool { - let AliasTy { + fn aggregate_projection_tys( + &mut self, + new: &ProjectionTy, + current: &ProjectionTy, + ) -> bool { + let ProjectionTy { associated_ty_id: new_name, substitution: new_substitution, } = new; - let AliasTy { + let ProjectionTy { associated_ty_id: current_name, substitution: current_substitution, } = current; diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs index bdd4068adcb..f860f48ebfa 100644 --- a/chalk-solve/src/solve/slg/aggregate.rs +++ b/chalk-solve/src/solve/slg/aggregate.rs @@ -239,9 +239,12 @@ impl AntiUnifier<'_, '_, I> { self.aggregate_application_tys(apply1, apply2) } - (TyData::Alias(alias1), TyData::Alias(alias2)) => { - self.aggregate_alias_tys(alias1, alias2) - } + ( + TyData::Alias(AliasTy::Projection(proj1)), + TyData::Alias(AliasTy::Projection(proj2)), + ) => self.aggregate_projection_tys(proj1, proj2), + + (TyData::Alias(_), TyData::Alias(_)) => todo!(), (TyData::Placeholder(placeholder1), TyData::Placeholder(placeholder2)) => { self.aggregate_placeholder_tys(placeholder1, placeholder2) @@ -293,23 +296,27 @@ impl AntiUnifier<'_, '_, I> { } } - fn aggregate_alias_tys(&mut self, alias1: &AliasTy, alias2: &AliasTy) -> Ty { + fn aggregate_projection_tys( + &mut self, + proj1: &ProjectionTy, + proj2: &ProjectionTy, + ) -> Ty { let interner = self.interner; - let AliasTy { + let ProjectionTy { associated_ty_id: name1, substitution: substitution1, - } = alias1; - let AliasTy { + } = proj1; + let ProjectionTy { associated_ty_id: name2, substitution: substitution2, - } = alias2; + } = proj2; self.aggregate_name_and_substs(name1, substitution1, name2, substitution2) .map(|(&associated_ty_id, substitution)| { - TyData::Alias(AliasTy { + TyData::Alias(AliasTy::Projection(ProjectionTy { associated_ty_id, substitution, - }) + })) .intern(interner) }) .unwrap_or_else(|| self.new_variable()) diff --git a/chalk-solve/src/split.rs b/chalk-solve/src/split.rs index 93d946475cf..0c01afa4343 100644 --- a/chalk-solve/src/split.rs +++ b/chalk-solve/src/split.rs @@ -15,17 +15,17 @@ pub trait Split: RustIrDatabase { /// any type parameters itself. fn split_projection<'p>( &self, - alias: &'p AliasTy, + projection: &'p ProjectionTy, ) -> ( Arc>, &'p [Parameter], &'p [Parameter], ) { let interner = self.interner(); - let AliasTy { + let ProjectionTy { associated_ty_id, ref substitution, - } = *alias; + } = *projection; let parameters = substitution.parameters(interner); let associated_ty_data = &self.associated_ty_data(associated_ty_id); let trait_datum = &self.trait_datum(associated_ty_data.trait_id); @@ -38,15 +38,18 @@ pub trait Split: RustIrDatabase { /// Given a projection `>::Item`, /// returns the trait parameters `[P0..Pn]` (see /// `split_projection`). - fn trait_parameters_from_projection<'p>(&self, alias: &'p AliasTy) -> &'p [Parameter] { - let (_, trait_params, _) = self.split_projection(alias); + fn trait_parameters_from_projection<'p>( + &self, + projection: &'p ProjectionTy, + ) -> &'p [Parameter] { + let (_, trait_params, _) = self.split_projection(projection); trait_params } /// Given a projection `>::Item`, /// returns the trait parameters `[P0..Pn]` (see /// `split_projection`). - fn trait_ref_from_projection<'p>(&self, projection: &'p AliasTy) -> TraitRef { + fn trait_ref_from_projection<'p>(&self, projection: &'p ProjectionTy) -> TraitRef { let interner = self.interner(); let (associated_ty_data, trait_params, _) = self.split_projection(&projection); TraitRef { @@ -120,7 +123,7 @@ pub trait Split: RustIrDatabase { &self, parameters: &'p [Parameter], associated_ty_value: &AssociatedTyValue, - ) -> (&'p [Parameter], AliasTy) { + ) -> (&'p [Parameter], ProjectionTy) { let interner = self.interner(); debug_heading!( "impl_parameters_and_projection_from_associated_ty_value(parameters={:?})", @@ -150,16 +153,16 @@ pub trait Split: RustIrDatabase { .cloned(), ); - let alias = AliasTy { + let projection = ProjectionTy { associated_ty_id: associated_ty_value.associated_ty_id, substitution: projection_substitution, }; debug!("impl_parameters: {:?}", impl_parameters); debug!("trait_ref: {:?}", trait_ref); - debug!("alias: {:?}", alias); + debug!("projection: {:?}", projection); - (impl_parameters, alias) + (impl_parameters, projection) } } diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index f735d69fee6..8a6aabdb771 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -105,11 +105,13 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { clauses.visit_with(self, outer_binder); } - TyData::Alias(alias) => { + TyData::Alias(AliasTy::Projection(proj)) => { push_ty(); - alias.visit_with(self, outer_binder); + proj.visit_with(self, outer_binder); } + TyData::Alias(_) => todo!(), + TyData::Placeholder(_) => { push_ty(); } @@ -490,7 +492,7 @@ impl WfWellKnownGoals { /// Computes a goal to prove Sized constraints on a struct definition. /// Struct is considered well-formed (in terms of Sized) when it either - /// has no fields or all of it's fields except the last are proven to be Sized. + /// has no fields or all of it's fields except the last are proven to be Sized. pub fn struct_sized_constraint( db: &dyn RustIrDatabase, fields: &[Ty], @@ -581,7 +583,7 @@ impl WfWellKnownGoals { /// c) Any bounds on the genereic parameters of the impl must be /// deductible from the bounds imposed by the struct definition /// (i.e. the implementation must be exactly as generic as the ADT definition). - /// + /// /// ```rust,ignore /// struct S { } /// struct Foo { } From 27180eee4a6d4a7fa2822acb47aafcc9904a46e4 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Jan 2020 20:25:09 +0100 Subject: [PATCH 02/42] Parse impl trait --- chalk-parse/src/ast.rs | 6 ++++++ chalk-parse/src/parser.lalrpop | 9 +++++++++ 2 files changed, 15 insertions(+) diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index cf6b348b322..b64f7cd7d00 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -77,6 +77,12 @@ pub struct AssocTyDefn { pub where_clauses: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct ImplTraitDefn { + pub ty: Ty, + pub bounds: Vec, +} + #[derive(Copy, Clone, PartialEq, Eq, Debug)] pub enum ParameterKind { Ty(Identifier), diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 7a6b523c00d..33c009a7e04 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -98,6 +98,15 @@ AssocTyDefn: AssocTyDefn = { } }; +ImplTraitDefn: ImplTraitDefn = { + "type" "=" "impl" > => { + ImplTraitDefn { + ty, + bounds: b, + } + } +} + InlineBound: InlineBound = { TraitBound => InlineBound::TraitBound(<>), AliasEqBound => InlineBound::AliasEqBound(<>), From 34b8e97cad39e94c734b8cee48b8c14e315fd6b7 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Jan 2020 21:36:33 +0100 Subject: [PATCH 03/42] Rename AliasEq back to ProjectionEq --- chalk-integration/src/lowering.rs | 35 +++++++++++++++------- chalk-ir/src/cast.rs | 4 +-- chalk-ir/src/debug.rs | 6 ++-- chalk-ir/src/lib.rs | 17 ++++++----- chalk-ir/src/zip.rs | 4 +-- chalk-parse/src/ast.rs | 14 ++++++--- chalk-parse/src/parser.lalrpop | 17 ++++++----- chalk-rust-ir/src/lib.rs | 12 ++++---- chalk-solve/src/clauses.rs | 13 ++++---- chalk-solve/src/clauses/program_clauses.rs | 31 +++++++++---------- chalk-solve/src/coinductive_goal.rs | 2 +- chalk-solve/src/infer/unify.rs | 18 +++++++---- chalk-solve/src/wf.rs | 4 +-- tests/lowering/mod.rs | 2 +- 14 files changed, 101 insertions(+), 78 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index f8001746d01..3a9bb8052a0 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -582,7 +582,7 @@ trait LowerWhereClause { /// Lower from an AST `where` clause to an internal IR. /// Some AST `where` clauses can lower to multiple ones, this is why we return a `Vec`. /// As for now, this is the only the case for `where T: Foo` which lowers to - /// `Implemented(T: Foo)` and `AliasEq(::Item = U)`. + /// `Implemented(T: Foo)` and `ProjectionEq(::Item = U)`. fn lower(&self, env: &Env) -> LowerResult>; } @@ -592,12 +592,12 @@ impl LowerWhereClause> for WhereClause { WhereClause::Implemented { trait_ref } => { vec![chalk_ir::WhereClause::Implemented(trait_ref.lower(env)?)] } - WhereClause::AliasEq { alias, ty } => vec![ - chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq { - alias: alias.lower(env)?, + WhereClause::ProjectionEq { projection, ty } => vec![ + chalk_ir::WhereClause::ProjectionEq(chalk_ir::ProjectionEq { + projection: projection.lower(env)?, ty: ty.lower(env)?, }), - chalk_ir::WhereClause::Implemented(alias.trait_ref.lower(env)?), + chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?), ], }; Ok(where_clauses) @@ -921,7 +921,19 @@ trait LowerAliasTy { impl LowerAliasTy for AliasTy { fn lower(&self, env: &Env) -> LowerResult> { - let AliasTy { + match self { + AliasTy::Projection(proj) => Ok(chalk_ir::AliasTy::Projection(proj.lower(env)?)), + } + } +} + +trait LowerProjectionTy { + fn lower(&self, env: &Env) -> LowerResult>; +} + +impl LowerProjectionTy for ProjectionTy { + fn lower(&self, env: &Env) -> LowerResult> { + let ProjectionTy { ref trait_ref, ref name, ref args, @@ -960,10 +972,10 @@ impl LowerAliasTy for AliasTy { args.extend(trait_substitution.iter(interner).cloned()); - Ok(chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { + Ok(chalk_ir::ProjectionTy { associated_ty_id: lookup.id, substitution: chalk_ir::Substitution::from(interner, args), - })) + }) } } @@ -1055,9 +1067,10 @@ impl LowerTy for Ty { .intern(interner)) } - Ty::Alias { ref alias } => { - Ok(chalk_ir::TyData::Alias(alias.lower(env)?).intern(interner)) - } + Ty::Projection { ref proj } => Ok(chalk_ir::TyData::Alias( + chalk_ir::AliasTy::Projection(proj.lower(env)?), + ) + .intern(interner)), Ty::ForAll { ref lifetime_names, diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs index 052ead6b6e2..86aca1042b9 100644 --- a/chalk-ir/src/cast.rs +++ b/chalk-ir/src/cast.rs @@ -89,9 +89,9 @@ impl CastTo> for TraitRef { } } -impl CastTo> for AliasEq { +impl CastTo> for ProjectionEq { fn cast_to(self, _interner: &I) -> WhereClause { - WhereClause::AliasEq(self) + WhereClause::ProjectionEq(self) } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index b7d805d39cd..66f24a2a26f 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -490,9 +490,9 @@ impl Debug for Normalize { } } -impl Debug for AliasEq { +impl Debug for ProjectionEq { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - write!(fmt, "AliasEq({:?} = {:?})", self.alias, self.ty) + write!(fmt, "ProjectionEq({:?} = {:?})", self.projection, self.ty) } } @@ -500,7 +500,7 @@ impl Debug for WhereClause { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { match self { WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()), - WhereClause::AliasEq(a) => write!(fmt, "{:?}", a), + WhereClause::ProjectionEq(p) => write!(fmt, "{:?}", p), } } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index ad325a0aae9..8b429f9647a 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -899,7 +899,7 @@ impl TraitRef { #[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner)] pub enum WhereClause { Implemented(TraitRef), - AliasEq(AliasEq), + ProjectionEq(ProjectionEq), } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] @@ -1032,7 +1032,7 @@ pub type QuantifiedWhereClause = Binders>; impl WhereClause { /// Turn a where clause into the WF version of it i.e.: /// * `Implemented(T: Trait)` maps to `WellFormed(T: Trait)` - /// * `AliasEq(::Item = Foo)` maps to `WellFormed(::Item = Foo)` + /// * `ProjectionEq(::Item = Foo)` maps to `WellFormed(::Item = Foo)` /// * any other clause maps to itself pub fn into_well_formed_goal(self, interner: &I) -> DomainGoal { match self { @@ -1136,9 +1136,10 @@ impl DomainGoal { pub fn inputs(&self, interner: &I) -> Vec> { match self { - DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { - vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern(interner)] - } + DomainGoal::Holds(WhereClause::ProjectionEq(proj_eq)) => vec![ParameterKind::Ty( + AliasTy::Projection(proj_eq.projection.clone()).intern(interner), + ) + .intern(interner)], _ => Vec::new(), } } @@ -1164,12 +1165,12 @@ pub struct Normalize { /// `U`. Equality can be proven via normalization, but we can also /// prove that `T::Foo = V::Foo` if `T = V` without normalizing. #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)] -pub struct AliasEq { - pub alias: AliasTy, +pub struct ProjectionEq { + pub projection: ProjectionTy, pub ty: Ty, } -impl HasInterner for AliasEq { +impl HasInterner for ProjectionEq { type Interner = I; } diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 1124f0c205d..0c104b6bfe0 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -235,7 +235,7 @@ struct_zip!(impl[ struct_zip!(impl[I: Interner] Zip for ApplicationTy { name, substitution }); struct_zip!(impl[I: Interner] Zip for DynTy { bounds }); struct_zip!(impl[I: Interner] Zip for Normalize { alias, ty }); -struct_zip!(impl[I: Interner] Zip for AliasEq { alias, ty }); +struct_zip!(impl[I: Interner] Zip for ProjectionEq { projection, ty }); struct_zip!(impl[I: Interner] Zip for EqGoal { a, b }); struct_zip!(impl[I: Interner] Zip for ProgramClauseImplication { consequence, @@ -325,7 +325,7 @@ macro_rules! enum_zip { enum_zip!(impl for WellFormed { Trait, Ty }); enum_zip!(impl for FromEnv { Trait, Ty }); -enum_zip!(impl for WhereClause { Implemented, AliasEq }); +enum_zip!(impl for WhereClause { Implemented, ProjectionEq }); enum_zip!(impl for DomainGoal { Holds, WellFormed, diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index b64f7cd7d00..a7561d4fe40 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -177,8 +177,8 @@ pub enum Ty { name: Identifier, args: Vec, }, - Alias { - alias: AliasTy, + Projection { + proj: ProjectionTy, }, ForAll { lifetime_names: Vec, @@ -192,7 +192,13 @@ pub enum Lifetime { } #[derive(Clone, PartialEq, Eq, Debug)] -pub struct AliasTy { +pub enum AliasTy { + Projection(ProjectionTy), + // TODO ImplTrait +} + +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct ProjectionTy { pub trait_ref: TraitRef, pub name: Identifier, pub args: Vec, @@ -238,7 +244,7 @@ impl fmt::Display for Identifier { #[derive(Clone, PartialEq, Eq, Debug)] pub enum WhereClause { Implemented { trait_ref: TraitRef }, - AliasEq { alias: AliasTy, ty: Ty }, + ProjectionEq { projection: ProjectionTy, ty: Ty }, } #[derive(Clone, PartialEq, Eq, Debug)] diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 33c009a7e04..6849ea5fffc 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -199,7 +199,7 @@ TyWithoutFor: Ty = { bounds: b, }, "<" > ">" => Ty::Apply { name: n, args: a }, - => Ty::Alias { alias: a }, + => Ty::Projection { proj: p }, "(" ")", }; @@ -212,8 +212,8 @@ Parameter: Parameter = { Lifetime => Parameter::Lifetime(<>), }; -AliasTy: AliasTy = { - "<" > ">" "::" > => AliasTy { +ProjectionTy: ProjectionTy = { + "<" > ">" "::" > => ProjectionTy { trait_ref: t, name: n, args: a }, }; @@ -270,15 +270,15 @@ InlineClause: Clause = { WhereClause: WhereClause = { > => WhereClause::Implemented { trait_ref: t }, - // `T: Foo` -- alias equality + // `T: Foo` -- projection equality ":" "<" > ",")?> > "=" ">" => { let mut args = vec![Parameter::Ty(s)]; if let Some(a) = a { args.extend(a); } let trait_ref = TraitRef { trait_name: t, args: args }; - let alias = AliasTy { trait_ref, name, args: a2 }; - WhereClause::AliasEq { alias, ty } + let projection = ProjectionTy { trait_ref, name, args: a2 }; + WhereClause::ProjectionEq { projection, ty } }, }; @@ -311,7 +311,10 @@ DomainGoal: DomainGoal = { "FromEnv" "(" > ")" => DomainGoal::TraitRefFromEnv { trait_ref: t }, // `::U -> Bar` -- a normalization - "Normalize" "(" "->" ")" => DomainGoal::Normalize { alias: a, ty: t }, + "Normalize" "(" "->" ")" => DomainGoal::Normalize { + alias: AliasTy::Projection(p), + ty: t, + }, "IsLocal" "(" ")" => DomainGoal::IsLocal { ty }, "IsUpstream" "(" ")" => DomainGoal::IsUpstream { ty }, diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index 1b498f49a8f..0b401413bc7 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -9,9 +9,9 @@ use chalk_ir::cast::Cast; use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ - AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, - Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, TraitId, - TraitRef, Ty, TyData, TypeName, WhereClause, + AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, Parameter, + ParameterKind, ProjectionEq, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, + TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -306,11 +306,11 @@ impl AliasEqBound { vec![ WhereClause::Implemented(trait_ref), - WhereClause::AliasEq(AliasEq { - alias: AliasTy::Projection(ProjectionTy { + WhereClause::ProjectionEq(ProjectionEq { + projection: ProjectionTy { associated_ty_id: self.associated_ty_id, substitution, - }), + }, ty: self.value.clone(), }), ] diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index d5afdb85b5d..42daf02926a 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -197,7 +197,7 @@ fn program_clauses_that_could_match( // ``` // dyn(exists { // forall<'a> { Implemented(T: Fn<'a>) }, - // forall<'a> { AliasEq(>::Output, ()) }, + // forall<'a> { ProjectionEq(>::Output, ()) }, // }) // ``` // @@ -212,7 +212,7 @@ fn program_clauses_that_could_match( // and // // ``` - // forall<'a> { AliasEq(>::Output, ()) }, + // forall<'a> { ProjectionEq(>::Output, ()) }, // ``` // // FIXME. This is presently rather wasteful, in that we @@ -268,12 +268,9 @@ fn program_clauses_that_could_match( ); } } - DomainGoal::Holds(WhereClause::AliasEq(alias_predicate)) => match &alias_predicate.alias { - AliasTy::Projection(proj) => db - .associated_ty_data(proj.associated_ty_id) - .to_program_clauses(builder), - _ => todo!(), - }, + DomainGoal::Holds(WhereClause::ProjectionEq(projection_predicate)) => db + .associated_ty_data(projection_predicate.projection.associated_ty_id) + .to_program_clauses(builder), DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { db.trait_datum(trait_predicate.trait_id) .to_program_clauses(builder); diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 61771144d1e..5fef1cfd2ea 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -525,18 +525,18 @@ impl ToProgramClauses for AssociatedTyDatum { /// we generate the 'fallback' rule: /// /// ```notrust - /// -- Rule AliasEq-Placeholder + /// -- Rule ProjectionEq-Placeholder /// forall { - /// AliasEq(::Assoc<'a, T> = (Foo::Assoc<'a, T>)). + /// ProjectionEq(::Assoc<'a, T> = (Foo::Assoc<'a, T>)). /// } /// ``` /// /// and /// /// ```notrust - /// -- Rule AliasEq-Normalize + /// -- Rule ProjectionEq-Normalize /// forall { - /// AliasEq(::Assoc<'a, T> = U) :- + /// ProjectionEq(::Assoc<'a, T> = U) :- /// Normalize(::Assoc -> U). /// } /// ``` @@ -545,14 +545,14 @@ impl ToProgramClauses for AssociatedTyDatum { /// /// ```notrust /// forall { - /// T: Foo :- exists { AliasEq(::Assoc = U) }. + /// T: Foo :- exists { ProjectionEq(::Assoc = U) }. /// } /// ``` /// /// but this caused problems with the recursive solver. In /// particular, whenever normalization is possible, we cannot /// solve that projection uniquely, since we can now elaborate - /// `AliasEq` to fallback *or* normalize it. So instead we + /// `ProjectionEq` to fallback *or* normalize it. So instead we /// handle this kind of reasoning through the `FromEnv` predicate. /// /// We also generate rules specific to WF requirements and implied bounds: @@ -601,8 +601,8 @@ impl ToProgramClauses for AssociatedTyDatum { } .intern(interner); - let alias_eq = AliasEq { - alias: AliasTy::Projection(projection.clone()), + let projection_eq = ProjectionEq { + projection: projection.clone(), ty: app_ty.clone(), }; @@ -610,9 +610,9 @@ impl ToProgramClauses for AssociatedTyDatum { // and placeholder type. // // forall { - // AliasEq(::Assoc = (Foo::Assoc)). + // ProjectionEq(::Assoc = (Foo::Assoc)). // } - builder.push_fact_with_priority(alias_eq, ClausePriority::Low); + builder.push_fact_with_priority(projection_eq, ClausePriority::Low); // Well-formedness of projection type. // @@ -679,19 +679,16 @@ impl ToProgramClauses for AssociatedTyDatum { ty: ty.clone(), }; - // `AliasEq(::Assoc = U)` - let alias_eq = AliasEq { - alias: AliasTy::Projection(projection), - ty, - }; + // `ProjectionEq(::Assoc = U)` + let projection_eq = ProjectionEq { projection, ty }; // Projection equality rule from above. // // forall { - // AliasEq(::Assoc = U) :- + // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U). // } - builder.push_clause(alias_eq, Some(normalize)); + builder.push_clause(projection_eq, Some(normalize)); }); }); } diff --git a/chalk-solve/src/coinductive_goal.rs b/chalk-solve/src/coinductive_goal.rs index 45bda7b9656..102ff3f655e 100644 --- a/chalk-solve/src/coinductive_goal.rs +++ b/chalk-solve/src/coinductive_goal.rs @@ -23,7 +23,7 @@ impl IsCoinductive for Goal { db.trait_datum(tr.trait_id).is_auto_trait() || db.trait_datum(tr.trait_id).is_coinductive_trait() } - WhereClause::AliasEq(..) => false, + WhereClause::ProjectionEq(..) => false, }, GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true, GoalData::Quantified(QuantifierKind::ForAll, goal) => { diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 2bf1f00600e..693a1c72907 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -170,14 +170,20 @@ impl<'t, I: Interner> Unifier<'t, I> { | (&TyData::Placeholder(_), &TyData::Alias(ref alias)) | (&TyData::Function(_), &TyData::Alias(ref alias)) | (&TyData::InferenceVar(_), &TyData::Alias(ref alias)) - | (&TyData::Dyn(_), &TyData::Alias(ref alias)) => self.unify_alias_ty(alias, a), + | (&TyData::Dyn(_), &TyData::Alias(ref alias)) => match alias { + AliasTy::Projection(ref proj) => self.unify_projection_ty(proj, a), + _ => todo!(), + }, (&TyData::Alias(ref alias), &TyData::Alias(_)) | (&TyData::Alias(ref alias), &TyData::Apply(_)) | (&TyData::Alias(ref alias), &TyData::Placeholder(_)) | (&TyData::Alias(ref alias), &TyData::Function(_)) | (&TyData::Alias(ref alias), &TyData::InferenceVar(_)) - | (&TyData::Alias(ref alias), &TyData::Dyn(_)) => self.unify_alias_ty(alias, b), + | (&TyData::Alias(ref alias), &TyData::Dyn(_)) => match alias { + AliasTy::Projection(ref proj) => self.unify_projection_ty(proj, b), + _ => todo!(), + }, (TyData::BoundVar(_), _) | (_, TyData::BoundVar(_)) => panic!( "unification encountered bound variable: a={:?} b={:?}", @@ -222,14 +228,14 @@ impl<'t, I: Interner> Unifier<'t, I> { /// type `ty` (which might also be a projection). Creates a goal like /// /// ```notrust - /// AliasEq(::Item = U) + /// ProjectionEq(::Item = U) /// ``` - fn unify_alias_ty(&mut self, alias: &AliasTy, ty: &Ty) -> Fallible<()> { + fn unify_projection_ty(&mut self, proj: &ProjectionTy, ty: &Ty) -> Fallible<()> { let interner = self.interner; Ok(self.goals.push(InEnvironment::new( self.environment, - AliasEq { - alias: alias.clone(), + ProjectionEq { + projection: proj.clone(), ty: ty.clone(), } .cast(interner), diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 8a6aabdb771..2852e045acd 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -75,8 +75,8 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { fn visit_where_clause(&mut self, where_clause: &WhereClause, outer_binder: DebruijnIndex) { match where_clause { - WhereClause::AliasEq(alias_eq) => { - TyData::Alias(alias_eq.alias.clone()) + WhereClause::ProjectionEq(alias_eq) => { + TyData::Alias(AliasTy::Projection(alias_eq.projection.clone())) .intern(self.interner) .visit_with(self, outer_binder); alias_eq.ty.visit_with(self, outer_binder); diff --git a/tests/lowering/mod.rs b/tests/lowering/mod.rs index cac5bf492d1..700bc1209de 100644 --- a/tests/lowering/mod.rs +++ b/tests/lowering/mod.rs @@ -215,7 +215,7 @@ fn atc_accounting() { "ForAll { \ ForAll { \ ForAll { \ - all(AliasEq(<^2.0 as Iterable>::Iter<'^1.0> = ^0.0), \ + all(ProjectionEq(<^2.0 as Iterable>::Iter<'^1.0> = ^0.0), \ Implemented(^2.0: Iterable)) \ } \ } \ From b5ae61c2f1172be855ccc3e3f045c2eb4affcde4 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Jan 2020 21:46:19 +0100 Subject: [PATCH 04/42] Remove TypeAlias from enum for now --- chalk-ir/src/lib.rs | 1 - chalk-ir/src/zip.rs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 8b429f9647a..ecf49f3accf 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -841,7 +841,6 @@ impl ParameterData { pub enum AliasTy { Projection(ProjectionTy), ImplTrait(()), - TypeAlias(()), } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 0c104b6bfe0..69444f5e5db 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -339,7 +339,7 @@ enum_zip!(impl for DomainGoal { DownstreamType }); enum_zip!(impl for ProgramClauseData { Implies, ForAll }); -enum_zip!(impl for AliasTy { Projection, ImplTrait, TypeAlias }); +enum_zip!(impl for AliasTy { Projection, ImplTrait }); impl Zip for Substitution { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> From 5465e59b6d4d4cd113fe93755e844956450f8a50 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Jan 2020 22:31:32 +0100 Subject: [PATCH 05/42] Allow impl trait items in ast --- chalk-integration/src/lowering.rs | 2 ++ chalk-parse/src/ast.rs | 3 ++- chalk-parse/src/parser.lalrpop | 7 ++++--- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 3a9bb8052a0..7f21359e9f9 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -239,6 +239,7 @@ impl LowerProgram for Program { trait_ids.insert(type_kind.name, id); trait_kinds.insert(id, type_kind); } + Item::ImplTrait(_impl_trait) => todo!(), Item::Impl(_) => continue, Item::Clause(_) => continue, }; @@ -361,6 +362,7 @@ impl LowerProgram for Program { Item::Clause(ref clause) => { custom_clauses.extend(clause.lower_clause(&empty_env)?); } + Item::ImplTrait(_) => todo!(), } } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index a7561d4fe40..cf88921d3f5 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -24,6 +24,7 @@ pub enum Item { TraitDefn(TraitDefn), Impl(Impl), Clause(Clause), + ImplTrait(ImplTrait), } #[derive(Clone, PartialEq, Eq, Debug)] @@ -78,7 +79,7 @@ pub struct AssocTyDefn { } #[derive(Clone, PartialEq, Eq, Debug)] -pub struct ImplTraitDefn { +pub struct ImplTrait { pub ty: Ty, pub bounds: Vec, } diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 6849ea5fffc..0bdf0cd76b5 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -15,6 +15,7 @@ Item: Option = { Comment => None, StructDefn => Some(Item::StructDefn(<>)), TraitDefn => Some(Item::TraitDefn(<>)), + ImplTrait => Some(Item::ImplTrait(<>)), Impl => Some(Item::Impl(<>)), Clause => Some(Item::Clause(<>)), }; @@ -98,9 +99,9 @@ AssocTyDefn: AssocTyDefn = { } }; -ImplTraitDefn: ImplTraitDefn = { - "type" "=" "impl" > => { - ImplTraitDefn { +ImplTrait: ImplTrait = { + "type" "=" "impl" > ";" => { + ImplTrait { ty, bounds: b, } From c3459fb9c882d1f536e96022d8e8854f467c5e71 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 20 Jan 2020 17:37:37 +0100 Subject: [PATCH 06/42] Revert adding AliasTy to ast --- chalk-integration/src/lowering.rs | 12 ++---------- chalk-parse/src/ast.rs | 8 +------- chalk-parse/src/parser.lalrpop | 5 +---- 3 files changed, 4 insertions(+), 21 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 7f21359e9f9..457d734ad5f 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -626,9 +626,9 @@ impl LowerDomainGoal for DomainGoal { .into_iter() .casted(interner) .collect(), - DomainGoal::Normalize { alias, ty } => { + DomainGoal::Normalize { projection, ty } => { vec![chalk_ir::DomainGoal::Normalize(chalk_ir::Normalize { - alias: alias.lower(env)?, + alias: chalk_ir::AliasTy::Projection(projection.lower(env)?), ty: ty.lower(env)?, })] } @@ -921,14 +921,6 @@ trait LowerAliasTy { fn lower(&self, env: &Env) -> LowerResult>; } -impl LowerAliasTy for AliasTy { - fn lower(&self, env: &Env) -> LowerResult> { - match self { - AliasTy::Projection(proj) => Ok(chalk_ir::AliasTy::Projection(proj.lower(env)?)), - } - } -} - trait LowerProjectionTy { fn lower(&self, env: &Env) -> LowerResult>; } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index cf88921d3f5..cad97b0e79f 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -192,12 +192,6 @@ pub enum Lifetime { Id { name: Identifier }, } -#[derive(Clone, PartialEq, Eq, Debug)] -pub enum AliasTy { - Projection(ProjectionTy), - // TODO ImplTrait -} - #[derive(Clone, PartialEq, Eq, Debug)] pub struct ProjectionTy { pub trait_ref: TraitRef, @@ -251,7 +245,7 @@ pub enum WhereClause { #[derive(Clone, PartialEq, Eq, Debug)] pub enum DomainGoal { Holds { where_clause: WhereClause }, - Normalize { alias: AliasTy, ty: Ty }, + Normalize { projection: ProjectionTy, ty: Ty }, TraitRefWellFormed { trait_ref: TraitRef }, TyWellFormed { ty: Ty }, TyFromEnv { ty: Ty }, diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 0bdf0cd76b5..981fbb56f97 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -312,10 +312,7 @@ DomainGoal: DomainGoal = { "FromEnv" "(" > ")" => DomainGoal::TraitRefFromEnv { trait_ref: t }, // `::U -> Bar` -- a normalization - "Normalize" "(" "->" ")" => DomainGoal::Normalize { - alias: AliasTy::Projection(p), - ty: t, - }, + "Normalize" "(" "->" ")" => DomainGoal::Normalize { projection: s, ty: t }, "IsLocal" "(" ")" => DomainGoal::IsLocal { ty }, "IsUpstream" "(" ")" => DomainGoal::IsUpstream { ty }, From a4d9b99b302c957d6e833254358e20dd1dfc53ec Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 20 Jan 2020 19:43:57 +0100 Subject: [PATCH 07/42] Add ImplTraitId --- chalk-integration/src/lowering.rs | 4 ++-- chalk-ir/src/debug.rs | 13 +++++++++++++ chalk-ir/src/fold/boring_impls.rs | 1 + chalk-ir/src/lib.rs | 25 ++++++++++++++++++------- chalk-ir/src/visit/boring_impls.rs | 9 +++++---- chalk-ir/src/zip.rs | 4 ++++ chalk-solve/src/clauses.rs | 3 ++- 7 files changed, 45 insertions(+), 14 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 457d734ad5f..c7473d39d37 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -239,7 +239,7 @@ impl LowerProgram for Program { trait_ids.insert(type_kind.name, id); trait_kinds.insert(id, type_kind); } - Item::ImplTrait(_impl_trait) => todo!(), + Item::ImplTrait(_impl_trait) => continue, Item::Impl(_) => continue, Item::Clause(_) => continue, }; @@ -362,7 +362,7 @@ impl LowerProgram for Program { Item::Clause(ref clause) => { custom_clauses.extend(clause.lower_clause(&empty_env)?); } - Item::ImplTrait(_) => todo!(), + Item::ImplTrait(ref _impl_trait) => todo!(), } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 66f24a2a26f..aa2b73941a2 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -110,6 +110,12 @@ impl Display for Substitution { } } +impl Debug for ImplTraitId { + fn fmt(&self, _fmt: &mut Formatter<'_>) -> Result<(), Error> { + todo!() + } +} + impl Display for UniverseIndex { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { write!(fmt, "U{}", self.counter) @@ -127,6 +133,7 @@ impl Debug for TypeName { match self { TypeName::Struct(id) => write!(fmt, "{:?}", id), TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty), + TypeName::ImplTrait(impl_trait) => write!(fmt, "{:?}", impl_trait), TypeName::Error => write!(fmt, "{{error}}"), } } @@ -465,6 +472,12 @@ impl ProjectionTy { } } +impl Debug for ImplTraitTy { + fn fmt(&self, _fmt: &mut Formatter<'_>) -> Result<(), Error> { + todo!() + } +} + pub struct Angle<'a, T>(pub &'a [T]); impl<'a, T: Debug> Debug for Angle<'a, T> { diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs index becd861befd..13dc18917fe 100644 --- a/chalk-ir/src/fold/boring_impls.rs +++ b/chalk-ir/src/fold/boring_impls.rs @@ -271,6 +271,7 @@ id_fold!(ImplId); id_fold!(StructId); id_fold!(TraitId); id_fold!(AssocTypeId); +id_fold!(ImplTraitId); impl> SuperFold for ProgramClauseData { fn super_fold_with<'i>( diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index ecf49f3accf..8bf9ee37a19 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -114,6 +114,9 @@ pub enum TypeName { /// an associated type like `Iterator::Item`; see `AssociatedType` for details AssociatedType(AssocTypeId), + /// a placeholder for some type like `impl Trait` + ImplTrait(ImplTraitId), + /// This can be used to represent an error, e.g. during name resolution of a type. /// Chalk itself will not produce this, just pass it through when given. Error, @@ -176,6 +179,9 @@ pub struct ClauseId(pub I::DefId); #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct AssocTypeId(pub I::DefId); +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct ImplTraitId(pub I::DefId); + impl_debugs!(ImplId, ClauseId); #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] @@ -840,13 +846,7 @@ impl ParameterData { #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub enum AliasTy { Projection(ProjectionTy), - ImplTrait(()), -} - -#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] -pub struct ProjectionTy { - pub associated_ty_id: AssocTypeId, - pub substitution: Substitution, + ImplTrait(ImplTraitTy), } impl AliasTy { @@ -867,6 +867,17 @@ impl AliasTy { } } +#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] +pub struct ProjectionTy { + pub associated_ty_id: AssocTypeId, + pub substitution: Substitution, +} + +#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] +pub struct ImplTraitTy { + pub impl_trait_id: ImplTraitId, +} + #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub struct TraitRef { pub trait_id: TraitId, diff --git a/chalk-ir/src/visit/boring_impls.rs b/chalk-ir/src/visit/boring_impls.rs index a78bd6c3785..463f793e6f2 100644 --- a/chalk-ir/src/visit/boring_impls.rs +++ b/chalk-ir/src/visit/boring_impls.rs @@ -5,10 +5,10 @@ //! The more interesting impls of `Visit` remain in the `visit` module. use crate::{ - AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, Interner, Parameter, ParameterKind, - PlaceholderIndex, ProgramClause, ProgramClauseData, ProgramClauses, QuantifiedWhereClauses, - QuantifierKind, StructId, Substitution, SuperVisit, TraitId, UniverseIndex, Visit, VisitResult, - Visitor, + AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, ImplTraitId, Interner, Parameter, + ParameterKind, PlaceholderIndex, ProgramClause, ProgramClauseData, ProgramClauses, + QuantifiedWhereClauses, QuantifierKind, StructId, Substitution, SuperVisit, TraitId, + UniverseIndex, Visit, VisitResult, Visitor, }; use chalk_engine::{context::Context, ExClause, FlounderedSubgoal, Literal}; use std::{marker::PhantomData, sync::Arc}; @@ -230,6 +230,7 @@ id_visit!(ImplId); id_visit!(StructId); id_visit!(TraitId); id_visit!(AssocTypeId); +id_visit!(ImplTraitId); impl SuperVisit for ProgramClause { fn super_visit_with<'i, R: VisitResult>( diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 69444f5e5db..9713f3e93cb 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -196,6 +196,7 @@ macro_rules! eq_zip { eq_zip!(I => StructId); eq_zip!(I => TraitId); eq_zip!(I => AssocTypeId); +eq_zip!(I => ImplTraitId); eq_zip!(I => TypeName); eq_zip!(I => QuantifierKind); eq_zip!(I => PhantomData); @@ -246,6 +247,9 @@ struct_zip!(impl[I: Interner] Zip for ProjectionTy { associated_ty_id, substitution }); +struct_zip!(impl[I: Interner] Zip for ImplTraitTy { + impl_trait_id +}); impl Zip for Environment { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 42daf02926a..7c83fece039 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -396,7 +396,7 @@ fn match_ty( .db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - TyData::Alias(_) => todo!(), + TyData::Alias(AliasTy::ImplTrait(_impl_trait)) => todo!(), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); quantified_ty @@ -414,6 +414,7 @@ fn match_ty( fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeName) { match name { TypeName::Struct(struct_id) => match_struct(builder, struct_id), + TypeName::ImplTrait(_impl_trait) => todo!(), TypeName::Error => {} TypeName::AssociatedType(type_id) => builder .db From d446354fcf2711d25382a1a5fa5d0964e573e957 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 20 Jan 2020 20:30:49 +0100 Subject: [PATCH 08/42] Implement lowering for impl trait --- chalk-integration/src/lowering.rs | 31 +++++++++++++++++++++++++----- chalk-integration/src/program.rs | 16 ++++++++++----- chalk-ir/src/visit/boring_impls.rs | 2 +- chalk-parse/src/ast.rs | 2 +- chalk-parse/src/parser.lalrpop | 4 ++-- chalk-rust-ir/src/lib.rs | 10 ++++++++++ 6 files changed, 51 insertions(+), 14 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index c7473d39d37..494ef948954 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1,12 +1,14 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::ChalkIr; use chalk_ir::{ - self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, QuantifiedWhereClauses, - StructId, Substitution, TraitId, + self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, ImplTraitId, + QuantifiedWhereClauses, StructId, Substitution, TraitId, }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; -use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, ToParameter}; +use chalk_rust_ir::{ + Anonymize, AssociatedTyValueId, ImplTraitValue, IntoWhereClauses, ToParameter, +}; use lalrpop_intern::intern; use std::collections::BTreeMap; use std::sync::Arc; @@ -225,6 +227,7 @@ impl LowerProgram for Program { let mut trait_ids = BTreeMap::new(); let mut struct_kinds = BTreeMap::new(); let mut trait_kinds = BTreeMap::new(); + let mut impl_trait_ids = BTreeMap::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { match item { Item::StructDefn(defn) => { @@ -239,7 +242,9 @@ impl LowerProgram for Program { trait_ids.insert(type_kind.name, id); trait_kinds.insert(id, type_kind); } - Item::ImplTrait(_impl_trait) => continue, + Item::ImplTrait(impl_trait) => { + impl_trait_ids.insert(impl_trait.identifier.str, ImplTraitId(raw_id)); + } Item::Impl(_) => continue, Item::Clause(_) => continue, }; @@ -251,6 +256,7 @@ impl LowerProgram for Program { let mut impl_data = BTreeMap::new(); let mut associated_ty_data = BTreeMap::new(); let mut associated_ty_values = BTreeMap::new(); + let mut impl_trait_values = BTreeMap::new(); let mut custom_clauses = Vec::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { let empty_env = Env { @@ -362,7 +368,20 @@ impl LowerProgram for Program { Item::Clause(ref clause) => { custom_clauses.extend(clause.lower_clause(&empty_env)?); } - Item::ImplTrait(ref _impl_trait) => todo!(), + Item::ImplTrait(ref impl_trait) => { + if let Some(value) = impl_trait_ids.get(&impl_trait.identifier.str) { + impl_trait_values.insert( + *value, + Arc::new(ImplTraitValue { + bounds: impl_trait + .bounds + .iter() + .map(|b| b.lower(&empty_env)) + .collect::, _>>()?, + }), + ); + } + } } } @@ -377,6 +396,8 @@ impl LowerProgram for Program { impl_data, associated_ty_values, associated_ty_data, + impl_trait_ids, + impl_trait_values, custom_clauses, }; diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 2d8bd4b6d02..b58e173443f 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -4,13 +4,13 @@ use chalk_ir::debug::Angle; use chalk_ir::interner::ChalkIr; use chalk_ir::tls; use chalk_ir::{ - debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime, - Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, StructId, - Substitution, TraitId, Ty, TypeName, + debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, + ImplTraitId, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, + ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, }; use chalk_rust_ir::{ - AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum, - TraitDatum, WellKnownTrait, + AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplTraitValue, ImplType, + StructDatum, TraitDatum, WellKnownTrait, }; use chalk_solve::split::Split; use chalk_solve::RustIrDatabase; @@ -42,6 +42,12 @@ pub struct Program { pub associated_ty_values: BTreeMap, Arc>>, + // From `impl Trait` name to item-id. Used during lowering only. + pub impl_trait_ids: BTreeMap>, + + /// For each `impl Trait` type: + pub impl_trait_values: BTreeMap, Arc>>, + /// For each trait: pub trait_data: BTreeMap, Arc>>, diff --git a/chalk-ir/src/visit/boring_impls.rs b/chalk-ir/src/visit/boring_impls.rs index 463f793e6f2..8e9d36d8d7e 100644 --- a/chalk-ir/src/visit/boring_impls.rs +++ b/chalk-ir/src/visit/boring_impls.rs @@ -229,8 +229,8 @@ macro_rules! id_visit { id_visit!(ImplId); id_visit!(StructId); id_visit!(TraitId); -id_visit!(AssocTypeId); id_visit!(ImplTraitId); +id_visit!(AssocTypeId); impl SuperVisit for ProgramClause { fn super_visit_with<'i, R: VisitResult>( diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index cad97b0e79f..0d9facc1c46 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -80,7 +80,7 @@ pub struct AssocTyDefn { #[derive(Clone, PartialEq, Eq, Debug)] pub struct ImplTrait { - pub ty: Ty, + pub identifier: Identifier, pub bounds: Vec, } diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 981fbb56f97..b5e14cf32cd 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -100,9 +100,9 @@ AssocTyDefn: AssocTyDefn = { }; ImplTrait: ImplTrait = { - "type" "=" "impl" > ";" => { + "type" "=" "impl" > ";" => { ImplTrait { - ty, + identifier, bounds: b, } } diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index 0b401413bc7..44fedfbb414 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -506,6 +506,16 @@ pub struct AssociatedTyValueBound { pub ty: Ty, } +/// Represents the bounds for an `impl Trait` type. +/// +/// ```ignore +/// impl A + B + C +/// ``` +#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)] +pub struct ImplTraitValue { + pub bounds: Vec>, +} + #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] pub enum Polarity { Positive, From f2047b2332f7ca6e8920901729def2f7cb5a5848 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 21 Jan 2020 19:40:46 +0100 Subject: [PATCH 09/42] Create clauses from ImplTraitDatum --- chalk-integration/src/db.rs | 6 ++++++ chalk-integration/src/lowering.rs | 15 ++++++++------- chalk-integration/src/program.rs | 8 ++++++-- chalk-rust-ir/src/lib.rs | 13 +++++++------ chalk-solve/src/clauses.rs | 5 ++++- chalk-solve/src/clauses/program_clauses.rs | 20 ++++++++++++++++++++ chalk-solve/src/lib.rs | 3 +++ 7 files changed, 54 insertions(+), 16 deletions(-) diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs index 8ce55700f01..64b7c5e4a58 100644 --- a/chalk-integration/src/db.rs +++ b/chalk-integration/src/db.rs @@ -10,6 +10,7 @@ use chalk_ir::Canonical; use chalk_ir::ConstrainedSubst; use chalk_ir::Goal; use chalk_ir::ImplId; +use chalk_ir::ImplTraitId; use chalk_ir::InEnvironment; use chalk_ir::Parameter; use chalk_ir::ProgramClause; @@ -21,6 +22,7 @@ use chalk_rust_ir::AssociatedTyDatum; use chalk_rust_ir::AssociatedTyValue; use chalk_rust_ir::AssociatedTyValueId; use chalk_rust_ir::ImplDatum; +use chalk_rust_ir::ImplTraitDatum; use chalk_rust_ir::StructDatum; use chalk_rust_ir::TraitDatum; use chalk_rust_ir::WellKnownTrait; @@ -104,6 +106,10 @@ impl RustIrDatabase for ChalkDatabase { self.program_ir().unwrap().associated_ty_values[&id].clone() } + fn impl_trait_datum(&self, id: ImplTraitId) -> Arc> { + self.program_ir().unwrap().impl_trait_data[&id].clone() + } + fn struct_datum(&self, id: StructId) -> Arc> { self.program_ir().unwrap().struct_datum(id) } diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 494ef948954..4719265323f 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -7,7 +7,7 @@ use chalk_ir::{ use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; use chalk_rust_ir::{ - Anonymize, AssociatedTyValueId, ImplTraitValue, IntoWhereClauses, ToParameter, + Anonymize, AssociatedTyValueId, ImplTraitDatum, IntoWhereClauses, ToParameter, }; use lalrpop_intern::intern; use std::collections::BTreeMap; @@ -256,7 +256,7 @@ impl LowerProgram for Program { let mut impl_data = BTreeMap::new(); let mut associated_ty_data = BTreeMap::new(); let mut associated_ty_values = BTreeMap::new(); - let mut impl_trait_values = BTreeMap::new(); + let mut impl_trait_data = BTreeMap::new(); let mut custom_clauses = Vec::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { let empty_env = Env { @@ -369,10 +369,11 @@ impl LowerProgram for Program { custom_clauses.extend(clause.lower_clause(&empty_env)?); } Item::ImplTrait(ref impl_trait) => { - if let Some(value) = impl_trait_ids.get(&impl_trait.identifier.str) { - impl_trait_values.insert( - *value, - Arc::new(ImplTraitValue { + if let Some(&value) = impl_trait_ids.get(&impl_trait.identifier.str) { + impl_trait_data.insert( + value, + Arc::new(ImplTraitDatum { + impl_trait_id: value, bounds: impl_trait .bounds .iter() @@ -397,7 +398,7 @@ impl LowerProgram for Program { associated_ty_values, associated_ty_data, impl_trait_ids, - impl_trait_values, + impl_trait_data, custom_clauses, }; diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index b58e173443f..064991c284c 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -9,7 +9,7 @@ use chalk_ir::{ ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, }; use chalk_rust_ir::{ - AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplTraitValue, ImplType, + AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplTraitDatum, ImplType, StructDatum, TraitDatum, WellKnownTrait, }; use chalk_solve::split::Split; @@ -46,7 +46,7 @@ pub struct Program { pub impl_trait_ids: BTreeMap>, /// For each `impl Trait` type: - pub impl_trait_values: BTreeMap, Arc>>, + pub impl_trait_data: BTreeMap, Arc>>, /// For each trait: pub trait_data: BTreeMap, Arc>>, @@ -272,6 +272,10 @@ impl RustIrDatabase for Program { self.associated_ty_values[&id].clone() } + fn impl_trait_datum(&self, id: ImplTraitId) -> Arc> { + self.impl_trait_data[&id].clone() + } + fn struct_datum(&self, id: StructId) -> Arc> { self.struct_data[&id].clone() } diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index 44fedfbb414..aad198e7877 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -9,9 +9,9 @@ use chalk_ir::cast::Cast; use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ - AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, Parameter, - ParameterKind, ProjectionEq, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, - TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, + AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, ImplTraitId, LifetimeData, + Parameter, ParameterKind, ProjectionEq, ProjectionTy, QuantifiedWhereClause, StructId, + Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -509,10 +509,11 @@ pub struct AssociatedTyValueBound { /// Represents the bounds for an `impl Trait` type. /// /// ```ignore -/// impl A + B + C +/// type Foo = impl A + B + C; /// ``` -#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)] -pub struct ImplTraitValue { +#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold)] +pub struct ImplTraitDatum { + pub impl_trait_id: ImplTraitId, pub bounds: Vec>, } diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 7c83fece039..5f2b2c86ad1 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -396,7 +396,10 @@ fn match_ty( .db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - TyData::Alias(AliasTy::ImplTrait(_impl_trait)) => todo!(), + TyData::Alias(AliasTy::ImplTrait(impl_trait)) => builder + .db + .impl_trait_datum(impl_trait.impl_trait_id) + .to_program_clauses(builder), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); quantified_ty diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 5fef1cfd2ea..e9edc46a1ec 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -118,6 +118,26 @@ impl ToProgramClauses for AssociatedTyValue { } } +impl ToProgramClauses for ImplTraitDatum { + /// Given `type Foo = impl A + B;`, we generate: + /// + /// ```notrust + /// Implemented(Foo: A), + /// Implemented(Foo: B), + /// Implemented(Foo: Foo: Send) :- Implemented(A + B: Send). // For all auto traits + /// ``` + fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { + let interner = builder.interner(); + for bound in &self.bounds { + let alias_ty = AliasTy::ImplTrait(ImplTraitTy { + impl_trait_id: self.impl_trait_id, + }); + builder.push_fact(bound.as_trait_ref(interner, Ty::new(interner, alias_ty))); + } + todo!() // auto traits + } +} + impl ToProgramClauses for StructDatum { /// Given the following type definition: `struct Foo { }`, generate: /// diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index e5dc4a8d056..e0d02631b19 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -40,6 +40,9 @@ pub trait RustIrDatabase: Debug { /// Returns the `AssociatedTyValue` with the given id. fn associated_ty_value(&self, id: AssociatedTyValueId) -> Arc>; + /// Returns the `ImplTraitDatum` with the given id. + fn impl_trait_datum(&self, id: ImplTraitId) -> Arc>; + /// If `id` is a struct id, returns `Some(id)` (but cast to `StructId`). fn as_struct_id(&self, id: &TypeName) -> Option>; From b513e4aacc3e6662c66f5c77b06e215cc29b96b8 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 21 Jan 2020 20:44:40 +0100 Subject: [PATCH 10/42] Generate auto trait clauses for impl trait --- chalk-integration/src/db.rs | 4 +++ chalk-integration/src/program.rs | 8 +++++ chalk-solve/src/clauses/program_clauses.rs | 35 ++++++++++++++++++---- chalk-solve/src/lib.rs | 3 ++ 4 files changed, 44 insertions(+), 6 deletions(-) diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs index 64b7c5e4a58..b1d175eb959 100644 --- a/chalk-integration/src/db.rs +++ b/chalk-integration/src/db.rs @@ -153,4 +153,8 @@ impl RustIrDatabase for ChalkDatabase { fn interner(&self) -> &ChalkIr { &ChalkIr } + + fn auto_traits(&self) -> Vec> { + self.program_ir().unwrap().auto_traits() + } } diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 064991c284c..88bc3436fbc 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -341,4 +341,12 @@ impl RustIrDatabase for Program { fn interner(&self) -> &ChalkIr { &ChalkIr } + + fn auto_traits(&self) -> Vec> { + self.trait_data + .iter() + .filter(|(_, auto_trait)| auto_trait.is_auto_trait()) + .map(|(trait_id, _)| *trait_id) + .collect() + } } diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index e9edc46a1ec..2c16ce37484 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -124,17 +124,40 @@ impl ToProgramClauses for ImplTraitDatum { /// ```notrust /// Implemented(Foo: A), /// Implemented(Foo: B), - /// Implemented(Foo: Foo: Send) :- Implemented(A + B: Send). // For all auto traits + /// Implemented(Foo: Send) :- Implemented(A + B: Send). // For all auto traits /// ``` fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - for bound in &self.bounds { - let alias_ty = AliasTy::ImplTrait(ImplTraitTy { + let ty = Ty::new( + interner, + AliasTy::ImplTrait(ImplTraitTy { impl_trait_id: self.impl_trait_id, - }); - builder.push_fact(bound.as_trait_ref(interner, Ty::new(interner, alias_ty))); + }), + ); + + for bound in &self.bounds { + builder.push_fact(bound.as_trait_ref(interner, ty.clone())); + } + + for auto_trait_id in builder.db.auto_traits() { + builder.push_clause( + TraitRef { + trait_id: auto_trait_id, + substitution: Substitution::from1(interner, ty.clone()), + }, + iter::once(TraitRef { + trait_id: auto_trait_id, + substitution: Substitution::from( + interner, + iter::once(ty.clone().cast(interner)).chain( + self.bounds + .iter() + .flat_map(|b| b.args_no_self.iter().cloned()), + ), + ), + }), + ); } - todo!() // auto traits } } diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index e0d02631b19..d1dfbd64a8a 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -88,6 +88,9 @@ pub trait RustIrDatabase: Debug { fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> Option>; fn interner(&self) -> &I; + + /// Returns the ids of all auto traits. + fn auto_traits(&self) -> Vec>; } pub use solve::Guidance; From a3b01aca3ca462f45397e917f0cfbcaf10a1e9f8 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 21 Jan 2020 20:59:55 +0100 Subject: [PATCH 11/42] Remove ImplTrait indirection in AliasTy --- chalk-ir/src/lib.rs | 2 +- chalk-ir/src/zip.rs | 3 --- chalk-solve/src/clauses.rs | 4 ++-- chalk-solve/src/clauses/program_clauses.rs | 7 +------ 4 files changed, 4 insertions(+), 12 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 8bf9ee37a19..5120bb3c7be 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -846,7 +846,7 @@ impl ParameterData { #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub enum AliasTy { Projection(ProjectionTy), - ImplTrait(ImplTraitTy), + ImplTrait(ImplTraitId), } impl AliasTy { diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 9713f3e93cb..7cf2d8025ef 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -247,9 +247,6 @@ struct_zip!(impl[I: Interner] Zip for ProjectionTy { associated_ty_id, substitution }); -struct_zip!(impl[I: Interner] Zip for ImplTraitTy { - impl_trait_id -}); impl Zip for Environment { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 5f2b2c86ad1..7e9205257c3 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -396,9 +396,9 @@ fn match_ty( .db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - TyData::Alias(AliasTy::ImplTrait(impl_trait)) => builder + TyData::Alias(AliasTy::ImplTrait(impl_trait_id)) => builder .db - .impl_trait_datum(impl_trait.impl_trait_id) + .impl_trait_datum(*impl_trait_id) .to_program_clauses(builder), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 2c16ce37484..947f5d287b1 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -128,12 +128,7 @@ impl ToProgramClauses for ImplTraitDatum { /// ``` fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - let ty = Ty::new( - interner, - AliasTy::ImplTrait(ImplTraitTy { - impl_trait_id: self.impl_trait_id, - }), - ); + let ty = Ty::new(interner, AliasTy::ImplTrait(self.impl_trait_id)); for bound in &self.bounds { builder.push_fact(bound.as_trait_ref(interner, ty.clone())); From f337c0f256d15b2353ad23729b45b54a3b012c50 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 21 Jan 2020 21:09:57 +0100 Subject: [PATCH 12/42] Debug impls --- chalk-integration/src/program.rs | 33 ++++++++++++++++++++++++++++---- chalk-ir/src/debug.rs | 5 +++-- chalk-ir/src/interner.rs | 20 +++++++++++++++++++ chalk-ir/src/tls.rs | 10 ++++++++-- 4 files changed, 60 insertions(+), 8 deletions(-) diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 88bc3436fbc..5cbf5058c3d 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -106,8 +106,8 @@ impl tls::DebugContext for Program { assoc_type_id: AssocTypeId, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { - if let Some(k) = self.associated_ty_data.get(&assoc_type_id) { - write!(fmt, "({:?}::{})", k.trait_id, k.name) + if let Some(d) = self.associated_ty_data.get(&assoc_type_id) { + write!(fmt, "({:?}::{})", d.trait_id, d.name) } else { fmt.debug_struct("InvalidItemId") .field("index", &assoc_type_id.0) @@ -115,14 +115,39 @@ impl tls::DebugContext for Program { } } + fn debug_impl_trait_id( + &self, + impl_trait_id: ImplTraitId, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error> { + if let Some(d) = self.impl_trait_data.get(&impl_trait_id) { + write!(fmt, "type {:?} = impl {:?}", d.impl_trait_id, d.bounds) + } else { + fmt.debug_struct("InvalidItemId") + .field("index", &impl_trait_id.0) + .finish() + } + } + fn debug_alias( &self, alias_ty: &AliasTy, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { match alias_ty { - AliasTy::Projection(proj) => self.debug_projection_ty(proj, fmt), - _ => todo!(), + AliasTy::Projection(proj) => { + let (associated_ty_data, trait_params, other_params) = self.split_projection(proj); + write!( + fmt, + "<{:?} as {:?}{:?}>::{}{:?}", + &trait_params[0], + associated_ty_data.trait_id, + Angle(&trait_params[1..]), + associated_ty_data.name, + Angle(&other_params) + ) + } + AliasTy::ImplTrait(impl_trait_id) => write!(fmt, "impl {:?}", impl_trait_id), } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index aa2b73941a2..515de52c186 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -111,8 +111,9 @@ impl Display for Substitution { } impl Debug for ImplTraitId { - fn fmt(&self, _fmt: &mut Formatter<'_>) -> Result<(), Error> { - todo!() + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { + I::debug_impl_trait_id(*self, fmt) + .unwrap_or_else(|| write!(fmt, "ImplTraitId({:?})", self.0)) } } diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs index 549bc43d075..9f996e7fbc5 100644 --- a/chalk-ir/src/interner.rs +++ b/chalk-ir/src/interner.rs @@ -4,6 +4,7 @@ use crate::AssocTypeId; use crate::Goal; use crate::GoalData; use crate::Goals; +use crate::ImplTraitId; use crate::Lifetime; use crate::LifetimeData; use crate::Parameter; @@ -171,6 +172,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } + // Prints the debug representation of an `impl trait`. To get good + /// results, this requires inspecting TLS, and is difficult to + /// code without reference to a specific type-family (and hence + /// fully known types). + /// + /// Returns `None` to fallback to the default debug output (e.g., + /// if no info about current program is available from TLS). + fn debug_impl_trait_id( + impl_trait_id: ImplTraitId, + fmt: &mut fmt::Formatter<'_>, + ) -> Option; + /// Prints the debug representation of an alias. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific interner (and hence @@ -548,6 +561,13 @@ mod default { tls::with_current_program(|prog| Some(prog?.debug_assoc_type_id(id, fmt))) } + fn debug_impl_trait_id( + id: ImplTraitId, + fmt: &mut fmt::Formatter<'_>, + ) -> Option { + tls::with_current_program(|prog| Some(prog?.debug_impl_trait_id(id, fmt))) + } + fn debug_alias( alias: &AliasTy, fmt: &mut fmt::Formatter<'_>, diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs index 4a915a5a808..a7a2fbe2a78 100644 --- a/chalk-ir/src/tls.rs +++ b/chalk-ir/src/tls.rs @@ -1,7 +1,7 @@ use crate::interner::ChalkIr; use crate::{ - debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime, - Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, + debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplTraitId, + Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, }; use std::cell::RefCell; @@ -31,6 +31,12 @@ pub trait DebugContext { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; + fn debug_impl_trait_id( + &self, + id: ImplTraitId, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error>; + fn debug_alias( &self, alias: &AliasTy, From cccfac73e893b00836a169c8bbb9833867cf1661 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 21 Jan 2020 21:12:15 +0100 Subject: [PATCH 13/42] Remove unused trait --- chalk-integration/src/lowering.rs | 4 ---- chalk-ir/src/interner.rs | 2 +- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 4719265323f..41526950b38 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -939,10 +939,6 @@ impl LowerTraitFlags for TraitFlags { } } -trait LowerAliasTy { - fn lower(&self, env: &Env) -> LowerResult>; -} - trait LowerProjectionTy { fn lower(&self, env: &Env) -> LowerResult>; } diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs index 9f996e7fbc5..aeb07262e83 100644 --- a/chalk-ir/src/interner.rs +++ b/chalk-ir/src/interner.rs @@ -172,7 +172,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } - // Prints the debug representation of an `impl trait`. To get good + /// Prints the debug representation of an `impl trait`. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific type-family (and hence /// fully known types). From 85659017ec1b0e46abd6188f0bfe32eb30a53704 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 23 Jan 2020 21:37:50 +0100 Subject: [PATCH 14/42] Re-introduce ImplTraitTy to include substitution --- chalk-integration/src/program.rs | 27 +++++++--------- chalk-ir/src/debug.rs | 37 ++++++++++++++++++++-- chalk-ir/src/interner.rs | 20 ++++++++++++ chalk-ir/src/lib.rs | 3 +- chalk-ir/src/tls.rs | 10 ++++-- chalk-ir/src/zip.rs | 4 +++ chalk-solve/src/clauses.rs | 4 +-- chalk-solve/src/clauses/program_clauses.rs | 8 ++++- 8 files changed, 89 insertions(+), 24 deletions(-) diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 5cbf5058c3d..9401ffc393a 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr; use chalk_ir::tls; use chalk_ir::{ debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, - ImplTraitId, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, - ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, + ImplTraitId, ImplTraitTy, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, + ProgramClauses, ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, }; use chalk_rust_ir::{ AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplTraitDatum, ImplType, @@ -135,19 +135,8 @@ impl tls::DebugContext for Program { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { match alias_ty { - AliasTy::Projection(proj) => { - let (associated_ty_data, trait_params, other_params) = self.split_projection(proj); - write!( - fmt, - "<{:?} as {:?}{:?}>::{}{:?}", - &trait_params[0], - associated_ty_data.trait_id, - Angle(&trait_params[1..]), - associated_ty_data.name, - Angle(&other_params) - ) - } - AliasTy::ImplTrait(impl_trait_id) => write!(fmt, "impl {:?}", impl_trait_id), + AliasTy::Projection(projection_ty) => self.debug_projection_ty(projection_ty, fmt), + AliasTy::ImplTrait(impl_trait_ty) => self.debug_impl_trait_ty(impl_trait_ty, fmt), } } @@ -168,6 +157,14 @@ impl tls::DebugContext for Program { ) } + fn debug_impl_trait_ty( + &self, + impl_trait_ty: &ImplTraitTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error> { + write!(fmt, "impl {:?}", impl_trait_ty.impl_trait_id) + } + fn debug_ty(&self, ty: &Ty, fmt: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { let interner = self.interner(); write!(fmt, "{:?}", ty.data(interner)) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 515de52c186..c29e2788b4d 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -96,6 +96,14 @@ impl Debug for QuantifiedWhereClauses { } } +impl Debug for ImplTraitTy { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { + I::debug_impl_trait_ty(self, fmt).unwrap_or_else(|| { + unimplemented!("cannot format ImplTraitTy without setting Program in tls") + }) + } +} + impl Debug for ProjectionTy { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { I::debug_projection_ty(self, fmt).unwrap_or_else(|| { @@ -473,9 +481,32 @@ impl ProjectionTy { } } -impl Debug for ImplTraitTy { - fn fmt(&self, _fmt: &mut Formatter<'_>) -> Result<(), Error> { - todo!() +pub struct ImplTraitTyDebug<'a, I: Interner> { + impl_trait_ty: &'a ImplTraitTy, + interner: &'a I, +} + +impl<'a, I: Interner> Debug for ImplTraitTyDebug<'a, I> { + fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { + let ImplTraitTyDebug { + impl_trait_ty, + interner, + } = self; + write!( + fmt, + "(impl {:?}){:?}", + impl_trait_ty.impl_trait_id, + impl_trait_ty.substitution.with_angle(interner) + ) + } +} + +impl ImplTraitTy { + pub fn debug<'a>(&'a self, interner: &'a I) -> ImplTraitTyDebug<'a, I> { + ImplTraitTyDebug { + impl_trait_ty: self, + interner, + } } } diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs index aeb07262e83..2dd31912ac3 100644 --- a/chalk-ir/src/interner.rs +++ b/chalk-ir/src/interner.rs @@ -5,6 +5,7 @@ use crate::Goal; use crate::GoalData; use crate::Goals; use crate::ImplTraitId; +use crate::ImplTraitTy; use crate::Lifetime; use crate::LifetimeData; use crate::Parameter; @@ -196,6 +197,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } + /// Prints the debug representation of an ImplTraitTy. To get good + /// results, this requires inspecting TLS, and is difficult to + /// code without reference to a specific interner (and hence + /// fully known types). + /// + /// Returns `None` to fallback to the default debug output (e.g., + /// if no info about current program is available from TLS). + fn debug_impl_trait_ty( + impl_trait_ty: &ImplTraitTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Option; + /// Prints the debug representation of a ProjectionTy. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific interner (and hence @@ -575,6 +588,13 @@ mod default { tls::with_current_program(|prog| Some(prog?.debug_alias(alias, fmt))) } + fn debug_impl_trait_ty( + impl_trait_ty: &ImplTraitTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Option { + tls::with_current_program(|prog| Some(prog?.debug_impl_trait_ty(impl_trait_ty, fmt))) + } + fn debug_projection_ty( proj: &ProjectionTy, fmt: &mut fmt::Formatter<'_>, diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 5120bb3c7be..cc92816410f 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -846,7 +846,7 @@ impl ParameterData { #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub enum AliasTy { Projection(ProjectionTy), - ImplTrait(ImplTraitId), + ImplTrait(ImplTraitTy), } impl AliasTy { @@ -876,6 +876,7 @@ pub struct ProjectionTy { #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub struct ImplTraitTy { pub impl_trait_id: ImplTraitId, + pub substitution: Substitution, } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs index a7a2fbe2a78..3fc99d0d062 100644 --- a/chalk-ir/src/tls.rs +++ b/chalk-ir/src/tls.rs @@ -1,8 +1,8 @@ use crate::interner::ChalkIr; use crate::{ debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplTraitId, - Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, - QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, + ImplTraitTy, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, + ProjectionTy, QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, }; use std::cell::RefCell; use std::fmt; @@ -43,6 +43,12 @@ pub trait DebugContext { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; + fn debug_impl_trait_ty( + &self, + impl_trait_ty: &ImplTraitTy, + fmt: &mut fmt::Formatter<'_>, + ) -> Result<(), fmt::Error>; + fn debug_projection_ty( &self, proj: &ProjectionTy, diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 7cf2d8025ef..040ecbaddc3 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -247,6 +247,10 @@ struct_zip!(impl[I: Interner] Zip for ProjectionTy { associated_ty_id, substitution }); +struct_zip!(impl[I: Interner] Zip for ImplTraitTy { + impl_trait_id, + substitution +}); impl Zip for Environment { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 7e9205257c3..5f2b2c86ad1 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -396,9 +396,9 @@ fn match_ty( .db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - TyData::Alias(AliasTy::ImplTrait(impl_trait_id)) => builder + TyData::Alias(AliasTy::ImplTrait(impl_trait)) => builder .db - .impl_trait_datum(*impl_trait_id) + .impl_trait_datum(impl_trait.impl_trait_id) .to_program_clauses(builder), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 947f5d287b1..23922abd508 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -128,7 +128,13 @@ impl ToProgramClauses for ImplTraitDatum { /// ``` fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - let ty = Ty::new(interner, AliasTy::ImplTrait(self.impl_trait_id)); + let ty = Ty::new( + interner, + AliasTy::ImplTrait(ImplTraitTy { + impl_trait_id: self.impl_trait_id, + substitution: builder.substitution_in_scope(), + }), + ); for bound in &self.bounds { builder.push_fact(bound.as_trait_ref(interner, ty.clone())); From 72d4e7a924b9ec963266e388ab15b3a20aae9bef Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 23 Jan 2020 22:07:22 +0100 Subject: [PATCH 15/42] aggregate_tys for impl trait --- chalk-solve/src/solve/slg.rs | 23 +++++++++++++++++++- chalk-solve/src/solve/slg/aggregate.rs | 30 +++++++++++++++++++++++++- chalk-solve/src/wf.rs | 5 ++++- 3 files changed, 55 insertions(+), 3 deletions(-) diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index aea1849e105..7c0ac4d6e26 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -513,7 +513,10 @@ impl MayInvalidate<'_, I> { TyData::Alias(AliasTy::Projection(proj2)), ) => self.aggregate_projection_tys(proj1, proj2), - (TyData::Alias(_), TyData::Alias(_)) => todo!(), + ( + TyData::Alias(AliasTy::ImplTrait(impl_trait1)), + TyData::Alias(AliasTy::ImplTrait(impl_trait2)), + ) => self.aggregate_impl_trait_tys(impl_trait1, impl_trait2), // For everything else, be conservative here and just say we may invalidate. (TyData::Function(_), _) @@ -580,6 +583,24 @@ impl MayInvalidate<'_, I> { ) } + fn aggregate_impl_trait_tys(&mut self, new: &ImplTraitTy, current: &ImplTraitTy) -> bool { + let ImplTraitTy { + impl_trait_id: new_name, + substitution: new_substitution, + } = new; + let ImplTraitTy { + impl_trait_id: current_name, + substitution: current_substitution, + } = current; + + self.aggregate_name_and_substs( + new_name, + new_substitution, + current_name, + current_substitution, + ) + } + fn aggregate_name_and_substs( &mut self, new_name: N, diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs index f860f48ebfa..d77fa18280a 100644 --- a/chalk-solve/src/solve/slg/aggregate.rs +++ b/chalk-solve/src/solve/slg/aggregate.rs @@ -244,7 +244,10 @@ impl AntiUnifier<'_, '_, I> { TyData::Alias(AliasTy::Projection(proj2)), ) => self.aggregate_projection_tys(proj1, proj2), - (TyData::Alias(_), TyData::Alias(_)) => todo!(), + ( + TyData::Alias(AliasTy::ImplTrait(impl_trait1)), + TyData::Alias(AliasTy::ImplTrait(impl_trait2)), + ) => self.aggregate_impl_trait_tys(impl_trait1, impl_trait2), (TyData::Placeholder(placeholder1), TyData::Placeholder(placeholder2)) => { self.aggregate_placeholder_tys(placeholder1, placeholder2) @@ -322,6 +325,31 @@ impl AntiUnifier<'_, '_, I> { .unwrap_or_else(|| self.new_variable()) } + fn aggregate_impl_trait_tys( + &mut self, + impl_trait1: &ImplTraitTy, + impl_trait2: &ImplTraitTy, + ) -> Ty { + let ImplTraitTy { + impl_trait_id: name1, + substitution: substitution1, + } = impl_trait1; + let ImplTraitTy { + impl_trait_id: name2, + substitution: substitution2, + } = impl_trait2; + + self.aggregate_name_and_substs(name1, substitution1, name2, substitution2) + .map(|(&impl_trait_id, substitution)| { + TyData::Alias(AliasTy::ImplTrait(ImplTraitTy { + impl_trait_id, + substitution, + })) + .intern(self.interner) + }) + .unwrap_or_else(|| self.new_variable()) + } + fn aggregate_name_and_substs( &mut self, name1: N, diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 2852e045acd..47a8b29071a 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -110,7 +110,10 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { proj.visit_with(self, outer_binder); } - TyData::Alias(_) => todo!(), + TyData::Alias(AliasTy::ImplTrait(impl_trait)) => { + accumulator.push(self.clone()); + impl_trait.substitution.fold(interner, accumulator); + } TyData::Placeholder(_) => { push_ty(); From 001d8dfed574aeffa147f6727cce4d7475d4c733 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 23 Jan 2020 22:14:03 +0100 Subject: [PATCH 16/42] visit_alias_ty for impl trait --- chalk-solve/src/wf.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 47a8b29071a..4e3324bc6c0 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -111,8 +111,8 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { } TyData::Alias(AliasTy::ImplTrait(impl_trait)) => { - accumulator.push(self.clone()); - impl_trait.substitution.fold(interner, accumulator); + push_ty(); + impl_trait.visit_with(self, outer_binder); } TyData::Placeholder(_) => { From 207f839c674963117bedf278cbf2aefb64f9df9e Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 23 Jan 2020 22:19:31 +0100 Subject: [PATCH 17/42] Fill in match_type_name for ImplTrait --- chalk-solve/src/clauses.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 5f2b2c86ad1..d673e1692d5 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -417,7 +417,10 @@ fn match_ty( fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeName) { match name { TypeName::Struct(struct_id) => match_struct(builder, struct_id), - TypeName::ImplTrait(_impl_trait) => todo!(), + TypeName::ImplTrait(impl_trait_id) => builder + .db + .impl_trait_datum(impl_trait_id) + .to_program_clauses(builder), TypeName::Error => {} TypeName::AssociatedType(type_id) => builder .db From d7dac1756cc3b0421cc1f651d11a02695cd155e0 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Fri, 24 Jan 2020 09:07:56 +0100 Subject: [PATCH 18/42] Introduce AliasEq --- chalk-integration/src/lowering.rs | 4 ++-- chalk-ir/src/cast.rs | 4 ++-- chalk-ir/src/debug.rs | 6 ++--- chalk-ir/src/lib.rs | 12 +++++----- chalk-ir/src/macros.rs | 2 +- chalk-ir/src/zip.rs | 4 ++-- chalk-rust-ir/src/lib.rs | 10 ++++----- chalk-solve/src/clauses.rs | 11 ++++++--- chalk-solve/src/clauses/program_clauses.rs | 9 +++++--- chalk-solve/src/coinductive_goal.rs | 2 +- chalk-solve/src/infer/unify.rs | 26 +++++++++------------- chalk-solve/src/wf.rs | 6 ++--- tests/lowering/mod.rs | 2 +- 13 files changed, 48 insertions(+), 50 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 41526950b38..bb6936e8ef4 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -617,8 +617,8 @@ impl LowerWhereClause> for WhereClause { vec![chalk_ir::WhereClause::Implemented(trait_ref.lower(env)?)] } WhereClause::ProjectionEq { projection, ty } => vec![ - chalk_ir::WhereClause::ProjectionEq(chalk_ir::ProjectionEq { - projection: projection.lower(env)?, + chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq { + alias: chalk_ir::AliasTy::Projection(projection.lower(env)?), ty: ty.lower(env)?, }), chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?), diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs index 86aca1042b9..052ead6b6e2 100644 --- a/chalk-ir/src/cast.rs +++ b/chalk-ir/src/cast.rs @@ -89,9 +89,9 @@ impl CastTo> for TraitRef { } } -impl CastTo> for ProjectionEq { +impl CastTo> for AliasEq { fn cast_to(self, _interner: &I) -> WhereClause { - WhereClause::ProjectionEq(self) + WhereClause::AliasEq(self) } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index c29e2788b4d..9656ee85131 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -535,9 +535,9 @@ impl Debug for Normalize { } } -impl Debug for ProjectionEq { +impl Debug for AliasEq { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - write!(fmt, "ProjectionEq({:?} = {:?})", self.projection, self.ty) + write!(fmt, "AliasEq({:?} = {:?})", self.alias, self.ty) } } @@ -545,7 +545,7 @@ impl Debug for WhereClause { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { match self { WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()), - WhereClause::ProjectionEq(p) => write!(fmt, "{:?}", p), + WhereClause::AliasEq(a) => write!(fmt, "{:?}", a), } } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index cc92816410f..52a4ffc96d5 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -910,7 +910,7 @@ impl TraitRef { #[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner)] pub enum WhereClause { Implemented(TraitRef), - ProjectionEq(ProjectionEq), + AliasEq(AliasEq), } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] @@ -1172,16 +1172,14 @@ pub struct Normalize { pub ty: Ty, } -/// Proves **equality** between a projection `T::Foo` and a type -/// `U`. Equality can be proven via normalization, but we can also -/// prove that `T::Foo = V::Foo` if `T = V` without normalizing. +/// Proves **equality** between an alias and a type. #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)] -pub struct ProjectionEq { - pub projection: ProjectionTy, +pub struct AliasEq { + pub alias: AliasTy, pub ty: Ty, } -impl HasInterner for ProjectionEq { +impl HasInterner for AliasEq { type Interner = I; } diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index 3c31150a2d4..74b18b1bbba 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -24,7 +24,7 @@ macro_rules! ty { }; (alias (item $n:tt) $($arg:tt)*) => { - chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { + chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { associated_ty_id: AssocTypeId(chalk_ir::interner::RawId { index: $n }), substitution: $crate::Substitution::from(&chalk_ir::interner::ChalkIr, vec![$(arg!($arg)),*] as Vec<$crate::Parameter<_>>), }).intern(&chalk_ir::interner::ChalkIr) diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 040ecbaddc3..d9897f7b4fd 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -236,7 +236,7 @@ struct_zip!(impl[ struct_zip!(impl[I: Interner] Zip for ApplicationTy { name, substitution }); struct_zip!(impl[I: Interner] Zip for DynTy { bounds }); struct_zip!(impl[I: Interner] Zip for Normalize { alias, ty }); -struct_zip!(impl[I: Interner] Zip for ProjectionEq { projection, ty }); +struct_zip!(impl[I: Interner] Zip for AliasEq { alias, ty }); struct_zip!(impl[I: Interner] Zip for EqGoal { a, b }); struct_zip!(impl[I: Interner] Zip for ProgramClauseImplication { consequence, @@ -330,7 +330,7 @@ macro_rules! enum_zip { enum_zip!(impl for WellFormed { Trait, Ty }); enum_zip!(impl for FromEnv { Trait, Ty }); -enum_zip!(impl for WhereClause { Implemented, ProjectionEq }); +enum_zip!(impl for WhereClause { Implemented, AliasEq }); enum_zip!(impl for DomainGoal { Holds, WellFormed, diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index aad198e7877..f42e127cd6c 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -9,8 +9,8 @@ use chalk_ir::cast::Cast; use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ - AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, ImplTraitId, LifetimeData, - Parameter, ParameterKind, ProjectionEq, ProjectionTy, QuantifiedWhereClause, StructId, + AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, ImplTraitId, + LifetimeData, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -306,11 +306,11 @@ impl AliasEqBound { vec![ WhereClause::Implemented(trait_ref), - WhereClause::ProjectionEq(ProjectionEq { - projection: ProjectionTy { + WhereClause::AliasEq(AliasEq { + alias: AliasTy::Projection(ProjectionTy { associated_ty_id: self.associated_ty_id, substitution, - }, + }), ty: self.value.clone(), }), ] diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index d673e1692d5..12a7f6fd2d3 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -268,9 +268,14 @@ fn program_clauses_that_could_match( ); } } - DomainGoal::Holds(WhereClause::ProjectionEq(projection_predicate)) => db - .associated_ty_data(projection_predicate.projection.associated_ty_id) - .to_program_clauses(builder), + DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => match &alias_eq.alias { + AliasTy::Projection(proj) => db + .associated_ty_data(proj.associated_ty_id) + .to_program_clauses(builder), + AliasTy::ImplTrait(impl_trait) => db + .impl_trait_datum(impl_trait.impl_trait_id) + .to_program_clauses(builder), + }, DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { db.trait_datum(trait_predicate.trait_id) .to_program_clauses(builder); diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 23922abd508..c61379a1270 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -645,8 +645,8 @@ impl ToProgramClauses for AssociatedTyDatum { } .intern(interner); - let projection_eq = ProjectionEq { - projection: projection.clone(), + let projection_eq = AliasEq { + alias: AliasTy::Projection(projection.clone()), ty: app_ty.clone(), }; @@ -724,7 +724,10 @@ impl ToProgramClauses for AssociatedTyDatum { }; // `ProjectionEq(::Assoc = U)` - let projection_eq = ProjectionEq { projection, ty }; + let projection_eq = AliasEq { + alias: AliasTy::Projection(projection), + ty, + }; // Projection equality rule from above. // diff --git a/chalk-solve/src/coinductive_goal.rs b/chalk-solve/src/coinductive_goal.rs index 102ff3f655e..45bda7b9656 100644 --- a/chalk-solve/src/coinductive_goal.rs +++ b/chalk-solve/src/coinductive_goal.rs @@ -23,7 +23,7 @@ impl IsCoinductive for Goal { db.trait_datum(tr.trait_id).is_auto_trait() || db.trait_datum(tr.trait_id).is_coinductive_trait() } - WhereClause::ProjectionEq(..) => false, + WhereClause::AliasEq(..) => false, }, GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true, GoalData::Quantified(QuantifierKind::ForAll, goal) => { diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 693a1c72907..d76ae6cc55f 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -164,26 +164,19 @@ impl<'t, I: Interner> Unifier<'t, I> { // Unifying two dyn is possible if they have the same bounds. (&TyData::Dyn(ref qwc1), &TyData::Dyn(ref qwc2)) => Zip::zip_with(self, qwc1, qwc2), - // Unifying an associated type projection `::Item` with some other type `U`. + // Unifying an alias type with some other type `U`. (&TyData::Apply(_), &TyData::Alias(ref alias)) | (&TyData::Placeholder(_), &TyData::Alias(ref alias)) | (&TyData::Function(_), &TyData::Alias(ref alias)) | (&TyData::InferenceVar(_), &TyData::Alias(ref alias)) - | (&TyData::Dyn(_), &TyData::Alias(ref alias)) => match alias { - AliasTy::Projection(ref proj) => self.unify_projection_ty(proj, a), - _ => todo!(), - }, + | (&TyData::Dyn(_), &TyData::Alias(ref alias)) => self.unify_alias_ty(alias, a), (&TyData::Alias(ref alias), &TyData::Alias(_)) | (&TyData::Alias(ref alias), &TyData::Apply(_)) | (&TyData::Alias(ref alias), &TyData::Placeholder(_)) | (&TyData::Alias(ref alias), &TyData::Function(_)) | (&TyData::Alias(ref alias), &TyData::InferenceVar(_)) - | (&TyData::Alias(ref alias), &TyData::Dyn(_)) => match alias { - AliasTy::Projection(ref proj) => self.unify_projection_ty(proj, b), - _ => todo!(), - }, + | (&TyData::Alias(ref alias), &TyData::Dyn(_)) => self.unify_alias_ty(alias, b), (TyData::BoundVar(_), _) | (_, TyData::BoundVar(_)) => panic!( "unification encountered bound variable: a={:?} b={:?}", @@ -224,18 +217,19 @@ impl<'t, I: Interner> Unifier<'t, I> { } } - /// Unify an associated type projection `proj` like `::Item` with some other - /// type `ty` (which might also be a projection). Creates a goal like + /// Unify an alias like `::Item` or `impl Trait` with some other + /// type `ty` (which might also be an alias). Creates a goal like /// /// ```notrust - /// ProjectionEq(::Item = U) + /// AliasEq(::Item = U) // associated type projection + /// AliasEq(impl Trait = U) // impl trait /// ``` - fn unify_projection_ty(&mut self, proj: &ProjectionTy, ty: &Ty) -> Fallible<()> { + fn unify_alias_ty(&mut self, alias: &AliasTy, ty: &Ty) -> Fallible<()> { let interner = self.interner; Ok(self.goals.push(InEnvironment::new( self.environment, - ProjectionEq { - projection: proj.clone(), + AliasEq { + alias: alias.clone(), ty: ty.clone(), } .cast(interner), diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 4e3324bc6c0..856cba91a98 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -75,10 +75,8 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { fn visit_where_clause(&mut self, where_clause: &WhereClause, outer_binder: DebruijnIndex) { match where_clause { - WhereClause::ProjectionEq(alias_eq) => { - TyData::Alias(AliasTy::Projection(alias_eq.projection.clone())) - .intern(self.interner) - .visit_with(self, outer_binder); + WhereClause::AliasEq(alias_eq) => { + alias_eq.alias.visit_with(self, outer_binder); alias_eq.ty.visit_with(self, outer_binder); } WhereClause::Implemented(trait_ref) => { diff --git a/tests/lowering/mod.rs b/tests/lowering/mod.rs index 700bc1209de..cac5bf492d1 100644 --- a/tests/lowering/mod.rs +++ b/tests/lowering/mod.rs @@ -215,7 +215,7 @@ fn atc_accounting() { "ForAll { \ ForAll { \ ForAll { \ - all(ProjectionEq(<^2.0 as Iterable>::Iter<'^1.0> = ^0.0), \ + all(AliasEq(<^2.0 as Iterable>::Iter<'^1.0> = ^0.0), \ Implemented(^2.0: Iterable)) \ } \ } \ From 8ed27944a7f520582222c36c4973ed54ed08176f Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Fri, 14 Feb 2020 15:11:26 +0100 Subject: [PATCH 19/42] Change ast defn to opaque type --- chalk-integration/src/db.rs | 4 +-- chalk-integration/src/lib.rs | 1 + chalk-integration/src/lowering.rs | 48 ++++++++++++++++++++++++++----- chalk-integration/src/program.rs | 2 +- chalk-parse/src/ast.rs | 5 ++-- chalk-parse/src/parser.lalrpop | 11 +++---- chalk-solve/src/clauses.rs | 6 ++-- chalk-solve/src/lib.rs | 2 +- tests/test/existential_types.rs | 19 ++++++++++++ 9 files changed, 77 insertions(+), 21 deletions(-) diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs index b1d175eb959..3549d4f37a9 100644 --- a/chalk-integration/src/db.rs +++ b/chalk-integration/src/db.rs @@ -106,8 +106,8 @@ impl RustIrDatabase for ChalkDatabase { self.program_ir().unwrap().associated_ty_values[&id].clone() } - fn impl_trait_datum(&self, id: ImplTraitId) -> Arc> { - self.program_ir().unwrap().impl_trait_data[&id].clone() + fn impl_trait_data(&self, id: ImplTraitId) -> Arc> { + self.program_ir().unwrap().impl_trait_data(id) } fn struct_datum(&self, id: StructId) -> Arc> { diff --git a/chalk-integration/src/lib.rs b/chalk-integration/src/lib.rs index fd272863dcc..e97af96c24a 100644 --- a/chalk-integration/src/lib.rs +++ b/chalk-integration/src/lib.rs @@ -18,6 +18,7 @@ use chalk_ir::Binders; pub enum TypeSort { Struct, Trait, + ImplTrait, } #[derive(Clone, Debug, PartialEq, Eq, Hash)] diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index bb6936e8ef4..107d66b28e0 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -19,6 +19,7 @@ use crate::{Identifier as Ident, RawId, TypeKind, TypeSort}; type StructIds = BTreeMap>; type TraitIds = BTreeMap>; +type ImplTraitIds = BTreeMap>; type StructKinds = BTreeMap, TypeKind>; type TraitKinds = BTreeMap, TypeKind>; type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId, Ident), AssociatedTyLookup>; @@ -34,6 +35,7 @@ struct Env<'k> { struct_kinds: &'k StructKinds, trait_ids: &'k TraitIds, trait_kinds: &'k TraitKinds, + impl_trait_ids: &'k ImplTraitIds, associated_ty_lookups: &'k AssociatedTyLookups, /// Parameter identifiers are used as keys, therefore /// all identifiers in an environment must be unique (no shadowing). @@ -68,6 +70,7 @@ struct AssociatedTyLookup { enum TypeLookup { Struct(chalk_ir::StructId), Parameter(BoundVar), + ImplTrait(chalk_ir::ImplTraitId), } enum LifetimeLookup { @@ -90,6 +93,9 @@ impl<'k> Env<'k> { return Ok(TypeLookup::Struct(*id)); } + if let Some(id) = self.impl_trait_ids.get(&name.str) { + return Ok(TypeLookup::ImplTrait(*id)); + } if let Some(_) = self.trait_ids.get(&name.str) { return Err(RustIrError::NotStruct(name)); } @@ -225,9 +231,10 @@ impl LowerProgram for Program { let mut struct_ids = BTreeMap::new(); let mut trait_ids = BTreeMap::new(); + let mut impl_trait_ids = BTreeMap::new(); let mut struct_kinds = BTreeMap::new(); let mut trait_kinds = BTreeMap::new(); - let mut impl_trait_ids = BTreeMap::new(); + let mut impl_trait_kinds = BTreeMap::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { match item { Item::StructDefn(defn) => { @@ -242,8 +249,11 @@ impl LowerProgram for Program { trait_ids.insert(type_kind.name, id); trait_kinds.insert(id, type_kind); } - Item::ImplTrait(impl_trait) => { - impl_trait_ids.insert(impl_trait.identifier.str, ImplTraitId(raw_id)); + Item::OpaqueTyDefn(defn) => { + let type_kind = defn.lower_type_kind()?; + let id = ImplTraitId(raw_id); + impl_trait_ids.insert(defn.identifier.str, id); + impl_trait_kinds.insert(id, type_kind); } Item::Impl(_) => continue, Item::Clause(_) => continue, @@ -264,6 +274,7 @@ impl LowerProgram for Program { struct_kinds: &struct_kinds, trait_ids: &trait_ids, trait_kinds: &trait_kinds, + impl_trait_ids: &impl_trait_ids, associated_ty_lookups: &associated_ty_lookups, parameter_map: BTreeMap::new(), }; @@ -368,13 +379,13 @@ impl LowerProgram for Program { Item::Clause(ref clause) => { custom_clauses.extend(clause.lower_clause(&empty_env)?); } - Item::ImplTrait(ref impl_trait) => { - if let Some(&value) = impl_trait_ids.get(&impl_trait.identifier.str) { + Item::OpaqueTyDefn(ref opaque_ty) => { + if let Some(&value) = impl_trait_ids.get(&opaque_ty.identifier.str) { impl_trait_data.insert( value, Arc::new(ImplTraitDatum { impl_trait_id: value, - bounds: impl_trait + bounds: opaque_ty .bounds .iter() .map(|b| b.lower(&empty_env)) @@ -575,6 +586,19 @@ impl LowerTypeKind for TraitDefn { } } +impl LowerTypeKind for OpaqueTyDefn { + fn lower_type_kind(&self) -> LowerResult { + Ok(TypeKind { + sort: TypeSort::ImplTrait, + name: self.identifier.str, + binders: chalk_ir::Binders { + binders: vec![], //TODO do we need binders here? + value: (), + }, + }) + } +} + impl LowerWhereClauses for TraitDefn { fn where_clauses(&self) -> &[QuantifiedWhereClause] { &self.where_clauses @@ -1017,6 +1041,13 @@ impl LowerTy for Ty { } } TypeLookup::Parameter(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)), + TypeLookup::ImplTrait(id) => Ok(chalk_ir::TyData::Alias( + chalk_ir::AliasTy::ImplTrait(chalk_ir::ImplTraitTy { + impl_trait_id: id, + substitution: chalk_ir::Substitution::empty(interner), + }), + ) + .intern(interner)), }, Ty::Dyn { ref bounds } => Ok(chalk_ir::TyData::Dyn(chalk_ir::DynTy { @@ -1045,7 +1076,9 @@ impl LowerTy for Ty { Ty::Apply { name, ref args } => { let id = match env.lookup_type(name)? { TypeLookup::Struct(id) => id, - TypeLookup::Parameter(_) => Err(RustIrError::CannotApplyTypeParameter(name))?, + TypeLookup::Parameter(_) | TypeLookup::ImplTrait(_) => { + Err(RustIrError::CannotApplyTypeParameter(name))? + } }; let k = env.struct_kind(id); @@ -1312,6 +1345,7 @@ impl LowerGoal for Goal { let env = Env { struct_ids: &program.struct_ids, trait_ids: &program.trait_ids, + impl_trait_ids: &program.impl_trait_ids, struct_kinds: &program.struct_kinds, trait_kinds: &program.trait_kinds, associated_ty_lookups: &associated_ty_lookups, diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 9401ffc393a..e706f4ac5e6 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -294,7 +294,7 @@ impl RustIrDatabase for Program { self.associated_ty_values[&id].clone() } - fn impl_trait_datum(&self, id: ImplTraitId) -> Arc> { + fn impl_trait_data(&self, id: ImplTraitId) -> Arc> { self.impl_trait_data[&id].clone() } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 0d9facc1c46..9131186c6bc 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -22,9 +22,9 @@ pub struct Program { pub enum Item { StructDefn(StructDefn), TraitDefn(TraitDefn), + OpaqueTyDefn(OpaqueTyDefn), Impl(Impl), Clause(Clause), - ImplTrait(ImplTrait), } #[derive(Clone, PartialEq, Eq, Debug)] @@ -79,7 +79,8 @@ pub struct AssocTyDefn { } #[derive(Clone, PartialEq, Eq, Debug)] -pub struct ImplTrait { +pub struct OpaqueTyDefn { + pub ty: Ty, pub identifier: Identifier, pub bounds: Vec, } diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index b5e14cf32cd..1087970ca67 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -15,7 +15,7 @@ Item: Option = { Comment => None, StructDefn => Some(Item::StructDefn(<>)), TraitDefn => Some(Item::TraitDefn(<>)), - ImplTrait => Some(Item::ImplTrait(<>)), + OpaqueTyDefn => Some(Item::OpaqueTyDefn(<>)), Impl => Some(Item::Impl(<>)), Clause => Some(Item::Clause(<>)), }; @@ -99,14 +99,15 @@ AssocTyDefn: AssocTyDefn = { } }; -ImplTrait: ImplTrait = { - "type" "=" "impl" > ";" => { - ImplTrait { +OpaqueTyDefn: OpaqueTyDefn = { + "opaque" "type" ":" > "=" ";" => { + OpaqueTyDefn { + ty, identifier, bounds: b, } } -} +}; InlineBound: InlineBound = { TraitBound => InlineBound::TraitBound(<>), diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 12a7f6fd2d3..63a2c24e586 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -273,7 +273,7 @@ fn program_clauses_that_could_match( .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), AliasTy::ImplTrait(impl_trait) => db - .impl_trait_datum(impl_trait.impl_trait_id) + .impl_trait_data(impl_trait.impl_trait_id) .to_program_clauses(builder), }, DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { @@ -403,7 +403,7 @@ fn match_ty( .to_program_clauses(builder), TyData::Alias(AliasTy::ImplTrait(impl_trait)) => builder .db - .impl_trait_datum(impl_trait.impl_trait_id) + .impl_trait_data(impl_trait.impl_trait_id) .to_program_clauses(builder), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); @@ -424,7 +424,7 @@ fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeNa TypeName::Struct(struct_id) => match_struct(builder, struct_id), TypeName::ImplTrait(impl_trait_id) => builder .db - .impl_trait_datum(impl_trait_id) + .impl_trait_data(impl_trait_id) .to_program_clauses(builder), TypeName::Error => {} TypeName::AssociatedType(type_id) => builder diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index d1dfbd64a8a..696a89bbaa4 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -41,7 +41,7 @@ pub trait RustIrDatabase: Debug { fn associated_ty_value(&self, id: AssociatedTyValueId) -> Arc>; /// Returns the `ImplTraitDatum` with the given id. - fn impl_trait_datum(&self, id: ImplTraitId) -> Arc>; + fn impl_trait_data(&self, id: ImplTraitId) -> Arc>; /// If `id` is a struct id, returns `Some(id)` (but cast to `StructId`). fn as_struct_id(&self, id: &TypeName) -> Option>; diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index 12584ec2890..e4be47b31b8 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -2,6 +2,25 @@ use super::*; +#[test] +fn opaque_bounds() { + test! { + program { + trait Trait { } + struct Ty { } + impl Trait for Ty { } + + opaque type T: Trait = Ty; + } + + goal { + T: Trait + } yields { + "Unique; substitution []" + } + } +} + #[test] fn dyn_Clone_is_Clone() { test! { From c30bf22149ced6bbbffb14b1654591ddd2a67791 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 17 Feb 2020 17:34:31 +0100 Subject: [PATCH 20/42] Fix debug impl for ImplTraitTy --- chalk-integration/src/program.rs | 2 +- chalk-ir/src/debug.rs | 2 +- chalk-solve/src/clauses.rs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index e706f4ac5e6..d7840ca245d 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -121,7 +121,7 @@ impl tls::DebugContext for Program { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { if let Some(d) = self.impl_trait_data.get(&impl_trait_id) { - write!(fmt, "type {:?} = impl {:?}", d.impl_trait_id, d.bounds) + write!(fmt, "{:?}", d.bounds) } else { fmt.debug_struct("InvalidItemId") .field("index", &impl_trait_id.0) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 9656ee85131..8ff4d92a2b6 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -494,7 +494,7 @@ impl<'a, I: Interner> Debug for ImplTraitTyDebug<'a, I> { } = self; write!( fmt, - "(impl {:?}){:?}", + "{:?}{:?}", impl_trait_ty.impl_trait_id, impl_trait_ty.substitution.with_angle(interner) ) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 63a2c24e586..0315e6fd5b6 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -321,7 +321,7 @@ fn program_clauses_that_could_match( trait_parameters, ); } - _ => todo!(), + AliasTy::ImplTrait(_) => (), }, DomainGoal::LocalImplAllowed(trait_ref) => db .trait_datum(trait_ref.trait_id) From d6480b8e8996d2a7a507c7712baca6cf05861972 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 26 Feb 2020 20:10:01 +0100 Subject: [PATCH 21/42] Generate AliasEq rules and introduce Reveal --- chalk-integration/src/lowering.rs | 1 + chalk-ir/src/debug.rs | 1 + chalk-ir/src/lib.rs | 4 +++ chalk-ir/src/zip.rs | 3 +- chalk-rust-ir/src/lib.rs | 8 ++++- chalk-solve/src/clauses.rs | 1 + chalk-solve/src/clauses/program_clauses.rs | 38 ++++++++++++++-------- 7 files changed, 40 insertions(+), 16 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 107d66b28e0..6645243cdd3 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -390,6 +390,7 @@ impl LowerProgram for Program { .iter() .map(|b| b.lower(&empty_env)) .collect::, _>>()?, + ty: opaque_ty.ty.lower(&empty_env)?, }), ); } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 8ff4d92a2b6..f538e9c132c 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -583,6 +583,7 @@ impl Debug for DomainGoal { } DomainGoal::Compatible(_) => write!(fmt, "Compatible"), DomainGoal::DownstreamType(n) => write!(fmt, "DownstreamType({:?})", n), + DomainGoal::Reveal(_) => write!(fmt, "Reveal"), } } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 52a4ffc96d5..4b997222483 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1036,6 +1036,10 @@ pub enum DomainGoal { /// /// This makes a new type `T` available and makes `DownstreamType(T)` provable for that type. DownstreamType(Ty), + + /// Used to activate the "reveal mode", in which opaque (`impl Trait`) types can be equated + /// to their actual type. + Reveal(()), } pub type QuantifiedWhereClause = Binders>; diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index d9897f7b4fd..26080b3114f 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -341,7 +341,8 @@ enum_zip!(impl for DomainGoal { IsFullyVisible, LocalImplAllowed, Compatible, - DownstreamType + DownstreamType, + Reveal, }); enum_zip!(impl for ProgramClauseData { Implies, ForAll }); enum_zip!(impl for AliasTy { Projection, ImplTrait }); diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index f42e127cd6c..b8fe9546786 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -509,12 +509,18 @@ pub struct AssociatedTyValueBound { /// Represents the bounds for an `impl Trait` type. /// /// ```ignore -/// type Foo = impl A + B + C; +/// opaque type T: A + B = HiddenTy; /// ``` #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold)] pub struct ImplTraitDatum { + /// The placeholder `!T` that corresponds to the opaque type `T`. pub impl_trait_id: ImplTraitId, + + /// Trait bounds for the opaque type. pub bounds: Vec>, + + /// The "hidden type" that the opaque type is equal to when revealed. + pub ty: Ty, } #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 0315e6fd5b6..f877f0b778b 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -327,6 +327,7 @@ fn program_clauses_that_could_match( .trait_datum(trait_ref.trait_id) .to_program_clauses(builder), DomainGoal::Compatible(()) => (), + DomainGoal::Reveal(()) => (), }; Ok(()) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index c61379a1270..cd3ac97e64f 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -119,38 +119,48 @@ impl ToProgramClauses for AssociatedTyValue { } impl ToProgramClauses for ImplTraitDatum { - /// Given `type Foo = impl A + B;`, we generate: + /// Given `opaque type T<..>: A + B = HiddenTy;`, we generate: /// /// ```notrust - /// Implemented(Foo: A), - /// Implemented(Foo: B), - /// Implemented(Foo: Send) :- Implemented(A + B: Send). // For all auto traits + /// AliasEq(T<..> = HiddenTy) :- Reveal. + /// AliasEq(T<..> = !T). + /// Implemented(!T: A). + /// Implemented(!T: B). + /// Implemented(!T: Send) :- Implemented(A + B: Send). // For all auto traits /// ``` + /// where `!T` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - let ty = Ty::new( - interner, - AliasTy::ImplTrait(ImplTraitTy { - impl_trait_id: self.impl_trait_id, - substitution: builder.substitution_in_scope(), - }), - ); + // TODO add this to the env elsewhere + builder.push_fact(DomainGoal::Reveal(())); + + let alias = AliasTy::ImplTrait(ImplTraitTy { + impl_trait_id: self.impl_trait_id, + substitution: builder.substitution_in_scope(), + }); + + builder.push_fact(DomainGoal::Holds(WhereClause::AliasEq(AliasEq { + alias: alias.clone(), + ty: self.ty.clone(), + }))); + + let alias_ty = Ty::new(interner, alias); for bound in &self.bounds { - builder.push_fact(bound.as_trait_ref(interner, ty.clone())); + builder.push_fact(bound.as_trait_ref(interner, alias_ty.clone())); } for auto_trait_id in builder.db.auto_traits() { builder.push_clause( TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, ty.clone()), + substitution: Substitution::from1(interner, alias_ty.clone()), }, iter::once(TraitRef { trait_id: auto_trait_id, substitution: Substitution::from( interner, - iter::once(ty.clone().cast(interner)).chain( + iter::once(alias_ty.clone().cast(interner)).chain( self.bounds .iter() .flat_map(|b| b.args_no_self.iter().cloned()), From c015b46f7b65693f04e47dada88e5d2f6e39eedf Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Sun, 1 Mar 2020 11:49:15 +0100 Subject: [PATCH 22/42] Improve clause generation for impl trait --- chalk-solve/src/clauses/program_clauses.rs | 30 +++++++++++++++++----- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index cd3ac97e64f..3c8252fb386 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -139,18 +139,36 @@ impl ToProgramClauses for ImplTraitDatum { substitution: builder.substitution_in_scope(), }); - builder.push_fact(DomainGoal::Holds(WhereClause::AliasEq(AliasEq { - alias: alias.clone(), - ty: self.ty.clone(), - }))); - - let alias_ty = Ty::new(interner, alias); + // AliasEq(T<..> = HiddenTy) :- Reveal. + builder.push_clause( + DomainGoal::Holds( + AliasEq { + alias: alias.clone(), + ty: self.ty.clone(), + } + .cast(interner), + ), + iter::once(DomainGoal::Reveal(())), + ); + + let alias_ty = Ty::new(interner, alias.clone()); + + // AliasEq(T<..> = !T). + builder.push_fact(DomainGoal::Holds( + AliasEq { + alias: alias.clone(), + ty: alias_ty.clone(), + } + .cast(interner), + )); for bound in &self.bounds { + // Implemented(!T: Bound). builder.push_fact(bound.as_trait_ref(interner, alias_ty.clone())); } for auto_trait_id in builder.db.auto_traits() { + // Implemented(!T: AutoTrait) :- Implemented(Bounds: AutoTrait). builder.push_clause( TraitRef { trait_id: auto_trait_id, From 1e2161cd3d3820efce5b298b7663a1965d653013 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 2 Mar 2020 19:27:10 +0100 Subject: [PATCH 23/42] Complete test by testing Reveal in goal --- chalk-integration/src/lowering.rs | 1 + chalk-parse/src/ast.rs | 1 + chalk-parse/src/parser.lalrpop | 2 ++ chalk-solve/src/clauses/program_clauses.rs | 3 --- tests/test/existential_types.rs | 10 +++++++++- 5 files changed, 13 insertions(+), 4 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 6645243cdd3..a953c56851a 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -705,6 +705,7 @@ impl LowerDomainGoal for DomainGoal { DomainGoal::DownstreamType { ty } => { vec![chalk_ir::DomainGoal::DownstreamType(ty.lower(env)?)] } + DomainGoal::Reveal => vec![chalk_ir::DomainGoal::Reveal(())], }; Ok(goals) } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 9131186c6bc..75947fcbe56 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -257,6 +257,7 @@ pub enum DomainGoal { LocalImplAllowed { trait_ref: TraitRef }, Compatible, DownstreamType { ty: Ty }, + Reveal, } #[derive(Clone, PartialEq, Eq, Debug)] diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 1087970ca67..dfc8bebac58 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -323,6 +323,8 @@ DomainGoal: DomainGoal = { "Compatible" => DomainGoal::Compatible, "DownstreamType" "(" ")" => DomainGoal::DownstreamType { ty }, + + "Reveal" => DomainGoal::Reveal, }; LeafGoal: LeafGoal = { diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 3c8252fb386..1f92ac32c23 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -131,9 +131,6 @@ impl ToProgramClauses for ImplTraitDatum { /// where `!T` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - // TODO add this to the env elsewhere - builder.push_fact(DomainGoal::Reveal(())); - let alias = AliasTy::ImplTrait(ImplTraitTy { impl_trait_id: self.impl_trait_id, substitution: builder.substitution_in_scope(), diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index e4be47b31b8..d53046ec6d3 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -14,10 +14,18 @@ fn opaque_bounds() { } goal { - T: Trait + if (Reveal) { + T: Trait + } } yields { "Unique; substitution []" } + + goal { + T: Trait + } yields { + "No possible solution" + } } } From 5fb73c0f846379c836e19a71792ef5efaf382df0 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 2 Mar 2020 19:40:34 +0100 Subject: [PATCH 24/42] Fix tests --- book/src/types/rust_types.md | 16 +++++++--------- chalk-ir/src/macros.rs | 4 ++-- chalk-solve/src/clauses.rs | 4 ++-- chalk-solve/src/clauses/program_clauses.rs | 18 +++++++++--------- chalk-solve/src/infer/test.rs | 2 +- 5 files changed, 21 insertions(+), 23 deletions(-) diff --git a/book/src/types/rust_types.md b/book/src/types/rust_types.md index eb4f5a11b2a..c2d228f95b6 100644 --- a/book/src/types/rust_types.md +++ b/book/src/types/rust_types.md @@ -56,7 +56,7 @@ evaluated. For example, when typing the body of a generic function like `fn foo`, the type `T` would be represented with a placeholder. Similarly, in that same function, the associated type `T::Item` might be represented with a placeholder. - + Like application types, placeholder *types* are only known to be equal. @@ -96,7 +96,7 @@ type. In chalk, these are represented as an existential type where we store the predicates that are known to be true. So a type like `dyn Write` would be represented as, effectively, an `exists { T: Write }` type. - + When equating, two `dyn P` and `dyn Q` types are equal if `P = Q` -- i.e., they have the same bounds. Note that -- for this purpose -- ordering of bounds is significant. That means that if you create a @@ -115,7 +115,7 @@ application types, but with one crucial difference: they also contain a `forall` binder that for lifetimes whose value is determined when the function is called. Consider e.g. a type like `fn(&u32)` or -- more explicitly -- `for<'a> fn(&'a u32)`. - + Two `Fn` types `A, B` are equal `A = B` if `A <: B` and `B <: A` Two `Fn` types `A, B` are subtypes `A <: B` if @@ -124,7 +124,7 @@ Two `Fn` types `A, B` are subtypes `A <: B` if * You can instantiate the lifetime parameters on `A` existentially... * And then you find that `P_B <: P_A` for every parameter type `P` on `A` and `B` and `R_A <: R_B` for the return type `R` of `A` and `B`. - + We currently handle type inference with a bit of a hack (same as rustc); when relating a `Fn` type `F` to an unbounded type variable `V`, we instantiate `V` with `F`. But in practice @@ -155,16 +155,14 @@ contained within. The `Alias` variant wraps an `AliasTy` and is used to represent some form of *type alias*. These correspond to associated type projections like `::Item` -but also `impl Trait` types and named type aliases like `type Foo = Vec`. +but also `impl Trait` types and named type aliases like `type Foo = Vec`. Each alias has an alias id as well as parameters. Aliases effectively represent a *type function*. Aliases are quite special when equating types. In general, an alias -type `A` can also be equal to *any other type* `T` if evaluating the -alias `A` yields `T` (this is currently handled in Chalk via a -`ProjectionEq` goal, but it would be renamed to `AliasEq` under this -proposal). +type `A` can also be equal to *any other type* `T` (`AliasEq`) if evaluating the +alias `A` yields `T`. However, some alias types can also be instantiated as "alias placeholders". This occurs when the precise type of the alias is not diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index 74b18b1bbba..a60a44e0f78 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -23,8 +23,8 @@ macro_rules! ty { }).intern(&chalk_ir::interner::ChalkIr) }; - (alias (item $n:tt) $($arg:tt)*) => { - chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { + (projection (item $n:tt) $($arg:tt)*) => { + chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy { associated_ty_id: AssocTypeId(chalk_ir::interner::RawId { index: $n }), substitution: $crate::Substitution::from(&chalk_ir::interner::ChalkIr, vec![$(arg!($arg)),*] as Vec<$crate::Parameter<_>>), }).intern(&chalk_ir::interner::ChalkIr) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index f877f0b778b..a67ee57c914 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -197,7 +197,7 @@ fn program_clauses_that_could_match( // ``` // dyn(exists { // forall<'a> { Implemented(T: Fn<'a>) }, - // forall<'a> { ProjectionEq(>::Output, ()) }, + // forall<'a> { AliasEq(>::Output, ()) }, // }) // ``` // @@ -212,7 +212,7 @@ fn program_clauses_that_could_match( // and // // ``` - // forall<'a> { ProjectionEq(>::Output, ()) }, + // forall<'a> { AliasEq(>::Output, ()) }, // ``` // // FIXME. This is presently rather wasteful, in that we diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 1f92ac32c23..e4d34696a0e 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -594,18 +594,18 @@ impl ToProgramClauses for AssociatedTyDatum { /// we generate the 'fallback' rule: /// /// ```notrust - /// -- Rule ProjectionEq-Placeholder + /// -- Rule AliasEq-Placeholder /// forall { - /// ProjectionEq(::Assoc<'a, T> = (Foo::Assoc<'a, T>)). + /// AliasEq(::Assoc<'a, T> = (Foo::Assoc<'a, T>)). /// } /// ``` /// /// and /// /// ```notrust - /// -- Rule ProjectionEq-Normalize + /// -- Rule AliasEq-Normalize /// forall { - /// ProjectionEq(::Assoc<'a, T> = U) :- + /// AliasEq(::Assoc<'a, T> = U) :- /// Normalize(::Assoc -> U). /// } /// ``` @@ -614,14 +614,14 @@ impl ToProgramClauses for AssociatedTyDatum { /// /// ```notrust /// forall { - /// T: Foo :- exists { ProjectionEq(::Assoc = U) }. + /// T: Foo :- exists { AliasEq(::Assoc = U) }. /// } /// ``` /// /// but this caused problems with the recursive solver. In /// particular, whenever normalization is possible, we cannot /// solve that projection uniquely, since we can now elaborate - /// `ProjectionEq` to fallback *or* normalize it. So instead we + /// `AliasEq` to fallback *or* normalize it. So instead we /// handle this kind of reasoning through the `FromEnv` predicate. /// /// We also generate rules specific to WF requirements and implied bounds: @@ -679,7 +679,7 @@ impl ToProgramClauses for AssociatedTyDatum { // and placeholder type. // // forall { - // ProjectionEq(::Assoc = (Foo::Assoc)). + // AliasEq(::Assoc = (Foo::Assoc)). // } builder.push_fact_with_priority(projection_eq, ClausePriority::Low); @@ -748,7 +748,7 @@ impl ToProgramClauses for AssociatedTyDatum { ty: ty.clone(), }; - // `ProjectionEq(::Assoc = U)` + // `AliasEq(::Assoc = U)` let projection_eq = AliasEq { alias: AliasTy::Projection(projection), ty, @@ -757,7 +757,7 @@ impl ToProgramClauses for AssociatedTyDatum { // Projection equality rule from above. // // forall { - // ProjectionEq(::Assoc = U) :- + // AliasEq(::Assoc = U) :- // Normalize(::Assoc -> U). // } builder.push_clause(projection_eq, Some(normalize)); diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs index 9d448ac82cf..1cf5f8d3e5b 100644 --- a/chalk-solve/src/infer/test.rs +++ b/chalk-solve/src/infer/test.rs @@ -151,7 +151,7 @@ fn projection_eq() { interner, &environment0, &a, - &ty!(apply (item 0) (alias (item 1) (expr a))), + &ty!(apply (item 0) (projection (item 1) (expr a))), ) .unwrap_err(); } From 5d39e9a5951070ed026066104eb43934429c7b36 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 11 Mar 2020 13:21:13 +0100 Subject: [PATCH 25/42] Improve generated rule for auto traits --- chalk-solve/src/clauses/program_clauses.rs | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index e4d34696a0e..c898f2bd15c 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -126,7 +126,7 @@ impl ToProgramClauses for ImplTraitDatum { /// AliasEq(T<..> = !T). /// Implemented(!T: A). /// Implemented(!T: B). - /// Implemented(!T: Send) :- Implemented(A + B: Send). // For all auto traits + /// Implemented(!T: Send) :- Implemented(HiddenTy: Send). // For all auto traits /// ``` /// where `!T` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { @@ -165,7 +165,7 @@ impl ToProgramClauses for ImplTraitDatum { } for auto_trait_id in builder.db.auto_traits() { - // Implemented(!T: AutoTrait) :- Implemented(Bounds: AutoTrait). + // Implemented(!T: AutoTrait) :- Implemented(HiddenTy: AutoTrait). builder.push_clause( TraitRef { trait_id: auto_trait_id, @@ -173,14 +173,7 @@ impl ToProgramClauses for ImplTraitDatum { }, iter::once(TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from( - interner, - iter::once(alias_ty.clone().cast(interner)).chain( - self.bounds - .iter() - .flat_map(|b| b.args_no_self.iter().cloned()), - ), - ), + substitution: Substitution::from1(interner, self.ty.clone()), }), ); } From a34a041d28a430ad64e21ac782df2711a43724d5 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 11 Mar 2020 14:33:14 +0100 Subject: [PATCH 26/42] Quantify bounds and add binders --- chalk-integration/src/lowering.rs | 22 ++++++++++-- chalk-parse/src/ast.rs | 3 +- chalk-parse/src/parser.lalrpop | 3 +- chalk-rust-ir/src/lib.rs | 4 +-- chalk-solve/src/clauses/program_clauses.rs | 42 +++++++++++----------- 5 files changed, 47 insertions(+), 27 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index a953c56851a..ff4073df0e1 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -381,16 +381,32 @@ impl LowerProgram for Program { } Item::OpaqueTyDefn(ref opaque_ty) => { if let Some(&value) = impl_trait_ids.get(&opaque_ty.identifier.str) { + let parameter_kinds = opaque_ty + .parameter_kinds + .iter() + .map(|k| k.lower()) + .collect::>(); + + let binders = empty_env + .in_binders(parameter_kinds, |env| opaque_ty.ty.lower(&env))?; + impl_trait_data.insert( value, Arc::new(ImplTraitDatum { impl_trait_id: value, bounds: opaque_ty .bounds + .lower(&empty_env)? .iter() - .map(|b| b.lower(&empty_env)) - .collect::, _>>()?, - ty: opaque_ty.ty.lower(&empty_env)?, + .flat_map(|qil| { + qil.into_where_clauses( + empty_env.interner(), + chalk_ir::TyData::BoundVar(0) + .intern(empty_env.interner()), + ) + }) + .collect(), + ty: binders, }), ); } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 75947fcbe56..d96fe692081 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -81,8 +81,9 @@ pub struct AssocTyDefn { #[derive(Clone, PartialEq, Eq, Debug)] pub struct OpaqueTyDefn { pub ty: Ty, + pub parameter_kinds: Vec, pub identifier: Identifier, - pub bounds: Vec, + pub bounds: Vec, } #[derive(Copy, Clone, PartialEq, Eq, Debug)] diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index dfc8bebac58..70e39c9e3c1 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -100,9 +100,10 @@ AssocTyDefn: AssocTyDefn = { }; OpaqueTyDefn: OpaqueTyDefn = { - "opaque" "type" ":" > "=" ";" => { + "opaque" "type" > ":" > "=" ";" => { OpaqueTyDefn { ty, + parameter_kinds: p, identifier, bounds: b, } diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index b8fe9546786..b19d5cd0518 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -517,10 +517,10 @@ pub struct ImplTraitDatum { pub impl_trait_id: ImplTraitId, /// Trait bounds for the opaque type. - pub bounds: Vec>, + pub bounds: Vec>, /// The "hidden type" that the opaque type is equal to when revealed. - pub ty: Ty, + pub ty: Binders>, } #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index c898f2bd15c..c8888a2d5ef 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -136,32 +136,34 @@ impl ToProgramClauses for ImplTraitDatum { substitution: builder.substitution_in_scope(), }); - // AliasEq(T<..> = HiddenTy) :- Reveal. - builder.push_clause( - DomainGoal::Holds( + let alias_ty = Ty::new(interner, alias.clone()); + + builder.push_binders(&self.ty, |builder, impl_trait_datum| { + // AliasEq(T<..> = HiddenTy) :- Reveal. + builder.push_clause( + DomainGoal::Holds( + AliasEq { + alias: alias.clone(), + ty: impl_trait_datum.clone(), + } + .cast(interner), + ), + iter::once(DomainGoal::Reveal(())), + ); + + // AliasEq(T<..> = !T). + builder.push_fact(DomainGoal::Holds( AliasEq { alias: alias.clone(), - ty: self.ty.clone(), + ty: alias_ty.clone(), } .cast(interner), - ), - iter::once(DomainGoal::Reveal(())), - ); - - let alias_ty = Ty::new(interner, alias.clone()); - - // AliasEq(T<..> = !T). - builder.push_fact(DomainGoal::Holds( - AliasEq { - alias: alias.clone(), - ty: alias_ty.clone(), - } - .cast(interner), - )); + )); + }); for bound in &self.bounds { // Implemented(!T: Bound). - builder.push_fact(bound.as_trait_ref(interner, alias_ty.clone())); + builder.push_fact(bound.value.clone().into_well_formed_goal(interner)); } for auto_trait_id in builder.db.auto_traits() { @@ -173,7 +175,7 @@ impl ToProgramClauses for ImplTraitDatum { }, iter::once(TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, self.ty.clone()), + substitution: Substitution::from1(interner, self.ty.value.clone()), }), ); } From 8eb7922512daa1807ee21acb3f1c6e21a716c448 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 18 Mar 2020 17:09:34 +0100 Subject: [PATCH 27/42] Rename ImplTrait types to OpaqueTy --- chalk-integration/src/db.rs | 8 +-- chalk-integration/src/lib.rs | 2 +- chalk-integration/src/lowering.rs | 73 +++++++++++----------- chalk-integration/src/program.rs | 36 +++++------ chalk-ir/src/debug.rs | 41 ++++++------ chalk-ir/src/fold/boring_impls.rs | 2 +- chalk-ir/src/interner.rs | 40 ++++++------ chalk-ir/src/lib.rs | 19 +++--- chalk-ir/src/tls.rs | 14 ++--- chalk-ir/src/visit/boring_impls.rs | 4 +- chalk-ir/src/zip.rs | 8 +-- chalk-rust-ir/src/lib.rs | 8 +-- chalk-solve/src/clauses.rs | 14 ++--- chalk-solve/src/clauses/program_clauses.rs | 14 ++--- chalk-solve/src/lib.rs | 4 +- chalk-solve/src/solve/slg.rs | 16 ++--- chalk-solve/src/solve/slg/aggregate.rs | 30 ++++----- chalk-solve/src/split.rs | 6 +- chalk-solve/src/wf.rs | 4 +- 19 files changed, 171 insertions(+), 172 deletions(-) diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs index 3549d4f37a9..8169b8a9423 100644 --- a/chalk-integration/src/db.rs +++ b/chalk-integration/src/db.rs @@ -10,8 +10,8 @@ use chalk_ir::Canonical; use chalk_ir::ConstrainedSubst; use chalk_ir::Goal; use chalk_ir::ImplId; -use chalk_ir::ImplTraitId; use chalk_ir::InEnvironment; +use chalk_ir::OpaqueTyId; use chalk_ir::Parameter; use chalk_ir::ProgramClause; use chalk_ir::StructId; @@ -22,7 +22,7 @@ use chalk_rust_ir::AssociatedTyDatum; use chalk_rust_ir::AssociatedTyValue; use chalk_rust_ir::AssociatedTyValueId; use chalk_rust_ir::ImplDatum; -use chalk_rust_ir::ImplTraitDatum; +use chalk_rust_ir::OpaqueTyDatum; use chalk_rust_ir::StructDatum; use chalk_rust_ir::TraitDatum; use chalk_rust_ir::WellKnownTrait; @@ -106,8 +106,8 @@ impl RustIrDatabase for ChalkDatabase { self.program_ir().unwrap().associated_ty_values[&id].clone() } - fn impl_trait_data(&self, id: ImplTraitId) -> Arc> { - self.program_ir().unwrap().impl_trait_data(id) + fn opaque_ty_data(&self, id: OpaqueTyId) -> Arc> { + self.program_ir().unwrap().opaque_ty_data(id) } fn struct_datum(&self, id: StructId) -> Arc> { diff --git a/chalk-integration/src/lib.rs b/chalk-integration/src/lib.rs index e97af96c24a..2bb1c8d08a3 100644 --- a/chalk-integration/src/lib.rs +++ b/chalk-integration/src/lib.rs @@ -18,7 +18,7 @@ use chalk_ir::Binders; pub enum TypeSort { Struct, Trait, - ImplTrait, + Opaque, } #[derive(Clone, Debug, PartialEq, Eq, Hash)] diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index ff4073df0e1..fdc7f674845 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1,14 +1,12 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::ChalkIr; use chalk_ir::{ - self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, ImplTraitId, + self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, QuantifiedWhereClauses, StructId, Substitution, TraitId, }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; -use chalk_rust_ir::{ - Anonymize, AssociatedTyValueId, ImplTraitDatum, IntoWhereClauses, ToParameter, -}; +use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, ToParameter}; use lalrpop_intern::intern; use std::collections::BTreeMap; use std::sync::Arc; @@ -19,7 +17,7 @@ use crate::{Identifier as Ident, RawId, TypeKind, TypeSort}; type StructIds = BTreeMap>; type TraitIds = BTreeMap>; -type ImplTraitIds = BTreeMap>; +type OpaqueTyIds = BTreeMap>; type StructKinds = BTreeMap, TypeKind>; type TraitKinds = BTreeMap, TypeKind>; type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId, Ident), AssociatedTyLookup>; @@ -35,7 +33,7 @@ struct Env<'k> { struct_kinds: &'k StructKinds, trait_ids: &'k TraitIds, trait_kinds: &'k TraitKinds, - impl_trait_ids: &'k ImplTraitIds, + opaque_ty_ids: &'k OpaqueTyIds, associated_ty_lookups: &'k AssociatedTyLookups, /// Parameter identifiers are used as keys, therefore /// all identifiers in an environment must be unique (no shadowing). @@ -70,7 +68,7 @@ struct AssociatedTyLookup { enum TypeLookup { Struct(chalk_ir::StructId), Parameter(BoundVar), - ImplTrait(chalk_ir::ImplTraitId), + Opaque(chalk_ir::OpaqueTyId), } enum LifetimeLookup { @@ -93,8 +91,8 @@ impl<'k> Env<'k> { return Ok(TypeLookup::Struct(*id)); } - if let Some(id) = self.impl_trait_ids.get(&name.str) { - return Ok(TypeLookup::ImplTrait(*id)); + if let Some(id) = self.opaque_ty_ids.get(&name.str) { + return Ok(TypeLookup::Opaque(*id)); } if let Some(_) = self.trait_ids.get(&name.str) { return Err(RustIrError::NotStruct(name)); @@ -231,10 +229,10 @@ impl LowerProgram for Program { let mut struct_ids = BTreeMap::new(); let mut trait_ids = BTreeMap::new(); - let mut impl_trait_ids = BTreeMap::new(); + let mut opaque_ty_ids = BTreeMap::new(); let mut struct_kinds = BTreeMap::new(); let mut trait_kinds = BTreeMap::new(); - let mut impl_trait_kinds = BTreeMap::new(); + let mut opaque_ty_kinds = BTreeMap::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { match item { Item::StructDefn(defn) => { @@ -251,9 +249,9 @@ impl LowerProgram for Program { } Item::OpaqueTyDefn(defn) => { let type_kind = defn.lower_type_kind()?; - let id = ImplTraitId(raw_id); - impl_trait_ids.insert(defn.identifier.str, id); - impl_trait_kinds.insert(id, type_kind); + let id = OpaqueTyId(raw_id); + opaque_ty_ids.insert(defn.identifier.str, id); + opaque_ty_kinds.insert(id, type_kind); } Item::Impl(_) => continue, Item::Clause(_) => continue, @@ -266,7 +264,7 @@ impl LowerProgram for Program { let mut impl_data = BTreeMap::new(); let mut associated_ty_data = BTreeMap::new(); let mut associated_ty_values = BTreeMap::new(); - let mut impl_trait_data = BTreeMap::new(); + let mut opaque_ty_data = BTreeMap::new(); let mut custom_clauses = Vec::new(); for (item, &raw_id) in self.items.iter().zip(&raw_ids) { let empty_env = Env { @@ -274,7 +272,7 @@ impl LowerProgram for Program { struct_kinds: &struct_kinds, trait_ids: &trait_ids, trait_kinds: &trait_kinds, - impl_trait_ids: &impl_trait_ids, + opaque_ty_ids: &opaque_ty_ids, associated_ty_lookups: &associated_ty_lookups, parameter_map: BTreeMap::new(), }; @@ -380,7 +378,7 @@ impl LowerProgram for Program { custom_clauses.extend(clause.lower_clause(&empty_env)?); } Item::OpaqueTyDefn(ref opaque_ty) => { - if let Some(&value) = impl_trait_ids.get(&opaque_ty.identifier.str) { + if let Some(&value) = opaque_ty_ids.get(&opaque_ty.identifier.str) { let parameter_kinds = opaque_ty .parameter_kinds .iter() @@ -390,10 +388,10 @@ impl LowerProgram for Program { let binders = empty_env .in_binders(parameter_kinds, |env| opaque_ty.ty.lower(&env))?; - impl_trait_data.insert( + opaque_ty_data.insert( value, - Arc::new(ImplTraitDatum { - impl_trait_id: value, + Arc::new(OpaqueTyDatum { + opaque_ty_id: value, bounds: opaque_ty .bounds .lower(&empty_env)? @@ -401,8 +399,11 @@ impl LowerProgram for Program { .flat_map(|qil| { qil.into_where_clauses( empty_env.interner(), - chalk_ir::TyData::BoundVar(0) - .intern(empty_env.interner()), + chalk_ir::TyData::BoundVar(BoundVar::new( + DebruijnIndex::INNERMOST, + todo!(), + )) + .intern(empty_env.interner()), ) }) .collect(), @@ -425,8 +426,8 @@ impl LowerProgram for Program { impl_data, associated_ty_values, associated_ty_data, - impl_trait_ids, - impl_trait_data, + opaque_ty_ids, + opaque_ty_data, custom_clauses, }; @@ -606,12 +607,12 @@ impl LowerTypeKind for TraitDefn { impl LowerTypeKind for OpaqueTyDefn { fn lower_type_kind(&self) -> LowerResult { Ok(TypeKind { - sort: TypeSort::ImplTrait, + sort: TypeSort::Opaque, name: self.identifier.str, - binders: chalk_ir::Binders { - binders: vec![], //TODO do we need binders here? - value: (), - }, + binders: chalk_ir::Binders::new( + vec![], //TODO do we need binders here? + (), + ), }) } } @@ -1059,12 +1060,12 @@ impl LowerTy for Ty { } } TypeLookup::Parameter(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)), - TypeLookup::ImplTrait(id) => Ok(chalk_ir::TyData::Alias( - chalk_ir::AliasTy::ImplTrait(chalk_ir::ImplTraitTy { - impl_trait_id: id, + TypeLookup::Opaque(id) => Ok(chalk_ir::TyData::Alias(chalk_ir::AliasTy::Opaque( + chalk_ir::OpaqueTy { + opaque_ty_id: id, substitution: chalk_ir::Substitution::empty(interner), - }), - ) + }, + )) .intern(interner)), }, @@ -1094,7 +1095,7 @@ impl LowerTy for Ty { Ty::Apply { name, ref args } => { let id = match env.lookup_type(name)? { TypeLookup::Struct(id) => id, - TypeLookup::Parameter(_) | TypeLookup::ImplTrait(_) => { + TypeLookup::Parameter(_) | TypeLookup::Opaque(_) => { Err(RustIrError::CannotApplyTypeParameter(name))? } }; @@ -1363,7 +1364,7 @@ impl LowerGoal for Goal { let env = Env { struct_ids: &program.struct_ids, trait_ids: &program.trait_ids, - impl_trait_ids: &program.impl_trait_ids, + opaque_ty_ids: &program.opaque_ty_ids, struct_kinds: &program.struct_kinds, trait_kinds: &program.trait_kinds, associated_ty_lookups: &associated_ty_lookups, diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index d7840ca245d..04038e5dab2 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -4,12 +4,12 @@ use chalk_ir::debug::Angle; use chalk_ir::interner::ChalkIr; use chalk_ir::tls; use chalk_ir::{ - debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, - ImplTraitId, ImplTraitTy, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, - ProgramClauses, ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, + debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime, + OpaqueTy, OpaqueTyId, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, + ProjectionTy, StructId, Substitution, TraitId, Ty, TypeName, }; use chalk_rust_ir::{ - AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplTraitDatum, ImplType, + AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, OpaqueTyDatum, StructDatum, TraitDatum, WellKnownTrait, }; use chalk_solve::split::Split; @@ -42,11 +42,11 @@ pub struct Program { pub associated_ty_values: BTreeMap, Arc>>, - // From `impl Trait` name to item-id. Used during lowering only. - pub impl_trait_ids: BTreeMap>, + // From opaque type name to item-id. Used during lowering only. + pub opaque_ty_ids: BTreeMap>, - /// For each `impl Trait` type: - pub impl_trait_data: BTreeMap, Arc>>, + /// For each opaque type: + pub opaque_ty_data: BTreeMap, Arc>>, /// For each trait: pub trait_data: BTreeMap, Arc>>, @@ -115,16 +115,16 @@ impl tls::DebugContext for Program { } } - fn debug_impl_trait_id( + fn debug_opaque_ty_id( &self, - impl_trait_id: ImplTraitId, + opaque_ty_id: OpaqueTyId, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { - if let Some(d) = self.impl_trait_data.get(&impl_trait_id) { + if let Some(d) = self.opaque_ty_data.get(&opaque_ty_id) { write!(fmt, "{:?}", d.bounds) } else { fmt.debug_struct("InvalidItemId") - .field("index", &impl_trait_id.0) + .field("index", &opaque_ty_id.0) .finish() } } @@ -136,7 +136,7 @@ impl tls::DebugContext for Program { ) -> Result<(), fmt::Error> { match alias_ty { AliasTy::Projection(projection_ty) => self.debug_projection_ty(projection_ty, fmt), - AliasTy::ImplTrait(impl_trait_ty) => self.debug_impl_trait_ty(impl_trait_ty, fmt), + AliasTy::Opaque(opaque_ty) => self.debug_opaque_ty(opaque_ty, fmt), } } @@ -157,12 +157,12 @@ impl tls::DebugContext for Program { ) } - fn debug_impl_trait_ty( + fn debug_opaque_ty( &self, - impl_trait_ty: &ImplTraitTy, + opaque_ty: &OpaqueTy, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { - write!(fmt, "impl {:?}", impl_trait_ty.impl_trait_id) + write!(fmt, "impl {:?}", opaque_ty.opaque_ty_id) } fn debug_ty(&self, ty: &Ty, fmt: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { @@ -294,8 +294,8 @@ impl RustIrDatabase for Program { self.associated_ty_values[&id].clone() } - fn impl_trait_data(&self, id: ImplTraitId) -> Arc> { - self.impl_trait_data[&id].clone() + fn opaque_ty_data(&self, id: OpaqueTyId) -> Arc> { + self.opaque_ty_data[&id].clone() } fn struct_datum(&self, id: StructId) -> Arc> { diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index f538e9c132c..bcb6c7630b7 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -96,18 +96,18 @@ impl Debug for QuantifiedWhereClauses { } } -impl Debug for ImplTraitTy { +impl Debug for ProjectionTy { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - I::debug_impl_trait_ty(self, fmt).unwrap_or_else(|| { - unimplemented!("cannot format ImplTraitTy without setting Program in tls") + I::debug_projection_ty(self, fmt).unwrap_or_else(|| { + unimplemented!("cannot format ProjectionTy without setting Program in tls") }) } } -impl Debug for ProjectionTy { +impl Debug for OpaqueTy { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - I::debug_projection_ty(self, fmt).unwrap_or_else(|| { - unimplemented!("cannot format ProjectionTy without setting Program in tls") + I::debug_opaque_ty(self, fmt).unwrap_or_else(|| { + unimplemented!("cannot format OpaqueTy without setting Program in tls") }) } } @@ -118,10 +118,9 @@ impl Display for Substitution { } } -impl Debug for ImplTraitId { +impl Debug for OpaqueTyId { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - I::debug_impl_trait_id(*self, fmt) - .unwrap_or_else(|| write!(fmt, "ImplTraitId({:?})", self.0)) + I::debug_opaque_ty_id(*self, fmt).unwrap_or_else(|| write!(fmt, "OpaqueTyId({:?})", self.0)) } } @@ -142,7 +141,7 @@ impl Debug for TypeName { match self { TypeName::Struct(id) => write!(fmt, "{:?}", id), TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty), - TypeName::ImplTrait(impl_trait) => write!(fmt, "{:?}", impl_trait), + TypeName::OpaqueType(opaque_ty) => write!(fmt, "{:?}", opaque_ty), TypeName::Error => write!(fmt, "{{error}}"), } } @@ -481,30 +480,30 @@ impl ProjectionTy { } } -pub struct ImplTraitTyDebug<'a, I: Interner> { - impl_trait_ty: &'a ImplTraitTy, +pub struct OpaqueTyDebug<'a, I: Interner> { + opaque_ty: &'a OpaqueTy, interner: &'a I, } -impl<'a, I: Interner> Debug for ImplTraitTyDebug<'a, I> { +impl<'a, I: Interner> Debug for OpaqueTyDebug<'a, I> { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - let ImplTraitTyDebug { - impl_trait_ty, + let OpaqueTyDebug { + opaque_ty, interner, } = self; write!( fmt, "{:?}{:?}", - impl_trait_ty.impl_trait_id, - impl_trait_ty.substitution.with_angle(interner) + opaque_ty.opaque_ty_id, + opaque_ty.substitution.with_angle(interner) ) } } -impl ImplTraitTy { - pub fn debug<'a>(&'a self, interner: &'a I) -> ImplTraitTyDebug<'a, I> { - ImplTraitTyDebug { - impl_trait_ty: self, +impl OpaqueTy { + pub fn debug<'a>(&'a self, interner: &'a I) -> OpaqueTyDebug<'a, I> { + OpaqueTyDebug { + opaque_ty: self, interner, } } diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs index 13dc18917fe..558ee96c395 100644 --- a/chalk-ir/src/fold/boring_impls.rs +++ b/chalk-ir/src/fold/boring_impls.rs @@ -271,7 +271,7 @@ id_fold!(ImplId); id_fold!(StructId); id_fold!(TraitId); id_fold!(AssocTypeId); -id_fold!(ImplTraitId); +id_fold!(OpaqueTyId); impl> SuperFold for ProgramClauseData { fn super_fold_with<'i>( diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs index 2dd31912ac3..5bc210fb48b 100644 --- a/chalk-ir/src/interner.rs +++ b/chalk-ir/src/interner.rs @@ -4,10 +4,10 @@ use crate::AssocTypeId; use crate::Goal; use crate::GoalData; use crate::Goals; -use crate::ImplTraitId; -use crate::ImplTraitTy; use crate::Lifetime; use crate::LifetimeData; +use crate::OpaqueTy; +use crate::OpaqueTyId; use crate::Parameter; use crate::ParameterData; use crate::ProgramClause; @@ -173,15 +173,15 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } - /// Prints the debug representation of an `impl trait`. To get good + /// Prints the debug representation of an opaque type. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific type-family (and hence /// fully known types). /// /// Returns `None` to fallback to the default debug output (e.g., /// if no info about current program is available from TLS). - fn debug_impl_trait_id( - impl_trait_id: ImplTraitId, + fn debug_opaque_ty_id( + opaque_ty_id: OpaqueTyId, fmt: &mut fmt::Formatter<'_>, ) -> Option; @@ -197,27 +197,27 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash { None } - /// Prints the debug representation of an ImplTraitTy. To get good + /// Prints the debug representation of a ProjectionTy. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific interner (and hence /// fully known types). /// /// Returns `None` to fallback to the default debug output (e.g., /// if no info about current program is available from TLS). - fn debug_impl_trait_ty( - impl_trait_ty: &ImplTraitTy, + fn debug_projection_ty( + projection_ty: &ProjectionTy, fmt: &mut fmt::Formatter<'_>, ) -> Option; - /// Prints the debug representation of a ProjectionTy. To get good + /// Prints the debug representation of an OpaqueTy. To get good /// results, this requires inspecting TLS, and is difficult to /// code without reference to a specific interner (and hence /// fully known types). /// /// Returns `None` to fallback to the default debug output (e.g., /// if no info about current program is available from TLS). - fn debug_projection_ty( - projection_ty: &ProjectionTy, + fn debug_opaque_ty( + opaque_ty: &OpaqueTy, fmt: &mut fmt::Formatter<'_>, ) -> Option; @@ -574,11 +574,11 @@ mod default { tls::with_current_program(|prog| Some(prog?.debug_assoc_type_id(id, fmt))) } - fn debug_impl_trait_id( - id: ImplTraitId, + fn debug_opaque_ty_id( + id: OpaqueTyId, fmt: &mut fmt::Formatter<'_>, ) -> Option { - tls::with_current_program(|prog| Some(prog?.debug_impl_trait_id(id, fmt))) + tls::with_current_program(|prog| Some(prog?.debug_opaque_ty_id(id, fmt))) } fn debug_alias( @@ -588,18 +588,18 @@ mod default { tls::with_current_program(|prog| Some(prog?.debug_alias(alias, fmt))) } - fn debug_impl_trait_ty( - impl_trait_ty: &ImplTraitTy, + fn debug_projection_ty( + proj: &ProjectionTy, fmt: &mut fmt::Formatter<'_>, ) -> Option { - tls::with_current_program(|prog| Some(prog?.debug_impl_trait_ty(impl_trait_ty, fmt))) + tls::with_current_program(|prog| Some(prog?.debug_projection_ty(proj, fmt))) } - fn debug_projection_ty( - proj: &ProjectionTy, + fn debug_opaque_ty( + opaque_ty: &OpaqueTy, fmt: &mut fmt::Formatter<'_>, ) -> Option { - tls::with_current_program(|prog| Some(prog?.debug_projection_ty(proj, fmt))) + tls::with_current_program(|prog| Some(prog?.debug_opaque_ty(opaque_ty, fmt))) } fn debug_ty(ty: &Ty, fmt: &mut fmt::Formatter<'_>) -> Option { diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 4b997222483..042ace29dc0 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -114,8 +114,8 @@ pub enum TypeName { /// an associated type like `Iterator::Item`; see `AssociatedType` for details AssociatedType(AssocTypeId), - /// a placeholder for some type like `impl Trait` - ImplTrait(ImplTraitId), + /// a placeholder for opaque types like `impl Trait` + OpaqueType(OpaqueTyId), /// This can be used to represent an error, e.g. during name resolution of a type. /// Chalk itself will not produce this, just pass it through when given. @@ -180,7 +180,7 @@ pub struct ClauseId(pub I::DefId); pub struct AssocTypeId(pub I::DefId); #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct ImplTraitId(pub I::DefId); +pub struct OpaqueTyId(pub I::DefId); impl_debugs!(ImplId, ClauseId); @@ -846,7 +846,7 @@ impl ParameterData { #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub enum AliasTy { Projection(ProjectionTy), - ImplTrait(ImplTraitTy), + Opaque(OpaqueTy), } impl AliasTy { @@ -874,8 +874,8 @@ pub struct ProjectionTy { } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] -pub struct ImplTraitTy { - pub impl_trait_id: ImplTraitId, +pub struct OpaqueTy { + pub opaque_ty_id: OpaqueTyId, pub substitution: Substitution, } @@ -1151,10 +1151,9 @@ impl DomainGoal { pub fn inputs(&self, interner: &I) -> Vec> { match self { - DomainGoal::Holds(WhereClause::ProjectionEq(proj_eq)) => vec![ParameterKind::Ty( - AliasTy::Projection(proj_eq.projection.clone()).intern(interner), - ) - .intern(interner)], + DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { + vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern(interner)] + } _ => Vec::new(), } } diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs index 3fc99d0d062..40cb40b6ee2 100644 --- a/chalk-ir/src/tls.rs +++ b/chalk-ir/src/tls.rs @@ -1,8 +1,8 @@ use crate::interner::ChalkIr; use crate::{ - debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplTraitId, - ImplTraitTy, Lifetime, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, - ProjectionTy, QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, + debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime, OpaqueTy, + OpaqueTyId, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy, + QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty, }; use std::cell::RefCell; use std::fmt; @@ -31,9 +31,9 @@ pub trait DebugContext { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; - fn debug_impl_trait_id( + fn debug_opaque_ty_id( &self, - id: ImplTraitId, + id: OpaqueTyId, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; @@ -43,9 +43,9 @@ pub trait DebugContext { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; - fn debug_impl_trait_ty( + fn debug_opaque_ty( &self, - impl_trait_ty: &ImplTraitTy, + opaque_ty: &OpaqueTy, fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error>; diff --git a/chalk-ir/src/visit/boring_impls.rs b/chalk-ir/src/visit/boring_impls.rs index 8e9d36d8d7e..c2c4d01e240 100644 --- a/chalk-ir/src/visit/boring_impls.rs +++ b/chalk-ir/src/visit/boring_impls.rs @@ -5,7 +5,7 @@ //! The more interesting impls of `Visit` remain in the `visit` module. use crate::{ - AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, ImplTraitId, Interner, Parameter, + AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, Interner, OpaqueTyId, Parameter, ParameterKind, PlaceholderIndex, ProgramClause, ProgramClauseData, ProgramClauses, QuantifiedWhereClauses, QuantifierKind, StructId, Substitution, SuperVisit, TraitId, UniverseIndex, Visit, VisitResult, Visitor, @@ -229,7 +229,7 @@ macro_rules! id_visit { id_visit!(ImplId); id_visit!(StructId); id_visit!(TraitId); -id_visit!(ImplTraitId); +id_visit!(OpaqueTyId); id_visit!(AssocTypeId); impl SuperVisit for ProgramClause { diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 26080b3114f..81467eced21 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -196,7 +196,7 @@ macro_rules! eq_zip { eq_zip!(I => StructId); eq_zip!(I => TraitId); eq_zip!(I => AssocTypeId); -eq_zip!(I => ImplTraitId); +eq_zip!(I => OpaqueTyId); eq_zip!(I => TypeName); eq_zip!(I => QuantifierKind); eq_zip!(I => PhantomData); @@ -247,8 +247,8 @@ struct_zip!(impl[I: Interner] Zip for ProjectionTy { associated_ty_id, substitution }); -struct_zip!(impl[I: Interner] Zip for ImplTraitTy { - impl_trait_id, +struct_zip!(impl[I: Interner] Zip for OpaqueTy { + opaque_ty_id, substitution }); @@ -345,7 +345,7 @@ enum_zip!(impl for DomainGoal { Reveal, }); enum_zip!(impl for ProgramClauseData { Implies, ForAll }); -enum_zip!(impl for AliasTy { Projection, ImplTrait }); +enum_zip!(impl for AliasTy { Projection, Opaque }); impl Zip for Substitution { fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index b19d5cd0518..46ca8ad0399 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -9,8 +9,8 @@ use chalk_ir::cast::Cast; use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ - AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, ImplTraitId, - LifetimeData, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, + AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, + OpaqueTyId, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -512,9 +512,9 @@ pub struct AssociatedTyValueBound { /// opaque type T: A + B = HiddenTy; /// ``` #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold)] -pub struct ImplTraitDatum { +pub struct OpaqueTyDatum { /// The placeholder `!T` that corresponds to the opaque type `T`. - pub impl_trait_id: ImplTraitId, + pub opaque_ty_id: OpaqueTyId, /// Trait bounds for the opaque type. pub bounds: Vec>, diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index a67ee57c914..38f885cdf58 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -272,8 +272,8 @@ fn program_clauses_that_could_match( AliasTy::Projection(proj) => db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - AliasTy::ImplTrait(impl_trait) => db - .impl_trait_data(impl_trait.impl_trait_id) + AliasTy::Opaque(opaque_ty) => db + .opaque_ty_data(opaque_ty.opaque_ty_id) .to_program_clauses(builder), }, DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { @@ -321,7 +321,7 @@ fn program_clauses_that_could_match( trait_parameters, ); } - AliasTy::ImplTrait(_) => (), + AliasTy::Opaque(_) => (), }, DomainGoal::LocalImplAllowed(trait_ref) => db .trait_datum(trait_ref.trait_id) @@ -402,9 +402,9 @@ fn match_ty( .db .associated_ty_data(proj.associated_ty_id) .to_program_clauses(builder), - TyData::Alias(AliasTy::ImplTrait(impl_trait)) => builder + TyData::Alias(AliasTy::Opaque(opaque_ty)) => builder .db - .impl_trait_data(impl_trait.impl_trait_id) + .opaque_ty_data(opaque_ty.opaque_ty_id) .to_program_clauses(builder), TyData::Function(quantified_ty) => { builder.push_fact(WellFormed::Ty(ty.clone())); @@ -423,9 +423,9 @@ fn match_ty( fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeName) { match name { TypeName::Struct(struct_id) => match_struct(builder, struct_id), - TypeName::ImplTrait(impl_trait_id) => builder + TypeName::OpaqueType(opaque_ty_id) => builder .db - .impl_trait_data(impl_trait_id) + .opaque_ty_data(opaque_ty_id) .to_program_clauses(builder), TypeName::Error => {} TypeName::AssociatedType(type_id) => builder diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index c8888a2d5ef..0ae1a6d3bbc 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -118,7 +118,7 @@ impl ToProgramClauses for AssociatedTyValue { } } -impl ToProgramClauses for ImplTraitDatum { +impl ToProgramClauses for OpaqueTyDatum { /// Given `opaque type T<..>: A + B = HiddenTy;`, we generate: /// /// ```notrust @@ -131,20 +131,20 @@ impl ToProgramClauses for ImplTraitDatum { /// where `!T` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); - let alias = AliasTy::ImplTrait(ImplTraitTy { - impl_trait_id: self.impl_trait_id, + let alias = AliasTy::Opaque(OpaqueTy { + opaque_ty_id: self.opaque_ty_id, substitution: builder.substitution_in_scope(), }); let alias_ty = Ty::new(interner, alias.clone()); - builder.push_binders(&self.ty, |builder, impl_trait_datum| { + builder.push_binders(&self.ty, |builder, opaque_ty_datum| { // AliasEq(T<..> = HiddenTy) :- Reveal. builder.push_clause( DomainGoal::Holds( AliasEq { alias: alias.clone(), - ty: impl_trait_datum.clone(), + ty: opaque_ty_datum.clone(), } .cast(interner), ), @@ -163,7 +163,7 @@ impl ToProgramClauses for ImplTraitDatum { for bound in &self.bounds { // Implemented(!T: Bound). - builder.push_fact(bound.value.clone().into_well_formed_goal(interner)); + builder.push_fact(bound.skip_binders().clone().into_well_formed_goal(interner)); } for auto_trait_id in builder.db.auto_traits() { @@ -175,7 +175,7 @@ impl ToProgramClauses for ImplTraitDatum { }, iter::once(TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, self.ty.value.clone()), + substitution: Substitution::from1(interner, self.ty.skip_binders().clone()), }), ); } diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index 696a89bbaa4..26e7c84dc04 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -40,8 +40,8 @@ pub trait RustIrDatabase: Debug { /// Returns the `AssociatedTyValue` with the given id. fn associated_ty_value(&self, id: AssociatedTyValueId) -> Arc>; - /// Returns the `ImplTraitDatum` with the given id. - fn impl_trait_data(&self, id: ImplTraitId) -> Arc>; + /// Returns the `OpaqueTyDatum` with the given id. + fn opaque_ty_data(&self, id: OpaqueTyId) -> Arc>; /// If `id` is a struct id, returns `Some(id)` (but cast to `StructId`). fn as_struct_id(&self, id: &TypeName) -> Option>; diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index 7c0ac4d6e26..146e7dcceb8 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -514,9 +514,9 @@ impl MayInvalidate<'_, I> { ) => self.aggregate_projection_tys(proj1, proj2), ( - TyData::Alias(AliasTy::ImplTrait(impl_trait1)), - TyData::Alias(AliasTy::ImplTrait(impl_trait2)), - ) => self.aggregate_impl_trait_tys(impl_trait1, impl_trait2), + TyData::Alias(AliasTy::Opaque(opaque_ty1)), + TyData::Alias(AliasTy::Opaque(opaque_ty2)), + ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2), // For everything else, be conservative here and just say we may invalidate. (TyData::Function(_), _) @@ -583,13 +583,13 @@ impl MayInvalidate<'_, I> { ) } - fn aggregate_impl_trait_tys(&mut self, new: &ImplTraitTy, current: &ImplTraitTy) -> bool { - let ImplTraitTy { - impl_trait_id: new_name, + fn aggregate_opaque_ty_tys(&mut self, new: &OpaqueTy, current: &OpaqueTy) -> bool { + let OpaqueTy { + opaque_ty_id: new_name, substitution: new_substitution, } = new; - let ImplTraitTy { - impl_trait_id: current_name, + let OpaqueTy { + opaque_ty_id: current_name, substitution: current_substitution, } = current; diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs index d77fa18280a..dcf9ad9f891 100644 --- a/chalk-solve/src/solve/slg/aggregate.rs +++ b/chalk-solve/src/solve/slg/aggregate.rs @@ -245,9 +245,9 @@ impl AntiUnifier<'_, '_, I> { ) => self.aggregate_projection_tys(proj1, proj2), ( - TyData::Alias(AliasTy::ImplTrait(impl_trait1)), - TyData::Alias(AliasTy::ImplTrait(impl_trait2)), - ) => self.aggregate_impl_trait_tys(impl_trait1, impl_trait2), + TyData::Alias(AliasTy::Opaque(opaque_ty1)), + TyData::Alias(AliasTy::Opaque(opaque_ty2)), + ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2), (TyData::Placeholder(placeholder1), TyData::Placeholder(placeholder2)) => { self.aggregate_placeholder_tys(placeholder1, placeholder2) @@ -325,24 +325,24 @@ impl AntiUnifier<'_, '_, I> { .unwrap_or_else(|| self.new_variable()) } - fn aggregate_impl_trait_tys( + fn aggregate_opaque_ty_tys( &mut self, - impl_trait1: &ImplTraitTy, - impl_trait2: &ImplTraitTy, + opaque_ty1: &OpaqueTy, + opaque_ty2: &OpaqueTy, ) -> Ty { - let ImplTraitTy { - impl_trait_id: name1, + let OpaqueTy { + opaque_ty_id: name1, substitution: substitution1, - } = impl_trait1; - let ImplTraitTy { - impl_trait_id: name2, + } = opaque_ty1; + let OpaqueTy { + opaque_ty_id: name2, substitution: substitution2, - } = impl_trait2; + } = opaque_ty2; self.aggregate_name_and_substs(name1, substitution1, name2, substitution2) - .map(|(&impl_trait_id, substitution)| { - TyData::Alias(AliasTy::ImplTrait(ImplTraitTy { - impl_trait_id, + .map(|(&opaque_ty_id, substitution)| { + TyData::Alias(AliasTy::Opaque(OpaqueTy { + opaque_ty_id, substitution, })) .intern(self.interner) diff --git a/chalk-solve/src/split.rs b/chalk-solve/src/split.rs index 0c01afa4343..1a93a0a2db2 100644 --- a/chalk-solve/src/split.rs +++ b/chalk-solve/src/split.rs @@ -137,9 +137,9 @@ pub trait Split: RustIrDatabase { let (impl_parameters, atv_parameters) = self.split_associated_ty_value_parameters(¶meters, associated_ty_value); let trait_ref = { - let impl_trait_ref = impl_datum.binders.map_ref(|b| &b.trait_ref); - debug!("impl_trait_ref: {:?}", impl_trait_ref); - impl_trait_ref.substitute(interner, impl_parameters) + let opaque_ty_ref = impl_datum.binders.map_ref(|b| &b.trait_ref); + debug!("opaque_ty_ref: {:?}", opaque_ty_ref); + opaque_ty_ref.substitute(interner, impl_parameters) }; // Create the parameters for the projection -- in our example diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 856cba91a98..a22d5966f46 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -108,9 +108,9 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { proj.visit_with(self, outer_binder); } - TyData::Alias(AliasTy::ImplTrait(impl_trait)) => { + TyData::Alias(AliasTy::Opaque(opaque_ty)) => { push_ty(); - impl_trait.visit_with(self, outer_binder); + opaque_ty.visit_with(self, outer_binder); } TyData::Placeholder(_) => { From afabe97e6f0f5d9503c22b137f7897c77c2e0740 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Fri, 20 Mar 2020 16:26:42 +0100 Subject: [PATCH 28/42] Introduce OpaqueTyBound --- chalk-integration/src/lowering.rs | 60 ++++++++++++++-------- chalk-integration/src/program.rs | 2 +- chalk-rust-ir/src/lib.rs | 12 +++-- chalk-solve/src/clauses/program_clauses.rs | 9 ++-- 4 files changed, 53 insertions(+), 30 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index fdc7f674845..c71a7c06382 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -6,7 +6,9 @@ use chalk_ir::{ }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; -use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, ToParameter}; +use chalk_rust_ir::{ + Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyBound, OpaqueTyDatum, ToParameter, +}; use lalrpop_intern::intern; use std::collections::BTreeMap; use std::sync::Arc; @@ -378,36 +380,50 @@ impl LowerProgram for Program { custom_clauses.extend(clause.lower_clause(&empty_env)?); } Item::OpaqueTyDefn(ref opaque_ty) => { - if let Some(&value) = opaque_ty_ids.get(&opaque_ty.identifier.str) { + if let Some(&opaque_ty_id) = opaque_ty_ids.get(&opaque_ty.identifier.str) { let parameter_kinds = opaque_ty .parameter_kinds .iter() .map(|k| k.lower()) .collect::>(); - let binders = empty_env - .in_binders(parameter_kinds, |env| opaque_ty.ty.lower(&env))?; + let binders = empty_env.in_binders(parameter_kinds, |env| { + let hidden_ty = opaque_ty.ty.lower(&env)?; + + let hidden_ty_bounds: chalk_ir::Binders>> = + env.in_binders( + Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), + |env1| { + let interner = env1.interner(); + Ok(opaque_ty + .bounds + .lower(&env1)? + .iter() + .flat_map(|qil| { + qil.into_where_clauses( + interner, + chalk_ir::TyData::BoundVar(BoundVar::new( + DebruijnIndex::INNERMOST, + todo!(), + )) + .intern(interner), + ) + }) + .collect()) + }, + )?; + + Ok(OpaqueTyBound { + hidden_ty, + bounds: hidden_ty_bounds.skip_binders().clone(), + }) + })?; opaque_ty_data.insert( - value, + opaque_ty_id, Arc::new(OpaqueTyDatum { - opaque_ty_id: value, - bounds: opaque_ty - .bounds - .lower(&empty_env)? - .iter() - .flat_map(|qil| { - qil.into_where_clauses( - empty_env.interner(), - chalk_ir::TyData::BoundVar(BoundVar::new( - DebruijnIndex::INNERMOST, - todo!(), - )) - .intern(empty_env.interner()), - ) - }) - .collect(), - ty: binders, + opaque_ty_id, + bound: binders, }), ); } diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 04038e5dab2..9985b79347a 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -121,7 +121,7 @@ impl tls::DebugContext for Program { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { if let Some(d) = self.opaque_ty_data.get(&opaque_ty_id) { - write!(fmt, "{:?}", d.bounds) + write!(fmt, "{:?}", d.bound) } else { fmt.debug_struct("InvalidItemId") .field("index", &opaque_ty_id.0) diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index 46ca8ad0399..91087c2a487 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -516,11 +516,17 @@ pub struct OpaqueTyDatum { /// The placeholder `!T` that corresponds to the opaque type `T`. pub opaque_ty_id: OpaqueTyId, + /// The type bound to when revealed. + pub bound: Binders>, +} + +#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)] +pub struct OpaqueTyBound { + /// The value for the "hidden type" for `opaque type Foo = ...` + pub hidden_ty: Ty, + /// Trait bounds for the opaque type. pub bounds: Vec>, - - /// The "hidden type" that the opaque type is equal to when revealed. - pub ty: Binders>, } #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 0ae1a6d3bbc..6ce2ed203ab 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -138,13 +138,13 @@ impl ToProgramClauses for OpaqueTyDatum { let alias_ty = Ty::new(interner, alias.clone()); - builder.push_binders(&self.ty, |builder, opaque_ty_datum| { + builder.push_binders(&self.bound, |builder, opaque_ty_bound| { // AliasEq(T<..> = HiddenTy) :- Reveal. builder.push_clause( DomainGoal::Holds( AliasEq { alias: alias.clone(), - ty: opaque_ty_datum.clone(), + ty: opaque_ty_bound.hidden_ty.clone(), } .cast(interner), ), @@ -161,7 +161,8 @@ impl ToProgramClauses for OpaqueTyDatum { )); }); - for bound in &self.bounds { + let opaque_ty_bound = &self.bound.skip_binders(); + for bound in &opaque_ty_bound.bounds { // Implemented(!T: Bound). builder.push_fact(bound.skip_binders().clone().into_well_formed_goal(interner)); } @@ -175,7 +176,7 @@ impl ToProgramClauses for OpaqueTyDatum { }, iter::once(TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, self.ty.skip_binders().clone()), + substitution: Substitution::from1(interner, opaque_ty_bound.hidden_ty.clone()), }), ); } From 3ba75879d1f18ec2bf07372b79397a030edf0202 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 1 Apr 2020 07:37:24 +0200 Subject: [PATCH 29/42] Use correct lowering for the hidden type --- chalk-integration/src/lowering.rs | 38 ++++++++++++------------------- 1 file changed, 15 insertions(+), 23 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index c71a7c06382..7eb3faea350 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1,7 +1,7 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::ChalkIr; use chalk_ir::{ - self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, + self, AssocTypeId, Binders, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, QuantifiedWhereClauses, StructId, Substitution, TraitId, }; use chalk_parse::ast::*; @@ -390,28 +390,20 @@ impl LowerProgram for Program { let binders = empty_env.in_binders(parameter_kinds, |env| { let hidden_ty = opaque_ty.ty.lower(&env)?; - let hidden_ty_bounds: chalk_ir::Binders>> = - env.in_binders( - Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), - |env1| { - let interner = env1.interner(); - Ok(opaque_ty - .bounds - .lower(&env1)? - .iter() - .flat_map(|qil| { - qil.into_where_clauses( - interner, - chalk_ir::TyData::BoundVar(BoundVar::new( - DebruijnIndex::INNERMOST, - todo!(), - )) - .intern(interner), - ) - }) - .collect()) - }, - )?; + let hidden_ty_bounds: Binders>> = env.in_binders( + Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), + |env1| { + let interner = env1.interner(); + Ok(opaque_ty + .bounds + .lower(&env1)? + .iter() + .flat_map(|qil| { + qil.into_where_clauses(interner, hidden_ty.clone()) + }) + .collect()) + }, + )?; Ok(OpaqueTyBound { hidden_ty, From ca0ae089e36c3ada74d24c4f5ecc03a3a8cf3232 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 1 Apr 2020 07:59:04 +0200 Subject: [PATCH 30/42] Write placeholder with type parameters in docs --- chalk-solve/src/clauses/program_clauses.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 6ce2ed203ab..b55d475646b 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -123,12 +123,12 @@ impl ToProgramClauses for OpaqueTyDatum { /// /// ```notrust /// AliasEq(T<..> = HiddenTy) :- Reveal. - /// AliasEq(T<..> = !T). - /// Implemented(!T: A). - /// Implemented(!T: B). - /// Implemented(!T: Send) :- Implemented(HiddenTy: Send). // For all auto traits + /// AliasEq(T<..> = !T<..>). + /// Implemented(!T<..>: A). + /// Implemented(!T<..>: B). + /// Implemented(!T<..>: Send) :- Implemented(HiddenTy: Send). // For all auto traits /// ``` - /// where `!T` is the placeholder for the unnormalized type `T<..>`. + /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); let alias = AliasTy::Opaque(OpaqueTy { @@ -151,7 +151,7 @@ impl ToProgramClauses for OpaqueTyDatum { iter::once(DomainGoal::Reveal(())), ); - // AliasEq(T<..> = !T). + // AliasEq(T<..> = !T<..>). builder.push_fact(DomainGoal::Holds( AliasEq { alias: alias.clone(), @@ -163,12 +163,12 @@ impl ToProgramClauses for OpaqueTyDatum { let opaque_ty_bound = &self.bound.skip_binders(); for bound in &opaque_ty_bound.bounds { - // Implemented(!T: Bound). + // Implemented(!T<..>: Bound). builder.push_fact(bound.skip_binders().clone().into_well_formed_goal(interner)); } for auto_trait_id in builder.db.auto_traits() { - // Implemented(!T: AutoTrait) :- Implemented(HiddenTy: AutoTrait). + // Implemented(!T<..>: AutoTrait) :- Implemented(HiddenTy: AutoTrait). builder.push_clause( TraitRef { trait_id: auto_trait_id, From 24041fe22f010a26882877523d675e5838929bec Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 1 Apr 2020 08:14:58 +0200 Subject: [PATCH 31/42] Use opaque TypeName instead of alias itself --- chalk-solve/src/clauses/program_clauses.rs | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index b55d475646b..f872c842907 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -131,12 +131,20 @@ impl ToProgramClauses for OpaqueTyDatum { /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { let interner = builder.interner(); + let substitution = builder.substitution_in_scope(); let alias = AliasTy::Opaque(OpaqueTy { opaque_ty_id: self.opaque_ty_id, - substitution: builder.substitution_in_scope(), + substitution: substitution.clone(), }); - let alias_ty = Ty::new(interner, alias.clone()); + let alias_ty = Ty::new( + interner, + ApplicationTy { + name: TypeName::OpaqueType(self.opaque_ty_id), + substitution, + } + .cast(interner), + ); builder.push_binders(&self.bound, |builder, opaque_ty_bound| { // AliasEq(T<..> = HiddenTy) :- Reveal. From 0a9369834860352a77259a78f53161a7703ace46 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 2 Apr 2020 15:41:03 +0200 Subject: [PATCH 32/42] Change test to be correct --- tests/test/existential_types.rs | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index d53046ec6d3..e97a4d86030 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -6,23 +6,31 @@ use super::*; fn opaque_bounds() { test! { program { - trait Trait { } + trait Direct { } + trait Indirect { } struct Ty { } - impl Trait for Ty { } + impl Direct for Ty { } + impl Indirect for Ty { } - opaque type T: Trait = Ty; + opaque type T: Direct = Ty; + } + + goal { + T: Direct + } yields { + "Unique; substitution []" } goal { if (Reveal) { - T: Trait + T: Indirect } } yields { "Unique; substitution []" } goal { - T: Trait + T: Indirect } yields { "No possible solution" } From 202d8032c76d58204d28b88f28262f0dfa1ec5e9 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Sun, 5 Apr 2020 10:14:26 +0200 Subject: [PATCH 33/42] Lower opaque type kind --- chalk-integration/src/lowering.rs | 6 ++--- chalk-solve/src/clauses/program_clauses.rs | 3 +-- tests/test/existential_types.rs | 27 +++++++++++++++------- 3 files changed, 22 insertions(+), 14 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 7eb3faea350..96d03107ccf 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -614,13 +614,11 @@ impl LowerTypeKind for TraitDefn { impl LowerTypeKind for OpaqueTyDefn { fn lower_type_kind(&self) -> LowerResult { + let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect(); Ok(TypeKind { sort: TypeSort::Opaque, name: self.identifier.str, - binders: chalk_ir::Binders::new( - vec![], //TODO do we need binders here? - (), - ), + binders: chalk_ir::Binders::new(binders.anonymize(), ()), }) } } diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index f872c842907..d40cdb048a5 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -142,8 +142,7 @@ impl ToProgramClauses for OpaqueTyDatum { ApplicationTy { name: TypeName::OpaqueType(self.opaque_ty_id), substitution, - } - .cast(interner), + }, ); builder.push_binders(&self.bound, |builder, opaque_ty_bound| { diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index e97a4d86030..edb4e53eae8 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -6,31 +6,42 @@ use super::*; fn opaque_bounds() { test! { program { - trait Direct { } - trait Indirect { } struct Ty { } - impl Direct for Ty { } - impl Indirect for Ty { } - opaque type T: Direct = Ty; + trait Clone { } + opaque type T: Clone = Ty; } goal { - T: Direct + T: Clone } yields { "Unique; substitution []" } + } +} + +#[test] +fn opaque_reveal() { + test! { + program { + struct Ty { } + trait Trait { } + impl Trait for Ty { } + + trait Clone { } + opaque type T: Clone = Ty; + } goal { if (Reveal) { - T: Indirect + T: Trait } } yields { "Unique; substitution []" } goal { - T: Indirect + T: Trait } yields { "No possible solution" } From be9f62a34f2f03e215f49e3b2a45bef6d7ae2f77 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Mon, 6 Apr 2020 22:27:14 +0200 Subject: [PATCH 34/42] Add binders to OpaqueTyDatumBound bounds --- chalk-integration/src/lowering.rs | 48 ++++++++++++---------- chalk-rust-ir/src/lib.rs | 6 +-- chalk-solve/src/clauses/program_clauses.rs | 44 +++++++++++--------- 3 files changed, 55 insertions(+), 43 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 96d03107ccf..855697d4576 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1,13 +1,14 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::ChalkIr; use chalk_ir::{ - self, AssocTypeId, Binders, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, + self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, QuantifiedWhereClauses, StructId, Substitution, TraitId, }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; use chalk_rust_ir::{ - Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyBound, OpaqueTyDatum, ToParameter, + Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound, + ToParameter, }; use lalrpop_intern::intern; use std::collections::BTreeMap; @@ -390,25 +391,30 @@ impl LowerProgram for Program { let binders = empty_env.in_binders(parameter_kinds, |env| { let hidden_ty = opaque_ty.ty.lower(&env)?; - let hidden_ty_bounds: Binders>> = env.in_binders( - Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), - |env1| { - let interner = env1.interner(); - Ok(opaque_ty - .bounds - .lower(&env1)? - .iter() - .flat_map(|qil| { - qil.into_where_clauses(interner, hidden_ty.clone()) - }) - .collect()) - }, - )?; - - Ok(OpaqueTyBound { - hidden_ty, - bounds: hidden_ty_bounds.skip_binders().clone(), - }) + let bounds: chalk_ir::Binders>> = env + .in_binders( + Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), + |env1| { + let interner = env1.interner(); + Ok(opaque_ty + .bounds + .lower(&env1)? + .iter() + .flat_map(|qil| { + qil.into_where_clauses( + interner, + chalk_ir::TyData::BoundVar(BoundVar::new( + DebruijnIndex::INNERMOST, + 0, + )) + .intern(interner), + ) + }) + .collect()) + }, + )?; + + Ok(OpaqueTyDatumBound { hidden_ty, bounds }) })?; opaque_ty_data.insert( diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index 91087c2a487..01096b6e374 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -517,16 +517,16 @@ pub struct OpaqueTyDatum { pub opaque_ty_id: OpaqueTyId, /// The type bound to when revealed. - pub bound: Binders>, + pub bound: Binders>, } #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)] -pub struct OpaqueTyBound { +pub struct OpaqueTyDatumBound { /// The value for the "hidden type" for `opaque type Foo = ...` pub hidden_ty: Ty, /// Trait bounds for the opaque type. - pub bounds: Vec>, + pub bounds: Binders>>, } #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index d40cdb048a5..99d4b99910a 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -166,27 +166,33 @@ impl ToProgramClauses for OpaqueTyDatum { } .cast(interner), )); - }); - let opaque_ty_bound = &self.bound.skip_binders(); - for bound in &opaque_ty_bound.bounds { - // Implemented(!T<..>: Bound). - builder.push_fact(bound.skip_binders().clone().into_well_formed_goal(interner)); - } + for bound in &opaque_ty_bound.bounds { + // Implemented(!T<..>: Bound). + builder.push_binders(&bound, |builder, bound| { + builder.push_binders(&bound, |builder, bound| { + builder.push_fact(bound.into_well_formed_goal(interner)); + }); + }); + } - for auto_trait_id in builder.db.auto_traits() { - // Implemented(!T<..>: AutoTrait) :- Implemented(HiddenTy: AutoTrait). - builder.push_clause( - TraitRef { - trait_id: auto_trait_id, - substitution: Substitution::from1(interner, alias_ty.clone()), - }, - iter::once(TraitRef { - trait_id: auto_trait_id, - substitution: Substitution::from1(interner, opaque_ty_bound.hidden_ty.clone()), - }), - ); - } + for auto_trait_id in builder.db.auto_traits() { + // Implemented(!T<..>: AutoTrait) :- Implemented(HiddenTy: AutoTrait). + builder.push_clause( + TraitRef { + trait_id: auto_trait_id, + substitution: Substitution::from1(interner, alias_ty.clone()), + }, + iter::once(TraitRef { + trait_id: auto_trait_id, + substitution: Substitution::from1( + interner, + opaque_ty_bound.hidden_ty.clone(), + ), + }), + ); + } + }); } } From b5f04ad21a04fc36a1f89c299cf35386d0ad1af8 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 14 Apr 2020 13:41:12 +0200 Subject: [PATCH 35/42] Move substitution into push_binders --- chalk-integration/src/lowering.rs | 5 +++ chalk-solve/src/clauses/program_clauses.rs | 42 +++++++++++----------- 2 files changed, 27 insertions(+), 20 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 855697d4576..02e4d782a3b 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -388,9 +388,13 @@ impl LowerProgram for Program { .map(|k| k.lower()) .collect::>(); + // Introduce the parameters declared on the opaque type definition. + // So if we have `type Foo = impl Trait`, this would introduce `P1..Pn` let binders = empty_env.in_binders(parameter_kinds, |env| { let hidden_ty = opaque_ty.ty.lower(&env)?; + // Introduce a variable to represent the hidden "self type". This will be used in the bounds. + // So the `impl Trait` will be lowered to `exists { Self: Trait }`. let bounds: chalk_ir::Binders>> = env .in_binders( Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))), @@ -401,6 +405,7 @@ impl LowerProgram for Program { .lower(&env1)? .iter() .flat_map(|qil| { + // Instantiate the bounds with the innermost bound variable, which represents Self, as the self type. qil.into_where_clauses( interner, chalk_ir::TyData::BoundVar(BoundVar::new( diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 99d4b99910a..82e3487ceda 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -130,22 +130,22 @@ impl ToProgramClauses for OpaqueTyDatum { /// ``` /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { - let interner = builder.interner(); - let substitution = builder.substitution_in_scope(); - let alias = AliasTy::Opaque(OpaqueTy { - opaque_ty_id: self.opaque_ty_id, - substitution: substitution.clone(), - }); + builder.push_binders(&self.bound, |builder, opaque_ty_bound| { + let interner = builder.interner(); + let substitution = builder.substitution_in_scope(); + let alias = AliasTy::Opaque(OpaqueTy { + opaque_ty_id: self.opaque_ty_id, + substitution: substitution.clone(), + }); - let alias_ty = Ty::new( - interner, - ApplicationTy { - name: TypeName::OpaqueType(self.opaque_ty_id), - substitution, - }, - ); + let alias_placeholder_ty = Ty::new( + interner, + ApplicationTy { + name: TypeName::OpaqueType(self.opaque_ty_id), + substitution, + }, + ); - builder.push_binders(&self.bound, |builder, opaque_ty_bound| { // AliasEq(T<..> = HiddenTy) :- Reveal. builder.push_clause( DomainGoal::Holds( @@ -162,17 +162,19 @@ impl ToProgramClauses for OpaqueTyDatum { builder.push_fact(DomainGoal::Holds( AliasEq { alias: alias.clone(), - ty: alias_ty.clone(), + ty: alias_placeholder_ty.clone(), } .cast(interner), )); for bound in &opaque_ty_bound.bounds { // Implemented(!T<..>: Bound). - builder.push_binders(&bound, |builder, bound| { - builder.push_binders(&bound, |builder, bound| { - builder.push_fact(bound.into_well_formed_goal(interner)); - }); + let bound_with_placeholder_ty = bound.substitute( + interner, + &Substitution::from1(interner, alias_placeholder_ty.clone()), + ); + builder.push_binders(&bound_with_placeholder_ty, |builder, bound| { + builder.push_fact(bound.into_well_formed_goal(interner)); }); } @@ -181,7 +183,7 @@ impl ToProgramClauses for OpaqueTyDatum { builder.push_clause( TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, alias_ty.clone()), + substitution: Substitution::from1(interner, alias_placeholder_ty.clone()), }, iter::once(TraitRef { trait_id: auto_trait_id, From 31c558525a257cfaf04d42765c30089234421d14 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 14 Apr 2020 20:29:19 +0200 Subject: [PATCH 36/42] Match program clauses for opaque placeholder --- chalk-solve/src/clauses.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 38f885cdf58..a55ceb6639d 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -258,6 +258,14 @@ fn program_clauses_that_could_match( }); } + if let TyData::Apply(ApplicationTy { + name: TypeName::OpaqueType(opaque_ty_id), + .. + }) = self_ty.data(interner) + { + db.opaque_ty_data(*opaque_ty_id).to_program_clauses(builder); + } + if let Some(well_known) = trait_datum.well_known { builtin_traits::add_builtin_program_clauses( db, From fe1839392e0a768ddb7cabf4a2b4ec691a23f28f Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Tue, 14 Apr 2020 21:38:14 +0200 Subject: [PATCH 37/42] Improve debug output --- chalk-integration/src/program.rs | 2 +- chalk-solve/src/clauses/program_clauses.rs | 8 +++----- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 9985b79347a..35383e92871 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -121,7 +121,7 @@ impl tls::DebugContext for Program { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { if let Some(d) = self.opaque_ty_data.get(&opaque_ty_id) { - write!(fmt, "{:?}", d.bound) + write!(fmt, "{:?}", d.bound.value.hidden_ty) } else { fmt.debug_struct("InvalidItemId") .field("index", &opaque_ty_id.0) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 82e3487ceda..b89987102fb 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -167,12 +167,10 @@ impl ToProgramClauses for OpaqueTyDatum { .cast(interner), )); + let substitution = Substitution::from1(interner, alias_placeholder_ty.clone()); for bound in &opaque_ty_bound.bounds { // Implemented(!T<..>: Bound). - let bound_with_placeholder_ty = bound.substitute( - interner, - &Substitution::from1(interner, alias_placeholder_ty.clone()), - ); + let bound_with_placeholder_ty = bound.substitute(interner, &substitution); builder.push_binders(&bound_with_placeholder_ty, |builder, bound| { builder.push_fact(bound.into_well_formed_goal(interner)); }); @@ -183,7 +181,7 @@ impl ToProgramClauses for OpaqueTyDatum { builder.push_clause( TraitRef { trait_id: auto_trait_id, - substitution: Substitution::from1(interner, alias_placeholder_ty.clone()), + substitution: substitution.clone(), }, iter::once(TraitRef { trait_id: auto_trait_id, From 657d371e4e0a01ed7adc85cc979d36790d43f1a8 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 14 Apr 2020 19:43:33 +0000 Subject: [PATCH 38/42] also add program clauses for the alias version of opaque type --- chalk-solve/src/clauses.rs | 17 +++++++++++------ chalk-solve/src/clauses/program_clauses.rs | 1 + 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index a55ceb6639d..2aa21df0a66 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -145,6 +145,8 @@ fn program_clauses_that_could_match( let interner = db.interner(); let builder = &mut ClauseBuilder::new(db, clauses); + debug_heading!("program_clauses_that_could_match(goal={:?})", goal); + match goal { DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { let trait_id = trait_ref.trait_id; @@ -258,12 +260,15 @@ fn program_clauses_that_could_match( }); } - if let TyData::Apply(ApplicationTy { - name: TypeName::OpaqueType(opaque_ty_id), - .. - }) = self_ty.data(interner) - { - db.opaque_ty_data(*opaque_ty_id).to_program_clauses(builder); + match self_ty.data(interner) { + TyData::Apply(ApplicationTy { + name: TypeName::OpaqueType(opaque_ty_id), + .. + }) + | TyData::Alias(AliasTy::Opaque(OpaqueTy { opaque_ty_id, .. })) => { + db.opaque_ty_data(*opaque_ty_id).to_program_clauses(builder); + } + _ => {} } if let Some(well_known) = trait_datum.well_known { diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index b89987102fb..cbbcf73e1b4 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -130,6 +130,7 @@ impl ToProgramClauses for OpaqueTyDatum { /// ``` /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) { + debug_heading!("to_program_clauses({:?})", self); builder.push_binders(&self.bound, |builder, opaque_ty_bound| { let interner = builder.interner(); let substitution = builder.substitution_in_scope(); From d0b3a66b904dcc308ddf6f355b339de05f1c8ccf Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 14 Apr 2020 19:45:56 +0000 Subject: [PATCH 39/42] don't push the well-formed goal, push the implemented goal --- chalk-solve/src/clauses/program_clauses.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index cbbcf73e1b4..89113f4cf80 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -173,7 +173,7 @@ impl ToProgramClauses for OpaqueTyDatum { // Implemented(!T<..>: Bound). let bound_with_placeholder_ty = bound.substitute(interner, &substitution); builder.push_binders(&bound_with_placeholder_ty, |builder, bound| { - builder.push_fact(bound.into_well_formed_goal(interner)); + builder.push_fact(bound); }); } From 9017856beb054ce2cb47608ad9f8d9a9b8a2a60a Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Apr 2020 17:08:07 +0200 Subject: [PATCH 40/42] Fix build after rebase --- chalk-integration/src/program.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 35383e92871..e73f52abd3b 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -121,7 +121,7 @@ impl tls::DebugContext for Program { fmt: &mut fmt::Formatter<'_>, ) -> Result<(), fmt::Error> { if let Some(d) = self.opaque_ty_data.get(&opaque_ty_id) { - write!(fmt, "{:?}", d.bound.value.hidden_ty) + write!(fmt, "{:?}", d.bound.skip_binders().hidden_ty) } else { fmt.debug_struct("InvalidItemId") .field("index", &opaque_ty_id.0) From 41121bf17e700f0ece71fe2ac0015aebd46b06c9 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Wed, 15 Apr 2020 17:19:52 +0200 Subject: [PATCH 41/42] Fix visitor --- chalk-solve/src/wf.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index a22d5966f46..018c4236b89 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -75,10 +75,11 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> { fn visit_where_clause(&mut self, where_clause: &WhereClause, outer_binder: DebruijnIndex) { match where_clause { - WhereClause::AliasEq(alias_eq) => { - alias_eq.alias.visit_with(self, outer_binder); - alias_eq.ty.visit_with(self, outer_binder); - } + WhereClause::AliasEq(alias_eq) => alias_eq + .alias + .clone() + .intern(self.interner) + .visit_with(self, outer_binder), WhereClause::Implemented(trait_ref) => { trait_ref.visit_with(self, outer_binder); } From d5a8faea335cd5e3e9b86157c3bec9d07acda0e3 Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Thu, 16 Apr 2020 14:28:18 +0200 Subject: [PATCH 42/42] Avoid enumerating traits for auto traits rules --- chalk-integration/src/db.rs | 4 ---- chalk-integration/src/program.rs | 8 -------- chalk-solve/src/clauses/program_clauses.rs | 17 ----------------- chalk-solve/src/lib.rs | 3 --- 4 files changed, 32 deletions(-) diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs index 8169b8a9423..6961906b86f 100644 --- a/chalk-integration/src/db.rs +++ b/chalk-integration/src/db.rs @@ -153,8 +153,4 @@ impl RustIrDatabase for ChalkDatabase { fn interner(&self) -> &ChalkIr { &ChalkIr } - - fn auto_traits(&self) -> Vec> { - self.program_ir().unwrap().auto_traits() - } } diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index e73f52abd3b..55d62709acd 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -363,12 +363,4 @@ impl RustIrDatabase for Program { fn interner(&self) -> &ChalkIr { &ChalkIr } - - fn auto_traits(&self) -> Vec> { - self.trait_data - .iter() - .filter(|(_, auto_trait)| auto_trait.is_auto_trait()) - .map(|(trait_id, _)| *trait_id) - .collect() - } } diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 89113f4cf80..3ffe1f8dbdf 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -176,23 +176,6 @@ impl ToProgramClauses for OpaqueTyDatum { builder.push_fact(bound); }); } - - for auto_trait_id in builder.db.auto_traits() { - // Implemented(!T<..>: AutoTrait) :- Implemented(HiddenTy: AutoTrait). - builder.push_clause( - TraitRef { - trait_id: auto_trait_id, - substitution: substitution.clone(), - }, - iter::once(TraitRef { - trait_id: auto_trait_id, - substitution: Substitution::from1( - interner, - opaque_ty_bound.hidden_ty.clone(), - ), - }), - ); - } }); } } diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index 26e7c84dc04..e5e4676fbc5 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -88,9 +88,6 @@ pub trait RustIrDatabase: Debug { fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> Option>; fn interner(&self) -> &I; - - /// Returns the ids of all auto traits. - fn auto_traits(&self) -> Vec>; } pub use solve::Guidance;