How does double_of_uint work? Float 5.0 and (u)int 5 have different representations so you can't just do static type change and get correct result, you need a runtime conversion. I suppose it might be special cased in the compiler, but in that case it's bit of a poor example.