feat(types): add Echo types (structured loss) across the pipeline

Introduce `Echo<A, B>` — the fibre of a function A → B (a retained
witness `x : A` with `f x ≡ y : B`) — and its residue `EchoR<A, B>`,
porting the echo-types (Agda) / EchoTypes.jl lineage into Error-Lang as
a runnable, stability-aware model of non-total erasure.

Pipeline:
- Types/Lexer: `Echo`/`EchoR` keywords; `TyEcho`/`TyEchoResidue`
  typeExpr with sugar (`Echo<A,B>`, `Echo<A>`, bare `Echo`).
- Parser: real `parseTypeExpr` (primitives, `Array<T>`, Echo/EchoR,
  nested `>>` splitting) wired into let annotations, struct fields and
  function params/return — annotations were previously dropped.
- TypeChecker: internal `TyEcho`/`TyEchoR` with conversion, display and
  unification. Echo and EchoR unify only with their own kind and never
  with each other, so erasure is irreversible at the type level.
  Builtins mirror EchoTypes.jl: echo, echo_to_residue,
  residue_strictly_loses, echo_input (illegal on a residue), echo_output.
- Runtime (Bytecode/VM/Codegen): `VEcho{input,output}` single-witness
  value and `VResidue{output}`; dedicated opcodes. Erasing an Echo to its
  residue debits stability (a Landauer-style cost; cf. fiber_erasure_bound).
- Pretty/LayerNavigator: render the new type forms.
- spec/type-system.md: new §7 (Echo Types) plus the [Stab-Erase] rule.
- Tests: type-checker, parser and lexer coverage for Echo/EchoR.

The core conversion/display/unification logic was compile-verified and
behaviourally checked in isolation (the wider compiler/ tree does not
build against mainstream ReScript for reasons predating this change).

Author: claude

compiler/src/Bytecode.res

@@ -50,6 +50,13 @@ type opcode =
   | OpUpdateStability       // Recalculate stability score
   | OpInjectParadox(paradoxType)  // Activate a paradox
 
+  // Echo types (structured loss)
+  | OpEcho                  // Pop output then input, push a fiber witness VEcho{input, output}
+  | OpEchoToResidue         // Pop an echo, push its residue (erases the witness; costs stability)
+  | OpResidueStrictlyLoses  // Pop a value, push VBool(true) iff it is a residue
+  | OpEchoInput             // Pop an echo, push its input witness (runtime error on a residue)
+  | OpEchoOutput            // Pop an echo or residue, push its retained output
+
   // Debug
   | OpPrint(bool)           // Print (println if true)
   | OpHalt                  // Stop execution
@@ -86,6 +93,11 @@ and value =
   | VNil
   | VArray(array<value>)
   | VFunction({arity: int, address: int, name: string})
+  // A single fiber witness: input `x` reached output `y` (one element of `Echo<A, B>`).
+  | VEcho({input: value, output: value})
+  // The residue of an echo after erasure: the input witness is gone (non-recoverable),
+  // only the reached output is retained. This is `EchoR<A, B>` at runtime.
+  | VResidue({output: value})
 
 // Compiled bytecode chunk
 type chunk = {
@@ -119,6 +131,8 @@ let valueToString = (v: value): string => {
       `[${items}]`
     }
   | VFunction({name}) => `<function ${name}>`
+  | VEcho({input, output}) => `echo(${valueToString(input)} ↦ ${valueToString(output)})`
+  | VResidue({output}) => `residue(↦ ${valueToString(output)})`
   }
 }
 
@@ -156,6 +170,11 @@ let opcodeToString = (op: opcode): string => {
   | OpCheckpoint(name) => `CHECKPOINT "${name}"`
   | OpUpdateStability => "UPDATE_STABILITY"
   | OpInjectParadox(_) => "INJECT_PARADOX"
+  | OpEcho => "ECHO"
+  | OpEchoToResidue => "ECHO_TO_RESIDUE"
+  | OpResidueStrictlyLoses => "RESIDUE_STRICTLY_LOSES"
+  | OpEchoInput => "ECHO_INPUT"
+  | OpEchoOutput => "ECHO_OUTPUT"
   | OpPrint(println) => println ? "PRINTLN" : "PRINT"
   | OpHalt => "HALT"
   }

compiler/src/Codegen.res

@@ -130,9 +130,35 @@ let rec compileExpr = (c: compiler, expr: expr): unit => {
       | BNot => ()  // Not implemented
       }
     }
-  | Call(_func, _args, loc) => {
-      // Function calls not fully implemented yet
-      emit(c, OpPush(VNil), loc)
+  | Call(callee, args, loc) => {
+      // Echo builtins compile to dedicated opcodes (the VM has no general call yet).
+      // Arguments are pushed left-to-right; for `echo(x, y)` the output `y` is on top,
+      // which is exactly what OpEcho pops first.
+      switch callee {
+      | Ident("echo", _) => {
+          args->Array.forEach(a => compileExpr(c, a))
+          emit(c, OpEcho, loc)
+        }
+      | Ident("echo_to_residue", _) => {
+          args->Array.forEach(a => compileExpr(c, a))
+          emit(c, OpEchoToResidue, loc)
+        }
+      | Ident("residue_strictly_loses", _) => {
+          args->Array.forEach(a => compileExpr(c, a))
+          emit(c, OpResidueStrictlyLoses, loc)
+        }
+      | Ident("echo_input", _) => {
+          args->Array.forEach(a => compileExpr(c, a))
+          emit(c, OpEchoInput, loc)
+        }
+      | Ident("echo_output", _) => {
+          args->Array.forEach(a => compileExpr(c, a))
+          emit(c, OpEchoOutput, loc)
+        }
+      | _ =>
+        // Other function calls not fully implemented yet
+        emit(c, OpPush(VNil), loc)
+      }
     }
   | Index(array, index, loc) => {
       compileExpr(c, array)

compiler/src/LayerNavigator.res

@@ -292,6 +292,18 @@ let typeExprToString = (t: typeExpr): string => {
   | TyString => "String"
   | TyBool => "Bool"
   | TyArray(inner) => `Array<${typeExprToString(inner)}>`
+  | TyEcho(a, b) =>
+    switch (a, b) {
+    | (None, _) => "Echo"
+    | (Some(ta), None) => `Echo<${typeExprToString(ta)}>`
+    | (Some(ta), Some(tb)) => `Echo<${typeExprToString(ta)}, ${typeExprToString(tb)}>`
+    }
+  | TyEchoResidue(a, b) =>
+    switch (a, b) {
+    | (None, _) => "EchoR"
+    | (Some(ta), None) => `EchoR<${typeExprToString(ta)}>`
+    | (Some(ta), Some(tb)) => `EchoR<${typeExprToString(ta)}, ${typeExprToString(tb)}>`
+    }
   | TyIdent(name) => name
   }
 }

compiler/src/Lexer.res

@@ -133,6 +133,8 @@ let keywords: Dict.t<tokenType> = Dict.fromArray([
   ("String", TString),
   ("Bool", TBool),
   ("Array", TArray),
+  ("Echo", TEcho),
+  ("EchoR", TEchoR),
   ("print", Identifier("print")),
   ("println", Identifier("println")),
 ])

compiler/src/Parser.res

@@ -552,6 +552,73 @@ and parsePrimary = (state: parserState): option<expr> => {
   }
 }
 
+// ============================================
+// Type Annotation Parsing
+// ============================================
+
+// Consume a closing '>' for a type-argument list. Because the lexer greedily
+// produces `>>` as a single `GreaterGreater` token, a closing angle that sits
+// directly against an enclosing one (e.g. `Echo<Array<Int>>`) arrives fused.
+// We split it in place: consume one '>' worth and leave a `Greater` behind for
+// the enclosing type to close against.
+let rec expectCloseAngle = (state: parserState): unit => {
+  switch peek(state) {
+  | Some({type_: Greater}) => advance(state)->ignore
+  | Some({type_: GreaterGreater, loc}) =>
+    state.tokens[state.pos] = {type_: Greater, lexeme: ">", loc}
+  | Some(tok) => addDiagnostic(state, E0006, "Expected '>' to close type arguments", tok.loc)
+  | None => ()
+  }
+}
+
+// Parse an optional `<A>` or `<A, B>` argument list. Returns (first, second).
+and parseTypeArgs = (state: parserState): (option<typeExpr>, option<typeExpr>) => {
+  if check(state, Less) {
+    advance(state)->ignore
+    let first = parseTypeExpr(state)
+    let second = if match_(state, [Comma]) {
+      parseTypeExpr(state)
+    } else {
+      None
+    }
+    expectCloseAngle(state)
+    (first, second)
+  } else {
+    (None, None)
+  }
+}
+
+// Parse a type expression: primitives, Array<T>, Echo / Echo<A> / Echo<A, B>,
+// EchoR / EchoR<A> / EchoR<A, B>, or a named identifier type.
+and parseTypeExpr = (state: parserState): option<typeExpr> => {
+  switch peek(state) {
+  | Some({type_: TInt}) => { advance(state)->ignore; Some(TyInt) }
+  | Some({type_: TFloat}) => { advance(state)->ignore; Some(TyFloat) }
+  | Some({type_: TString}) => { advance(state)->ignore; Some(TyString) }
+  | Some({type_: TBool}) => { advance(state)->ignore; Some(TyBool) }
+  | Some({type_: TArray}) => {
+      advance(state)->ignore
+      switch parseTypeArgs(state) {
+      | (Some(inner), _) => Some(TyArray(inner))
+      // Bare `Array` with no parameter: default the element type to `Any`.
+      | (None, _) => Some(TyArray(TyIdent("Any")))
+      }
+    }
+  | Some({type_: TEcho}) => {
+      advance(state)->ignore
+      let (a, b) = parseTypeArgs(state)
+      Some(TyEcho(a, b))
+    }
+  | Some({type_: TEchoR}) => {
+      advance(state)->ignore
+      let (a, b) = parseTypeArgs(state)
+      Some(TyEchoResidue(a, b))
+    }
+  | Some({type_: Identifier(name)}) => { advance(state)->ignore; Some(TyIdent(name)) }
+  | _ => None
+  }
+}
+
 // ============================================
 // Statement Parsing
 // ============================================
@@ -567,12 +634,17 @@ let parseStatement = (state: parserState): option<stmt> => {
       switch peek(state) {
       | Some({type_: Identifier(name)}) => {
           advance(state)->ignore
-          // Optional type annotation (skip for now)
+          // Optional type annotation: `let x: Type = ...`
+          let type_ = if match_(state, [Colon]) {
+            parseTypeExpr(state)
+          } else {
+            None
+          }
           expect(state, Equal, "Expected '=' after variable name")->ignore
           switch parseExpression(state) {
           | Some(value) => {
               let loc = {start: startLoc.start, end_: currentLoc(state).end_, file: state.file}
-              Some(LetStmt({mutable_, name, type_: None, value, loc}))
+              Some(LetStmt({mutable_, name, type_, value, loc}))
             }
           | None => None
           }
@@ -809,14 +881,15 @@ let parseDeclaration = (state: parserState): option<decl> => {
           advance(state)->ignore
           expect(state, LParen, "Expected '(' after function name")->ignore
 
-          // Parse parameters
+          // Parse parameters (each with an optional `: Type` annotation)
           let params = ref([])
           skipNewlines(state)
           if !check(state, RParen) {
             switch peek(state) {
             | Some({type_: Identifier(pname), loc: ploc}) => {
                 advance(state)->ignore
-                params := Array.concat(params.contents, [{name: pname, type_: None, loc: ploc}])
+                let ptype = if match_(state, [Colon]) { parseTypeExpr(state) } else { None }
+                params := Array.concat(params.contents, [{name: pname, type_: ptype, loc: ploc}])
               }
             | _ => ()
             }
@@ -825,20 +898,26 @@ let parseDeclaration = (state: parserState): option<decl> => {
               switch peek(state) {
               | Some({type_: Identifier(pname), loc: ploc}) => {
                   advance(state)->ignore
-                  params := Array.concat(params.contents, [{name: pname, type_: None, loc: ploc}])
+                  let ptype = if match_(state, [Colon]) { parseTypeExpr(state) } else { None }
+                  params := Array.concat(params.contents, [{name: pname, type_: ptype, loc: ploc}])
                 }
               | _ => ()
               }
             }
           }
           expect(state, RParen, "Expected ')' after parameters")->ignore
 
-          // Optional return type (skip for now)
+          // Optional return type: `function f(...) -> Type`
+          let returnType = if match_(state, [Arrow]) {
+            parseTypeExpr(state)
+          } else {
+            None
+          }
           skipNewlines(state)
 
           let body = parseBlock(state)
           let loc = {start: startLoc.start, end_: currentLoc(state).end_, file: state.file}
-          Some(FunctionDecl({name, params: params.contents, returnType: None, body, loc}))
+          Some(FunctionDecl({name, params: params.contents, returnType, body, loc}))
         }
       | _ => {
           addDiagnostic(state, E0001, "Expected function name", currentLoc(state))
@@ -869,29 +948,10 @@ let parseDeclaration = (state: parserState): option<decl> => {
             | Some({type_: Identifier(fname)}) => {
                 advance(state)->ignore
                 expect(state, Colon, "Expected ':' after field name")->ignore
-                // Simple type parsing
-                switch peek(state) {
-                | Some({type_: TInt}) => {
-                    advance(state)->ignore
-                    fields := Array.concat(fields.contents, [(fname, TyInt)])
-                  }
-                | Some({type_: TFloat}) => {
-                    advance(state)->ignore
-                    fields := Array.concat(fields.contents, [(fname, TyFloat)])
-                  }
-                | Some({type_: TString}) => {
-                    advance(state)->ignore
-                    fields := Array.concat(fields.contents, [(fname, TyString)])
-                  }
-                | Some({type_: TBool}) => {
-                    advance(state)->ignore
-                    fields := Array.concat(fields.contents, [(fname, TyBool)])
-                  }
-                | Some({type_: Identifier(tname)}) => {
-                    advance(state)->ignore
-                    fields := Array.concat(fields.contents, [(fname, TyIdent(tname))])
-                  }
-                | _ => ()
+                // Full type parsing (primitives, Array<T>, Echo<A, B>, EchoR<A, B>, idents)
+                switch parseTypeExpr(state) {
+                | Some(ty) => fields := Array.concat(fields.contents, [(fname, ty)])
+                | None => ()
                 }
               }
             | _ => ()

compiler/src/Pretty.res

@@ -61,9 +61,29 @@ let rec ppTypeExpr = (p, ty) =>
     emit(p, "[")
     ppTypeExpr(p, inner)
     emit(p, "]")
+  | TyEcho(a, b) => ppEchoLike(p, "Echo", a, b)
+  | TyEchoResidue(a, b) => ppEchoLike(p, "EchoR", a, b)
   | TyIdent(name) => emit(p, name)
   }
 
+// Print an Echo/EchoR head with its optional `<A>` or `<A, B>` arguments.
+and ppEchoLike = (p, head, a, b) => {
+  emit(p, head)
+  switch (a, b) {
+  | (None, _) => ()
+  | (Some(ta), None) =>
+    emit(p, "<")
+    ppTypeExpr(p, ta)
+    emit(p, ">")
+  | (Some(ta), Some(tb)) =>
+    emit(p, "<")
+    ppTypeExpr(p, ta)
+    emit(p, ", ")
+    ppTypeExpr(p, tb)
+    emit(p, ">")
+  }
+}
+
 and ppBinaryOp = (p, op) =>
   emit(
     p,