Rollup merge of #108033 - lcnr:coinductive-attr, r=compiler-errors
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``
This commit is contained in:
commit
edcdab08a4
@ -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 {
|
||||
@ -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,
|
||||
@ -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."
|
||||
|
@ -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
|
||||
@ -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 {
|
||||
|
@ -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>> {
|
||||
|
@ -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.
|
||||
@ -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>,
|
||||
|
@ -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)
|
||||
}
|
||||
@ -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 {
|
||||
|
@ -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,
|
||||
|
@ -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);
|
||||
}
|
||||
|
||||
|
@ -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[¤t_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.
|
||||
|
@ -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.
|
||||
}
|
||||
|
54
tests/ui/coinduction/canonicalization-rerun.rs
Normal file
54
tests/ui/coinduction/canonicalization-rerun.rs
Normal file
@ -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::<_, _>();
|
||||
}
|
Loading…
x
Reference in New Issue
Block a user