diff --git a/src/solve/invariants.md b/src/solve/invariants.md
index 8ec15f339..d6e360cbc 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 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 ✅