What is the feature you would like to see in a future version of Dafny?

Pulling out the discussion in the comments section of #3076 into its own issue:

I was recently bitten by a super-silly precondition of mine, essentially of the form requires x < x for some x: int, and only much later did I realise I had, somewhere, tied myself in a knot[1]. By this point, the contradiction was in a totally different module that I had paged out of my mind, so it took awhile to find. It would be nice if Dafny could expose up impossible preconditions so the user knows that they're not inadvertently introducing an exfalso style hole in their proofs. It'd be fine if this was only a warning, indicating the presence of such a precondition or that a proof transitively involves such a precondition (via a required predicate or lemma, for instance.)

@MikaelMayer replied thus:

This is a very interesting idea that indeed deserves to be studied on its own. It has its own challenges: Trying to prove "false" when it's not possible can be extremely expensive for a verifier. How to ensure we can do both? Maybe caching down the road?

This seems like a problem, indeed - most of the type proving false would not be possible, presumably, so in the typical case we'd be giving the solver an unnecessary workout.

To this end, Mikael proposed a subset of the feature, where straightforward contradictory syntactic patterns could be caught cheaply:

x < x    where x is a variable
x > x
x != x
x == x.field  where x is a datatype.
exists x :: E where can be easily inferred to be always false
!E where E can be easily inferred to be always true
E && B   if E or B are always false.
E || B   if E and B are always false.

I suspect something like this would have caught my particular issue (technically my "reflexive inequality" involved an array access, akin to a[i] < a[i], but presumably it's no more complex to pull in an array axiom or two?)

I might suggest two points of discussion:

1. Another potential pitfall that would be nice to have a story around would be for "obvious contradictions" between preconditions: for instance, if I require a[i] == b[i], I better not also require a != b, or some such thing. In terms of implementation this could well be orthogonal to a localised syntax-driven check. By the same token, I could also imagine at some level all preconditions get ANDed together into some (in this case contradictory) formula. This could still abut complexity issues, of course.

2. There could be a concern that users might expect the precondition contradiction checker to be smarter than it is, and rely on it for more complicated cases than it knows about. For instance, suppose that array indexing equality was not part of the hardcoded syntactic checks (as it isn't listed in the above set of expressions): I might conclude that the issue in my project was elsewhere from the requires a[i] < a[i] case, since I might assume that Dafny catches precondition contradictions in general. I don't know how often users trip over things like this.

Thanks!
Nathan

[1]: power dafny user lesson 1: if your code is consistently passing the verifier and you're starting to think, "boy, am I ever good at writing correct programs", be wary ;-)