Some kind of dependently typed backend

[L-as]

This will be a good exercise in showing how to embed more powerful type theories.