Split CONSIDER coverage diagnostics: exhaustiveness → error, redundancy → warning

[mengwong]

Follow-up to making warnings non-fatal for typecheck success. Currently both CONSIDER coverage diagnostics are SWarn (non-fatal). The desired end-state: exhaustiveness (a CONSIDER/pattern match missing cases) should be a blocking SError, while redundancy (a dead/overlapping WHEN branch) stays a non-blocking SWarn.

Emission sites (already distinct constructors)

Both are emitted from the CONSIDER coverage analysis in checkConsider:

• jl4-core/src/L4/TypeCheck.hs:1426 — addWarning $ PatternMatchesMissing missing → exhaustiveness
• jl4-core/src/L4/TypeCheck.hs:1428 — addWarning $ PatternMatchRedundant redundant → redundancy
• Suppressed for primitive scrutinees (isPrimitiveType, TypeCheck.hs:1848 — NUMBER/STRING/DATE; BOOLEAN is analyzed).
• Constructors: data CheckWarning = PatternMatchRedundant [Branch Resolved] | PatternMatchesMissing [BranchLhs Resolved] (jl4-core/src/L4/TypeCheck/Types.hs:122-124); addWarning = addError . CheckWarning (Types.hs:530-531). These are the only addWarning sites in the typechecker.

The lumping is purely at severity classification, which exists in two copies that must change in lockstep:

• jl4-core/src/L4/TypeCheck.hs:3420-3425 — severity :: CheckErrorWithContext -> Severity (CheckWarning {} -> SWarn, catch-all _ -> SError); drives the LSP path.
• jl4-core/src/L4/Diagnostic.hs:99-104 — an inline duplicate inside checkErrorToDiagnostic, drives the core-API path. L4.Diagnostic already imports L4.TypeCheck (prettyCheckError), so there is no module cycle — the duplicate can be deleted in favor of TypeCheck.severity.

Implementation options

Option A (minimal, ~2 lines + tests): special-case in severity:

CheckWarning (PatternMatchesMissing {}) -> SError
CheckWarning {}                         -> SWarn

in TypeCheck.hs:3423-3424 and Diagnostic.hs:103 (or unify the two first). Downside: a constructor named CheckWarning … that classifies as SError is a semantic trap.

Option B (recommended): promote PatternMatchesMissing out of CheckWarning to a top-level CheckError constructor (e.g. NonExhaustiveConsider [BranchLhs Resolved]). It then hits both _ -> SError catch-alls automatically with zero severity-logic changes. Touch points: emission site (TypeCheck.hs:1426, addWarning → addError . NonExhaustiveConsider); move the pretty-case from prettyCheckWarning (TypeCheck.hs:3670) into prettyCheckError; HasSrcRange CheckError needs nothing (warnings already fall through rangeOf _ = Nothing and take their range from the WhileCheckingDecide context). No exhaustive matches on CheckError exist outside prettyCheckError.

Companion fixes (pre-existing core-API inconsistencies; the non-fatal LSP change did NOT touch these)

The non-fatal change only covered the LSP/Shake partition (jl4-lsp/src/LSP/L4/Rules.hs). The core-API pipeline still treats SWarn as fatal in three places and should be aligned:

• jl4-core/src/L4/API.hs:232 — filter (\e -> severity e /= SInfo) in l4Eval; should be == SError.
• jl4-core/src/L4/API.hs:573 — not (null result.tcdErrors) fails on any diagnostic incl. SInfo.
• jl4-core/src/L4/Import/Resolution.hs:322 — tcdSuccess = null result.errors, same problem.

Bucket/golden & risk surface

• jl4/examples/ok/empty.l4 emits both kinds; with exhaustiveness→SError it fails typecheck again and must leave ok/. Recommended split: (a) a redundancy-only fixture that stays in ok/ (exhaustive CONSIDER + a duplicate WHEN), (b) a non-exhaustive fixture in not-ok/tc/. Regenerate 4 goldens each. No other corpus file emits either warning today (grep-verified), so no further movement — but any future ok/ example with a partial CONSIDER will flip.
• Breaking deploy-surface change: all SuccessfulTypeCheck consumers begin refusing non-exhaustive CONSIDERs — CLI l4 check/run/schema/render/openfisca/state-graph/batch/trace, LSP visualization/schema, and jl4-service deploys (Compiler.hs:155-160 blockingErrs filters severity e == SError, so the promotion propagates automatically — previously-deployable models with partial CONSIDERs become rejected). Needs a release note.
• Preview against hosted deployments before shipping. We have some visibility into all hosted deployments, so before promoting exhaustiveness → SError we should preview this potentially-breaking change against them: scan the currently-deployed models for partial CONSIDERs that would begin to be rejected, quantify the blast radius, and coordinate/notify the affected owners before the change lands (don't ship it blind).
• CLI exit codes flip automatically and consistently via hasBlockingError (jl4/app/L4/Cli/Common.hs:216-219, keyed on DiagnosticSeverity_Error derived from the same classification). Editor UX: missing-cases squiggles turn yellow→red (intended).
• Suites to re-baseline: jl4-test (moved fixtures' goldens; dumped-diagnostic "Severity: …_Warning" label lines become _Error for the failing fixture); check jl4-service corpora for partial CONSIDERs; jl4-core-test only if the API.hs companion fixes are bundled.