Ensure that pattern matching is indeed exhaustive

[RalfJung]

See this Zulip thread for a bunch of discussion. The short summary is that currently one can write non-UB code which enters a x & Some(_) arm where in that match arm x.is_some() returns false. We might want to ensure "match consistency" and make this UB, but that is not a trivial task, and it will almost certainly involve the aliasing model (so we'll need to have the basics of that in MiniRust before we can explore the pattern match question).