Syntax for refinement types
Proposal:

```
from typing_extensions import Annotated

UserId = Annotated[int, lambda u: 0 < u < 100]
num1 = UserId(80) + 1  # ok
num2 = UserId(800) + 1 # TypeError
```

[PEP-593](https://www.python.org/dev/peps/pep-0593/) has the rationale. Introduced in python3.9.
3.8 users will need to use `typing_extensions`.

Related to #440. More discussion in https://github.com/python/typing/issues/600.
