Check TinyIdris exactly-once duplication and erased-type example

[isomorphisms]

Purpose

Add an AICI acceptance check for the first quantity/type-erasure example in one-room-schoolhouse/TinyIdris#2.

The teaching example is:

duplicate :
  {0 value_type : Type} →
  (1 value : value_type) →
  (value_type, value_type)

duplicate value = ?duplicate_right

It is intentionally incomplete. It asks for one value of an arbitrary type, permits exactly one use of that value, and asks for two values of the same type. The erased value_type and the exactly-once value are separate facts.

Required checks

1. Named-hole fixture

   • The source parses with →.
   • The compiler reports the named hole rather than treating the program as complete.

2. Expected rejection

   duplicate value = (value, value)

   must be rejected because the binder marked 1 is used twice.

3. Positive exactly-once control

   A definition that uses the linear value once must compile, for example:

   keep_once : (1 value : value_type) → value_type
   keep_once value = value

4. Positive unrestricted contrast

   Ordinary duplication must compile when the exactly-once restriction is removed:

   duplicate_unrestricted : value_type → (value_type, value_type)
   duplicate_unrestricted value = (value, value)

5. Erasure boundary

   • Record that 0 applies to value_type, not to value.
   • Do not describe this as a String operation or as runtime duplication of type information.
   • Preserve a compiler-stage receipt showing that the type argument is erased where the available compiler representation can demonstrate it. Otherwise record that part as NOT_VERIFIED rather than guessing from source spelling.

Receipt

Report the fixtures separately as:

unicode_arrow_parse
named_hole_reported
linear_single_use_accepts
linear_double_use_rejects
unrestricted_duplicate_accepts
type_argument_erasure_observed

Each field must be PASS, FAIL, or NOT_VERIFIED, with compiler revision, command, exit status, and diagnostic/output evidence. An expected compiler rejection is a passing test only when it rejects for the intended exactly-once-use reason.

Boundary

This issue checks the meaning of the example. It does not claim that duplicate has an implementation, and a source file containing only the named hole is not a completed compiler acceptance result.