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 #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.

[jhjourdan]

My plan for this issue is to:

• [ ] Syntactically detect types that might be empty. Apart from !, these types are ADTs such that all the constructors have at least one recursive field. We need to be careful that empty types might be mutually recursive.
• [ ] Translate these types to an ADT with one additional constructor with no field (i.e., we add a value to the type), and emit a warning.
• [ ] Modify the structural type invariant of these types to ensure that no value of this type in executable code should be equal to this additional value.

Hence, in executable code, the values of such a type are exactly those of the type declared by the user, and the user can use the type invariant to leverage this in her reasoning. In the logic, on the contrary, we have added a constructor, so that we are sure that no type in the logic is uninhabited.

We need to be careful, though, with the syntactic criterion, especially when dealing with mutually recursive types or nested recursive types. Examples of types that need to be flagged as potentially empty:

struct A{ // Empty type
    x: B;
}

struct B { // Empty type
    y: Box<A>;
}

struct C { // Non-empy type, because in A has been added a value
   x : A;
}

struct D<T> {  // Non empty type
   x : Box<T>;
}

struct E { // Empty type
    x : D<E>;
}

[jhjourdan]

Of course, @Lysxia, you are welcome to attack this issue. Please simply tell us that you are working on it.