Coerce Idriç floating requests to Float16 with warnings

[isomorphisms]

Purpose

Make .idric floating precision tolerant of ragged type information instead of treating a wider spelling as a fatal source error.

Source-language rule

In .idric files:

• Float16 is the ordinary floating type.
• decimal floating literals are immediately passed through a binary16 rounding boundary;
• Float16 arithmetic rounds again after +, -, *, and /;
• Double, Float, Float32, and Float64 are accepted as precision requests, normalized to Float16, and produce a nonfatal warning such as:

Idriç: requested Double; running this as Float16

Canonical Float16 and bare decimal literals do not produce a narrowing warning.

Ordinary .idr files retain inherited Idris Double behavior.

Current representation boundary

This PR does not pretend that every backend already has a native half-precision register path. The source Float16 value currently uses inherited Double as an implementation carrier, but construction and basic arithmetic pass through an executable IEEE-754 binary16 round-to-nearest-even boundary. The carrier is therefore not the source precision.

Direct CPU/GPU backends can later replace that carrier with native or unboxed Float16 storage/instructions without changing the source-language rule.

Regression

tests/idris2/basic/edric007 now checks that:

• all four wider spellings compile;
• each wider spelling emits the expected Float16 narrowing warning;
• canonical Float16 compiles without a narrowing warning;
• a bare decimal literal compiles without a narrowing warning;
• 2048.0 + 1.0 evaluates as 2048.0, proving binary16 rounding occurs at an arithmetic-operation boundary rather than merely renaming a Double carrier;
• an ordinary .idr file still accepts inherited Double unchanged.

The focused ./edric test path continues to include edric007.

Boundary

This is a filename-scoped Idriç source policy. Compiler implementation code and compatibility code may still use wider host arithmetic internally. That does not make those wider precisions the normal .idric semantics.

Precision-line relation

This head is the Float16-coercion design. The genuine-binary32 commit 249921a30b9fc5b9e842dbb6489a4d8d231b6174, pinned by futhark-benchmarks#1, is a divergent historical head rather than an ancestor of this PR; it is preserved as archive/genuine-binary32-futhark. PR #48 is one commit atop this PR and changes only the carrier-division totality wrappers.

[isomorphisms]

Classification: SUPERSEDED by the final stack tip #49.

#49 carries forward the source-visible Float16 policy work from this branch, but deliberately replaces Double as the Prelude carrier with the primitive Float representation.

This intermediate state should not merge independently. Its branch is being retained because #48/#49 still record the stack ancestry; the final Float16 line still needs reconciliation onto current Idriç.