Function check_module_with 

pub fn check_module_with(
    module: &Node,
    mode: Mode,
    imports: &[(String, Interface)],
    diags: &mut Diagnostics,
) -> Program

Check a module against the interfaces it imports — §3.6’s separate compilation.

The importing module sees signatures and nothing else: types, parameter and result types, effect rows and placements. It never sees a body, which is exactly why editing one downstream costs nothing here.