### Question

Why do I need a witness clause in subtype definitions like

type A = s: int | Prime(x) witness 13


There are defaults for the witness clause, so you don’t always have to have one. The default value is some zero-equivalent value: 0 for int based types, 0.0 for real-based types, empty sets, sequence and maps for those base types.
And, it is permitted to have possibly empty types by using a witness clause witness *, but there are restrictions on the use of possibly empty types. For instance, a declaration of a variable with a possibly-empty type will need an initializer, if that variable is ever used, because Dafny requires variables to be ‘definitely assigned’ before being used.