From f8aea29cd31087578e9d1a409689365fa7dc7321 Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 1 Dec 2025 13:29:33 +0100 Subject: [PATCH 1/2] add invariant --- src/solve/invariants.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/solve/invariants.md b/src/solve/invariants.md index 8ec15f339..bdf974099 100644 --- a/src/solve/invariants.md +++ b/src/solve/invariants.md @@ -116,6 +116,12 @@ We do however break this invariant in a few cases, some of which are due to bugs - the builtin trait object trait implementation can overlap with a user-defined impl: [#57893](https://github.com/rust-lang/rust/issues/57893) +### Goals with can be proven in a non-empty environment also hold during monomorphization ✅ + +If a goal can be proven in a generic environment, the goal should still hold after instantiating +it with fully concrete types and no where-clauses in scope. + +This is assumed by codegen whicih ICEs when encountering non-overflow ambiguity. This invariant is currently broken by specialization ([#147507](https://github.com/rust-lang/rust/issues/147507)) and by marker traits ([#149502](https://github.com/rust-lang/rust/issues/149502)). #### The type system is complete during the implicit negative overlap check in coherence ✅ From a5a3fd4e765c66527e3c21a4d4406f82e04eb96c Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 1 Dec 2025 21:38:23 +0100 Subject: [PATCH 2/2] Update src/solve/invariants.md Co-authored-by: Tshepang Mbambo --- src/solve/invariants.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solve/invariants.md b/src/solve/invariants.md index bdf974099..d6e360cbc 100644 --- a/src/solve/invariants.md +++ b/src/solve/invariants.md @@ -121,7 +121,7 @@ We do however break this invariant in a few cases, some of which are due to bugs If a goal can be proven in a generic environment, the goal should still hold after instantiating it with fully concrete types and no where-clauses in scope. -This is assumed by codegen whicih ICEs when encountering non-overflow ambiguity. This invariant is currently broken by specialization ([#147507](https://github.com/rust-lang/rust/issues/147507)) and by marker traits ([#149502](https://github.com/rust-lang/rust/issues/149502)). +This is assumed by codegen which ICEs when encountering non-overflow ambiguity. This invariant is currently broken by specialization ([#147507](https://github.com/rust-lang/rust/issues/147507)) and by marker traits ([#149502](https://github.com/rust-lang/rust/issues/149502)). #### The type system is complete during the implicit negative overlap check in coherence ✅