Function refinement_info_for_in_scope 

pub fn refinement_info_for_in_scope<'a>(
    type_name: &str,
    inputs: &ProofLowerInputs<'a>,
    scope: Option<&str>,
) -> Option<RefinementInfo<'a>>

Module-scoped variant of refinement_info_for. scope = None means “look in entry items only”; scope = Some(prefix) means “look in the dep module whose prefix matches”.

Refinement-via-opaque is a single-module pattern: the record is declared exposes opaque [X] and the smart constructor lives in the same module (the carrier field isn’t reachable from outside, so the constructor can’t reside elsewhere). Scoping the search to one module gives each scope its own predicate, which is what populate_refined_types needs so canonical A.Natural and B.Natural slots don’t share a predicate from whichever module happened to walk first.