Skip to content

Reclassify the match-arm proven-disjoint InternalError as a located TypeMismatch #13595

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
gunbai-bot wants to merge 2 commits into from
Closed

Reclassify the match-arm proven-disjoint InternalError as a located TypeMismatch #13595

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4983592
Reclassify the match-arm disjointness InternalError as a located Type…
Oct 8, 2026
df2c362
Regenerate the infer mirror; collection class assertion admits the se…
Oct 8, 2026
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
36 changes: 36 additions & 0 deletions dag/test/claim/match_arm_join_disjoint_coproduct_witness_test.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,26 @@
module test.claim.match_arm_join_disjoint_coproduct_witness_test

import gunbc.compile_diagnostic_census {
CompileDiagnosticCensus,
CensusObserved,
CensusNotRunnable,
census_blocking_rows,
census_rows_of_class,
census_total_count
}
import std.types { String, Bool }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

fn maj_blocking_count(source: String, wanted: String) -> Int {
match compile_dag_diagnostic_census(source) {
CensusObserved { rows: rows } =>
census_total_count(rows: census_rows_of_class(rows: census_blocking_rows(rows: rows), wanted: wanted))
CensusNotRunnable { cause: _ } => 0 - 1
}
}

// A MATCH JOIN ANSWERED WITH ONE ARM AND NEVER JUDGED THE REST, SO THE VERDICT FLIPPED WITH ARM
// ORDER. v1.compiler.infer builds a match expression's type by folding every arm's body type through
// v1.compiler.infer_types prefer_specific_type, whose tie-break for two disjoint coproducts is the
Expand Down Expand Up @@ -178,3 +199,18 @@ test fn maj_matching_ground_element_collection_arms_still_compile() -> Bool {
[]
)
}

// A DISJOINT ARM IS A SOURCE TYPE ERROR, so it is a typed TypeMismatch located at the offending arm,
// never an InternalError: InternalError names a compiler defect (a state the compiler could not
// have been handed), and reading it as one sent authors looking for a bug in a correct compiler.
// Both the scalar and the collection ground relations are asserted by CLASS, and the InternalError
// count is pinned to zero so the reclassification cannot silently revert.
test fn maj_kernel_arm_mismatch_is_a_typed_mismatch() -> Bool {
maj_blocking_count(source: maj_kernel_arm_mismatch_fixture_source(), wanted: "TypeMismatch") == 1
&& maj_blocking_count(source: maj_kernel_arm_mismatch_fixture_source(), wanted: "InternalError") == 0
}

test fn maj_collection_arm_mismatch_is_a_typed_mismatch() -> Bool {
maj_blocking_count(source: maj_ground_element_collection_mismatch_fixture_source(), wanted: "TypeMismatch") >= 1
&& maj_blocking_count(source: maj_ground_element_collection_mismatch_fixture_source(), wanted: "InternalError") == 0
}
10 changes: 3 additions & 7 deletions src/v1/04_infer.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3081,13 +3081,9 @@ fn match_arm_join_diagnostics(unified_arm_type: Node, arm: ArmInferResult, scope
arm_type: arm.body_type,
scope: scope
) {
[inference_error(
message: concat(
"match arms produce proven-disjoint types: ",
node_type_shape(n: unified_arm_type, source_indices: scope.type_env.source_indices),
" vs ",
node_type_shape(n: arm.body_type, source_indices: scope.type_env.source_indices)
),
[type_mismatch_error(
expected: node_type_shape(n: unified_arm_type, source_indices: scope.type_env.source_indices),
got: node_type_shape(n: arm.body_type, source_indices: scope.type_env.source_indices),
span: arm_body(n: arm.typed_arm).span,
module_name: scope.module_name
Comment on lines +3084 to 3088

@chatgpt-codex-connector chatgpt-codex-connector Bot Oct 9, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Update the existing disjoint-arm witness

When the full claim suite runs present_payload_arm_disjoint_from_sibling_still_refuses in self_host_equality_admission_witness_test.dag, that test still requires one InternalError with the removed message match arms produce proven-disjoint types: .... This branch now emits only a TypeMismatch, so the count becomes zero and the existing witness fails even though the source is still correctly rejected. Update that witness to assert the new diagnostic class and subject along with this reclassification.

Useful? React with 👍 / 👎.

)]
Expand Down
24 changes: 8 additions & 16 deletions src/v1/stage0/src/v1_compiler_infer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4312,22 +4312,14 @@ pub fn match_arm_join_diagnostics(
arm.body_type.clone(),
scope.clone(),
) {
Rc::new(vec![inference_error(
v1_rt::concat(
v1_rt::concat(
v1_rt::concat(
"match arms produce proven-disjoint types: ".to_string(),
crate::v1_compiler_infer_types::node_type_shape(
unified_arm_type.clone(),
scope.type_env.clone().source_indices.clone(),
),
),
" vs ".to_string(),
),
crate::v1_compiler_infer_types::node_type_shape(
arm.body_type.clone(),
scope.type_env.clone().source_indices.clone(),
),
Rc::new(vec![type_mismatch_error(
crate::v1_compiler_infer_types::node_type_shape(
unified_arm_type.clone(),
scope.type_env.clone().source_indices.clone(),
),
crate::v1_compiler_infer_types::node_type_shape(
arm.body_type.clone(),
scope.type_env.clone().source_indices.clone(),
),
crate::v1_std_core::arm_body(arm.typed_arm.clone())
.span
Expand Down
Loading