Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 23 additions & 19 deletions src/v1/stage0/src/v1_compiler_infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4781,27 +4781,31 @@ pub fn nominal_product_head_name_if_declared_product(
name: String,
scope: Rc<InferScope>,
) -> String {
let representative =
transparent_alias_representative(scope.type_env.clone().symbol_index.clone(), name.clone());
match crate::v1_compiler_infer_env::lookup_type_by_name(
scope.type_env.clone(),
representative.clone(),
) {
Some(decl) => {
let peeled = crate::v1_compiler_infer_resolve::peel_nominal_alias_identity(
decl.clone(),
scope.type_env.clone(),
scope.module_name.clone(),
);
if ((peeled.connective.clone() == Connective::Conj)
&& ((peeled.children.clone().len() as i64) > 0))
{
name.clone()
} else {
"".to_string()
{
let representative = transparent_alias_representative(
scope.type_env.clone().symbol_index.clone(),
name.clone(),
);
match crate::v1_compiler_infer_env::lookup_type_by_name(
scope.type_env.clone(),
representative.clone(),
) {
Some(decl) => {
let peeled = crate::v1_compiler_infer_resolve::peel_nominal_alias_identity(
decl.clone(),
scope.type_env.clone(),
scope.module_name.clone(),
);
if ((peeled.connective.clone() == Connective::Conj)
&& ((peeled.children.clone().len() as i64) > 0))
{
name.clone()
} else {
"".to_string()
}
}
std::option::Option::None => "".to_string(),
}
std::option::Option::None => "".to_string(),
}
}

Expand Down
16 changes: 14 additions & 2 deletions src/v2/workflow/floor_expected_red.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1086,7 +1086,19 @@ fn floor_expected_red_chunk_interpreter_first_optional_divergence() -> List<Stri
// different heads are admitted. The claim was a guess wearing a measurement's clothes, and it is
// the same failure this file already records one paragraph above.
//
// SEVEN IDENTITIES, because each names a discrimination a partial repair could miss while greening
// SIX IDENTITIES NOW, SEVEN AS ENROLLED, and the difference is a climb rather than an edit. The
// plain-record row -- a different plain record at a declared return -- PASSED on 2026-09-04 after
// #10402 enforced concrete nominal record inhabitance at declarations, so the roster's
// self-emptying arm fired exactly as the paragraph below says it would: the row named itself for
// removal by reddening the build, and it is removed here. Its witness is NOT retired; under
// DESIGN 4b(4) `w_a_different_plain_record_at_a_declared_return_is_refused` stays enrolled in
// `dag/test/claim/declared_type_expected_type_path_witness_test.dag` as a permanent regression
// control, and it is now a passing one. WHAT DID NOT CLIMB: the six application rows below still
// fail, so the honest statement above is unchanged for them -- in declared-return position two
// nominal APPLICATIONS are still not compared. #10402 closed the plain-record half of that
// sentence and nothing else, which is why this is one removal and not the roster emptying.
//
// EACH REMAINING IDENTITY names a discrimination a partial repair could miss while greening
// the others -- and greening them is not harmless, since this roster SELF-EMPTIES on pass. A repair
// comparing only the first argument would retire the two position-zero rows while the production
// Measure<Memory, Gibi, Nat> hole, which differs at the MIDDLE argument, stayed open. One comparing
Expand All @@ -1110,7 +1122,7 @@ fn floor_expected_red_chunk_24() -> List<String> {
tail: Cons { head: "test.claim.declared_type_expected_type_path_witness.w_a_different_application_head_at_a_declared_return_is_refused",
tail: Cons { head: "test.claim.declared_type_expected_type_path_witness.w_a_wrong_last_type_argument_at_a_declared_return_is_refused",
tail: Cons { head: "test.claim.declared_type_expected_type_path_witness.w_a_wrong_nested_type_argument_at_a_declared_return_is_refused",
tail: Cons { head: "test.claim.declared_type_expected_type_path_witness.w_a_different_plain_record_at_a_declared_return_is_refused", tail: Empty {} } } } } } } }
tail: Empty {} } } } } } }
}

fn floor_expected_red_chunk_live_tree_admission() -> List<String> {
Expand Down
Loading