Fix #17871 (inconsistency with native_compute and primitive floats)

[proux01]

The Array.of_list in Nativevalues.args_of_accu could result in an OCaml double array when some argument was a primitive float, making all other argument sometimes wrongfully appear as float themselves.

Fixes / closes #17871

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation. (I guess we have to update the cirtical bugs file)
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[silene]

It is worth adding a testcase and an entry in dev/doc/critical-bugs.

[herbelin]

Fix was quick!

So, iiuc, it is that Array.of_list takes internal-representation decisions on the implicit assumption that all elements of an non-empty list have the same internal representation than the first element of the list. The assumption is justified by typing, but may be wrong in the presence of magic.

Conversely, can we say that OCaml runtime has no proper notion of untyped array (as soon as floats are around)?

[proux01]

So, iiuc, it is that Array.of_list takes internal-representation decisions on the implicit assumption that all elements of an non-empty list have the same internal representation than the first element of the list. The assumption is justified by typing, but may be wrong in the presence of magic.

Conversely, can we say that OCaml runtime has no proper notion of untyped array (as soon as floats are around)?

Yes and this makes perfect sense since, as Pierre Marie likes to recall, "Obj.magic is not part of OCaml".

[silene]

Array.of_list takes internal-representation decisions on the implicit assumption that all elements of an non-empty list have the same internal representation than the first element of the list.

Yes and no. This is not specific to Array.of_list. This applies to Array.make and [|....|], and by extension to any function that creates an array. For instance, Array.of_list calls Array.make using the head of the list. If this element happens to be a pointer to a floating-point number, then Array.make decides to create an array of floating-point numbers rather than an array of pointers to floating-point numbers.

[proux01]

@maximedenes @gares I'm putting the 8.18+rc1 milestone as this is an inconsistency fix but feel free to do whateve you want with that milestone.

[proux01]

@coqbot run full ci

[proux01]

@coqbot run full ci

[proux01]

@silene CI green

[silene]

@coqbot merge now