Idris can compile to c, it requires no runtime. You're probably thinking of Haskell with its RTS.

Idris is closer to ocaml in that regard.

I cough may have already tried using idris in a kernel module. (for fun, not for serious)

I'm not thinking of Haskell. Idris compiles to C but there is an open question there, with regards to how memory will be handled now and in the future. Swift does not need a runtime either, since it uses automatic reference counting for everything; but it has not gone as far as Rust, which defaults to stack allocation everywhere.

This is not to say I doubt the ultimate approach of Idris: with dependent types you can do everything Rust is doing, and more. It's just a matter of project focus and ergonomics.

And how did it go?

It worked surprisingly enough, well enough to make me consider trying out some gpio stuff to play around with.

From there I'll let you know, I'm still learning Idris and dependent types so I'm a fairly boring test case. This was more of a: lets try it and see what goes kaboom test.