types: a module's interface carries the records and opaque types it references

DESIGN.md

@@ -893,7 +893,8 @@ checker already uses for built-in/in-file modules, so the existing `Field`-node
 cross-module reference with no new lookup logic. A module's interface is its top-level **`let`
 values** plus its **sum types** (since the cross-module-ADT follow-on; `ModuleExports` carries each public
 sum type's name, arity, and constructors) **and its records** (since the cross-module-record follow-on;
-`ModuleExports` also carries each public record's name + fields). A consumer can construct (`Geometry.Circle
+`ModuleExports` also carries each public record's name + fields) **and its opaque handle types** (name +
+arity, so `extern type Rng` can be named across the boundary). A consumer can construct (`Geometry.Circle
 2.0`) and pattern-match (`| Geometry.Circle r ->`, a qualified constructor pattern) the imported type's
 values, with **exhaustiveness checked across the boundary** (a missing arm reports the qualified witness
 `Geometry.Rect _ _`). **Records cross too** (`DESIGN.md` §8.3): construct `Geometry.Point { x = 1, y = 2 }`,
@@ -904,10 +905,26 @@ an ADT variant payload or an `extern` signature. Both spellings are accepted, ba
 `Shapes.Placed`, and they denote the same type: an imported type registers under its bare identity name
 (unique across everything visible, as the import clash check enforces) plus a qualified key, and a written
 qualifier is validated and then folded back to that identity, so the two unify freely. Prefer the qualified
-spelling where the reader benefits from knowing which module a type came from. The one thing this does not
-extend to is *transitive* naming: a third module importing `Holder` without importing `Shapes` can hold and
-pass its `item` around, but cannot access that value's fields or construct one, since only `Shapes` brings
-`Placed`'s field registry into scope. **Externs and
+spelling where the reader benefits from knowing which module a type came from. **Opaque handle types
+(`extern type Rng`, §6) cross like any other type name:** the interface carries the name + arity, so a
+consumer can write `Gen.Rng` (or bare `Rng`) in a record field, an ADT payload, or an `extern` signature;
+values of the type always crossed through the exported schemes. **Interfaces close transitively over what
+they reference:** a record or opaque type that an exported scheme, constructor, or record field mentions is
+carried in the exporter's interface, tagged with the module that declares it, and the pull repeats through
+each hop (a worklist walk with a seen set, so mutually referencing records terminate). A third module
+importing `Holder` without importing `Shapes` can therefore hold its `item`, read that value's fields, and
+name its type bare (`Placed`). A carried type crosses as an *identity*, not as a member: constructing it,
+pattern-matching it, or writing the qualified spelling still requires importing the declaring module
+directly. A carried name already taken here (by a local type or a direct import) is skipped silently rather
+than reported, since the consumer never wrote that name: local and direct declarations win the bare name,
+the same record arriving along two import paths is recognized by its declaring module and admitted once,
+and a genuinely different type shadows the carried record, whose fields then feed the "unknown record
+field" diagnostic (the message names the hidden record and the module that declares it). Field lookup
+mirrors the same precedence: in a by-name field access (a base whose type is not yet known), records
+declared here or imported directly form the deciding tier, and a carried record owns a field only when no
+record in that tier declares it, so editing a dependency two hops away can never make a working access
+ambiguous. Two carried records that alone declare a field still tie, and the ambiguity message names
+them. **Externs and
 measures cross too:** an imported `extern` (`Mathx.cbrt`) is exported like a value (its scheme joins the
 interface) and — in the project lowering path — also **bound at top level in its own module** (`cbrt =
 math.cbrt`, `import math` hoisted) so a dependent module references it as `mathx.cbrt`; single-file lowering

INTERNALS.md

@@ -430,8 +430,9 @@ returned topological order (dependencies first, entry last). `project::build_fro
 in the entry's directory). Cross-module *checking* and *emit* consume this `Project`.
 
 **Cross-module checking** (`types::check_module` + `project::check`). *Implementation:* the single-file `run` was generalized to take the imports map and return the module's
-exported value schemes (which now include `extern` names), its exported sum types, **its exported records**,
-**and its measures + measure-aliases**; `check_module(module,
+`ModuleExports` interface: its exported value schemes (which include `extern` names), its exported sum
+types, **its exported records**, **its opaque handle types** (`collect_exported_opaques` /
+`ExportedOpaque`: name + arity, issue #72), **and its measures + measure-aliases**; `check_module(module,
 imports)` seeds imported values under qualified keys and imported sum types into the decls under **qualified
 constructor keys**. The type merge happens in **two halves**, because a local `type` declaration may name an
 imported type (`type Holder = { item: Shapes.Placed }`, DESIGN §6.1): `merge_imported_type_names` runs
@@ -456,6 +457,30 @@ and leaked local variables into the "free in the env" set — blocking generaliz
 bindings, which then exported un-quantified and cascaded onward (#26). Every imported scheme is therefore
 alpha-renamed into the consumer's id space as it is seeded (`Infer::refresh_scheme`, values and constructors
 alike, in sorted order so the ids do not depend on `HashMap` iteration).
+*Transitive interface closure* (issues #72/#75): before `run` hands back its `ModuleExports`,
+`close_over_references` walks every exported scheme, constructor scheme, and record field for `Ty::Con`
+names (`collect_con_names`) and pulls any name satisfied by an import's record/opaque tables into this
+module's own exports, tagged `origin: Some(declaring module)` (own declarations carry `origin: None`);
+newly pulled records are walked in turn, and a seen set terminates the walk on mutually referencing
+records. Each import's interface is itself closed, so one pull per hop reaches any depth. On the consumer
+side `merge_imported_type_names` registers carried entries **last** and under the **bare identity name
+only** (no qualified key, no `record_aliases` entry, so constructing or pattern-matching a carried record
+still requires the direct import); a taken bare name skips the carried entry silently (`record_home`
+recognizes the same record arriving along two paths). By-name field lookup applies the same precedence in
+tiers (`Infer::field_owner_tier`, consulted by `record_of_field` and the pending-field fallback): local
+and directly imported records decide first, and a carried record owns a field only when no direct one
+declares it, so a carried record can never make an existing access ambiguous; a tie between carried
+records with no direct owner is still the ambiguity error, naming the tier that decided. A genuinely
+shadowed record's fields land in
+`Decls::field_hints`, which `record_of_field` / `record_of_field_on` render as "the record `Config` in
+module `Inner` declares this field" instead of a bare unknown. Constructing or matching a carried record
+bare is refused with the fix spelled out (`resolve_record_tag` via `Decls::carried_record_home`: "the
+record `Config` is declared in module `Inner`; import `Inner` to construct its values here", the pattern
+site says "to match"), while a name that is no record at all keeps "not a record type". The lowering side:
+`ModuleExports::carried_records` feeds `project::compile`'s per-module `ImportContext::record_class_modules`
+plus field data keyed by the *declaring* module's tag, so a record **update** in a consumer that never
+imports the declaring module still reconstructs via the right class (`inner.Config(...)`,
+`Lowerer::record_class_name` accepts those modules and hoists their imports).
 `project::check` threads the `ModuleExports` map through the topological order, seeding each module from
 only the modules it actually imports (so an unimported module's members/constructors stay invisible), and
 returns errors grouped by module. *Lowering* routes a qualified constructor — in expression or pattern

src/lowering/mod.rs

@@ -122,6 +122,12 @@ pub struct ImportContext {
     /// (`x` → `Geometry.Point`), so a cross-module update `{ p with x = 3 }`
     /// (which carries no tag) routes to the imported class.
     pub record_field_owners: HashMap<String, String>,
+    /// Modules that declare a **transitively** visible record (`DESIGN.md` §6.1)
+    /// without being imported by this module directly. A record update on such a
+    /// record reconstructs via the declaring module's class (`inner.Config(...)`),
+    /// so its module must be recognized as a class source (and its Python import
+    /// hoisted) even though no `import` names it here.
+    pub record_class_modules: HashSet<String>,
 }
 
 /// A module lowered as part of a multi-file project.
@@ -149,6 +155,7 @@ pub fn lower_in_project(
     let mut lowerer = Lowerer::new(module);
     lowerer.float_literals = float_literals.clone();
     lowerer.imported_modules = ctx.modules.clone();
+    lowerer.record_class_modules = ctx.record_class_modules.clone();
     lowerer.imported_nullary_ctors = ctx.nullary_ctors.clone();
     lowerer
         .newtype_ctors
@@ -318,6 +325,11 @@ struct Lowerer {
     /// A `Geometry.member` reference routes to Python `geometry.member` (vs the
     /// `Geometry_member` mangling used for in-file `module` declarations).
     imported_modules: HashSet<String>,
+    /// Modules that declare a transitively visible record without being imported
+    /// here directly ([`ImportContext::record_class_modules`]). Consulted only by
+    /// [`Lowerer::record_class_name`], so nothing but a record reconstruction can
+    /// route through such a module.
+    record_class_modules: HashSet<String>,
     /// Qualified names of imported nullary constructors (`Palette.Red`), referenced
     /// as values, which must lower to a call (`palette.Red()`) not the bare class.
     imported_nullary_ctors: HashSet<String>,
@@ -610,6 +622,7 @@ impl Lowerer {
             float_literals: HashSet::new(),
             cur_module: None,
             imported_modules: HashSet::new(),
+            record_class_modules: HashSet::new(),
             imported_nullary_ctors: HashSet::new(),
             use_runtime: false,
             project_mode: false,
@@ -2850,10 +2863,13 @@ impl Lowerer {
     /// file module (`Geometry.Point`) becomes dotted attribute access on that module
     /// (`geometry.Point`, with `import geometry` hoisted) so it references the *same*
     /// class the module defines (the consumer never redefines it); a bare tag is the
-    /// record class name (mangled for the reserved `Exception`).
+    /// record class name (mangled for the reserved `Exception`). A tag rooted in a
+    /// module visible only through a transitively carried record
+    /// (`record_class_modules`) routes the same way — an update on such a record
+    /// reconstructs via the declaring module's class.
     fn record_class_name(&mut self, tag: &str) -> String {
         if let Some((base, rec)) = tag.split_once('.')
-            && self.imported_modules.contains(base)
+            && (self.imported_modules.contains(base) || self.record_class_modules.contains(base))
         {
             let module = self.py_module_ref(base);
             format!("{module}.{}", py_record_class(rec))

src/project/mod.rs

@@ -242,9 +242,11 @@ pub fn compile_targeting(
     // Per-module spans of integer literals that inference resolved to `float`, so
     // lowering emits them as `7.0`. Computed in topological order (like `check`) so
     // each module's imports are seeded before it — a literal's float-ness can depend
-    // on a cross-module call. Exports are threaded forward in the same pass.
+    // on a cross-module call. Exports are threaded forward in the same pass and kept:
+    // an import's interface also carries the records it references transitively
+    // (`DESIGN.md` §6.1), which the lowering context below needs.
+    let mut exports: HashMap<String, crate::types::ModuleExports> = HashMap::new();
     let float_spans: HashMap<String, std::collections::HashSet<crate::lexer::Span>> = {
-        let mut exports: HashMap<String, crate::types::ModuleExports> = HashMap::new();
         let mut spans = HashMap::new();
         for module in &project.modules {
             let imports: HashMap<String, crate::types::ModuleExports> = module
@@ -294,6 +296,26 @@ pub fn compile_targeting(
                 }
             }
         }
+        // Records an import's interface carries transitively (declared in a
+        // module this one does not import directly): keyed by the *declaring*
+        // module's tag, so an update on such a record reconstructs via the right
+        // class (`inner.Config(...)`, with `import inner` hoisted). Registered
+        // after the direct entries, which keep precedence for shared field names.
+        for import in &module.imports {
+            let Some(exp) = exports.get(import) else {
+                continue;
+            };
+            for (origin, rec, fields) in exp.carried_records() {
+                let tag = format!("{origin}.{rec}");
+                for field in &fields {
+                    ctx.record_field_owners
+                        .entry(field.clone())
+                        .or_insert_with(|| tag.clone());
+                }
+                ctx.record_fields.entry(tag).or_insert(fields);
+                ctx.record_class_modules.insert(origin);
+            }
+        }
         let floats = float_spans.get(&module.name).unwrap_or(&no_floats);
         let lowered = lowering::lower_in_project(&module.ast, &ctx, floats)?;
         needs_runtime |= lowered.uses_runtime;