Coherence checking

Coherence checking lives in check/coherence.rs and runs as part of crate checking.

check_coherence

check_coherence(program: Program, current_crate: Crate) => ()

At a high level, check_coherence:

• rejects duplicate impls in the current crate
• checks the current crate’s impls for overlap against all impls in the program
• runs orphan checking for positive impls in the current crate
• runs orphan checking for negative impls in the current crate

Orphan checking

orphan_check(program: Program, impl_a: TraitImpl) => ()

orphan_check instantiates the impl binder universally and proves that the trait reference is local under the impl’s where-clauses.

Negative impls have the same structure:

orphan_check_neg(program: Program, impl_a: NegTraitImpl) => ()

Overlap checking

overlap_check_impl compares two impls of the same trait. It first skips identical impls and impls for different traits. For matching trait ids, it tries to prove that the impls cannot both apply. If that fails, it reports the impls as overlapping.

Proving locality

The is_local module determines whether a trait reference could have been defined locally, which is the key predicate for orphan checking:

is_local_trait_ref(_decls: Program, env: Env, assumptions: Wcs, goal: TraitRef,) => Constraints

A parameter is considered local if it is a local type or a fundamental rigid type wrapping a local parameter:

is_local_parameter(_decls: Program, env: Env, assumptions: Wcs, goal: Parameter,) => Constraints

The complement — determining whether a trait reference may come from a remote crate — is used in coherence mode:

may_be_remote(_decls: Program, env: Env, assumptions: Wcs, goal: TraitRef,) => Constraints