Repository navigation
Refine empty collection constraints through generic callback results - #11313
Closed
gunbai-bot[bot] wants to merge 8 commits into
Closed
gunbai-bot[bot] wants to merge 8 commits into
gunbai-bot[bot] wants to merge 8 commits into
Conversation
Contributor
Author
|
Baseline control receipt: The positive assertions at this checkpoint inspect the InternalError class; they returned true but exceeded budget. The three negatives returned false: the expected InternalError was absent. This demonstrates the missing refusal class, not clean compilation of the positive programs. Commit 34c3135 strengthens positives to require zero total blocking diagnostics; those stronger assertions await execution. Source-check probe over src/v1/04_infer.dag with the baseline seed reports a blocking unresolved fold_terminal_expr outside the changed functions. It is not a green compiler-closure receipt; baseline comparison is running. No generated mirrors have been installed. |
Contributor
Author
|
Canonical-seed RED receipt for strengthened controls at 34c3135, using #11277 seed from bb124a8 via capped local claim_batch (Rayon4, ulimit -v22000000, unchanged500ms ceiling). All three clean-compilation positives return false; both conflict-refusal controls also return false. The missing-field negative returns true but exceeds the cap; by itself it does not establish the intended element was determined, so it must be paired with the positive after repair. The read-only src/v1/04_infer.dag check reports the same sole blocking fold_terminal_expr unresolved call on both the modified source and untouched b55fb52. There are no diagnostics at the changed functions in that check; it is not an emitted-route or fixed-point receipt. |
This was referenced Sep 13, 2026
Source f511bb0. required-regen --regen-affected-scope selected WholePopulationScope; planned/executed/adjudicated 155, first_generation_equal=false, sole generated-surface drift v1_compiler_infer.rs. Entire candidate src comparison confirms precisely that mirror differs. Candidate-only Cargo.toml is crate-layout output and was not installed. RLIMIT_AS 23622320128 bytes; sampled peak RSS 11275136 KiB. No generated mirror hand edits.
Contributor
Author
|
Regeneration at source f511bb0 completed under RLIMIT_AS=23622320128 bytes (22 GiB), with Final elapsed751.511s, sampled peak RSS11,275,200KiB. This final peak supersedes the commit message's earlier sampled reading of11,275,136KiB. Exit1 is the pre-installation drift verdict, not a fixed-point pass. The earlier invocation omitted source roots and stopped at CLI validation before any emission. The regenerated seed rebuild and behavioral controls remain pending. Regeneration logRSS samples |
Contributor
Author
|
Baseline acceptance check for the two conflict controls: the same source strings from test.claim.empty_collection_constraint_witness were compiled through compile_declared_import_closure_only_with_pool, with is_interpreter_blocking_diagnostic counting the complete diagnostic population. Both programs have zero blocking diagnostics, including their source modules. Thus first-binding retention and skipped callback-result constraints are observed fail-open behaviors, not an existing refusal under another class. Baseline seed: b55fb52; scoped source inputs and read-only probe below. Probe sourceuse v1_compiler::cli_run::compile_declared_import_closure_only_with_pool;
use v1_compiler::v1_std_core::{diagnostic_to_message, diagnostic_to_span, is_interpreter_blocking_diagnostic};
fn main() {
let roots=vec!["dag".to_owned(),"src/v2".to_owned(),"target/conflict-fixtures".to_owned()];
for name in ["conflicting_established_constraints_refuse", "callback_result_conflict_refuses"] {
let entry=format!("target/conflict-fixtures/{name}.dag");
let result=compile_declared_import_closure_only_with_pool(&roots,&entry,None).expect("readable fixture");
let mut total=0; let mut subject=0;
for d in result.diagnostics.iter() {
if is_interpreter_blocking_diagnostic(d.diagnostic.clone()) {
total+=1;
let span=diagnostic_to_span(d.diagnostic.clone());
if span.file.ends_with(&format!("{name}.dag")) { subject+=1; println!("{name}: {:?}: {}",d.diagnostic,diagnostic_to_message(d.diagnostic.clone())); }
}
}
println!("{name}: blocking_total={total} subject_blocking={subject}");
}
}callback_result_conflict_refuses.dag conflicting_established_constraints_refuse.dag |
Contributor
Author
|
Regenerated seed dbbcbde builds, but scoped control entry resolution refuses at v2.std.diagnostic.sequence_outcome before any claim evaluates. The typed-body probe identifies the exact constraints: empty is Outcome<FreeMonoid>, callback result is Outcome<List>. The new refinement incorrectly compared raw constructor names. The existing v1.compiler.infer_types.canonical_template_name is already the declared container-algebra head projection used by compatibility; the source correction consumes that projection without changing compatibility or adding an alias table. A source-level collection_alias_callback_result_binds control preserves this alias boundary. No corpus spelling changed. Read-only typed-body probeuse v1_compiler::cli_run::compile_declared_import_closure_only_with_pool;
use v1_compiler::v1_std_core::{Node, ExprData, InferredNode, authored_name_at, arg_name_at, arg_value, diagnostic_to_span, diagnostic_to_message, is_interpreter_blocking_diagnostic};
use v1_compiler::v1_compiler_infer_types::resolved_type;
fn shape(n: &Node, depth: usize) -> String {
if depth == 0 { return "<depth-limit>".into(); }
let inferred = match n.inferred.as_deref() {
Some(InferredNode::TypeVariable { id }) => format!("TV({id})"),
Some(InferredNode::Resolved { node }) => format!("resolved({})", shape(node, depth - 1)),
Some(_) => "other-inferred".into(),
None => "uninferred".into(),
};
format!("{}:{:?}[{}]:{}", n.name, n.connective,
n.children.iter().map(|c| shape(c, depth - 1)).collect::<Vec<_>>().join(","), inferred)
}
fn main() {
let roots=vec!["dag".into(),"src/v2".into()];
let result=compile_declared_import_closure_only_with_pool(&roots,"src/v2/std/diagnostic.dag",None).expect("readable corpus module");
if let Some(graph)=&result.graph {
for module in graph.modules.iter() { for item in module.items.iter() {
if authored_name_at(result.source_indices.clone(),item.clone())!="sequence_outcome" {continue;}
println!("sequence_outcome progress={:?}",module.progress);
let mut work=vec![item.clone()];
while let Some(n)=work.pop() {
if matches!(n.expr_data.as_ref(),ExprData::ExprCall{..}) && authored_name_at(result.source_indices.clone(),n.clone())=="fold_list" {
for a in n.children.iter() {println!("argument {:?}: {}",arg_name_at(a.clone(),result.source_indices.clone()),shape(&resolved_type(arg_value(a.clone())),7));}
}
work.extend(n.children.iter().cloned()); if let Some(body)=&n.body {work.push(body.clone());}
}
}}
}
for d in result.diagnostics.iter() { if is_interpreter_blocking_diagnostic(d.diagnostic.clone()) {println!("blocking {:?}: {}",diagnostic_to_span(d.diagnostic.clone()),diagnostic_to_message(d.diagnostic.clone()));}}
}The corpus probe with this seed still observes unresolved receiver T and conflict diagnostics, so no type-binding closure or floor green is claimed. A further regeneration is needed for the measured source correction; the earlier regeneration is not reused as validation of changed source. |
Source a5df024. required-regen --regen-affected-scope: WholePopulationScope; planned/executed/adjudicated 155; sole generated drift v1_compiler_infer.rs. Whole candidate src comparison confirms only this mirror differs; candidate-only Cargo.toml not installed. Elapsed 742.539 seconds, sampled peak RSS 11272528 KiB, RLIMIT_AS 23622320128 bytes. Pre-installation drift receipt, not fixed-point pass; no generated hand edits.
Contributor
Author
|
Alias-correction regeneration at a5df024 completed under the same22GiB RLIMIT_AS. WholePopulationScope planned/executed/adjudicated155; only v1_compiler_infer.rs drifted. Whole candidate src comparison independently agrees; candidate-only Cargo.toml was not installed. Mirror committed at d946695. Elapsed742.539s; sampled peak RSS11,272,528KiB. Exit1 is expected pre-installation drift, not a fixed-point pass. Rebuilt-seed controls are pending; this receipt does not green the first run's refusal. Regeneration logRSS samples |
Contributor
Author
|
Investigated run 34784750994 at a5df024: both the floor and heal jobs refused |
Contributor
Author
|
Regenerated seed at d946695 builds successfully. Scoped seven-control run completed: A read-only compile probe of the same three authored positive source strings finds exactly one blocking InternalError in each: conflicting established generic constraints at the inner |
Contributor
Author
|
Remaining positive-control refusal reduced on d946695 with a read-only typed-node probe of the exact Gatekeeper decision requested (dashboard message msg_6a5f7bc4-c0a8-4642-a19d-967ea47c4a3b): compose canonical projection and refinement, or move the prerequisite projection into an earlier cut. No private unwrap or second argument reader is being introduced here. The current required ordering cannot be treated as evidence that the standalone branch has the prerequisite. |
Contributor
Author
|
Investigated d946695 run 34785453117, heal-generated-artifacts job 103802061984: regeneration refuses corpus generic constraints (including body_producer_forward); sequence_outcome is no longer listed. This is not a passing standalone head. Fierce-lark/eager-raven ruling msg_223de1ef now composes this refinement with canonical argument projection inside #11277. The merge is in progress; its two generated conflicts are being regenerated from the combined authorities. #11313 will close as superseded once that merge is committed and pushed, retaining its model, controls and receipts. |
Contributor
Author
|
Superseded by #11277 under fierce-lark/eager-raven composition ruling msg_223de1ef. Merge commit 87ed64a, pushed as part of dfc7d1f, retains this PR’s model, controls and history; its receipts remain linked from #11277. This closes the separate PR, not the outstanding composed validation obligation. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Empty accumulators lose their element constraint: an unresolved expected formal produces Unit, the generic pass ignores callback results, and unification keeps its first binding. The canonical seed in #11277 exposes this on
v2.compiler.compile.native_lane_universe_after_ownership. This prerequisite repairs the seed rule before #11277 consumes it.PURPOSE: bounded v1 maintenance serves the self-host program's executable seed route. Authorized by fierce-lark via eager-raven msg_c3639cd6. No new builtin, admission row or public surface. Draft implementation at dbbcbde. The model and controls landed first, then the approved caller migration and the regenerated inference mirror. Regenerated-seed execution and composition validation are pending.
Model: [] contributes an unresolved element variable. Concrete arguments and callback results refine unresolved substitution slots; the rebinding pass applies the result. Established constructor structure and cardinality remain constraints; conflicts produce existing inference_error diagnostics at the call argument. No arbitrary concrete preference or node_type_compatible widening. Never-constrained enclosing T must still refuse field access after composition with #11285; callee-unbound generics retain their existing deferral scope.
Approved caller census (msg_bca90a0c): infer_call_arguments_generic_pass; infer_expr_body ExprListLit/ExprLambda and ExprCall borrowed-function-value branch; unify_generics; borrowed_callable_call_type; unify_record_lit_field_walk; unify_record_lit_generics. A shared substitution-and-diagnostics carrier replaces the Map-only result throughout; diagnostics cannot be discarded. New internal declarations require a seed-growth receipt.
Controls: test.claim.empty_collection_constraint_witness empty fold, nested empty fold, callback-result-determined element, missing field on the determined element, conflicting concrete arguments and conflicting callback result. Corpus RED on the canonical seed: paired baseline and current receipt. Baseline controls and the canonical-seed REDs are executed. The two conflict programs also compile with zero total blocking diagnostics on the baseline seed, establishing accepted invalid constraints; see the linked receipts below. The #11285 never-constrained-generic discriminator and both same-spelling/lambda binding controls must compose; its branch is not yet on main.
One bounded regeneration completed and installed only v1_compiler_infer.rs after whole candidate comparison. Scoped regenerated-seed execution, canonical-seed composition, exact-head CI, gatekeeper review and srv2 adjudication-grain receipt remain owed. The v2-side substitution trigger is fierce-swift's adhoc-8760f34f-ec2; a seed repair does not retire that obligation.
OWED DELETION — side-chat ApproveTemporaryIntroduction turn d8e989c8 admits exactly one identity adapter, v2.compiler.body_lowering_fold.body_lower_allocation_edge_population, at body_lower_fold_children / occurrence_allocation_fold xs in #11267. The scaffold obligation discharges only when the canonical generic-argument substitution repair represented by #11277 is present in the composition AND body_lower_allocation_edge_population and its sole call are deleted, with the direct parent.children -> occurrence_allocation_fold(xs: ...) route passing the discriminator. #11277 cannot close while the adapter survives. The substitution-capable landing must include deletion; merge of a repair alone is insufficient.
Regeneration and RSS receipt, canonical-seed REDs, and baseline accepts conflicting arguments and callback result. The unchanged 500ms ceiling still applies: earlier positive class checks exceeded it, and no floor timing pass is claimed. The seed-growth row records four new .dag declarations and generated-only Rust growth; hand-authored Rust growth is zero.