Skip to content

Commit

Permalink
Implementing support for Fundamental Traits
Browse files Browse the repository at this point in the history
  • Loading branch information
sunjay committed Jul 24, 2018
1 parent a63119a commit 62beeb3
Show file tree
Hide file tree
Showing 6 changed files with 73 additions and 6 deletions.
1 change: 1 addition & 0 deletions chalk-parse/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ pub struct TraitFlags {
pub auto: bool,
pub marker: bool,
pub upstream: bool,
pub fundamental: bool,
pub deref: bool,
}

Expand Down
3 changes: 2 additions & 1 deletion chalk-parse/src/parser.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ StructDefn: StructDefn = {
};

TraitDefn: TraitDefn = {
<auto:AutoKeyword?> <marker:MarkerKeyword?> <upstream:UpstreamKeyword?> <deref:DerefLangItem?> "trait" <n:Id><p:Angle<ParameterKind>>
<auto:AutoKeyword?> <marker:MarkerKeyword?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <deref:DerefLangItem?> "trait" <n:Id><p:Angle<ParameterKind>>
<w:QuantifiedWhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn
{
name: n,
Expand All @@ -69,6 +69,7 @@ TraitDefn: TraitDefn = {
auto: auto.is_some(),
marker: marker.is_some(),
upstream: upstream.is_some(),
fundamental: fundamental.is_some(),
deref: deref.is_some(),
},
}
Expand Down
33 changes: 33 additions & 0 deletions src/coherence/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,39 @@ fn downstream_impl_of_fundamental_43355() {
}
}

#[test]
fn fundamental_traits() {
// We want to enable negative reasoning about some traits. For example, consider the str type.
// We know that str is never going to be Sized and we have made a decision to allow people to
// depend on that. The following two impls are rejected as overlapping despite the fact that we
// know that str will never be Sized.
lowering_error! {
program {
#[upstream] trait Sized { }
#[upstream] struct str { }
trait Bar { }
impl Bar for str { }
impl<T> Bar for T where T: Sized { }
} error_msg {
"overlapping impls of trait \"Bar\""
}
}

// If we make Sized fundamental, we're telling the Rust compiler that it can reason negatively
// about it. That means that `not { str: Sized }` is provable. With that change, these two
// impls are now valid.
lowering_success! {
program {
#[upstream] #[fundamental] trait Sized { }
#[upstream] struct str { }
trait Bar { }
impl Bar for str { }
impl<T> Bar for T where T: Sized { }
}
}

}

#[test]
fn orphan_check() {
// These tests are largely adapted from the compile-fail coherence-*.rs tests from rustc
Expand Down
1 change: 1 addition & 0 deletions src/ir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,7 @@ pub struct TraitFlags {
crate auto: bool,
crate marker: bool,
crate upstream: bool,
crate fundamental: bool,
pub deref: bool,
}

Expand Down
1 change: 1 addition & 0 deletions src/ir/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1056,6 +1056,7 @@ impl LowerTrait for TraitDefn {
auto: self.flags.auto,
marker: self.flags.marker,
upstream: self.flags.upstream,
fundamental: self.flags.fundamental,
deref: self.flags.deref,
},
})
Expand Down
40 changes: 35 additions & 5 deletions src/rules.rs
Original file line number Diff line number Diff line change
Expand Up @@ -503,6 +503,32 @@ impl TraitDatum {
// IsUpstream(V),
// CannotProve, // returns ambiguous
// }
//
// In certain situations, this is too restrictive. Consider the following code:
//
// // In crate std:
// trait Sized { }
// struct str { }
//
// // In crate bar: (depends on std)
// trait Bar { }
// impl Bar for str { }
// impl<T> Bar for T where T: Sized { }
//
// Here, because of the rules we've defined, these two impls overlap. The std crate is
// upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str
// can implement Sized in a compatible future, these two impls definitely overlap since the
// second impl covers all types that implement Sized.
//
// The solution we've got right now is to mark Sized as "fundamental" when it is defined.
// This signals to the Rust compiler that it can rely on the fact that str does not
// implement Sized in all contexts. A consequence of this is that we can no longer add an
// implementation of Sized compatibly for str. This is the trade off you make when defining
// a fundamental trait.
//
// To implement fundamental traits, we simply just do not add the rule above that allows
// upstream types to implement upstream traits. Fundamental traits are not allowed to
// compatibly do that.

let mut clauses = Vec::new();

Expand Down Expand Up @@ -578,19 +604,23 @@ impl TraitDatum {
clauses.push(impl_maybe_allowed);
}

let impl_may_exist = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
conditions: bound_datum.where_clauses
// Fundamental traits can be reasoned about negatively without any ambiguity, so no
// need for this rule if the trait is fundamental.
if !self.binders.value.flags.fundamental {
let impl_may_exist = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
conditions: bound_datum.where_clauses
.iter()
.cloned()
.casted()
.chain(iter::once(DomainGoal::Compatible(()).cast()))
.chain(bound_datum.trait_ref.type_parameters().map(|ty| DomainGoal::IsUpstream(ty).cast()))
.chain(iter::once(Goal::CannotProve(())))
.collect(),
}).cast();
}).cast();

clauses.push(impl_may_exist);
clauses.push(impl_may_exist);
}
}

let condition = DomainGoal::FromEnv(FromEnv::Trait(trait_ref.clone()));
Expand Down

0 comments on commit 62beeb3

Please sign in to comment.