Skip to content

Request hidden opaque types lazily #478

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

Merged
merged 2 commits into from
May 27, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
6 changes: 5 additions & 1 deletion chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use crate::{
use chalk_engine::forest::SubstitutionResult;
use chalk_ir::{
AdtId, AssocTypeId, Canonical, ConstrainedSubst, Environment, FnDefId, GenericArg, Goal,
ImplId, InEnvironment, OpaqueTyId, ProgramClause, ProgramClauses, TraitId, UCanonical,
ImplId, InEnvironment, OpaqueTyId, ProgramClause, ProgramClauses, TraitId, Ty, UCanonical,
};
use chalk_solve::rust_ir::{
AdtDatum, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, FnDefDatum, ImplDatum,
Expand Down Expand Up @@ -97,6 +97,10 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
self.program_ir().unwrap().opaque_ty_data(id)
}

fn hidden_opaque_type(&self, id: OpaqueTyId<ChalkIr>) -> Ty<ChalkIr> {
self.program_ir().unwrap().hidden_opaque_type(id)
}

fn adt_datum(&self, id: AdtId<ChalkIr>) -> Arc<AdtDatum<ChalkIr>> {
self.program_ir().unwrap().adt_datum(id)
}
Expand Down
5 changes: 4 additions & 1 deletion chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,7 @@ impl LowerProgram for Program {
let mut associated_ty_data = BTreeMap::new();
let mut associated_ty_values = BTreeMap::new();
let mut opaque_ty_data = BTreeMap::new();
let mut hidden_opaque_types = BTreeMap::new();
let mut custom_clauses = Vec::new();
for (item, &raw_id) in self.items.iter().zip(&raw_ids) {
let empty_env = Env {
Expand Down Expand Up @@ -500,6 +501,7 @@ impl LowerProgram for Program {
// So if we have `type Foo<P1..Pn> = impl Trait<T1..Tn>`, this would introduce `P1..Pn`
let binders = empty_env.in_binders(variable_kinds, |env| {
let hidden_ty = opaque_ty.ty.lower(&env)?;
hidden_opaque_types.insert(opaque_ty_id, Arc::new(hidden_ty));

// 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> }`.
Expand Down Expand Up @@ -530,7 +532,7 @@ impl LowerProgram for Program {
},
)?;

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

opaque_ty_data.insert(
Expand Down Expand Up @@ -562,6 +564,7 @@ impl LowerProgram for Program {
opaque_ty_ids,
opaque_ty_kinds,
opaque_ty_data,
hidden_opaque_types,
custom_clauses,
object_safe_traits,
};
Expand Down
7 changes: 7 additions & 0 deletions chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,9 @@ pub struct Program {
/// For each opaque type:
pub opaque_ty_data: BTreeMap<OpaqueTyId<ChalkIr>, Arc<OpaqueTyDatum<ChalkIr>>>,

/// Stores the hidden types for opaque types
pub hidden_opaque_types: BTreeMap<OpaqueTyId<ChalkIr>, Arc<Ty<ChalkIr>>>,

/// For each trait:
pub trait_data: BTreeMap<TraitId<ChalkIr>, Arc<TraitDatum<ChalkIr>>>,

Expand Down Expand Up @@ -336,6 +339,10 @@ impl RustIrDatabase<ChalkIr> for Program {
self.opaque_ty_data[&id].clone()
}

fn hidden_opaque_type(&self, id: OpaqueTyId<ChalkIr>) -> Ty<ChalkIr> {
(*self.hidden_opaque_types[&id]).clone()
}

fn adt_datum(&self, id: AdtId<ChalkIr>) -> Arc<AdtDatum<ChalkIr>> {
self.adt_data[&id].clone()
}
Expand Down
5 changes: 3 additions & 2 deletions chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -142,8 +142,9 @@ pub fn push_auto_trait_impls_opaque<I: Interner>(
1
);

let binders = opaque_ty_datum.bound.map_ref(|b| &b.hidden_ty);
builder.push_binders(&binders, |builder, hidden_ty| {
let hidden_ty = builder.db.hidden_opaque_type(opaque_id);
let binders = opaque_ty_datum.bound.clone();
builder.push_binders(&binders, |builder, _| {
let self_ty: Ty<_> = ApplicationTy {
name: opaque_id.cast(interner),
substitution: builder.substitution_in_scope(),
Expand Down
2 changes: 1 addition & 1 deletion chalk-solve/src/clauses/program_clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
DomainGoal::Holds(
AliasEq {
alias: alias.clone(),
ty: opaque_ty_bound.hidden_ty.clone(),
ty: builder.db.hidden_opaque_type(self.opaque_ty_id),
}
.cast(interner),
),
Expand Down
3 changes: 3 additions & 0 deletions chalk-solve/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
/// Returns the `OpaqueTyDatum` with the given id.
fn opaque_ty_data(&self, id: OpaqueTyId<I>) -> Arc<OpaqueTyDatum<I>>;

/// Returns the "hidden type" corresponding with the opaque type.
fn hidden_opaque_type(&self, id: OpaqueTyId<I>) -> Ty<I>;

/// Returns a list of potentially relevant impls for a given
/// trait-id; we also supply the type parameters that we are
/// trying to match (if known: these parameters may contain
Expand Down
3 changes: 0 additions & 3 deletions chalk-solve/src/rust_ir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -544,9 +544,6 @@ pub struct OpaqueTyDatum<I: Interner> {

#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)]
pub struct OpaqueTyDatumBound<I: Interner> {
/// The value for the "hidden type" for `opaque type Foo = ...`
pub hidden_ty: Ty<I>,

/// Trait bounds for the opaque type.
pub bounds: Binders<Vec<QuantifiedWhereClause<I>>>,
}
Expand Down
4 changes: 4 additions & 0 deletions tests/integration/panic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,10 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
unimplemented!()
}

fn hidden_opaque_type(&self, id: OpaqueTyId<ChalkIr>) -> Ty<ChalkIr> {
unimplemented!()
}

fn adt_datum(&self, id: AdtId<ChalkIr>) -> Arc<AdtDatum<ChalkIr>> {
unimplemented!()
}
Expand Down