Note: Exceptions and panics arenât quite the same thing. Exceptions are typed and are generally used to return common errors. Panics are an untyped way to say âsomething went really wrong and I just want to bailâ.
Treat any function that can panic but doesnât return an error or result have itâs type signature implicitly change from -> Foo to -> Result<Foo,!>any Result<Foo,MyErr> types would have their Error types implicitly be converted to enum AnonMyErrWrapper { Die(!),Error}
(Technical Digression 1) Errors and results arenât special in any way; theyâre just conventions. The compiler canât know if a function already returns an âerrorâ because the compiler canât distinguish between an error and a normal return type (they look the same).
(Technical Digression 2) ! is just a type for things that cannot be âinstantiatedâ (no value of that type can exist). The only relation to panic!() is that panic âreturnsâ ! because panic!() never returns. This means that, logically, value(a) is (type(A) OR type(!)) reduces to value(a) is type(A). So, if you tried to statically analyse Result<Foo, !>, your static analysis program would just reduce it to Foo and youâd be back where you started.
The benefit, of course, being that exceptions are effectively lifted into the type system, and it would be possible to reason about them, perform static analysis on them, etc.
One usually canât (or doesnât want to) reason about panics. Thatâs the entire point of having them; theyâre an escape hatch to let the programmer toss in the proverbial towel.
So, it looks like you want a way to statically prove constraints about your program. Instead of a runtime panic!(), you want a compile-time statically_unreachable!() (one could use ! as a value to indicate that some block of code is unreachable). Unfortunately, this is impossible to do in the general case (due to the halting problem) and hard to do even in limited cases. This is generally called certified programming and often requires the programmer to either write their programs in non turing complete languages or manually prove their programs correct. If youâre interested in this subject, take a look at Coq.
