<div dir="ltr">What's your use case? Agda IO is implemented using the FFI so calling arbitrary IO functions from TC is not possible. Internally TC runs on top of IO though, so if you have a particular IO function in mind it could conceivably be added as a primitive.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Oct 14, 2016 at 9:54 AM, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Sorry for the off-topic, but is it possible to run a TC computation<br>
inside the IO monad? Would be nice to type check terms that come from<br>
IO in IO.<br>
</blockquote></div><br></div>