Ask HN: Good examples of Turing-complete to Turing-incomplete transpilation?

I’m doing some research on the topic. I’m specially interested in understanding how to deal with removing the set of features the incomplete programming language wouldn’t have. Say I want to use typescript to write agda code. What would be some strategies to make this work? Books and other references are also welcome.