diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 59315de..8b8d5c6 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -4390,16 +4390,60 @@ pub(crate) fn synth( } } // Step 4: build the Forall-var → concrete-Type mapping - // from the Type-positional args (in order). + // from the Type-positional args (in order). The written type + // is the binding declaration of each result-only forall var + // (#51): the author's `(con Int)` IS the element type, never + // inferred from later use. let mut mapping: BTreeMap = BTreeMap::new(); + let mut written_type_args: Vec = Vec::with_capacity(vars.len()); for (var, arg) in vars.iter().zip(args.iter()) { if let NewArg::Type(t) = arg { mapping.insert(var.clone(), t.clone()); + written_type_args.push(t.clone()); } // The kind-check loop above guarantees this branch // matches; defensive: a Value arg in a Type slot // would have raised NewArgKindMismatch already. } + // Steps 4b/4c (#51): only for a polymorphic `new` (the call + // carries written type-args binding result-only forall vars). + if !vars.is_empty() { + // Step 4b: the written element type is subject to the + // constructed type's `param-in` restricted set. synth is + // the correct site for this enforcement (unlike + // `pre_desugar_validation`, which has no registry + // access): construct the result `Type::Con` with the + // written args and run it through + // `check_type_well_formed`, which fires + // `ParamNotInRestrictedSet` naming the forbidden element + // (e.g. `Unit`). This is the leg-2 reject; it must run + // before codegen ever mints a `RawBuf_new__` symbol. + let constructed = Type::Con { + name: type_name.clone(), + args: written_type_args.clone(), + }; + check_type_well_formed(&constructed, env)?; + // Step 4c: push a `FreeFnCall` observation so the mono + // pass mints the `RawBuf_new__` specialisation for + // the written element type — bound DIRECTLY (`?a := Int`), + // not via an inference channel. The metas carry the + // written concrete types, so `subst.apply` recovers them + // verbatim and the unobservable-var Unit-default (which + // still applies to genuinely-unpinned vars elsewhere) is + // never reached here. Pushed BEFORE the value-args are + // synthesised so the observation order matches the mono + // walker's `Term::New` arm (which consumes this site's + // slot before descending into the value-args). `new` + // carries no class constraints, so no residuals are + // pushed alongside. + free_fn_calls.push(FreeFnCall { + name: "new".to_string(), + owner_module: home_module.clone(), + forall_vars: vars.clone(), + metas: written_type_args.clone(), + scope: Some(bare_type.clone()), + }); + } // Step 5: synth each value-arg, unify against the // (substituted) corresponding param type. let value_args = &args[vars.len()..]; diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 3be6b8d..96ff174 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -1328,16 +1328,67 @@ fn rewrite_mono_calls( rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); } } - // prep.2 (kernel-extension-mechanics): walker through - // NewArg::Value subterms; type args carry no callable term. - // The Term::New site itself does not consume a mono cursor - // slot — synth desugars it to a global-fn call in a later - // milestone, at which point the call site reads as a Term::App - // and rides the existing Var-arm channel. - Term::New { args, .. } => { - for arg in args.iter_mut() { - if let NewArg::Value(v) = arg { - rewrite_mono_calls(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); + // #51: a `Term::New` carrying a written `NewArg::Type` survives + // desugar (polymorphic `new`, e.g. `(new RawBuf (con Int) 3)`) + // and is lowered to a monomorphised global-fn call HERE. synth + // pushed exactly one `FreeFnCall` observation for this site + // (BEFORE its value-args), so the cursor slot at `*cursor` is the + // mono target for `RawBuf_new__`. We rename the call to the + // mangled symbol, then descend into the value-args (which become + // the App args) so their own cursor advances stay aligned. + // + // A type-arg-free `Term::New` (monomorphic `new`, e.g. + // `(new Counter 42)`) was already lowered to `(app T.new …)` at + // desugar and never reaches this arm — synth pushed no + // observation, so no slot is consumed. + Term::New { type_name, args, .. } => { + let has_type_arg = args.iter().any(|a| matches!(a, NewArg::Type(_))); + if has_type_arg { + let callee_name = if let Some(Some(MonoTarget::FreeFn { + name: fn_name, + type_args, + defining_module, + scope, + })) = ordered_targets.get(*cursor) + { + let sym = mono_symbol_n(&scoped_base(scope, fn_name), type_args.as_slice()); + if defining_module == caller_module { + sym + } else { + format!("{}.{}", defining_module, sym) + } + } else { + // Slot is None / non-concrete: leave an unmangled + // type-scoped spelling. The written type-arg is + // concrete (it is the author's annotation), so this + // branch is not expected; fall back to the + // type-scoped name (`RawBuf` from `raw_buf.RawBuf`) + // rather than panic. + let bare_type = + type_name.rsplit('.').next().unwrap_or(type_name.as_str()); + format!("{bare_type}.new") + }; + *cursor += 1; + // Rewrite value-args in place (advances the cursor for + // any nested mono calls), then replace the node with the + // equivalent app to the monomorphised `new`. + let mut value_args: Vec = Vec::new(); + for arg in args.iter_mut() { + if let NewArg::Value(v) = arg { + rewrite_mono_calls(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); + value_args.push(v.clone()); + } + } + *body = Term::App { + callee: Box::new(Term::Var { name: callee_name }), + args: value_args, + tail: false, + }; + } else { + for arg in args.iter_mut() { + if let NewArg::Value(v) = arg { + rewrite_mono_calls(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); + } } } } @@ -1719,10 +1770,20 @@ fn interleave_slots( interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); } } - // prep.2 (kernel-extension-mechanics): walker through - // NewArg::Value subterms; Term::New itself does not push a - // mono slot — see `rewrite_mono_calls`'s arm for the rationale. + // #51: a `Term::New` carrying a written `NewArg::Type` survives + // desugar and synth pushed exactly one `FreeFnCall` observation + // for it (BEFORE its value-args), so it consumes one free-fn + // slot HERE — mirroring `rewrite_mono_calls`'s `Term::New` arm + // so the two walkers stay in lockstep. A type-arg-free `Term::New` + // was lowered to `(app T.new …)` at desugar and never reaches + // this arm, pushing no slot. Term::New { args, .. } => { + let has_type_arg = args.iter().any(|a| matches!(a, NewArg::Type(_))); + if has_type_arg { + let slot = free_fn_slots.get(*free_cur).cloned().unwrap_or(None); + out.push(slot); + *free_cur += 1; + } for arg in args { if let NewArg::Value(v) = arg { interleave_slots(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 16718f4..32b3c06 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -1051,29 +1051,50 @@ impl Desugarer { in_full } Term::New { type_name, args } => { - // raw-buf.4: (new T ) desugars to - // (app T.new ) — a type-scoped call so synth's - // dotted-name branch resolves it through the - // TypeDef-first ladder and the raw-buf.3 scope threading - // mints `T_new__`. The leading NewArg::Type is - // dropped: the AST carries no type-args on App, and the - // element type is recovered by ordinary inference from - // how the result is used (spec § Term::New desugar). - // Runs before check, so no Term::New reaches the - // type-checker or codegen. - let value_args: Vec = args - .iter() - .filter_map(|arg| match arg { - NewArg::Value(v) => Some(self.desugar_term(v, scope)), - NewArg::Type(_) => None, - }) - .collect(); - Term::App { - callee: Box::new(Term::Var { - name: format!("{type_name}.new"), - }), - args: value_args, - tail: false, + // #51: honour the written element type-arg. When the + // `new` is polymorphic (the call carries a leading + // `NewArg::Type`, e.g. `(new RawBuf (con Int) 3)`), the + // written type is the binding declaration of the result's + // forall var — it must NOT be discarded. We keep + // `Term::New` surviving into synth, which binds that var + // directly to the written type (`?a := Int`) and pushes + // the matching mono observation so codegen mints + // `RawBuf_new__Int` (and enforces `param-in` on the + // written type). The value-args are desugared in place. + // + // When the `new` is monomorphic (no `NewArg::Type`, e.g. + // `(new Counter 42)`) there is no var to bind, so we keep + // the raw-buf.4 lowering to `(app T.new )` — a + // type-scoped call that synth's dotted-name branch + // resolves through the TypeDef-first ladder. + let has_type_arg = args.iter().any(|a| matches!(a, NewArg::Type(_))); + if has_type_arg { + let desugared_args: Vec = args + .iter() + .map(|arg| match arg { + NewArg::Value(v) => NewArg::Value(self.desugar_term(v, scope)), + NewArg::Type(ty) => NewArg::Type(ty.clone()), + }) + .collect(); + Term::New { + type_name: type_name.clone(), + args: desugared_args, + } + } else { + let value_args: Vec = args + .iter() + .filter_map(|arg| match arg { + NewArg::Value(v) => Some(self.desugar_term(v, scope)), + NewArg::Type(_) => None, + }) + .collect(); + Term::App { + callee: Box::new(Term::Var { + name: format!("{type_name}.new"), + }), + args: value_args, + tail: false, + } } } Term::Intrinsic => t.clone(),