[GHC] #14384: real numbers, digits after the decimal point - digits of precision