Floating point scientific notation does not work for 1e100

[tinlyx]

Steps to Reproduce

Loading the following definitions of floating point values into the REPL (0.6.0):

f1 : Double
f1 = 1.0e100

f2 : Double
f2 = 1e100  --this notation does not work in Idris2 but works in Haskell.

Expected Behavior

Both f1 and f2 should be accepted.

Observed Behavior

The second notation f2 = 1e100 which works in Haskell and most other languages, generates the following error:

Welcome to Idris 2.  Enjoy yourself!
1/1: Building sci (sci.idr)
Error: While processing right hand side of f2. Undefined name e100.

[CodingCellist]

I suspect this is to do with the 1-literal being considered an Integer by default in Idris, whereas the 1.0-literal is clearly a Double. However, I'm not sure if this is a parse error, or if it should be considered expected behaviour?... Maybe the former, since we know it's not an Integer thanks to the immediately following e (scientific notation "usually" denotes floats/doubles in programming languages, right)?...

[buzden]

Maybe the former, since we know it's not an Integer thanks to the immediately following e (scientific notation "usually" denotes floats/doubles in programming languages, right)?...

Since anyway double literals are overloadable in Idris, we can implement appropriate fromDouble resulting in an Integer, that statically checks that the given Double contains really an integer. However, here would be a bad behaviour when exponent is too big -- definitely representable by Integer, but not representable by Double.

More general solution would be inventing an overloadable fromSciNotation which would be given a Double and an Integer, and then could be implemented for different types correctly (with appropriate static checks using dependent types, if needed).