Felix is on my big list of interesting languages, but I didn't really think of it in the same category as these. I'm sort of aiming for something better than C when I get around to writing an OS kernel, you know, "someday".
I think for your use case decac, clay, bitC and Cyclone would indeed be ideal. There is this Haskell like language with effects based typesystem that might be worth looking at, the name continues to escape me.
One can go very low level with Felix, after all you can write inline C, C++ and define C and C++ functions, but those are not type checked. ABI could also be an issue given that it compiles to C++.
All the best for fun with kernel writing :)
Disciple ? (DDC) http://disciple.ouroborus.net/
http://www.codeblog.ch/2011/06/statically-linked-linux-execu...