Use closed-world assumption for simple refinement types

[bvssvni]

Alternative to #642

Instead of reporting an error explicitly with a special refinement type, one can assume that all refinement types are listed. If the type checker does not detect any ambiguity, yet a type does not match any refinement, an error is reported.