From 77dbe5782b2488af3bb489ad702eaff438f465bf Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 6 Nov 2023 10:38:06 +0100 Subject: [PATCH] add a new type system invariant --- src/solve/invariants.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/solve/invariants.md b/src/solve/invariants.md index 5d50aa9e62d7a..75ae530700bbf 100644 --- a/src/solve/invariants.md +++ b/src/solve/invariants.md @@ -26,7 +26,16 @@ types. This is unfortunately broken for `>::Output` due to implied bounds, resulting in [#114936]. -### applying inference results from a goal does not change its result ❌ +### Structural equality modulo regions implies semantic equality ✅ + +If you have a some type and equate it to itself after replacing any regions with unique +inference variables in both the lhs and rhs, the now potentially structurally different +types should still be equal to each other. + +Needed to prevent goals from succeeding in HIR typeck and then failing in MIR borrowck. +If this does invariant is broken MIR typeck ends up failing with an ICE. + +### Applying inference results from a goal does not change its result ❌ TODO: this invariant is formulated in a weird way and needs to be elaborated. Pretty much: I would like this check to only fail if there's a solver bug: