SoundX, introduced in "Sound type-dependent syntactic language extension", uses a model of language extension where extension modules build on a host language, defining new typing rules and rule for desugaring new syntax. Evaluation is defined only for the host language. Programs are type checked using the extended language, but then desugared before being evaluated.
In this example, we emulate SoundX by defining typing over extensions, but evaluation only over the host language. We also define desugaring relations to translate extended syntax to the host language.