extra_float_digits and casting from real to numeric

A customer recently upgraded their jdbc driver from 8.4 to 9.2. This
enabled the binary wire protocol (effectively between 9.1 and 9.2).
They reported that single precision values inserted into a
numeric(10,2) column were suddenly rounded wrongly, i.e. 10000.18 was
inserted as 10000.20, while that worked before. Of course we told them
that single is the wrong data type for this, but still, this is a
regression.

The behavior is easily reproducible with SELECT 10000.18::real which
returns 10000.2. Now, the jdbc driver sets extra_float_digits = 3,
which makes the this ::real cast return 10000.1797 in psql. This is
consistent with the documentation which suggests that
extra_float_digits = 0 will return the same representation on all
platforms, so it must be rounded a bit to account for different
implementations.

But if extra_float_digits > 0 is set, I'd expect not only the float4
output to be affected by it, but also casts to other datatypes, which
is not the case now:

set extra_float_digits = 0;
select 10000.18::real, 10000.18::real::numeric(10,2), 10000.18::real::text, to_char(10000.18::real, '99999D999');
float4 | numeric | text | to_char
---------+----------+---------+----------
10000.2 | 10000.20 | 10000.2 | 10000.2

set extra_float_digits = 1;
select 10000.18::real, 10000.18::real::numeric(10,2), 10000.18::real::text, to_char(10000.18::real, '99999D999');
float4 | numeric | text | to_char
----------+----------+----------+----------
10000.18 | 10000.20 | 10000.18 | 10000.2

set extra_float_digits = 3;
select 10000.18::real, 10000.18::real::numeric(10,2), 10000.18::real::text, to_char(10000.18::real, '99999D999');
float4 | numeric | text | to_char
------------+----------+------------+----------
10000.1797 | 10000.20 | 10000.1797 | 10000.2

Is that sane? Shouldn't FLT_DIG in float4_numeric() be replaced with
"FLT_DIG + extra_float_digits" like float4out() does, so the extra
precision is not lost when inserting float4 data into numeric columns?
Likewise, float4_to_char() should be adjusted for to_char output, and
correspondingly float8_numeric() and float8_to_char()?

Christoph
--
cb(at)df7cb(dot)de | http://www.df7cb.de/