Sorry for the off-topic, but is it possible to run a TC computation inside the IO monad? Would be nice to type check terms that come from IO in IO.