Fix uncovered set of literal patterns

Issues #16289 (closed) and #15713 (closed) are proof that the pattern match checker did an unsound job of estimating the value set abstraction corresponding to the uncovered set.

The reason is that the fix from #11303 (closed) introducing NLit was incomplete: The LitCon case desugared to Var rather than LitVar, which would have done the necessary case splitting analogous to the ConVar case.

This patch rectifies that by introducing the fresh unification variable in LitCon in value abstraction position rather than pattern postition, recording a constraint equating it to the constructor expression rather than the literal. Fixes #16289 (closed) and #15713 (closed).