Skip to content

Commit

Permalink
Merge pull request #468 from detrumi/opaque-auto-traits
Browse files Browse the repository at this point in the history
Generate auto trait clauses for opaque type goals
  • Loading branch information
nikomatsakis authored May 26, 2020
2 parents 215b9e1 + 39cb46b commit e5aaf83
Show file tree
Hide file tree
Showing 4 changed files with 110 additions and 3 deletions.
9 changes: 9 additions & 0 deletions chalk-ir/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,15 @@ where
}
}

impl<I> CastTo<TypeName<I>> for OpaqueTyId<I>
where
I: Interner,
{
fn cast_to(self, _interner: &I) -> TypeName<I> {
TypeName::OpaqueType(self)
}
}

impl<T> CastTo<T> for &T
where
T: Clone + HasInterner,
Expand Down
70 changes: 69 additions & 1 deletion chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,69 @@ pub fn push_auto_trait_impls<I: Interner>(
});
}

/// Leak auto traits for opaque types, just like `push_auto_trait_impls` does for structs.
///
/// For example, given the following program:
///
/// ```notrust
/// #[auto] trait Send { }
/// trait Trait { }
/// struct Bar { }
/// opaque type Foo: Trait = Bar
/// ```
/// Checking the goal `Foo: Send` would generate the following:
///
/// ```notrust
/// Foo: Send :- Bar: Send
/// ```
pub fn push_auto_trait_impls_opaque<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
auto_trait_id: TraitId<I>,
opaque_id: OpaqueTyId<I>,
) {
debug_heading!(
"push_auto_trait_impls_opaque({:?}, {:?})",
auto_trait_id,
opaque_id
);

let opaque_ty_datum = &builder.db.opaque_ty_data(opaque_id);
let interner = builder.interner();

// Must be an auto trait.
assert!(builder.db.trait_datum(auto_trait_id).is_auto_trait());

// Auto traits never have generic parameters of their own (apart from `Self`).
assert_eq!(
builder.db.trait_datum(auto_trait_id).binders.len(interner),
1
);

let binders = opaque_ty_datum.bound.map_ref(|b| &b.hidden_ty);
builder.push_binders(&binders, |builder, hidden_ty| {
let self_ty: Ty<_> = ApplicationTy {
name: opaque_id.cast(interner),
substitution: builder.substitution_in_scope(),
}
.intern(interner);

// trait_ref = `OpaqueType<...>: MyAutoTrait`
let auto_trait_ref = TraitRef {
trait_id: auto_trait_id,
substitution: Substitution::from1(interner, self_ty),
};

// OpaqueType<...>: MyAutoTrait :- HiddenType: MyAutoTrait
builder.push_clause(
auto_trait_ref,
std::iter::once(TraitRef {
trait_id: auto_trait_id,
substitution: Substitution::from1(interner, hidden_ty.clone()),
}),
);
});
}

/// Given some goal `goal` that must be proven, along with
/// its `environment`, figures out the program clauses that apply
/// to this goal from the Rust program. So for example if the goal
Expand Down Expand Up @@ -163,7 +226,12 @@ fn program_clauses_that_could_match<I: Interner>(

if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() {
let self_ty = trait_ref.self_type_parameter(interner);
if self_ty.bound_var(interner).is_some()

if let TyData::Alias(AliasTy::Opaque(opaque_ty)) = self_ty.data(interner) {
if trait_datum.is_auto_trait() {
push_auto_trait_impls_opaque(builder, trait_id, opaque_ty.opaque_ty_id)
}
} else if self_ty.bound_var(interner).is_some()
|| self_ty.inference_var(interner).is_some()
{
return Err(Floundered);
Expand Down
3 changes: 1 addition & 2 deletions chalk-solve/src/clauses/program_clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,6 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
/// 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<..>`.
fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) {
Expand All @@ -142,7 +141,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
let alias_placeholder_ty = Ty::new(
interner,
ApplicationTy {
name: TypeName::OpaqueType(self.opaque_ty_id),
name: self.opaque_ty_id.cast(interner),
substitution,
},
);
Expand Down
31 changes: 31 additions & 0 deletions tests/test/opaque_types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -98,3 +98,34 @@ fn opaque_generics() {

}
}

#[test]
fn opaque_auto_traits() {
test! {
program {
struct Bar { }
struct Baz { }
trait Trait { }

#[auto]
trait Send { }

impl !Send for Baz { }

opaque type Opaque1: Trait = Bar;
opaque type Opaque2: Trait = Baz;
}

goal {
Opaque1: Send
} yields {
"Unique"
}

goal {
Opaque2: Send
} yields {
"No possible solution"
}
}
}

0 comments on commit e5aaf83

Please sign in to comment.