Missing warning for useless pattern in quantifier.
When writing
invariant { forall k. true }
We got: This variable has polymorphic type 'xi2 where type variable 'xi2 is never named explicitly
.
When doing:
invariant { forall k: int. true }
We got: unused variable k
.
But when doing:
invariant { forall _: int. true }
There's nothing displayed. I don't see a case where one would do this on purpose, so adding a warning seems like something we could do.