Commit Graph

3 Commits

Author SHA1 Message Date
Slava Pestov
dac8d666ee Stop passing -requirement-machine-{abstract,inferred,protocol}-signatures flags in tests
These flags are now no-ops.
2022-05-10 12:56:17 -04:00
Slava Pestov
cdcc8ed8fc RequirementMachine: Enable loop normalization by default 2022-03-26 22:12:12 -04:00
Slava Pestov
b6a641bc07 RequirementMachine: New way of introducing concrete conformance rules
Define the relation as

    [concrete: C].[P] =>> [concrete: C].[concrete: C : P]

instead of

    [concrete: C].[P] =>> [concrete: C : P]

This changes the rewrite loop recorded for a rule T.[concrete: C : P]
to have (T.[concrete: C] => T) appearing twice in context instead of
just once.

We don't ever want a concrete conformance rule to be able to imply a
concrete type rule. This became possible with loop normalization
because the single occurrence of (T.[concrete: C] => T).[P] could
cancel with a subsequent step (T => T.[concrete: C]).[P] in another
rewrite loop after substitution.
2022-03-08 23:21:58 -05:00