diff --git a/compiler/build.odin b/compiler/build.odin
index 4e44933..8977061 100644
--- a/compiler/build.odin
+++ b/compiler/build.odin
@@ -336,7 +336,7 @@ unwrap_coercions :: proc(m: ^hir.Module, id: hir.Expr_Id) -> hir.Expr_Id {
 	for cur != hir.INVALID_EXPR && int(cur) < len(m.exprs) {
 		#partial switch m.exprs[cur].kind {
 		case .Retype, .Pointer_Cast, .Weaken_Slice, .Weaken_Pointer, .Decay_Array_Pointer, .Slice_Ptr,
-		     .Widen, .Sum_Widen, .Optional_Some, .C_Coerce, .Scalar_Cast:
+		     .Widen, .Sum_Widen, .Sum_Project, .Optional_Some, .C_Coerce, .Scalar_Cast:
 			cur = m.exprs[cur].left
 		case:
 			return cur
diff --git a/compiler/checker/checker.odin b/compiler/checker/checker.odin
index 9638e84..460e7f3 100644
--- a/compiler/checker/checker.odin
+++ b/compiler/checker/checker.odin
@@ -95,6 +95,11 @@ Defer_Entry :: struct {
 	capture:    hir.Local_Id,
 }
 
+Error_Refinement :: struct {
+	local:    hir.Local_Id,
+	variants: []u32,
+}
+
 Build_Ctx :: struct {
 	checker:      ^Checker,
 	pkg:          ast.Package_Id,
@@ -109,6 +114,7 @@ Build_Ctx :: struct {
 	global_reads: ^[dynamic]hir.Global_Id,
 	calls:        ^[dynamic]hir.Function_Id,
 	problematic:  ^bool,
+	error_refinements: ^[dynamic]Error_Refinement,
 	// Stack of labeled value-loops being built (innermost last); see Yield_Target.
 	yield_targets: ^[dynamic]Yield_Target,
 	// `defer` lowering. Deferred statements are built once at the `defer` site and
@@ -7738,6 +7744,63 @@ fallible_aggregate :: proc(
 	})
 }
 
+refined_error_projection :: proc(
+	ctx: ^Build_Ctx,
+	expr_id: hir.Expr_Id,
+	target: types.Type,
+	span: source.Span,
+) -> (hir.Expr_Id, bool) {
+	checker := ctx.checker
+	if expr_id == hir.INVALID_EXPR || int(expr_id) >= len(checker.module.exprs) {
+		return hir.INVALID_EXPR, false
+	}
+	expr := checker.module.exprs[expr_id]
+	if expr.kind != .Local {
+		return hir.INVALID_EXPR, false
+	}
+	local := hir.as_local(expr.target)
+	if local == hir.INVALID_LOCAL || int(local) >= len(ctx.hir_locals^) || ctx.hir_locals^[local].mutable {
+		return hir.INVALID_EXPR, false
+	}
+	candidates: []u32
+	for index := len(ctx.error_refinements^) - 1; index >= 0; index -= 1 {
+		refinement := ctx.error_refinements^[index]
+		if refinement.local == local {
+			candidates = refinement.variants
+			break
+		}
+	}
+	if len(candidates) == 0 {
+		return hir.INVALID_EXPR, false
+	}
+	selected: [dynamic]u32
+	selected.allocator = checker.allocator
+	defer delete(selected)
+	for candidate in candidates {
+		allowed := true
+		for refinement in ctx.error_refinements^ {
+			if refinement.local != local {
+				continue
+			}
+			found := false
+			for variant in refinement.variants {
+				found = found || variant == candidate
+			}
+			allowed = allowed && found
+		}
+		if allowed {
+			append(&selected, candidate)
+		}
+	}
+	if !types.selected_sum_fits(expr.type, target, selected[:], &checker.module.types) {
+		return hir.INVALID_EXPR, false
+	}
+	return add_hir_expr(checker, hir.Expr{
+		kind=.Sum_Project, span=span, type=target, left=expr_id,
+		target=hir.INVALID_REF, right=hir.INVALID_EXPR, diagnostic=source.INVALID_DIAGNOSTIC,
+	}), true
+}
+
 build_compound_expr :: proc(
 	checker: ^Checker,
 	expr: ast.Expr,
@@ -10837,11 +10900,24 @@ build_block :: proc(
 						types.INVALID, ctx.pkg, ctx.file,
 					)
 					probe_type := checker.module.exprs[probe].type
-					if can_implicitly_convert_type(checker, probe_type, error_type) &&
-					   !can_implicitly_convert_type(checker, probe_type, success) {
+					returns_success := can_implicitly_convert_type(checker, probe_type, success)
+					returns_error := can_implicitly_convert_type(checker, probe_type, error_type)
+					if returns_error && !returns_success {
 						error_exit = true
 						value = probe
-					} else if can_implicitly_convert_type(checker, probe_type, success) {
+					} else if !returns_success {
+						if projected, refined := refined_error_projection(ctx, probe, error_type, statement.span); refined {
+							error_exit = true
+							value = projected
+						} else if types.is_enum(probe_type, store) || types.is_tagged_union(probe_type, store) {
+							id := source.addf(
+								checker.diagnostics, statement.span,
+								"cannot return %s as success type %s or error type %s",
+								type_label(checker, probe_type), type_label(checker, success), type_label(checker, error_type),
+							)
+							value = invalid_hir_expr(checker, statement.span, id, success)
+						}
+					} else {
 						value = probe
 					}
 				}
@@ -12155,6 +12231,14 @@ emit_match :: proc(
 		kind = .Declaration, span = span, local = subj_local, expr = spill_value,
 		diagnostic = source.INVALID_DIAGNOSTIC,
 	})
+	refinement_local := hir.INVALID_LOCAL
+	if checker.module.exprs[subject].kind == .Local {
+		candidate := hir.as_local(checker.module.exprs[subject].target)
+		if candidate != hir.INVALID_LOCAL && int(candidate) < len(ctx.hir_locals^) &&
+		   !ctx.hir_locals^[candidate].mutable {
+			refinement_local = candidate
+		}
+	}
 
 	// 2. Dispatch key: a tagged union reads its discriminant into its own temp; an enum
 	//    or scalar compares the subject directly.
@@ -12261,7 +12345,7 @@ emit_match :: proc(
 					}
 					arm_body, body_ok := build_match_arm_body(
 						ctx, body_arm, subject_type, subj_local, subj_is_pointer, ptr_type, subj_writable,
-						field_index, field.type, as_value, slot, slot_type, span,
+						field_index, field.type, refinement_local, []u32{u32(name)}, as_value, slot, slot_type, span,
 					)
 					pop_static_bindings(checker, static_start)
 					ok = body_ok && ok
@@ -12289,7 +12373,7 @@ emit_match :: proc(
 					body_arm.captures = nil
 					arm_body, body_ok := build_match_arm_body(
 						ctx, body_arm, subject_type, subj_local, subj_is_pointer, ptr_type, subj_writable,
-						-1, types.INVALID, as_value, slot, slot_type, span,
+						-1, types.INVALID, refinement_local, []u32{u32(name)}, as_value, slot, slot_type, span,
 					)
 					pop_static_bindings(checker, static_start)
 					ok = body_ok && ok
@@ -12308,6 +12392,8 @@ emit_match :: proc(
 		field_index := -1
 		payload_type := types.INVALID
 		has_capture := len(arm.captures) > 0
+		refinement_variants: [dynamic]u32
+		refinement_variants.allocator = checker.allocator
 
 		if is_else {
 			if has_capture {
@@ -12315,6 +12401,12 @@ emit_match :: proc(
 				ok = false
 			}
 			has_else = true
+			member_enum := tag_enum if is_tagged else subject_type
+			for member in types.enum_members_for(store, member_enum) {
+				if !contains_name(covered[:], symbol.Id(member.name)) {
+					append(&refinement_variants, member.name)
+				}
+			}
 		} else if is_tagged || is_enum_subject {
 			// The capture payload (if any) must be one type across every listed variant.
 			capture_field := -1
@@ -12338,6 +12430,7 @@ emit_match :: proc(
 					ok = false
 				} else {
 					append(&covered, pattern.name)
+					append(&refinement_variants, u32(pattern.name))
 				}
 				if is_tagged {
 					index, field, found := find_struct_field(checker, subject_type, pattern.name)
@@ -12432,7 +12525,11 @@ emit_match :: proc(
 			}
 		}
 
-		arm_body, body_ok := build_match_arm_body(ctx, arm, subject_type, subj_local, subj_is_pointer, ptr_type, subj_writable, field_index, payload_type, as_value, slot, slot_type, span)
+		arm_body, body_ok := build_match_arm_body(
+			ctx, arm, subject_type, subj_local, subj_is_pointer, ptr_type, subj_writable,
+			field_index, payload_type, refinement_local, refinement_variants[:], as_value, slot, slot_type, span,
+		)
+		delete(refinement_variants)
 		if !body_ok {
 			ok = false
 		}
@@ -12541,6 +12638,8 @@ build_match_arm_body :: proc(
 	subj_writable: bool,
 	field_index: int,
 	payload_type: types.Type,
+	refinement_local: hir.Local_Id,
+	refinement_variants: []u32,
 	as_value: bool,
 	slot: ^hir.Local_Id,
 	slot_type: ^types.Type,
@@ -12550,6 +12649,10 @@ build_match_arm_body :: proc(
 	result: [dynamic]hir.Stmt_Id
 	result.allocator = checker.allocator
 	capture_start := len(ctx.locals^)
+	refinement_start := len(ctx.error_refinements^)
+	if refinement_local != hir.INVALID_LOCAL && len(refinement_variants) > 0 {
+		append(ctx.error_refinements, Error_Refinement{local=refinement_local, variants=refinement_variants})
+	}
 	capture_ok := true
 
 	if len(arm.captures) > 0 && field_index >= 0 {
@@ -12603,6 +12706,7 @@ build_match_arm_body :: proc(
 		body_ok = build_value_arm(ctx, &result, arm.body, slot, slot_type, span) && body_ok
 	}
 	resize(ctx.locals, capture_start)
+	resize(ctx.error_refinements, refinement_start)
 	return result[:], body_ok
 }
 
@@ -13339,6 +13443,8 @@ build_function :: proc(checker: ^Checker, id: Spec_Id) {
 	loop_is_loop.allocator = checker.allocator
 	yield_targets: [dynamic]Yield_Target
 	yield_targets.allocator = checker.allocator
+	error_refinements: [dynamic]Error_Refinement
+	error_refinements.allocator = checker.allocator
 	ctx := Build_Ctx{
 		checker = checker,
 		pkg = function.pkg,
@@ -13353,6 +13459,7 @@ build_function :: proc(checker: ^Checker, id: Spec_Id) {
 		global_reads = &global_reads,
 		calls = &calls,
 		problematic = &problematic,
+		error_refinements = &error_refinements,
 		defers = &defers,
 		loop_defer_starts = &loop_defer_starts,
 		loop_labels = &loop_labels,
@@ -13443,6 +13550,7 @@ build_function :: proc(checker: ^Checker, id: Spec_Id) {
 	delete(loop_labels)
 	delete(loop_is_loop)
 	delete(yield_targets)
+	delete(error_refinements)
 	delete(locals)
 	delete(local_spans)
 	delete(local_used)
diff --git a/compiler/checker/comptime.odin b/compiler/checker/comptime.odin
index fdeaa29..198695e 100644
--- a/compiler/checker/comptime.odin
+++ b/compiler/checker/comptime.odin
@@ -286,6 +286,11 @@ Ct_Binding :: struct {
 	mutable: bool,
 }
 
+Ct_Error_Refinement :: struct {
+	cell:     Ct_Cell_Id,
+	variants: []u32,
+}
+
 Ct_Flow_Kind :: enum u8 {
 	Normal,
 	Return,
@@ -311,8 +316,10 @@ Ct_State :: struct {
 	places:     [dynamic]Ct_Place,
 	paths:      [dynamic]Ct_Path_Elem,
 	bindings:   [dynamic]Ct_Binding,
+	error_refinements: [dynamic]Ct_Error_Refinement,
 	defers:     [dynamic]Ct_Defer,
 	defer_depth: int,
+	value_return_depth: int,
 	steps:      int,
 	error:      Ct_Error_Kind,
 	diagnostic: source.Diagnostic_Id,
@@ -350,6 +357,7 @@ ct_state_make :: proc(
 	state.places.allocator = checker.allocator
 	state.paths.allocator = checker.allocator
 	state.bindings.allocator = checker.allocator
+	state.error_refinements.allocator = checker.allocator
 	state.defers.allocator = checker.allocator
 	for value in values {
 		if value.kind == .Integer {
@@ -387,6 +395,7 @@ ct_state_destroy :: proc(state: ^Ct_State) {
 	delete(state.places)
 	delete(state.paths)
 	delete(state.bindings)
+	delete(state.error_refinements)
 	delete(state.defers)
 }
 
@@ -3776,7 +3785,9 @@ ct_eval_catch_expr :: proc(state: ^Ct_State, expr: ast.Expr, expected: types.Typ
 		ct_pop_bindings(state, scope_start)
 		return result, result_flow, result_ok
 	}
+	state.value_return_depth += 1
 	handler, handler_ok := ct_exec_statements(state, expr.body, true, depth+1)
+	state.value_return_depth -= 1
 	ct_pop_bindings(state, scope_start)
 	if !handler_ok {
 		return INVALID_CT_VALUE, handler, false
@@ -3791,6 +3802,9 @@ ct_eval_catch_expr :: proc(state: ^Ct_State, expr: ast.Expr, expected: types.Typ
 		value := ct_add_value(state, Ct_Value{kind=.Void, type=types.VOID})
 		return value, ct_flow(.Normal), true
 	}
+	if handler.kind == .Return {
+		return INVALID_CT_VALUE, handler, true
+	}
 	return INVALID_CT_VALUE, handler, ct_fail(state, .Not_Comptime, expr.span, "catch block must yield a value")
 }
 
@@ -3802,6 +3816,99 @@ ct_make_fallible :: proc(state: ^Ct_State, result_type: types.Type, payload: Ct_
 	})
 }
 
+ct_refined_error_return :: proc(state: ^Ct_State, expr_id: ast.Expr_Id, target: types.Type) -> bool {
+	checker := state.checker
+	if expr_id == ast.INVALID_EXPR || int(expr_id) >= len(checker.ast_module.exprs) {
+		return false
+	}
+	expr := checker.ast_module.exprs[expr_id]
+	if expr.kind != .Name || symbol.is_valid(expr.qualifier) {
+		return false
+	}
+	index, found := ct_find_binding_index(state, expr.name)
+	if !found || state.bindings[index].mutable {
+		return false
+	}
+	binding := state.bindings[index]
+	candidates: []u32
+	for refinement_index := len(state.error_refinements) - 1; refinement_index >= 0; refinement_index -= 1 {
+		refinement := state.error_refinements[refinement_index]
+		if refinement.cell == binding.cell {
+			candidates = refinement.variants
+			break
+		}
+	}
+	if len(candidates) == 0 {
+		return false
+	}
+	selected: [dynamic]u32
+	selected.allocator = checker.allocator
+	defer delete(selected)
+	for candidate in candidates {
+		allowed := true
+		for refinement in state.error_refinements {
+			if refinement.cell != binding.cell {
+				continue
+			}
+			found_variant := false
+			for variant in refinement.variants {
+				found_variant = found_variant || variant == candidate
+			}
+			allowed = allowed && found_variant
+		}
+		if allowed {
+			append(&selected, candidate)
+		}
+	}
+	return types.selected_sum_fits(binding.type, target, selected[:], &checker.module.types)
+}
+
+ct_project_sum_value :: proc(state: ^Ct_State, value_id: Ct_Value_Id, target: types.Type, span: source.Span) -> (Ct_Value_Id, bool) {
+	checker := state.checker
+	if value_id == INVALID_CT_VALUE || int(value_id) >= len(state.values) {
+		return INVALID_CT_VALUE, false
+	}
+	value := state.values[value_id]
+	name := symbol.INVALID
+	if types.is_enum(value.type, &checker.module.types) && value.kind == .Integer {
+		for member in types.enum_members_for(&checker.module.types, value.type) {
+			if member.value == value.integer {
+				name = symbol.Id(member.name)
+				break
+			}
+		}
+	} else if types.is_tagged_union(value.type, &checker.module.types) && value.kind == .Struct {
+		fields := types.fields_for(&checker.module.types, value.type)
+		if value.active >= 0 && int(value.active) < len(fields) {
+			name = symbol.Id(fields[value.active].name)
+		}
+	}
+	if !symbol.is_valid(name) {
+		return INVALID_CT_VALUE, ct_fail(state, .Not_Comptime, span, "invalid refined error value")
+	}
+	if types.is_enum(target, &checker.module.types) {
+		member, found := find_enum_member(checker, target, name)
+		if !found {
+			return INVALID_CT_VALUE, ct_fail(state, .Not_Comptime, span, "refined error is not in the declared error type")
+		}
+		return ct_add_value(state, Ct_Value{kind=.Integer, type=target, integer=member.value}), true
+	}
+	if !types.is_tagged_union(target, &checker.module.types) {
+		return INVALID_CT_VALUE, ct_fail(state, .Not_Comptime, span, "declared error type is not a sum")
+	}
+	field_index, _, found := find_struct_field(checker, target, name)
+	if !found {
+		return INVALID_CT_VALUE, ct_fail(state, .Not_Comptime, span, "refined error is not in the declared error type")
+	}
+	start := len(state.children)
+	if value.kind == .Struct {
+		append(&state.children, ..ct_child_slice(state, value))
+	}
+	return ct_add_value(state, Ct_Value{
+		kind=.Struct, type=target, active=i64(field_index), start=u32(start), count=u32(len(state.children)-start),
+	}), true
+}
+
 ct_return_value :: proc(state: ^Ct_State, expr_id: ast.Expr_Id, span: source.Span, depth: int) -> (Ct_Flow, bool) {
 	checker := state.checker
 	if types.is_void(state.result) {
@@ -3822,15 +3929,33 @@ ct_return_value :: proc(state: ^Ct_State, expr_id: ast.Expr_Id, span: source.Spa
 		expr := checker.ast_module.exprs[expr_id]
 		error_path := false
 		expected := success
+		project_error := false
 		if expr.kind == .Enum_Literal && types.sum_has_name(&checker.module.types, error_type, u32(expr.name)) {
 			error_path = true
 			expected = error_type
+		} else if expr.kind == .Name && !symbol.is_valid(expr.qualifier) {
+			if index, found := ct_find_binding_index(state, expr.name); found {
+				actual := state.bindings[index].type
+				if can_implicitly_convert_type(checker, actual, error_type) &&
+				   !can_implicitly_convert_type(checker, actual, success) {
+					error_path = true
+					expected = error_type
+				} else if ct_refined_error_return(state, expr_id, error_type) {
+					error_path = true
+					project_error = true
+					expected = types.INVALID
+				}
+			}
 		}
 		value, flow, ok := ct_eval_expr(state, expr_id, expected, depth+1)
 		if !ok || flow.kind != .Normal {
 			return flow, ok
 		}
-		value, ok = ct_coerce_value(state, value, expected, span)
+		if project_error {
+			value, ok = ct_project_sum_value(state, value, error_type, span)
+		} else {
+			value, ok = ct_coerce_value(state, value, expected, span)
+		}
 		if !ok {
 			return ct_flow(.Normal), false
 		}
@@ -3913,7 +4038,7 @@ ct_exec_statements :: proc(
 		case .Expression:
 			_, flow, ok = ct_eval_expr(state, statement.expr, types.INVALID, depth+1)
 		case .Return:
-			if yield_returns {
+			if yield_returns && state.value_return_depth == 0 {
 				ok = ct_fail(state, .Not_Comptime, statement.span, "'return' is not valid in this comptime block")
 			} else if statement.value_control_flow {
 				value_flow, value_ok := ct_exec_statements(state, statement.body, true, depth+1)
@@ -4526,6 +4651,13 @@ ct_select_match_arm :: proc(
 
 ct_exec_match :: proc(state: ^Ct_State, statement: ast.Stmt, yield_returns: bool, depth: int) -> (Ct_Flow, bool) {
 	checker := state.checker
+	refinement_cell := INVALID_CT_CELL
+	subject_expr := checker.ast_module.exprs[statement.expr]
+	if subject_expr.kind == .Name && !symbol.is_valid(subject_expr.qualifier) {
+		if index, found := ct_find_binding_index(state, subject_expr.name); found && !state.bindings[index].mutable {
+			refinement_cell = state.bindings[index].cell
+		}
+	}
 	subject, flow, ok := ct_eval_expr(state, statement.expr, types.INVALID, depth+1)
 	if !ok || flow.kind != .Normal {
 		return flow, ok
@@ -4552,6 +4684,63 @@ ct_exec_match :: proc(state: ^Ct_State, statement: ast.Stmt, yield_returns: bool
 	selection, selected := ct_select_match_arm(state, statement, subject, depth+1)
 	if selected {
 		arm := checker.ast_module.statements[selection.arm]
+		refinement_variants: [dynamic]u32
+		refinement_variants.allocator = checker.allocator
+		defer delete(refinement_variants)
+		subject_type := state.values[subject].type
+		if refinement_cell != INVALID_CT_CELL &&
+		   (types.is_enum(subject_type, &checker.module.types) || types.is_tagged_union(subject_type, &checker.module.types)) {
+			if arm.expand {
+				if types.is_enum(subject_type, &checker.module.types) {
+					for member in types.enum_members_for(&checker.module.types, subject_type) {
+						if member.value == state.values[subject].integer {
+							append(&refinement_variants, member.name)
+							break
+						}
+					}
+				} else {
+					fields := types.fields_for(&checker.module.types, subject_type)
+					active := state.values[subject].active
+					if active >= 0 && int(active) < len(fields) {
+						append(&refinement_variants, fields[active].name)
+					}
+				}
+			} else if len(arm.patterns) > 0 {
+				for pattern_id in arm.patterns {
+					pattern := checker.ast_module.exprs[pattern_id]
+					if pattern.kind == .Enum_Literal {
+						append(&refinement_variants, u32(pattern.name))
+					}
+				}
+			} else {
+				covered: [dynamic]symbol.Id
+				covered.allocator = checker.allocator
+				defer delete(covered)
+				for candidate_id in statement.body {
+					if candidate_id == selection.arm {
+						break
+					}
+					candidate := checker.ast_module.statements[candidate_id]
+					for pattern_id in candidate.patterns {
+						pattern := checker.ast_module.exprs[pattern_id]
+						if pattern.kind == .Enum_Literal {
+							append(&covered, pattern.name)
+						}
+					}
+				}
+				member_enum := types.union_tag_enum(subject_type, &checker.module.types) if types.is_tagged_union(subject_type, &checker.module.types) else subject_type
+				for member in types.enum_members_for(&checker.module.types, member_enum) {
+					if !contains_name(covered[:], symbol.Id(member.name)) {
+						append(&refinement_variants, member.name)
+					}
+				}
+			}
+		}
+		refinement_start := len(state.error_refinements)
+		if refinement_cell != INVALID_CT_CELL && len(refinement_variants) > 0 {
+			append(&state.error_refinements, Ct_Error_Refinement{cell=refinement_cell, variants=refinement_variants[:]})
+		}
+		defer resize(&state.error_refinements, refinement_start)
 		scope_start := len(state.bindings)
 		if arm.expand && types.is_enum(state.values[subject].type, &checker.module.types) {
 			if len(arm.captures) > 0 && arm.captures[0] != checker.sink_symbol {
diff --git a/compiler/hir/hir.odin b/compiler/hir/hir.odin
index f73fe07..4f2d409 100644
--- a/compiler/hir/hir.odin
+++ b/compiler/hir/hir.odin
@@ -102,6 +102,7 @@ Expr_Kind :: enum u8 {
 	Catch,
 	Widen,
 	Sum_Widen,
+	Sum_Project,
 	C_Coerce,
 	C_Vararg_Promote,
 	Retype,
diff --git a/compiler/ir/ir.odin b/compiler/ir/ir.odin
index 2e97b42..53fb378 100644
--- a/compiler/ir/ir.odin
+++ b/compiler/ir/ir.odin
@@ -97,6 +97,7 @@ Opcode :: enum u8 {
 	Orelse,
 	Widen,
 	Sum_Widen,
+	Sum_Project,
 	C_Coerce,
 	C_Vararg_Promote,
 	Retype,
diff --git a/compiler/llvm/llvm.odin b/compiler/llvm/llvm.odin
index c39f3d7..4cb4451 100644
--- a/compiler/llvm/llvm.odin
+++ b/compiler/llvm/llvm.odin
@@ -287,7 +287,7 @@ valid_value :: proc(
 	     .Load_Global, .Function_Address, .Address_Of, .Load, .Union_Tag, .Slice, .Length, .Slice_Ptr,
 	     .Fallible_Error, .Extract, .Select, .Unwrap,
 	     .Optional_Is_Some, .Optional_Value, .Orelse,
-	     .Widen, .Sum_Widen, .C_Coerce, .C_Vararg_Promote, .Retype, .Scalar_Cast, .Pointer_Cast, .Const_Cast, .Weaken_Pointer, .Weaken_Slice, .Decay_Array_Pointer,
+	     .Widen, .Sum_Widen, .Sum_Project, .C_Coerce, .C_Vararg_Promote, .Retype, .Scalar_Cast, .Pointer_Cast, .Const_Cast, .Weaken_Pointer, .Weaken_Slice, .Decay_Array_Pointer,
 	     .Neg_Checked, .Add_Checked, .Sub_Checked, .Mul_Checked, .Div_Checked,
 	     .Div_Trunc_Checked, .Div_Floor_Checked, .Div_Exact_Checked, .Div_Ceil_Checked,
 	     .Rem_Checked, .Mod_Checked,
@@ -1748,10 +1748,14 @@ emit_instruction_stream :: proc(
 			fmt.sbprintf(&emitter.builder, "  %%v%d = %s %s ", instruction_index, operation, llvm_type(from_type, &emitter.module.types))
 			write_operand(&emitter.builder, instructions, instruction.a, from_type, &emitter.module.types)
 			fmt.sbprintf(&emitter.builder, " to %s\n", llvm_type(instruction.type, &emitter.module.types))
-		case .Sum_Widen:
-			if !valid_instruction(instructions, instruction.a) ||
-			   !types.can_sum_widen(instructions[instruction.a].type, instruction.type, &emitter.module.types) {
-				emit_recovery_value(emitter, instruction_index, instruction, "invalid sum widening operand")
+		case .Sum_Widen, .Sum_Project:
+			project := instruction.op == .Sum_Project
+			valid_conversion := valid_instruction(instructions, instruction.a) &&
+				(types.can_sum_project(instructions[instruction.a].type, instruction.type, &emitter.module.types) if project else
+				 types.can_sum_widen(instructions[instruction.a].type, instruction.type, &emitter.module.types))
+			if !valid_conversion {
+				emit_recovery_value(emitter, instruction_index, instruction,
+					"invalid sum projection operand" if project else "invalid sum widening operand")
 				continue
 			}
 			from_type := instructions[instruction.a].type
@@ -1799,6 +1803,9 @@ emit_instruction_stream :: proc(
 				from_payload_offset := types.union_payload_offset(from_type, &emitter.module.types, emitter.module.target)
 				to_payload_offset := types.union_payload_offset(instruction.type, &emitter.module.types, emitter.module.target)
 				payload_size := types.sum_payload_size(from_type, &emitter.module.types, emitter.module.target)
+				if project {
+					payload_size = min(payload_size, types.sum_payload_size(instruction.type, &emitter.module.types, emitter.module.target))
+				}
 				if payload_size > 0 {
 					fmt.sbprintf(&emitter.builder, "  %%sum_from_payload%d = getelementptr i8, ptr %%sum_from_slot%d, i64 %d\n", instruction_index, instruction_index, from_payload_offset)
 					fmt.sbprintf(&emitter.builder, "  %%sum_to_payload%d = getelementptr i8, ptr %%sum_to_slot%d, i64 %d\n", instruction_index, instruction_index, to_payload_offset)
@@ -1807,7 +1814,8 @@ emit_instruction_stream :: proc(
 				fmt.sbprintf(&emitter.builder, "  %%v%d = load %s, ptr %%sum_to_slot%d\n", instruction_index, to_name, instruction_index)
 				continue
 			}
-			emit_recovery_value(emitter, instruction_index, instruction, "unsupported sum widening operand")
+			emit_recovery_value(emitter, instruction_index, instruction,
+				"unsupported sum projection operand" if project else "unsupported sum widening operand")
 		case .C_Coerce:
 			if !valid_instruction(instructions, instruction.a) ||
 			   !(types.can_coerce_c_integer(instructions[instruction.a].type, instruction.type, emitter.module.target) ||
diff --git a/compiler/lower/lower.odin b/compiler/lower/lower.odin
index 51bb839..1c33139 100644
--- a/compiler/lower/lower.odin
+++ b/compiler/lower/lower.odin
@@ -497,6 +497,15 @@ lower_compound_expr :: proc(state: ^State, expr_id: hir.Expr_Id) -> ir.Instructi
 						target=ir.INVALID_REF, a=ir.INVALID_INSTRUCTION, b=ir.INVALID_INSTRUCTION,
 						diagnostic=source.INVALID_DIAGNOSTIC,
 					})
+				} else if expr.right == hir.INVALID_EXPR {
+					// A terminating handler can still end in a synthetic match/if merge label
+					// after its returns. Seal that unreachable continuation before the success
+					// label so LLVM never sees adjacent basic-block labels.
+					append_instruction(state, ir.Instruction{
+						op=.Trap, span=expr.span, type=types.NORETURN, integer=1,
+						target=ir.INVALID_REF, a=ir.INVALID_INSTRUCTION, b=ir.INVALID_INSTRUCTION,
+						diagnostic=source.INVALID_DIAGNOSTIC,
+					})
 				}
 			}
 			if expr.right != hir.INVALID_EXPR {
@@ -768,7 +777,7 @@ lower_expr :: proc(state: ^State, expr_id: hir.Expr_Id) -> ir.Instruction_Id {
 					})
 				}
 				_ = pop(&stack)
-			case .Widen, .Sum_Widen, .C_Coerce, .C_Vararg_Promote, .Retype, .Scalar_Cast, .Pointer_Cast, .Const_Cast, .Weaken_Pointer, .Weaken_Slice, .Decay_Array_Pointer:
+			case .Widen, .Sum_Widen, .Sum_Project, .C_Coerce, .C_Vararg_Promote, .Retype, .Scalar_Cast, .Pointer_Cast, .Const_Cast, .Weaken_Pointer, .Weaken_Slice, .Decay_Array_Pointer:
 				stack[frame_index].stage = 1
 				append(&stack, Lower_Expr_Frame{expr=expr.left})
 			case .Negate, .Bit_Not:
@@ -829,6 +838,7 @@ lower_expr :: proc(state: ^State, expr_id: hir.Expr_Id) -> ir.Instruction_Id {
 			op := ir.Opcode.Widen
 			#partial switch expr.kind {
 			case .Sum_Widen:           op = .Sum_Widen
+			case .Sum_Project:         op = .Sum_Project
 			case .Weaken_Pointer:      op = .Weaken_Pointer
 			case .Weaken_Slice:        op = .Weaken_Slice
 			case .Decay_Array_Pointer: op = .Decay_Array_Pointer
diff --git a/compiler/types/types.odin b/compiler/types/types.odin
index a1b5d71..63b828c 100644
--- a/compiler/types/types.odin
+++ b/compiler/types/types.odin
@@ -552,6 +552,73 @@ can_sum_widen :: proc(from, to: Type, store: ^Store) -> bool {
 	return true
 }
 
+// Reports whether every selected variant from `from` is represented identically in
+// `to`. The checker uses this only after control flow has proven that the source value
+// is one of `selected`; it is not a general implicit narrowing rule.
+selected_sum_fits :: proc(from, to: Type, selected: []u32, store: ^Store) -> bool {
+	if len(selected) == 0 {
+		return false
+	}
+	from_variants: [dynamic]Sum_Variant
+	from_variants.allocator = store.allocator
+	defer delete(from_variants)
+	to_variants: [dynamic]Sum_Variant
+	to_variants.allocator = store.allocator
+	defer delete(to_variants)
+	if !append_sum_variants(store, from, &from_variants) ||
+	   !append_sum_variants(store, to, &to_variants) {
+		return false
+	}
+	for name in selected {
+		source_variant: Sum_Variant
+		source_found := false
+		for variant in from_variants {
+			if variant.name == name {
+				source_variant = variant
+				source_found = true
+				break
+			}
+		}
+		if !source_found {
+			return false
+		}
+		matched := false
+		for variant in to_variants {
+			if variant.id == source_variant.id && variant.payload == source_variant.payload {
+				matched = true
+				break
+			}
+		}
+		if !matched {
+			return false
+		}
+	}
+	return true
+}
+
+// Sum_Project is emitted only with a checker proof. This weaker structural predicate is
+// retained by the backend as a defensive check that the two sums share a valid variant.
+can_sum_project :: proc(from, to: Type, store: ^Store) -> bool {
+	from_variants: [dynamic]Sum_Variant
+	from_variants.allocator = store.allocator
+	defer delete(from_variants)
+	to_variants: [dynamic]Sum_Variant
+	to_variants.allocator = store.allocator
+	defer delete(to_variants)
+	if !append_sum_variants(store, from, &from_variants) ||
+	   !append_sum_variants(store, to, &to_variants) {
+		return false
+	}
+	for source_variant in from_variants {
+		for target_variant in to_variants {
+			if target_variant.id == source_variant.id && target_variant.payload == source_variant.payload {
+				return true
+			}
+		}
+	}
+	return false
+}
+
 define_struct :: proc(store: ^Store, id: Type, fields: []Field, c_layout, opaque: bool) -> bool {
 	return define_record(store, id, fields, c_layout, opaque)
 }
diff --git a/compiler_tests.odin b/compiler_tests.odin
index a2a012e..854d616 100644
--- a/compiler_tests.odin
+++ b/compiler_tests.odin
@@ -6349,6 +6349,192 @@ main func() i32 {
 	testing.expect_value(t, state.exit_code, 0)
 }
 
+@(test)
+matched_error_residuals_return_at_runtime_and_comptime :: proc(t: ^testing.T) {
+	text := `KeyError :: enum { key_exists }
+AllocError :: enum { out_of_memory }
+AError :: enum { a }
+BError :: enum { b }
+CError :: enum { c }
+DetailError :: union(enum) { out_of_memory i32 }
+
+key_or_alloc func(code i32) void ! (KeyError | AllocError) {
+	if code == 1 { return .key_exists }
+	if code == 2 { return .out_of_memory }
+}
+abc func(code i32) void ! (AError | BError | CError) {
+	if code == 1 { return .a }
+	if code == 2 { return .b }
+	if code == 3 { return .c }
+}
+detail func() void ! (KeyError | DetailError) { return .out_of_memory{41} }
+
+via_else func() i32 ! AllocError {
+	key_or_alloc(2) catch |err| {
+		match err {
+			.key_exists: unreachable
+			else: return err
+		}
+	}
+	return 0
+}
+via_group func() i32 ! (AError | BError) {
+	abc(2) catch |err| {
+		match err {
+			.a, .b: return err
+			.c: unreachable
+		}
+	}
+	return 0
+}
+via_nested func() i32 ! AError {
+	abc(1) catch |err| {
+		match err {
+			.a, .b: match err {
+				.a: return err
+				else: unreachable
+			}
+			.c: unreachable
+		}
+	}
+	return 0
+}
+via_expand func() i32 ! AError {
+	abc(1) catch |err| {
+		match err {
+			expand |tag|: match tag {
+				.a: return err
+				else: unreachable
+			}
+		}
+	}
+	return 0
+}
+via_payload func() i32 ! DetailError {
+	detail() catch |err| {
+		match err {
+			.key_exists: unreachable
+			else: return err
+		}
+	}
+	return 0
+}
+ct_project func() i32 ! AError {
+	abc(1) catch |err| {
+		match err {
+			.a: return err
+			else: unreachable
+		}
+	}
+	return 0
+}
+ct_recover func() i32 {
+	return ct_project() catch |_| 5
+}
+main func() i32 {
+	a :: via_else() catch |_| 1
+	b :: via_group() catch |err| match err {
+		.a: 1
+		.b: 2
+	}
+	c :: via_nested() catch |_| 3
+	d :: via_expand() catch |_| 4
+	e :: via_payload() catch |err| match err { .out_of_memory |code|: code }
+	f i32 :: $ct_recover()
+	return a + b + c + d + e + f - 56
+}
+`
+	directory := "/tmp/brolang-test-matched-error-residuals"
+	main_path := "/tmp/brolang-test-matched-error-residuals/main.bro"
+	output := "/tmp/brolang-test-matched-error-residuals-output"
+	_ = os2.remove_all(directory)
+	defer _ = os2.remove_all(directory)
+	defer _ = os.remove(output)
+	testing.expect(t, os.make_directory(directory) == nil)
+	testing.expect(t, os.write_entire_file(main_path, transmute([]byte)text))
+	testing.expect_value(t, compiler_core.compile_package(directory, output), 0)
+	state := run_executable(output)
+	testing.expect_value(t, state.exit_code, 0)
+}
+
+@(test)
+unproven_error_returns_are_rejected_against_both_channels :: proc(t: ^testing.T) {
+	text := `BadError :: enum { bad }
+GoodError :: enum { good }
+Combined :: alias (BadError | GoodError)
+source func() void ! Combined { return .good }
+unrefined func() usize ! GoodError {
+	source() catch |err| { return err }
+	return 0
+}
+incompatible func() usize ! GoodError {
+	source() catch |err| {
+		match err {
+			.bad: return err
+			else: unreachable
+		}
+	}
+	return 0
+}
+aliased func() usize ! GoodError {
+	source() catch |err| {
+		match err {
+			.bad: unreachable
+			else: {
+				copy :: err
+				return copy
+			}
+		}
+	}
+	return 0
+}
+mutable_subject func() usize ! GoodError {
+	source() catch |err| {
+		value Combined = err
+		match value {
+			.bad: unreachable
+			else: return value
+		}
+	}
+	return 0
+}
+main func() void {
+	_ = unrefined() catch 0
+	_ = incompatible() catch 0
+	_ = aliased() catch 0
+	_ = mutable_subject() catch 0
+}
+`
+	directory := "/tmp/brolang-test-unproven-error-returns"
+	main_path := "/tmp/brolang-test-unproven-error-returns/main.bro"
+	_ = os2.remove_all(directory)
+	defer _ = os2.remove_all(directory)
+	testing.expect(t, os.make_directory(directory) == nil)
+	testing.expect(t, os.write_entire_file(main_path, transmute([]byte)text))
+	sources := source.init_store()
+	defer source.destroy_store(&sources)
+	diagnostics := source.init_store_diagnostics(&sources)
+	defer source.destroy_diagnostics(&diagnostics)
+	symbols := symbol.init_table()
+	defer symbol.destroy_table(&symbols)
+	ast_module, loaded := loader.load(directory, &sources, &diagnostics, &symbols)
+	defer ast.destroy_module(&ast_module)
+	hir_module := checker.check(&ast_module, &diagnostics, &symbols)
+	defer hir.destroy_module(&hir_module)
+
+	testing.expect(t, loaded)
+	return_errors := 0
+	for _, diagnostic_index in diagnostics.items {
+		message := source.format(&diagnostics, source.diagnostic_id(diagnostic_index))
+		if strings.contains(message, "cannot return") &&
+		   strings.contains(message, "as success type usize or error type GoodError") {
+			return_errors += 1
+		}
+		delete(message)
+	}
+	testing.expect_value(t, return_errors, 4)
+}
+
 @(test)
 conversion_diagnostics_render_source_types :: proc(t: ^testing.T) {
 	text := `Allocator :: struct {