Provide a witness pattern for non-exhaustive patterns

Fixed #4321
Check pattern refutability the same way exhaustiveness is checked
Add support for fixed size vectors in let/arg patterns

Fixes #7784
Add unreachability detection for missized patterns of fixed size vectors

Fixed #13482
Update tests with the new error messages