Sorry, I wasn't clear enough. I mean the other way around: `runTC : ∀ {α} {A : Set α} -> TC A -> IO A`. I want to type check some runtime terms using TC facilities.