Soundness and empty types

[jhjourdan]

Why3 assumes that every type is non-empty, and so do all the SMT solvers.

However, for several reasons, it seems like we need to support empty types:

• The "never" type (! in Rust), and friends like Infaillible are use in crucial places in the standard library (see the Try trait).
• Types with invariants may be empty if the invariant is absurd. In Invariant cleanup #880, we are in the process of removing the is_inhabited law, which guaranteed that types with invariants are not empty. The reasons are:
  • It is cumbersome to prove inhabitedness of type invariants, like Why3 does, (because many types do not have easy ways to exhibit inhabitants, both in Pearlite and in Why3 logic language)
  • Sometimes, invariants are purposely not provably uninhabited. This is the case of the Map iterator, which can be uninhabited if the pre and post-conditions of the closure do not match.