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)