Slava Pestov f0d59d5d4d RequirementMachine: Handle equivalence classes that both have a concrete type and protocol requirements ...

If a type parameter has a protocol conformance and a concrete type,
we want to map associated types of the conformance to their concrete
type witnesses.

This is implemented as a post-processing pass in the completion
procedure that runs after the equivalence class map has been built.

If we have an equivalence class T => { conforms_to: [ P ], concrete: Foo },
then for each associated type A of P, we generate a new rule:

    T.[P:A].[concrete: Foo.A] => T.[P:A]  (if Foo.A is concrete)
    T.[P:A] => T.(Foo.A)                  (if Foo.A is abstract)

If this process introduced any new rules, we check for any new
overlaps by re-running Knuth-Bendix completion; this may in turn
introduce new concrete associated type overlaps, and so on.

The overall completion procedure now alternates between Knuth-Bendix
and rebuilding the equivalence class map; the rewrite system is
complete when neither step is able to introduce any new rules.

2021-07-09 00:04:36 -04:00

36 KiB

Raw Blame History

View Raw