Projection of an uninhabited (`!`) field is reported as an unsupported construct instead of unreachable code

[feliperodri]

Summary

Projecting a field whose type is uninhabited (!) is reported as an unsupported construct
("Projection mismatch") rather than as unreachable code. The projection is dead by construction —
no value of ! exists — so Kani should codegen it as unreachable instead of telling the user that
ordinary coroutine code contains two constructs Kani does not support.

Reproduction

tests/kani/Coroutines/main.rs, unchanged, on the nightly-2026-09-22 toolchain (the bump for
#4774; this path is not reached on main's pinned nightly-2026-08-21). The derived
PartialEq for CoroutineState<u8, !> compares the fields of the uninhabited Complete variant:

WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
... field: "0" ... typ: Unsignedbv { width: 8 }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-Never")

warning: Found the following unsupported constructs:
             - Projection mismatch (2)
             ...
         Verification will fail if one or more of these constructs is reachable.

Check 6: unsupported_construct.1
	 - Status: SUCCESS
	 - Description: "Projection mismatch is not currently supported by Kani. Please post your
	   example at https://github.com/model-checking/kani/issues/277"

Verification succeeds, because the checks sit in code CBMC proves unreachable
(<CoroutineState<u8, !> as PartialEq>::eq.unreachable.1 is SUCCESS in the same run).

What is happening

CoroutineState<u8, !> has one inhabited variant, so its layout is just the u8 payload — there
is no field corresponding to the Complete variant's !. When MIR projects
((*_1) as Complete).0, codegen_field resolves field 0 of that layout (a u8) while the MIR
field type is !, check_expr_typ_mismatch sees Unsignedbv(8) vs StructTag("tag-Never"), and
the projection bails out through UnimplementedData (kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs).

Why it is worth fixing

• The diagnosis is wrong and user-visible: nothing about this program is unsupported. A user
  verifying a coroutine gets a warning telling them verification "will fail if one or more of these
  constructs is reachable", for a construct that cannot be reached.
• It hides real unsupported constructs in the same summary.
• Any code that reaches such a projection in live code would report "unsupported" rather than the
  contradiction it actually is.

Suggested fix

In codegen_field (or in check_expr_typ_mismatch), detect that the MIR field type is uninhabited
and emit unreachable code — e.g. codegen_sanity(false, ...) / a Stmt::assert_false-style stub of
the right type — rather than an UnimplementedData carrying the "Projection mismatch" message.

Notes

Found while bumping the toolchain for #4774. Before that PR the same path ICEd
(assign statement with unequal types lhs Pointer<Never> rhs Never) because
codegen_place_ref_stable typed its unsupported-projection stub as the place rather than a
reference to it; that part is fixed there, which is what leaves this cosmetic-but-misleading
behaviour behind. #277, referenced by the check's message, is closed and was about a different
projection assertion.

[feliperodri]

The ICE described at the bottom of this issue is fixed in #4833 (the nightly-2026-09-22 bump): codegen_place_ref_stable now types its unsupported-projection stub as a reference to the place rather than as the place itself. That is what leaves the behaviour this issue is about — tests/kani/Coroutines/main.rs verifies, but reports two "Projection mismatch" unsupported constructs in code CBMC proves unreachable.