Features

- Add `admit-vcs` option to generate VCs without sending them to the solver
- Add support for indexed types in scalac frontend

Improvements

- Generalize specification helpers (#828)

Bug fixes

- Remove unsound type-checking rule for function types, and add subtying rules instead