Skip to content

Commit

Permalink
Rollup merge of #108033 - lcnr:coinductive-attr, r=compiler-errors
Browse files Browse the repository at this point in the history
add an unstable `#[rustc_coinductive]` attribute

useful to test coinduction, especially in the new solver.

as this attribute should remain permanently unstable I don't think this needs any official approval. cc ``@rust-lang/types``

had to weaken the check for stable query results in the solver to prevent an ICE if there's a coinductive cycle with constraints.

r? ``@compiler-errors``
  • Loading branch information
matthiaskrgr committed Feb 14, 2023
2 parents 7e0127b + a2f0303 commit edcdab0
Show file tree
Hide file tree
Showing 10 changed files with 130 additions and 37 deletions.
15 changes: 11 additions & 4 deletions compiler/rustc_feature/src/builtin_attrs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -414,7 +414,10 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
),

// Linking:
gated!(naked, Normal, template!(Word), WarnFollowing, @only_local: true, naked_functions, experimental!(naked)),
gated!(
naked, Normal, template!(Word), WarnFollowing, @only_local: true,
naked_functions, experimental!(naked)
),

// Plugins:
BuiltinAttribute {
Expand All @@ -441,7 +444,8 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
),
// RFC #1268
gated!(
marker, Normal, template!(Word), WarnFollowing, marker_trait_attr, experimental!(marker)
marker, Normal, template!(Word), WarnFollowing, @only_local: true,
marker_trait_attr, experimental!(marker)
),
gated!(
thread_local, Normal, template!(Word), WarnFollowing,
Expand Down Expand Up @@ -682,14 +686,17 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
"language items are subject to change",
),
rustc_attr!(
rustc_pass_by_value, Normal,
template!(Word), ErrorFollowing,
rustc_pass_by_value, Normal, template!(Word), ErrorFollowing,
"#[rustc_pass_by_value] is used to mark types that must be passed by value instead of reference."
),
rustc_attr!(
rustc_coherence_is_core, AttributeType::CrateLevel, template!(Word), ErrorFollowing, @only_local: true,
"#![rustc_coherence_is_core] allows inherent methods on builtin types, only intended to be used in `core`."
),
rustc_attr!(
rustc_coinductive, AttributeType::Normal, template!(Word), WarnFollowing, @only_local: true,
"#![rustc_coinductive] changes a trait to be coinductive, allowing cycles in the trait solver."
),
rustc_attr!(
rustc_allow_incoherent_impl, AttributeType::Normal, template!(Word), ErrorFollowing, @only_local: true,
"#[rustc_allow_incoherent_impl] has to be added to all impl items of an incoherent inherent impl."
Expand Down
12 changes: 7 additions & 5 deletions compiler/rustc_hir_analysis/src/collect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -934,9 +934,10 @@ fn trait_def(tcx: TyCtxt<'_>, def_id: DefId) -> ty::TraitDef {
}

let is_marker = tcx.has_attr(def_id, sym::marker);
let rustc_coinductive = tcx.has_attr(def_id, sym::rustc_coinductive);
let skip_array_during_method_dispatch =
tcx.has_attr(def_id, sym::rustc_skip_array_during_method_dispatch);
let spec_kind = if tcx.has_attr(def_id, sym::rustc_unsafe_specialization_marker) {
let specialization_kind = if tcx.has_attr(def_id, sym::rustc_unsafe_specialization_marker) {
ty::trait_def::TraitSpecializationKind::Marker
} else if tcx.has_attr(def_id, sym::rustc_specialization_trait) {
ty::trait_def::TraitSpecializationKind::AlwaysApplicable
Expand Down Expand Up @@ -1036,16 +1037,17 @@ fn trait_def(tcx: TyCtxt<'_>, def_id: DefId) -> ty::TraitDef {
no_dups.then_some(list)
});

ty::TraitDef::new(
ty::TraitDef {
def_id,
unsafety,
paren_sugar,
is_auto,
has_auto_impl: is_auto,
is_marker,
is_coinductive: rustc_coinductive || is_auto,
skip_array_during_method_dispatch,
spec_kind,
specialization_kind,
must_implement_one_of,
)
}
}

fn are_suggestable_generic_args(generic_args: &[hir::GenericArg<'_>]) -> bool {
Expand Down
10 changes: 6 additions & 4 deletions compiler/rustc_middle/src/ty/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2388,15 +2388,17 @@ impl<'tcx> TyCtxt<'tcx> {
self.trait_def(trait_def_id).has_auto_impl
}

/// Returns `true` if this is coinductive, either because it is
/// an auto trait or because it has the `#[rustc_coinductive]` attribute.
pub fn trait_is_coinductive(self, trait_def_id: DefId) -> bool {
self.trait_def(trait_def_id).is_coinductive
}

/// Returns `true` if this is a trait alias.
pub fn trait_is_alias(self, trait_def_id: DefId) -> bool {
self.def_kind(trait_def_id) == DefKind::TraitAlias
}

pub fn trait_is_coinductive(self, trait_def_id: DefId) -> bool {
self.trait_is_auto(trait_def_id) || self.lang_items().sized_trait() == Some(trait_def_id)
}

/// Returns layout of a generator. Layout might be unavailable if the
/// generator is tainted by errors.
pub fn generator_layout(self, def_id: DefId) -> Option<&'tcx GeneratorLayout<'tcx>> {
Expand Down
31 changes: 9 additions & 22 deletions compiler/rustc_middle/src/ty/trait_def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,15 @@ pub struct TraitDef {
/// and thus `impl`s of it are allowed to overlap.
pub is_marker: bool,

/// If `true`, then this trait has to `#[rustc_coinductive]` attribute or
/// is an auto trait. This indicates that trait solver cycles involving an
/// `X: ThisTrait` goal are accepted.
///
/// In the future all traits should be coinductive, but we need a better
/// formal understanding of what exactly that means and should probably
/// also have already switched to the new trait solver.
pub is_coinductive: bool,

/// If `true`, then this trait has the `#[rustc_skip_array_during_method_dispatch]`
/// attribute, indicating that editions before 2021 should not consider this trait
/// during method dispatch if the receiver is an array.
Expand Down Expand Up @@ -81,28 +90,6 @@ impl TraitImpls {
}

impl<'tcx> TraitDef {
pub fn new(
def_id: DefId,
unsafety: hir::Unsafety,
paren_sugar: bool,
has_auto_impl: bool,
is_marker: bool,
skip_array_during_method_dispatch: bool,
specialization_kind: TraitSpecializationKind,
must_implement_one_of: Option<Box<[Ident]>>,
) -> TraitDef {
TraitDef {
def_id,
unsafety,
paren_sugar,
has_auto_impl,
is_marker,
skip_array_during_method_dispatch,
specialization_kind,
must_implement_one_of,
}
}

pub fn ancestors(
&self,
tcx: TyCtxt<'tcx>,
Expand Down
15 changes: 15 additions & 0 deletions compiler/rustc_passes/src/check_attr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ impl CheckAttrVisitor<'_> {
| sym::rustc_dirty
| sym::rustc_if_this_changed
| sym::rustc_then_this_would_need => self.check_rustc_dirty_clean(&attr),
sym::rustc_coinductive => self.check_rustc_coinductive(&attr, span, target),
sym::cmse_nonsecure_entry => {
self.check_cmse_nonsecure_entry(hir_id, attr, span, target)
}
Expand Down Expand Up @@ -1608,6 +1609,20 @@ impl CheckAttrVisitor<'_> {
}
}

/// Checks if the `#[rustc_coinductive]` attribute is applied to a trait.
fn check_rustc_coinductive(&self, attr: &Attribute, span: Span, target: Target) -> bool {
match target {
Target::Trait => true,
_ => {
self.tcx.sess.emit_err(errors::AttrShouldBeAppliedToTrait {
attr_span: attr.span,
defn_span: span,
});
false
}
}
}

/// Checks if `#[link_section]` is applied to a function or static.
fn check_link_section(&self, hir_id: HirId, attr: &Attribute, span: Span, target: Target) {
match target {
Expand Down
1 change: 1 addition & 0 deletions compiler/rustc_span/src/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1224,6 +1224,7 @@ symbols! {
rustc_capture_analysis,
rustc_clean,
rustc_coherence_is_core,
rustc_coinductive,
rustc_const_stable,
rustc_const_unstable,
rustc_conversion_suggestion,
Expand Down
10 changes: 8 additions & 2 deletions compiler/rustc_trait_selection/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -265,12 +265,18 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
// could constrain `U` to `u32` which would cause this check to result in a
// solver cycle.
if cfg!(debug_assertions) && has_changed && !self.in_projection_eq_hack {
if cfg!(debug_assertions)
&& has_changed
&& !self.in_projection_eq_hack
&& !self.search_graph.in_cycle()
{
let mut orig_values = OriginalQueryValues::default();
let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
let canonical_response =
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
assert!(canonical_response.value.var_values.is_identity());
if !canonical_response.value.var_values.is_identity() {
bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
}
assert_eq!(certainty, canonical_response.value.certainty);
}

Expand Down
18 changes: 18 additions & 0 deletions compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,24 @@ impl<'tcx> SearchGraph<'tcx> {
&& !self.overflow_data.did_overflow()
}

/// Whether we're currently in a cycle. This should only be used
/// for debug assertions.
pub(super) fn in_cycle(&self) -> bool {
if let Some(stack_depth) = self.stack.last() {
// Either the current goal on the stack is the root of a cycle...
if self.stack[stack_depth].has_been_used {
return true;
}

// ...or it depends on a goal with a lower depth.
let current_goal = self.stack[stack_depth].goal;
let entry_index = self.provisional_cache.lookup_table[&current_goal];
self.provisional_cache.entries[entry_index].depth != stack_depth
} else {
false
}
}

/// Tries putting the new goal on the stack, returning an error if it is already cached.
///
/// This correctly updates the provisional cache if there is a cycle.
Expand Down
1 change: 1 addition & 0 deletions library/core/src/marker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ unsafe impl<T: Sync + ?Sized> Send for &T {}
#[fundamental] // for Default, for example, which requires that `[T]: !Default` be evaluatable
#[rustc_specialization_trait]
#[rustc_deny_explicit_impl]
#[cfg_attr(not(bootstrap), rustc_coinductive)]
pub trait Sized {
// Empty.
}
Expand Down
54 changes: 54 additions & 0 deletions tests/ui/coinduction/canonicalization-rerun.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
// check-pass
// revisions: old new
//[new] compile-flags: -Ztrait-solver=next

// If we use canonical goals during trait solving we have to reevaluate
// the root goal of a cycle until we hit a fixpoint.
//
// Here `main` has a goal `(?0, ?1): Trait` which is canonicalized to
// `exists<^0, ^1> (^0, ^1): Trait`.
//
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
// - COINDUCTIVE CYCLE OK (no constraints)
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
// - OK (^0 = u32 -apply-> ?0 = u32)
// - OK (?0 = u32 -canonicalize-> ^0 = u32)
// - coinductive cycle with provisional result != final result, rerun
//
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
// - COINDUCTIVE CYCLE OK (^0 = u32 -apply-> ?1 = u32)
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
// - OK (^0 = u32 -apply-> ?1 = u32)
// - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32)
// - coinductive cycle with provisional result != final result, rerun
//
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
// - COINDUCTIVE CYCLE OK (^0 = u32, ^1 = u32 -apply-> ?1 = u32, ?0 = u32)
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
// - OK (^0 = u32 -apply-> ?1 = u32)
// - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32)
// - coinductive cycle with provisional result == final result, DONE
#![feature(rustc_attrs)]
#[rustc_coinductive]
trait Trait {}

impl<T, U> Trait for (T, U)
where
(U, T): Trait,
(): ConstrainToU32<T>,
{}

trait ConstrainToU32<T> {}
impl ConstrainToU32<u32> for () {}

fn impls_trait<T, U>()
where
(T, U): Trait,
{}

fn main() {
impls_trait::<_, _>();
}

0 comments on commit edcdab0

Please sign in to comment.