Feature contract: Text literals#

1. Lexical and grammar rules, including precedence and termination#

A text-literal is a quoted token "…". Raw UTF-8 scalars, escaped quote and backslash, \n, \t, \r, and \u{H…} are accepted. Unicode escapes require one to six hexadecimal digits and a closing brace. Surrogates and values above U+10FFFF are rejected. Raw CR/LF are rejected even after a backslash. --, spaces and parentheses within the token are content. Empty text is valid. Whole source UTF-8 is validated before comment/literal processing; no replacement characters.

2. Scope and binding rules, including generated names#

No bindings are introduced. Literal contents never participate in identifier or comment recognition. Identifiers remain ASCII.

3. Type and quantity requirements#

The result has foundation type StdText (alias Text). StdTextOf stores Bytes and an erased proof that stdUtf8Valid bytes equals StdTrue. The ordinary kernel checks the witness. Invalid bytes cannot be admitted by writing refl.

4. Effects, totality, and evaluation-order rules#

Literal construction is pure. stdTextDecodeUtf8 returns a StdResult for runtime bytes. stdTextBytes explicitly exposes the encoding. No implicit normalization or lossy decoding. stdTextEqual compares scalar sequences through canonical UTF-8 bytes; stdTextScalarCount counts scalars, not graphemes.

5. Elaboration into existing core or a specifically versioned new core extension#

"é" expands to (constructor StdText StdTextOf (bytes 195 169) (refl (family StdBool) (constructor StdBool StdTrue))). Both parsers construct the existing constructor/reflexivity representation; no trusted Text primitive.

6. Representation and target support, where relevant#

Data.UTF8 is the validation/encoding owner. The witness is erased. Byte length and scalar count differ. Host/kernel proof checks and native-evaluator execution are verified locally; direct lowering of runtime Text is not yet qualified.

7. Error codes and primary/secondary origins#

ALPHA-SOURCE-INVALID-UTF8 identifies the first malformed source byte sequence. Literal errors use ALPHA-LITERAL-UNTERMINATED, -NEWLINE, -INCOMPLETE-ESCAPE, -UNKNOWN-ESCAPE, -UNICODE-ESCAPE, and -SCALAR. Bootstrap primary spans are half-open UTF-8 byte ranges with scalar line/columns. LSP defaults to UTF-16 or negotiates UTF-8. Alpha decoder failures retain start and exclusive end offsets; parser/module/linter results preserve these into StdDiagnostic. Rich batch wire serialization and direct-lowering qualification remain open.

8. Formatting and migration rules#

Preserve original quoted spelling and trivia, including escape choice. No Unicode normalization. Diagnostic-message reauthoring is a separate mechanical L14b task.

9. Positive, negative, execution, and edge-case tests#

tests/language/text/alpha-tests checks UTF-8 laws, rejected byte sources, Alpha parser preservation/editions, payload decoding, encoder boundaries and AST elaboration. The language-server replay suites (lsp-replays-utf16-*, lsp-replays-utf8-*; tools/registry/build_lsp_replays.py) check protocol encoding/ranges after a multibyte literal. NativeLiterals.alpha and NativeRuntime.alpha provide emitted-executable probes; 62 exact-output cases passed on the native evaluator lane. Direct file effects and dependent-family projection remain open.

10. Compatibility with the old edition, serialized forms, and cache keys#

Draft alpha-2027 only; alpha-2026 rejects the new token syntax with ALPHA-EDITION-UNSUPPORTED-FORM. Existing decimal byte arrays remain accepted. No new core constructor or serialized core tag. Edition is already a cache-key component. Full old-edition/cache identity and native diagnostic-origin parity still require the L14 qualification gate; focused checks do not prove that gate.

debug/text-conversion-check.py --alpha COMPILER --evidence DIR verifies the well-typed replacement-character mutant is rejected, and checks empty/Unicode literal core identity against explicit constructors with changed-value controls.