Skip to content

Commit 90d7c6f

Browse files
authored
Merge pull request #167 from sunjay/fun-traits
Implementing support for Fundamental Traits
2 parents a63119a + 62beeb3 commit 90d7c6f

File tree

6 files changed

+73
-6
lines changed

6 files changed

+73
-6
lines changed

chalk-parse/src/ast.rs

+1
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ pub struct TraitFlags {
5555
pub auto: bool,
5656
pub marker: bool,
5757
pub upstream: bool,
58+
pub fundamental: bool,
5859
pub deref: bool,
5960
}
6061

chalk-parse/src/parser.lalrpop

+2-1
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ StructDefn: StructDefn = {
5858
};
5959

6060
TraitDefn: TraitDefn = {
61-
<auto:AutoKeyword?> <marker:MarkerKeyword?> <upstream:UpstreamKeyword?> <deref:DerefLangItem?> "trait" <n:Id><p:Angle<ParameterKind>>
61+
<auto:AutoKeyword?> <marker:MarkerKeyword?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <deref:DerefLangItem?> "trait" <n:Id><p:Angle<ParameterKind>>
6262
<w:QuantifiedWhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn
6363
{
6464
name: n,
@@ -69,6 +69,7 @@ TraitDefn: TraitDefn = {
6969
auto: auto.is_some(),
7070
marker: marker.is_some(),
7171
upstream: upstream.is_some(),
72+
fundamental: fundamental.is_some(),
7273
deref: deref.is_some(),
7374
},
7475
}

src/coherence/test.rs

+33
Original file line numberDiff line numberDiff line change
@@ -257,6 +257,39 @@ fn downstream_impl_of_fundamental_43355() {
257257
}
258258
}
259259

260+
#[test]
261+
fn fundamental_traits() {
262+
// We want to enable negative reasoning about some traits. For example, consider the str type.
263+
// We know that str is never going to be Sized and we have made a decision to allow people to
264+
// depend on that. The following two impls are rejected as overlapping despite the fact that we
265+
// know that str will never be Sized.
266+
lowering_error! {
267+
program {
268+
#[upstream] trait Sized { }
269+
#[upstream] struct str { }
270+
trait Bar { }
271+
impl Bar for str { }
272+
impl<T> Bar for T where T: Sized { }
273+
} error_msg {
274+
"overlapping impls of trait \"Bar\""
275+
}
276+
}
277+
278+
// If we make Sized fundamental, we're telling the Rust compiler that it can reason negatively
279+
// about it. That means that `not { str: Sized }` is provable. With that change, these two
280+
// impls are now valid.
281+
lowering_success! {
282+
program {
283+
#[upstream] #[fundamental] trait Sized { }
284+
#[upstream] struct str { }
285+
trait Bar { }
286+
impl Bar for str { }
287+
impl<T> Bar for T where T: Sized { }
288+
}
289+
}
290+
291+
}
292+
260293
#[test]
261294
fn orphan_check() {
262295
// These tests are largely adapted from the compile-fail coherence-*.rs tests from rustc

src/ir.rs

+1
Original file line numberDiff line numberDiff line change
@@ -272,6 +272,7 @@ pub struct TraitFlags {
272272
crate auto: bool,
273273
crate marker: bool,
274274
crate upstream: bool,
275+
crate fundamental: bool,
275276
pub deref: bool,
276277
}
277278

src/ir/lowering.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1056,6 +1056,7 @@ impl LowerTrait for TraitDefn {
10561056
auto: self.flags.auto,
10571057
marker: self.flags.marker,
10581058
upstream: self.flags.upstream,
1059+
fundamental: self.flags.fundamental,
10591060
deref: self.flags.deref,
10601061
},
10611062
})

src/rules.rs

+35-5
Original file line numberDiff line numberDiff line change
@@ -503,6 +503,32 @@ impl TraitDatum {
503503
// IsUpstream(V),
504504
// CannotProve, // returns ambiguous
505505
// }
506+
//
507+
// In certain situations, this is too restrictive. Consider the following code:
508+
//
509+
// // In crate std:
510+
// trait Sized { }
511+
// struct str { }
512+
//
513+
// // In crate bar: (depends on std)
514+
// trait Bar { }
515+
// impl Bar for str { }
516+
// impl<T> Bar for T where T: Sized { }
517+
//
518+
// Here, because of the rules we've defined, these two impls overlap. The std crate is
519+
// upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str
520+
// can implement Sized in a compatible future, these two impls definitely overlap since the
521+
// second impl covers all types that implement Sized.
522+
//
523+
// The solution we've got right now is to mark Sized as "fundamental" when it is defined.
524+
// This signals to the Rust compiler that it can rely on the fact that str does not
525+
// implement Sized in all contexts. A consequence of this is that we can no longer add an
526+
// implementation of Sized compatibly for str. This is the trade off you make when defining
527+
// a fundamental trait.
528+
//
529+
// To implement fundamental traits, we simply just do not add the rule above that allows
530+
// upstream types to implement upstream traits. Fundamental traits are not allowed to
531+
// compatibly do that.
506532

507533
let mut clauses = Vec::new();
508534

@@ -578,19 +604,23 @@ impl TraitDatum {
578604
clauses.push(impl_maybe_allowed);
579605
}
580606

581-
let impl_may_exist = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
582-
consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
583-
conditions: bound_datum.where_clauses
607+
// Fundamental traits can be reasoned about negatively without any ambiguity, so no
608+
// need for this rule if the trait is fundamental.
609+
if !self.binders.value.flags.fundamental {
610+
let impl_may_exist = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
611+
consequence: DomainGoal::Holds(WhereClause::Implemented(bound_datum.trait_ref.clone())),
612+
conditions: bound_datum.where_clauses
584613
.iter()
585614
.cloned()
586615
.casted()
587616
.chain(iter::once(DomainGoal::Compatible(()).cast()))
588617
.chain(bound_datum.trait_ref.type_parameters().map(|ty| DomainGoal::IsUpstream(ty).cast()))
589618
.chain(iter::once(Goal::CannotProve(())))
590619
.collect(),
591-
}).cast();
620+
}).cast();
592621

593-
clauses.push(impl_may_exist);
622+
clauses.push(impl_may_exist);
623+
}
594624
}
595625

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

0 commit comments

Comments
 (0)