Develop a type-directed operational semantics for expressions

[cyrus-]

https://i.cs.hku.hk/~bruno/papers/ecoop2021.pdf

Would allow us to skip the elaboration phase, or large parts of it, and instead do "casts" directly via type ascriptions.