circular reasoning is a potential source of unsoundness [LWN.net]

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 15:05 UTC (Mon) by garyguo (subscriber, #173367)
Parent article: Rust's next-generation trait solver

> In this case, however, it should be possible in theory for the compiler to generate an implementation of Debug for the same reason that assemblers can handle instructions that refer to their own address: the compiler can start generating the implementation, leaving a placeholder for the address, and then fill the address in once it knows it.

This can be quite worrying because it can expose the type system to circular reasoning. Trait bounds are obligations that the trait system needs to prove, and if the trait system can make use of a bound that it is proving, would the corresponding mathematical reasoning with Curry–Howard correspondence be flawed as well?

Having said that, I've tried out the example in article and it is still rejected with `-Znext-solver=globally` with "overflow evaluating the requirement `Link<MyWrapper>: Debug`", so it's a relief.

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 15:29 UTC (Mon) by daroc (editor, #160859) [Link] (5 responses)

I didn't go as deep into the weeds as I could have with the details of when circular reasoning is or isn't sound; the Rust compiler documentation that I linked goes into more detail. There are two different kinds of cycles that one can have in a type system: inductive and coinductive. Inductive cycles are always unsound (and the plan remains to have the Rust type system reject them). Coinductive cycles can be sound, with the right logical foundations.

Via the Curry-Howard correspondence, an inductive cycle is an infinite loop, or a recursive function without a base case. A coinductive cycle, on the other hand, corresponds to something like a generator: a process that continues indefinitely, but does some additional work at each step such that, when consumed by a process that doesn't try to reach the "end" of the sequence, it all works out.

The main thing is that, when attempting to find a coinductive proof, it's necessary to ensure that the cycle has a length greater than one (or, to use type theory jargon, that the loop is productive). Note that that doesn't prevent the actual generated code from being an infinite loop (because Rust doesn't consider that to be unsound, and a programmer could already write a trait implementation that way), but it does prevent a "impl<T> Trait for T where T: Trait" situation, which is probably undesirable.

Right now, the next-generation solver will only do coinductive reasoning for a limited number of autotraits (Send, etc.). If/when it can be shown safe to extend this to user-defined traits, then it will be. But since this whole area is complex and subtle, the types team is moving slowly and making sure they don't introduce unsoundness.

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 17:10 UTC (Mon) by NYKevin (subscriber, #129325) [Link] (4 responses)

The "obvious" concern I would have with this is user-defined unsafe traits.

In the case of Send and Sync, the traits impose a negative obligation. Types in Rust are thread-safe by default, and they can only become thread-unsafe through the use of interior mutability or raw pointers. So it's entirely reasonable to coinductively infer Send and Sync. If you never encounter something manifestly !Send or !Sync in your chain of reasoning, then there can't be any source of thread-unsafety, so inferring Send or Sync is fine.

On the other hand, the unsafe trait TrustedLen imposes a positive obligation. Specifically, if a type implements TrustedLen, then unsafe code may soundly assume that its len() method returns the right value, and execute UB if that assumption turns out to be wrong. In pragmatic terms, that means the Source of Truth for len() must be hidden behind some visibility annotation so that foreign safe code cannot mess with it. If len() is computed by calling into something else, then that callee is under the same obligation, transitively all the way down to the ground truth.

In the case of TrustedLen, I don't think there exists a counterexample where coinduction actually produces an unsound implementation. Coinduction implies, to my mind, that you end up with TrustedLen-or-some-equivalent all the way down, and there's no actual soundness hole. But it is the sort of thing that would keep me awake at night if I were responsible for trait-solving in Rust. Users can define arbitrary unsafe traits with arbitrary soundness requirements, and those requirements typically exist only in documentation or comments, not in actual code the compiler can read and understand. Who is to say whether any one of those unsafe traits might be incompatible with coinduction?

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 17:34 UTC (Mon) by daroc (editor, #160859) [Link] (2 responses)

I suspect the answer is the same as any other unsafe thing that breaks the language: "don't do that". You can't have a coinductive loop without at least one trait implementation block, so for an unsafe trait, that unsafe trait implementation is the specific use of unsafe that could break things.

But yes, one of the remaining open items to work on before the next-generation trait solver can be stabilized is documentation, which will presumably include documenting how any proposed changes to the type system interact with unsafe code.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 1:22 UTC (Tue) by NYKevin (subscriber, #129325) [Link] (1 responses)

Sure, but what happens if someone has already constructed an incomplete loop, which is only sound in the current version of Rust because coinduction is impossible (and therefore the loop cannot be closed)? You could imagine a situation where the "missing link" of the loop is implementable in safe code, and that would retroactively render the existing (unsafe) implementations unsound.

I don't think you can fix it with an edition, either. Trait solving is semantic, not syntactic.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 11:49 UTC (Tue) by daroc (editor, #160859) [Link]

Oh, I see your point! That's an interesting thought.

You're right; I'm not sure how that ought to be handled. I don't think the list of considerations for unsafe code to be aware of have changed very much over time.

Perhaps it would still be possible to make it an edition change by tagging each trait implementation with which edition it comes from, and disallowing coinductive cycles that dip into previous editions, but that's pure speculation on my part.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 3:36 UTC (Tue) by theemathas (guest, #183008) [Link]

This exact issue has been raised in https://github.com/rust-lang/rust/issues/149743

There's currently no good answer to this yet.

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 18:57 UTC (Mon) by iabervon (subscriber, #722) [Link]

I think it would be unsound if you could say "impl Debug for Link where Link: Debug {}", but that's not allowed, and the impl thing that is allowed is really saying: this type has Debug, and I'll tell you how, but I need to be able to call its methods if so. It's more of an induction step than circular reasoning: an object of this type has this trait if any other objects of this type that it references have the trait, and any other obligations are met.

circular reasoning is a potential source of unsoundness

Posted Apr 1, 2026 15:43 UTC (Wed) by smoofra (subscriber, #86163) [Link]

I think the right way to think about it is not that circular reasoning, or impredicativity is a source of unsoundness, but that predicativity is just a really powerful tool to constrain logics so they don't accidentally become unsound.

Just like it's absurdly easy for a programming language to accidentally become Turing-complete, it's absurdly easy for a logic to accidentally become unsound. But I don't think that impredicativity is the source of the unsoundness. There's impredicative logics like say, second order arithmetic that are sound. There's probably whole worlds of them nobody has thought about yet. But it's easier to think about soundness and prove it for predicative logics.

circular reasoning is a potential source of unsoundness

Posted Apr 12, 2026 1:31 UTC (Sun) by suckfish (guest, #69919) [Link]

In mathematical terms, the "circular reasoning" appears to arise from taking the greatest-fixed-point of an operator or some sort or partially ordered structure as opposed to the more common least-fixed-point.

How to do this soundly and then reason correctly about the results has been well understood for over 30 years in the functional programming community.