> “Narrowing” a compile-time invariant without a corresponding proof is formally unsound and does not “respect” the declared invariant in any reasonable sense

> “Narrowing” a compile-time invariant without a corresponding proof is formally unsound and does not “respect” the declared invariant in any reasonable sense The invariant is that either condition X applies or condition Y applies. "Panic and stop execution if X, continue execution with the invariant Y if Y" is not unsound and does respect the original invariant in every possible sense. It may be the wrong choice of behavior given the frequency of X occurring and the costs incurred by the decision to panic, but that’s not a type-level problem.