Staged compilation with two-level type theory [pdf]