Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Impl Trait #324

Merged
merged 42 commits into from
Apr 16, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
42 commits
Select commit Hold shift + click to select a range
f474280
Make AliasTy an enum of Projection, ImplTrait and TypeAlias
detrumi Jan 14, 2020
27180ee
Parse impl trait
detrumi Jan 15, 2020
34b8e97
Rename AliasEq back to ProjectionEq
detrumi Jan 15, 2020
b5ae61c
Remove TypeAlias from enum for now
detrumi Jan 15, 2020
5465e59
Allow impl trait items in ast
detrumi Jan 15, 2020
c3459fb
Revert adding AliasTy to ast
detrumi Jan 20, 2020
a4d9b99
Add ImplTraitId
detrumi Jan 20, 2020
d446354
Implement lowering for impl trait
detrumi Jan 20, 2020
f2047b2
Create clauses from ImplTraitDatum
detrumi Jan 21, 2020
b513e4a
Generate auto trait clauses for impl trait
detrumi Jan 21, 2020
a3b01ac
Remove ImplTrait indirection in AliasTy
detrumi Jan 21, 2020
f337c0f
Debug impls
detrumi Jan 21, 2020
cccfac7
Remove unused trait
detrumi Jan 21, 2020
8565901
Re-introduce ImplTraitTy to include substitution
detrumi Jan 23, 2020
72d4e7a
aggregate_tys for impl trait
detrumi Jan 23, 2020
001d8df
visit_alias_ty for impl trait
detrumi Jan 23, 2020
207f839
Fill in match_type_name for ImplTrait
detrumi Jan 23, 2020
d7dac17
Introduce AliasEq
detrumi Jan 24, 2020
8ed2794
Change ast defn to opaque type
detrumi Feb 14, 2020
c30bf22
Fix debug impl for ImplTraitTy
detrumi Feb 17, 2020
d6480b8
Generate AliasEq rules and introduce Reveal
detrumi Feb 26, 2020
c015b46
Improve clause generation for impl trait
detrumi Mar 1, 2020
1e2161c
Complete test by testing Reveal in goal
detrumi Mar 2, 2020
5fb73c0
Fix tests
detrumi Mar 2, 2020
5d39e9a
Improve generated rule for auto traits
detrumi Mar 11, 2020
a34a041
Quantify bounds and add binders
detrumi Mar 11, 2020
8eb7922
Rename ImplTrait types to OpaqueTy
detrumi Mar 18, 2020
afabe97
Introduce OpaqueTyBound
detrumi Mar 20, 2020
3ba7587
Use correct lowering for the hidden type
detrumi Apr 1, 2020
ca0ae08
Write placeholder with type parameters in docs
detrumi Apr 1, 2020
24041fe
Use opaque TypeName instead of alias itself
detrumi Apr 1, 2020
0a93698
Change test to be correct
detrumi Apr 2, 2020
202d803
Lower opaque type kind
detrumi Apr 5, 2020
be9f62a
Add binders to OpaqueTyDatumBound bounds
detrumi Apr 6, 2020
b5f04ad
Move substitution into push_binders
detrumi Apr 14, 2020
31c5585
Match program clauses for opaque placeholder
detrumi Apr 14, 2020
fe18393
Improve debug output
detrumi Apr 14, 2020
657d371
also add program clauses for the alias version of opaque type
nikomatsakis Apr 14, 2020
d0b3a66
don't push the well-formed goal, push the implemented goal
nikomatsakis Apr 14, 2020
9017856
Fix build after rebase
detrumi Apr 15, 2020
41121bf
Fix visitor
detrumi Apr 15, 2020
d5a8fae
Avoid enumerating traits for auto traits rules
detrumi Apr 16, 2020
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 7 additions & 9 deletions book/src/types/rust_types.md
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ evaluated. For example, when typing the body of a generic function
like `fn foo<T: Iterator>`, 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.

Expand Down Expand Up @@ -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> { 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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 `<T as Iterator>::Item`
but also `impl Trait` types and named type aliases like `type Foo<X> = Vec<X>`.
but also `impl Trait` types and named type aliases like `type Foo<X> = Vec<X>`.

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
Expand Down
6 changes: 6 additions & 0 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ use chalk_ir::ConstrainedSubst;
use chalk_ir::Goal;
use chalk_ir::ImplId;
use chalk_ir::InEnvironment;
use chalk_ir::OpaqueTyId;
use chalk_ir::Parameter;
use chalk_ir::ProgramClause;
use chalk_ir::StructId;
Expand All @@ -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::OpaqueTyDatum;
use chalk_rust_ir::StructDatum;
use chalk_rust_ir::TraitDatum;
use chalk_rust_ir::WellKnownTrait;
Expand Down Expand Up @@ -104,6 +106,10 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
self.program_ir().unwrap().associated_ty_values[&id].clone()
}

fn opaque_ty_data(&self, id: OpaqueTyId<ChalkIr>) -> Arc<OpaqueTyDatum<ChalkIr>> {
self.program_ir().unwrap().opaque_ty_data(id)
}

fn struct_datum(&self, id: StructId<ChalkIr>) -> Arc<StructDatum<ChalkIr>> {
self.program_ir().unwrap().struct_datum(id)
}
Expand Down
1 change: 1 addition & 0 deletions chalk-integration/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use chalk_ir::Binders;
pub enum TypeSort {
Struct,
Trait,
Opaque,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
Expand Down
133 changes: 114 additions & 19 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,15 @@
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, OpaqueTyId,
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, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound,
ToParameter,
};
use lalrpop_intern::intern;
use std::collections::BTreeMap;
use std::sync::Arc;
Expand All @@ -17,6 +20,7 @@ use crate::{Identifier as Ident, RawId, TypeKind, TypeSort};

type StructIds = BTreeMap<Ident, chalk_ir::StructId<ChalkIr>>;
type TraitIds = BTreeMap<Ident, chalk_ir::TraitId<ChalkIr>>;
type OpaqueTyIds = BTreeMap<Ident, chalk_ir::OpaqueTyId<ChalkIr>>;
type StructKinds = BTreeMap<chalk_ir::StructId<ChalkIr>, TypeKind>;
type TraitKinds = BTreeMap<chalk_ir::TraitId<ChalkIr>, TypeKind>;
type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
Expand All @@ -32,6 +36,7 @@ struct Env<'k> {
struct_kinds: &'k StructKinds,
trait_ids: &'k TraitIds,
trait_kinds: &'k TraitKinds,
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).
Expand Down Expand Up @@ -66,6 +71,7 @@ struct AssociatedTyLookup {
enum TypeLookup {
Struct(chalk_ir::StructId<ChalkIr>),
Parameter(BoundVar),
Opaque(chalk_ir::OpaqueTyId<ChalkIr>),
}

enum LifetimeLookup {
Expand All @@ -88,6 +94,9 @@ impl<'k> Env<'k> {
return Ok(TypeLookup::Struct(*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));
}
Expand Down Expand Up @@ -223,8 +232,10 @@ impl LowerProgram for Program {

let mut struct_ids = BTreeMap::new();
let mut 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 opaque_ty_kinds = BTreeMap::new();
for (item, &raw_id) in self.items.iter().zip(&raw_ids) {
match item {
Item::StructDefn(defn) => {
Expand All @@ -239,6 +250,12 @@ impl LowerProgram for Program {
trait_ids.insert(type_kind.name, id);
trait_kinds.insert(id, type_kind);
}
Item::OpaqueTyDefn(defn) => {
let type_kind = defn.lower_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,
};
Expand All @@ -250,13 +267,15 @@ 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 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 {
struct_ids: &struct_ids,
struct_kinds: &struct_kinds,
trait_ids: &trait_ids,
trait_kinds: &trait_kinds,
opaque_ty_ids: &opaque_ty_ids,
associated_ty_lookups: &associated_ty_lookups,
parameter_map: BTreeMap::new(),
};
Expand Down Expand Up @@ -361,6 +380,57 @@ impl LowerProgram for Program {
Item::Clause(ref clause) => {
custom_clauses.extend(clause.lower_clause(&empty_env)?);
}
Item::OpaqueTyDefn(ref opaque_ty) => {
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::<Vec<_>>();

// Introduce the parameters declared on the opaque type definition.
// So if we have `type Foo<P1..Pn> = impl Trait<T1..Tn>`, 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<T1..Tn>` will be lowered to `exists<Self> { Self: Trait<T1..Tn> }`.
let bounds: chalk_ir::Binders<Vec<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| {
// 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(
DebruijnIndex::INNERMOST,
0,
))
.intern(interner),
)
})
.collect())
},
)?;

Ok(OpaqueTyDatumBound { hidden_ty, bounds })
})?;

opaque_ty_data.insert(
opaque_ty_id,
Arc::new(OpaqueTyDatum {
opaque_ty_id,
bound: binders,
}),
);
}
}
}
}

Expand All @@ -375,6 +445,8 @@ impl LowerProgram for Program {
impl_data,
associated_ty_values,
associated_ty_data,
opaque_ty_ids,
opaque_ty_data,
custom_clauses,
};

Expand Down Expand Up @@ -551,6 +623,17 @@ impl LowerTypeKind for TraitDefn {
}
}

impl LowerTypeKind for OpaqueTyDefn {
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
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(binders.anonymize(), ()),
})
}
}

impl LowerWhereClauses for TraitDefn {
fn where_clauses(&self) -> &[QuantifiedWhereClause] {
&self.where_clauses
Expand Down Expand Up @@ -582,7 +665,7 @@ trait LowerWhereClause<T> {
/// 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<Item = U>` which lowers to
/// `Implemented(T: Foo)` and `AliasEq(<T as Foo>::Item = U)`.
/// `Implemented(T: Foo)` and `ProjectionEq(<T as Foo>::Item = U)`.
fn lower(&self, env: &Env) -> LowerResult<Vec<T>>;
}

Expand All @@ -592,12 +675,12 @@ impl LowerWhereClause<chalk_ir::WhereClause<ChalkIr>> for WhereClause {
WhereClause::Implemented { trait_ref } => {
vec![chalk_ir::WhereClause::Implemented(trait_ref.lower(env)?)]
}
WhereClause::AliasEq { alias, ty } => vec![
WhereClause::ProjectionEq { projection, ty } => vec![
chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq {
alias: alias.lower(env)?,
alias: chalk_ir::AliasTy::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)
Expand All @@ -624,9 +707,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)?,
})]
}
Expand Down Expand Up @@ -656,6 +739,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)
}
Expand Down Expand Up @@ -915,13 +999,13 @@ impl LowerTraitFlags for TraitFlags {
}
}

trait LowerAliasTy {
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::AliasTy<ChalkIr>>;
trait LowerProjectionTy {
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::ProjectionTy<ChalkIr>>;
}

impl LowerAliasTy for AliasTy {
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::AliasTy<ChalkIr>> {
let AliasTy {
impl LowerProjectionTy for ProjectionTy {
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::ProjectionTy<ChalkIr>> {
let ProjectionTy {
ref trait_ref,
ref name,
ref args,
Expand Down Expand Up @@ -960,7 +1044,7 @@ impl LowerAliasTy for AliasTy {

args.extend(trait_substitution.iter(interner).cloned());

Ok(chalk_ir::AliasTy {
Ok(chalk_ir::ProjectionTy {
associated_ty_id: lookup.id,
substitution: chalk_ir::Substitution::from(interner, args),
})
Expand Down Expand Up @@ -993,6 +1077,13 @@ impl LowerTy for Ty {
}
}
TypeLookup::Parameter(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)),
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)),
},

Ty::Dyn { ref bounds } => Ok(chalk_ir::TyData::Dyn(chalk_ir::DynTy {
Expand Down Expand Up @@ -1021,7 +1112,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::Opaque(_) => {
Err(RustIrError::CannotApplyTypeParameter(name))?
}
};

let k = env.struct_kind(id);
Expand Down Expand Up @@ -1055,9 +1148,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,
Expand Down Expand Up @@ -1287,6 +1381,7 @@ impl LowerGoal<LoweredProgram> for Goal {
let env = Env {
struct_ids: &program.struct_ids,
trait_ids: &program.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,
Expand Down
Loading