Javascript backend represents 32-bit floats as 64-bit floats

A fact I heard at the GHC Contributor's Workshop, although I may be misremembering the details (cc @hsyl20 ).

When someone has expressly asked for 32-bit floats, perhaps for compatibility with some other system, the different behavior regarding precision and over/underflow will likely be an issue.

I think the standard reply could be "don't do that", but some quick searching yields some possible ways of improving correctness:

• https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Math/fround
• https://blog.mozilla.org/javascript/2013/11/07/efficient-float32-arithmetic-in-javascript/