[RequirementMachine] Substitution simplification records projections #41381

slavapestov · 2022-02-15T09:04:13Z

The Requirement Machine had three components that did similar things:

The simplifyLeftHandSideSubstitutions() pass ran during completion, simplifying rules like T.[concrete: G<Y>] => T down to T.[concrete: G<X>] => T, given Y => X
The concretelySimplifyLeftHandSideSubstitutions() pass ran after property map construction, simplifying rules like T.[concrete: G<X>] => T down to T.[concrete: G<Int>] => T, given X.[concrete: Int] => X
The PropertyMap::unifyConcreteTypes() operation would compute the meet of concrete type terms, so for example given T.[concrete: G<X>] => T and T.[concrete: G<Y>] => T, it would record an induced rule Y => X.

There were two problems here:

The first two passes are almost identical; the difference is that the second one can also replace subterms of a concrete type with concrete types, whereas the first one only rewrites type parameters appearing in substitutions to other type parameters. This PR refactors concretelySimplifyLeftHandSideSubstitutions() so that it can work without a PropertyMap, in which case it operates like the old simplifyLeftHandSideSubstitutions(), allowing simplifyLeftHandSideSubstitutions() to be removed entirely.
All three passes would record a loop that would derive the concrete type rules from each other using the induced rules on the substitutions, but only the last one would record rewrite loops expressing the induced rules in terms of the concrete type rules. This meant that in some cases, we would be unable to eliminate the induced rule.

Additionally, this PR fixes a couple of unrelated issues where Sema would emit duplicate diagnostics when resolving TypeReprs; in particular, this would manifest when running tests with -requirement-machine-inferred-signatures=verify, which resolves each TypeRepr appearing in a where clause twice (once for the GSB and once for the RequirementMachine).

When emitting a diagnostic, mark the TypeRepr as invalid and return an ErrorType to ensure that the diagnostic is not emitted again, and to muffle downstream diagnostics.

…Substitutions() Now that the PropertyMap to the concrete simplification version is optional, we can just pass nullptr here to get the old behavior where type terms are simplified to canonical anchors and no concrete simplification is performed.

The inverted form no longer has to replace substitutions; we use the inverted form of DecomposeConcrete for that. So just assert that the substitutions are equal.

…aring code with concrete simplification

…rom PropertyMap to RewriteSystem

…riends from PropertyUnification.cpp to RewriteSystem.cpp

…deSubstitutions()

- Prefer rewrite loops not involving Decompose - Prefer more deeply nested concrete types

slavapestov · 2022-02-15T09:05:15Z

@swift-ci Please test source compatibility

slavapestov · 2022-02-15T12:58:44Z

@swift-ci Please smoke test

slavapestov · 2022-02-15T12:58:51Z

@swift-ci Please test source compatibility

slavapestov · 2022-02-15T16:52:01Z