I don't think there's any particular issue (as such) with things being TC. I mean, we've been doing TC DSLs and EDSLs for ages now. As you note, I think the key

I don't think there's any particular issue (as such) with things being TC. I mean, we've been doing TC DSLs and EDSLs for ages now. As you note, I think the key here is to be disciplined about it. Even though it can be hard, I would probably advocate a sort of gradual approach, but with full-on rewrites/finding a new host language when deemed necessary. Oh, and I just have to put this in here, because it's so deserving of a meme of its own... Edwin Brady of dependently-typed Idris fame(?) advocates a different and more, IMO, useful term: Pacman Completeness. If you can implement Pacman in $LANGUAGE, it's Turing Complete enough.