I believe this question is a red herring. In case "constant propagation" is an optimization aimed primarily at run-time program code (this is mainly why compilers exist) then it doesn't exactly apply to compile-time math, aka compile-time execution of non-program code. In other words, compile-time execution for the purpose of solving compiler math (not program math) could be done entirely without any this would preserve
compiler-math correctness and/or make it match run-time program-math correctness then it would yes be worth doing.

James Richters: The result of math when using constants MUST be the same as the result of identical math using variables.

Agree.

if the developer explicitly wants reduced precision, then [that's fine].

Agree.

But reduced precision should not come unexpectedly

Agree.

It is possible math is being done differently by the compiler than by programs? For math-related source code, the compiler compiles the instructions and writes them to the program file for compile-time constant calculations that produce run-time constant values, one would expect the compiler to compile the instructions, execute them during compilation, and write the resulting value to the program file for
instructions are discarded, because the program does not need them. If math is being compiled differently for program-executed calculations versus compiler-executed calculations, then that would be a problem.

I'll try to comment on this using some source code which hopefully does conform to FPC,
but I am not sure, because I am not familiar with FPC standards. Please look:

Const
    A_const = Integer(8427);
    B_const = Byte(33);
    C_const = Single(1440.5);
y1 := A_const + C_const / B_const;
y2 := 8427 + 1440.5 / 33;

In my understanding, in the first assignment the constants have types, which are given to them
by the const declarations. And that's why the computation is done using single precision.
This would be OK for me, because the developers decided to do the definitions this way,
and so he or she takes responsibility.
If the computation is done at run time or at compile time, DOESN'T MATTER.

In the second case, using literal constants, the compiler should do the math using the maximum
precision available (IMO), because one constant (1440.5) has a FP representation. It does and should
not matter, that this constant can be stored exactly in a single FP field. Here again:
If the computation is done at run time or at compile time, DOESN'T MATTER.

Maybe this is not how FPC works today, but IMO this is how it should be done, because we want
(IMO) Pascal to be a clear language which is simple to explain, easy to use and easy to implement.

The case would be different, of course, if you do the same casting in the y2 case as in the const
declarations.

Kind regards

Bernd