types: alpha-rename imported schemes into the consumer's id space

INTERNALS.md

@@ -339,7 +339,14 @@ plus imported measures merged unqualified into `decls.measures`/`measure_aliases
 check), so construction (the `Record`/`Field` arms), qualified ctor/record patterns (`bind_pattern`),
 exhaustiveness (`ctor_signature`), and `<…>` unit resolution all resolve with no special cases. Transplanting a scheme across modules is sound
 because a top-level binding (and a constructor) generalizes against an env of closed schemes, so its own
-scheme is closed and `instantiate` refreshes the quantified vars in the dependent module's id space.
+scheme is closed — but *closed is not enough*: every module allocates variable ids from its own counter
+starting at `RESERVED_VARS`, so an imported scheme arrives holding ids the consumer will hand out again.
+`instantiate` alone survives that (it refreshes the quantified vars before substituting), yet `env_free_vars`
+applies the **local** substitution to every env scheme, so a single id collision rewrote the imported scheme
+and leaked local variables into the "free in the env" set — blocking generalization of the consumer's own
+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).
 `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/types/mod.rs

@@ -1001,14 +1001,24 @@ fn run(module: &Module, record: bool, imports: &HashMap<String, ModuleExports>)
     let mut env = ctor_env;
     // Seed imported modules' exported values (under qualified keys like
     // `Geometry.area`) and constructors (`Geometry.Circle`) so the `Field` access
-    // path resolves cross-module references.
-    for (module_name, exports) in imports {
-        for (member, scheme) in &exports.schemes {
-            env.insert(format!("{module_name}.{member}"), scheme.clone());
+    // path resolves cross-module references. Each scheme is alpha-renamed into
+    // this module's variable space first ([`Infer::refresh_scheme`]) — it arrives
+    // holding the exporting module's ids, which this module allocates too.
+    // Sorted so the ids handed out do not depend on `HashMap` iteration order.
+    let mut import_names: Vec<&String> = imports.keys().collect();
+    import_names.sort();
+    for module_name in import_names {
+        let exports = &imports[module_name];
+        let mut members: Vec<&String> = exports.schemes.keys().collect();
+        members.sort();
+        for member in members {
+            let scheme = inf.refresh_scheme(&exports.schemes[member]);
+            env.insert(format!("{module_name}.{member}"), scheme);
         }
         for ty in &exports.types {
             for (ctor, info) in &ty.ctors {
-                env.insert(format!("{module_name}.{ctor}"), info.scheme.clone());
+                let scheme = inf.refresh_scheme(&info.scheme);
+                env.insert(format!("{module_name}.{ctor}"), scheme);
             }
         }
     }
@@ -6268,6 +6278,82 @@ impl Infer {
         subst_all(&scheme.ty, &tmap, &umap, &nmap, &emap)
     }
 
+    /// Alpha-rename an imported scheme into *this* module's variable space.
+    ///
+    /// Every module's inference allocates ids from its own counter starting at
+    /// [`RESERVED_VARS`], so a scheme transplanted from a dependency arrives
+    /// holding ids this module will hand out again. [`Infer::instantiate`] is safe
+    /// on its own (it refreshes the quantified vars before substituting), but
+    /// [`Infer::env_free_vars`] applies the **local** substitution to every env
+    /// scheme — so one collision silently rewrites the imported scheme *and* leaks
+    /// local variables into the "free in the environment" set, which then blocks
+    /// generalization of this module's own bindings (an importing module's
+    /// `let f a b = (a, b)` going monomorphic). Refreshing every id once, at the
+    /// boundary, makes the collision impossible.
+    ///
+    /// Renames free ids as well as quantified ones: a scheme should arrive closed,
+    /// but a free id is exactly the case that must not alias a local variable.
+    fn refresh_scheme(&mut self, scheme: &Scheme) -> Scheme {
+        let mut t_ids = scheme.vars.clone();
+        free_type_vars(&scheme.ty, &mut |v| {
+            if !t_ids.contains(&v) {
+                t_ids.push(v);
+            }
+        });
+        let mut u_ids = scheme.uvars.clone();
+        free_unit_vars(&scheme.ty, &mut |v| {
+            if !u_ids.contains(&v) {
+                u_ids.push(v);
+            }
+        });
+        let mut n_ids = scheme.num_vars.clone();
+        free_num_vars(&scheme.ty, &mut |v| {
+            if !n_ids.contains(&v) {
+                n_ids.push(v);
+            }
+        });
+        let mut e_ids = scheme.eff_vars.clone();
+        free_eff_vars(&scheme.ty, &mut |v| {
+            if !e_ids.contains(&v) {
+                e_ids.push(v);
+            }
+        });
+
+        let tmap: HashMap<u32, u32> = t_ids.into_iter().map(|v| (v, self.fresh_id())).collect();
+        let umap: HashMap<u32, u32> = u_ids.into_iter().map(|v| (v, self.fresh_id())).collect();
+        let nmap: HashMap<u32, u32> = n_ids.into_iter().map(|v| (v, self.fresh_id())).collect();
+        let emap: HashMap<u32, u32> = e_ids.into_iter().map(|v| (v, self.fresh_id())).collect();
+
+        let rename = |ids: &[u32], map: &HashMap<u32, u32>| -> Vec<u32> {
+            ids.iter().map(|v| *map.get(v).unwrap_or(v)).collect()
+        };
+        let ty = subst_all(
+            &scheme.ty,
+            &tmap
+                .iter()
+                .map(|(old, new)| (*old, Ty::Var(*new)))
+                .collect(),
+            &umap
+                .iter()
+                .map(|(old, new)| (*old, Unit::var(*new)))
+                .collect(),
+            &nmap,
+            &emap
+                .iter()
+                .map(|(old, new)| (*old, Effect::var(*new)))
+                .collect(),
+        );
+        Scheme {
+            vars: rename(&scheme.vars, &tmap),
+            uvars: rename(&scheme.uvars, &umap),
+            num_vars: rename(&scheme.num_vars, &nmap),
+            ord_vars: rename(&scheme.ord_vars, &tmap),
+            eff_vars: rename(&scheme.eff_vars, &emap),
+            mutable: scheme.mutable,
+            ty,
+        }
+    }
+
     fn generalize(&self, env: &Env, ty: &Ty) -> Scheme {
         let ty = self.apply(ty);
         let (env_t, env_u, env_n, env_e) = self.env_free_vars(env);

tests/project.rs

@@ -953,3 +953,56 @@ fn e2e_an_option_crosses_the_module_boundary() {
         assert_eq!(out.trim(), "7");
     }
 }
+
+#[test]
+fn an_importing_module_keeps_its_own_functions_polymorphic() {
+    // An imported scheme arrives holding the *exporting* module's variable ids,
+    // which this module allocates too. Before those ids were refreshed at the
+    // boundary, one collision let `env_free_vars` rewrite the imported scheme and
+    // leak local variables into the environment's free set — blocking
+    // generalization of Main's own bindings, so `f1` went monomorphic and its
+    // second use was rejected. Main does not even use the import; the exact shapes
+    // matter only in that they make the two modules' id ranges overlap.
+    let project = build_mem(
+        "Main",
+        &[
+            (
+                "Main",
+                "import Helper\nlet f0 a b = (a, b)\nlet f1 a b = (a, b)\nprint (f1 1 2)\nprint (f1 \"x\" \"y\")",
+            ),
+            ("Helper", "let id x = x\nlet id2 y = y"),
+        ],
+    );
+    let errors = project::check(&project);
+    assert!(
+        errors.is_empty(),
+        "an importing module's own function must stay polymorphic: {errors:?}"
+    );
+}
+
+#[test]
+fn an_under_generalized_export_does_not_cascade_to_a_consumer() {
+    // The contagious half, one module further along: `Middle` imports `Helper`,
+    // and the blocked generalization above made `Middle.f1` *export* with nothing
+    // quantified — so `Main` received one shared type variable for every use site
+    // and its second use was rejected, naming a function two modules away.
+    let project = build_mem(
+        "Main",
+        &[
+            (
+                "Main",
+                "import Middle\nprint (Middle.f1 1 2)\nprint (Middle.f1 \"x\" \"y\")",
+            ),
+            (
+                "Middle",
+                "import Helper\nlet f0 a b = (a, b)\nlet f1 a b = (a, b)",
+            ),
+            ("Helper", "let id x = x\nlet id2 y = y"),
+        ],
+    );
+    let errors = project::check(&project);
+    assert!(
+        errors.is_empty(),
+        "an exported polymorphic function must instantiate freshly per use: {errors:?}"
+    );
+}