Regression tests for #4485 and #4487 (fixed by #4515)

[nikswamy]

This adds regression tests for two soundness bugs in the VC simplifier. Neither reproduces on current master: both were fixed by #4515.

Since #4515, a computation type carries only a result type, and its specification is a refinement of that type.

• Soundness: the VC simplifier judges an empty function type inhabited, proving False #4485: clearly_inhabited decided that an arrow type was inhabited by looking only at its result type, ignoring the postcondition. unit -> Pure int True (fun _ -> False) is now unit -> r:int{False}. A refined type is not on clearly_inhabited's list of inhabited types, so nonempty e and exists (g:e). True are no longer rewritten to True.
• Soundness: U.term_eq ignores a computation type's pre/postcondition, so the VC simplifier rewrites a false implication to True #4487: U.term_eq compared computation types by effect and result type only, ignoring their effect arguments. Two arrows that differ only in their postcondition now have different (refined) result types. So p ==> q and p <==> q are no longer rewritten to True for such p and q.

Tests

• tests/bug-reports/closed/Bug4485.fst: the nonempty and exists repros, a bool variant, and the issue's three controls (an inhabited arrow type, an empty one given by a refinement of its result type, and a vacuously inhabited one), all as expect_failure. It also includes two definitions that must be accepted: witness_gives_false, and a witness that the vacuous type is inhabited.
• tests/bug-reports/closed/Bug4487.fst:
  • the ==> and <==> repros, both inline and through type abbreviations, as expect_failure;
  • the effect-name control, as expect_failure;
  • the issue's proof of False, with the false implication as a hypothesis;
  • the control comparing an arrow type with an identical one, which must be accepted.

Checked:

• Current master (0f0c557, stage-1 compiler): both tests pass, and every repro from the two issues fails with Error 19.
• A pre-Simplify effects further #4515 build: the Soundness: U.term_eq ignores a computation type's pre/postcondition, so the VC simplifier rewrites a false implication to True #4487 repros and Soundness: the VC simplifier judges an empty function type inhabited, proving False #4485's exists repro verify, i.e. they prove False (the nonempty repro can't be checked there, since that Prims has no nonempty), and both tests fail.

Fixes #4485
Fixes #4487