mirror of
https://github.com/carbon-language/carbon-lang.git
synced 2026-10-04 22:02:52 +01:00
Dana Jansens
517bec24ef
Given a facet type: `(Z where .X = .Y) where .X =.Y`
The rewrite constraints in the inner facet type are each an
`ImplWitnessAccess` into a witness for the self of type `Z` (which is
the facet type before the `where`). The rewrite constraints in the outer
facet type are each an `ImplWitnessAccess` for the self of type `Z where
.X = .Y`, which is a different self facet type.
This means when deduping in canonicalization, the first `.X` and the
second `.X` are different instructions, and different constant values,
so they both remain in the rewrite constraints, incorrectly. Then if the
outer `.X` is allowed to evaluate to a value from its facet type, it
finds `.Y` resulting in `.Y = .Y` which is also incorrect.
Because of the failure to dedupe the first facet type, that is also
diagnosed as two different assignments to the same `.X`. To resolve
that, we introduce `CompareFacetTypeConstraintValues()` compare values
in facet type constraints, and treat accesses to the same associated
constant in the same facet value as `equivalent` even when through
different witnesses. This allows us to dedupe the two `.X = .Y` rules
into one in the combined facet type.
Given a different facet type: `(Z where .X = ()) where .X = {}`. Here we
want to diagnose that `.X` has been assigned two different values. To do
so, we need to see that the two `.X` values are the same, and we use
`CompareFacetTypeConstraintValues()` to do this comparison. Then we see
two rewrite rules for the same LHS, and we can diagnose that.
We enable evaluating `ImplWitnessAccess` on `.Self` to pull a value from
rewrite constraints in a facet type so that we can see that we are not
incorrect evaluating the LHS of rewrite constraints and producing
cycles. By doing so, also enable generic code to see and use concrete
values in associated constants in facet types.