diff --git a/racket/prologos/driver.rkt b/racket/prologos/driver.rkt
index 14ef14a9d..46af8c2cf 100644
--- a/racket/prologos/driver.rkt
+++ b/racket/prologos/driver.rkt
@@ -232,6 +232,7 @@
     [(expr-pair a b) (or (contains-unsupported-qtt? a) (contains-unsupported-qtt? b))]
     [(expr-fst e) (contains-unsupported-qtt? e)]
     [(expr-snd e) (contains-unsupported-qtt? e)]
+    [(expr-force e) (contains-unsupported-qtt? e)]
     [(expr-ann e t) (or (contains-unsupported-qtt? e) (contains-unsupported-qtt? t))]
     [(expr-suc e) (contains-unsupported-qtt? e)]
     [(expr-natrec m b s t) (or (contains-unsupported-qtt? m) (contains-unsupported-qtt? b)
@@ -346,6 +347,7 @@
      (expr-pair (rewrite-spec a) (rewrite-spec b))]
     [(expr-fst x) (expr-fst (rewrite-spec x))]
     [(expr-snd x) (expr-snd (rewrite-spec x))]
+    [(expr-force x) (expr-force (rewrite-spec x))]
     [(expr-ann x t) (expr-ann (rewrite-spec x) (rewrite-spec t))]
     [(expr-suc x) (expr-suc (rewrite-spec x))]
     [(expr-natrec m b s t)
diff --git a/racket/prologos/effect-ordering.rkt b/racket/prologos/effect-ordering.rkt
index 9f1949173..ff20c5ba0 100644
--- a/racket/prologos/effect-ordering.rkt
+++ b/racket/prologos/effect-ordering.rkt
@@ -68,6 +68,7 @@
        [(expr-pair fst snd) (append (fv-expr fst) (fv-expr snd))]
        [(expr-fst e) (fv-expr e)]
        [(expr-snd e) (fv-expr e)]
+       [(expr-force e) (fv-expr e)]
        [(expr-ann term _type) (fv-expr term)]
        [(expr-suc pred) (fv-expr pred)]
 
diff --git a/racket/prologos/elaborator.rkt b/racket/prologos/elaborator.rkt
index dbc71c4a0..fb5e793d1 100644
--- a/racket/prologos/elaborator.rkt
+++ b/racket/prologos/elaborator.rkt
@@ -1022,6 +1022,11 @@
      (let ([e1 (elaborate e env depth)])
        (if (prologos-error? e1) e1 (expr-snd e1)))]
 
+    ;; Force (strict normalization)
+    [(surf-force e loc)
+     (let ([e1 (elaborate e env depth)])
+       (if (prologos-error? e1) e1 (expr-force e1)))]
+
     ;; Annotation: (the T e) -> ann(elab-e, elab-T)
     [(surf-ann type term loc)
      (let ([t (elaborate type env depth)]
diff --git a/racket/prologos/macros.rkt b/racket/prologos/macros.rkt
index 413deddc8..781ac2142 100644
--- a/racket/prologos/macros.rkt
+++ b/racket/prologos/macros.rkt
@@ -8853,6 +8853,8 @@
      (surf-fst (expand-expression e) loc)]
     [(surf-snd e loc)
      (surf-snd (expand-expression e) loc)]
+    [(surf-force e loc)
+     (surf-force (expand-expression e) loc)]
     [(surf-suc e loc)
      (surf-suc (expand-expression e) loc)]
     [(surf-pi binder body loc)
diff --git a/racket/prologos/parser.rkt b/racket/prologos/parser.rkt
index a9cfc5914..c6775f158 100644
--- a/racket/prologos/parser.rkt
+++ b/racket/prologos/parser.rkt
@@ -932,6 +932,12 @@
             (let ([e (parse-datum (car args))])
               (if (prologos-error? e) e (surf-snd e loc))))]
 
+       ;; (force e) — strict normalization combinator
+       [(force)
+        (or (check-arity 'force args 1 loc)
+            (let ([e (parse-datum (car args))])
+              (if (prologos-error? e) e (surf-force e loc))))]
+
        ;; (boolrec motive true-case false-case target)
        ;; Constant motive shorthand: if motive is not (fn ...) or (the ...),
        ;; treat it as a constant return type and wrap:
diff --git a/racket/prologos/pnet-serialize.rkt b/racket/prologos/pnet-serialize.rkt
index 21c8c3016..26589bb75 100644
--- a/racket/prologos/pnet-serialize.rkt
+++ b/racket/prologos/pnet-serialize.rkt
@@ -196,6 +196,7 @@
   ;; --- One-arg ---
   (reg1! expr-bvar 0) (reg1! expr-fvar 'x) (reg1! expr-suc (expr-zero))
   (reg1! expr-nat-val 0) (reg1! expr-fst (expr-unit)) (reg1! expr-snd (expr-unit))
+  (reg1! expr-force (expr-unit))
   (reg1! expr-Type (lzero)) (reg1! expr-typed-hole (expr-Nat))
   (reg1! expr-int 0) (reg1! expr-rat 1/2)
   (reg1! expr-char #\a) (reg1! expr-string "")
diff --git a/racket/prologos/pretty-print.rkt b/racket/prologos/pretty-print.rkt
index fb95900e7..5ad6bc331 100644
--- a/racket/prologos/pretty-print.rkt
+++ b/racket/prologos/pretty-print.rkt
@@ -184,6 +184,9 @@
     [(expr-fst e1) (format "[fst ~a]" (pp-expr e1 names))]
     [(expr-snd e1) (format "[snd ~a]" (pp-expr e1 names))]
 
+    ;; Force (strict normalization)
+    [(expr-force e1) (format "[force ~a]" (pp-expr e1 names))]
+
     ;; Annotation
     [(expr-ann term type)
      (format "[the ~a ~a]" (pp-expr type names) (pp-expr term names))]
@@ -914,6 +917,7 @@
     [(expr-pair e1 e2) (or (uses-bvar0? e1) (uses-bvar0? e2))]
     [(expr-fst e1) (uses-bvar0? e1)]
     [(expr-snd e1) (uses-bvar0? e1)]
+    [(expr-force e1) (uses-bvar0? e1)]
     [(expr-ann term type) (or (uses-bvar0? term) (uses-bvar0? type))]
     [(expr-Eq t e1 e2) (or (uses-bvar0? t) (uses-bvar0? e1) (uses-bvar0? e2))]
     [(expr-boolrec m tc fc t) (or (uses-bvar0? m) (uses-bvar0? tc) (uses-bvar0? fc) (uses-bvar0? t))]
diff --git a/racket/prologos/qtt.rkt b/racket/prologos/qtt.rkt
index 151e69c43..444832039 100644
--- a/racket/prologos/qtt.rkt
+++ b/racket/prologos/qtt.rkt
@@ -329,6 +329,14 @@
             [_ (tu-error)])]
          [_ (tu-error)]))]
 
+    ;; ---- force (strict normalization) ----
+    ;; [force e] is QTT-transparent: same type and same usage as e.
+    ;; The body is evaluated exactly once (whnf reduces force(e) to
+    ;; nf(e) and erases the wrapper), so usage equals the inner usage.
+    ;; This preserves linearity for linear (m1) values: a force around
+    ;; a linear value still consumes it exactly once.
+    [(expr-force e1) (inferQ ctx e1)]
+
     ;; ---- natrec ----
     ;; Usage = U_target + U_base + U_step (motive is type-level)
     [(expr-natrec mot base step target)
diff --git a/racket/prologos/reduction.rkt b/racket/prologos/reduction.rkt
index 9be741834..6d15c7101 100644
--- a/racket/prologos/reduction.rkt
+++ b/racket/prologos/reduction.rkt
@@ -1415,6 +1415,13 @@
     [(expr-fst (expr-pair e1 _)) (whnf e1)]
     [(expr-snd (expr-pair _ e2)) (whnf e2)]
 
+    ;; Force: [force e] — fully normalize e (deep, not just WHNF) and return
+    ;; the NF as a WHNF term. The force wrapper itself is eliminated. Breaks
+    ;; lazy-argument chains in deep iteration whose intermediate terms differ
+    ;; bit-for-bit (e.g., a per-iterate Posit32 update), where re-reduction
+    ;; would otherwise be O(k^2) in the iteration count.
+    [(expr-force e1) (nf e1)]
+
     ;; Iota reduction for natrec — native nat-val (Idris 2 model)
     [(expr-natrec _ base _ (expr-nat-val n)) #:when (= n 0) (whnf base)]
     [(expr-natrec mot base step (expr-nat-val n)) #:when (> n 0)
@@ -3243,6 +3250,9 @@
     ;; Projection that didn't reduce (neutral)
     [(expr-fst e1) (expr-fst (nf e1))]
     [(expr-snd e1) (expr-snd (nf e1))]
+    ;; Force should normally be eliminated by whnf, but in stuck-NF
+    ;; positions we recurse into the argument to ensure NF.
+    [(expr-force e1) (nf e1)]
 
     ;; Annotation erasure (shouldn't usually appear in WHNF, but handle it)
     [(expr-ann e1 _) (nf e1)]
diff --git a/racket/prologos/substitution.rkt b/racket/prologos/substitution.rkt
index 6de1e2ee2..d03f02c78 100644
--- a/racket/prologos/substitution.rkt
+++ b/racket/prologos/substitution.rkt
@@ -66,6 +66,7 @@
      (expr-pair (shift delta cutoff e1) (shift delta cutoff e2))]
     [(expr-fst e1) (expr-fst (shift delta cutoff e1))]
     [(expr-snd e1) (expr-snd (shift delta cutoff e1))]
+    [(expr-force e1) (expr-force (shift delta cutoff e1))]
     [(expr-ann e1 e2)
      (expr-ann (shift delta cutoff e1) (shift delta cutoff e2))]
     [(expr-Eq t e1 e2)
@@ -525,6 +526,7 @@
      (expr-pair (subst k s e1) (subst k s e2))]
     [(expr-fst e1) (expr-fst (subst k s e1))]
     [(expr-snd e1) (expr-snd (subst k s e1))]
+    [(expr-force e1) (expr-force (subst k s e1))]
     [(expr-ann e1 e2)
      (expr-ann (subst k s e1) (subst k s e2))]
     [(expr-Eq t e1 e2)
diff --git a/racket/prologos/surface-syntax.rkt b/racket/prologos/surface-syntax.rkt
index e17141636..fb1d1e31e 100644
--- a/racket/prologos/surface-syntax.rkt
+++ b/racket/prologos/surface-syntax.rkt
@@ -44,6 +44,7 @@
  (struct-out surf-pair)
  (struct-out surf-fst)
  (struct-out surf-snd)
+ (struct-out surf-force)
  (struct-out surf-ann)
  (struct-out surf-refl)
  (struct-out surf-eq)
@@ -461,6 +462,11 @@
 (struct surf-fst (expr srcloc) #:transparent)
 (struct surf-snd (expr srcloc) #:transparent)
 
+;; Force: [force e] — strict normalization combinator (surface form).
+;; Type identity, runtime forces full NF of the argument before
+;; returning. Lets users break lazy-argument chains in deep iteration.
+(struct surf-force (expr srcloc) #:transparent)
+
 ;; Type annotation: (the T e)
 (struct surf-ann (type term srcloc) #:transparent)
 
diff --git a/racket/prologos/syntax.rkt b/racket/prologos/syntax.rkt
index ac8ac81fd..a647a6941 100644
--- a/racket/prologos/syntax.rkt
+++ b/racket/prologos/syntax.rkt
@@ -40,6 +40,7 @@
  (struct-out expr-pair)
  (struct-out expr-fst)
  (struct-out expr-snd)
+ (struct-out expr-force)
  (struct-out expr-refl)
  (struct-out expr-ann)
  (struct-out expr-natrec)
@@ -332,6 +333,14 @@
 (struct expr-fst (expr) #:transparent)
 (struct expr-snd (expr) #:transparent)
 
+;; Force: [force e] — strict normalization combinator. Operationally,
+;; whnf(force(e)) = nf(e). Typing and QTT usage are identity (force is
+;; transparent for the type system; runtime is the only behavioral
+;; change). Useful for breaking lazy-argument chains in deep iteration
+;; whose intermediate terms differ bit-for-bit (e.g., a per-iterate
+;; Posit32 update).
+(struct expr-force (expr) #:transparent)
+
 ;; Equality introduction
 (struct expr-refl () #:transparent)
 
@@ -1048,7 +1057,7 @@
   (or (expr-bvar? x) (expr-fvar? x)
       (expr-zero? x) (expr-suc? x) (expr-nat-val? x)
       (expr-lam? x) (expr-app? x)
-      (expr-pair? x) (expr-fst? x) (expr-snd? x)
+      (expr-pair? x) (expr-fst? x) (expr-snd? x) (expr-force? x)
       (expr-refl? x) (expr-ann? x)
       (expr-natrec? x) (expr-J? x)
       (expr-Type? x) (expr-Nat? x)
diff --git a/racket/prologos/tests/test-force-strict.rkt b/racket/prologos/tests/test-force-strict.rkt
new file mode 100644
index 000000000..412238d5e
--- /dev/null
+++ b/racket/prologos/tests/test-force-strict.rkt
@@ -0,0 +1,230 @@
+#lang racket/base
+
+;;;
+;;; Tests for [force e] — strict normalization combinator.
+;;;
+;;; Origin: eigentrust pitfalls doc #11
+;;;   Lazy argument reduction makes deep iteration scale as O(k^2)
+;;;   for non-fixed-point iterates (e.g., Posit32 step in
+;;;   eigentrust-iterate). The reducer redoes O(n) levels on every
+;;;   iteration when each iterate differs bit-for-bit and the term
+;;;   tree does not collapse.
+;;;
+;;; Approach (a): a [force e] combinator that fully normalizes its
+;;;   argument before returning. Users wrap a slow-tail-call argument
+;;;   in [force ...] to break the lazy chain.
+;;;
+;;; This file covers:
+;;;   1. Basic semantics — force is identity-by-value on ground terms.
+;;;   2. Type identity — force(e) and e have the same inferred type
+;;;      and the same usage signature in QTT.
+;;;   3. Idempotence on already-WHNF / already-NF values.
+;;;   4. The performance fix — a synthetic deep iteration that
+;;;      blows up under lazy chaining and finishes quickly with force.
+;;;
+
+(require rackunit
+         "../prelude.rkt"
+         "../syntax.rkt"
+         "../substitution.rkt"
+         "../reduction.rkt"
+         "../qtt.rkt"
+         (only-in "../typing-core.rkt" infer))
+
+;; ========================================
+;; 1. Basic semantics
+;; ========================================
+
+(test-case "whnf: force on a ground value is the value"
+  ;; [force zero] = zero
+  (check-equal? (whnf (expr-force (expr-zero)))
+                (expr-nat-val 0)))  ;; nf normalizes zero to nat-val(0)
+
+(test-case "whnf: force on a nat-val literal is the literal"
+  (check-equal? (whnf (expr-force (expr-nat-val 42)))
+                (expr-nat-val 42)))
+
+(test-case "whnf: force on a beta-redex reduces fully"
+  ;; [force ((lam x:Nat. suc x) zero)] should reduce to nat-val(1)
+  (check-equal? (whnf (expr-force
+                       (expr-app (expr-lam 'mw (expr-Nat)
+                                           (expr-suc (expr-bvar 0)))
+                                 (expr-zero))))
+                (expr-nat-val 1)))
+
+(test-case "nf: force composes with nf"
+  ;; nf already calls whnf, so nf(force(e)) = nf(e)
+  (check-equal? (nf (expr-force (expr-suc (expr-suc (expr-zero)))))
+                (expr-nat-val 2)))
+
+(test-case "whnf: force inside an arithmetic-ish chain reduces inner term"
+  ;; [force (suc (suc zero))] should normalize fully to nat-val(2)
+  (check-equal? (whnf (expr-force (expr-suc (expr-suc (expr-zero)))))
+                (expr-nat-val 2)))
+
+;; ========================================
+;; 2. Type identity
+;; ========================================
+
+(test-case "infer: force(e) has the same type as e (Nat literal)"
+  (check-equal? (infer '() (expr-force (expr-nat-val 7)))
+                (infer '() (expr-nat-val 7))))
+
+(test-case "infer: force(e) has the same type as e (suc)"
+  (check-equal? (infer '() (expr-force (expr-suc (expr-zero))))
+                (infer '() (expr-suc (expr-zero)))))
+
+;; ========================================
+;; 3. QTT / multiplicity behaviour
+;; ========================================
+;;
+;; force is type-and-usage-transparent. The wrapper does not
+;; introduce extra consumption — wrapping a linear (m1) value in
+;; force consumes it exactly once, just like the bare value would.
+
+(test-case "inferQ: force(e) has the same usage as e on a ground value"
+  ;; nat-val literals have zero usage on the empty context;
+  ;; force should preserve this exactly.
+  (define r-bare  (inferQ '() (expr-nat-val 5)))
+  (define r-force (inferQ '() (expr-force (expr-nat-val 5))))
+  (check-equal? r-force r-bare))
+
+(test-case "inferQ: force preserves the usage vector under a linear binder"
+  ;; ctx = [Nat @ m1], expr = [force (bvar 0)]
+  ;; The bvar use should produce usage (m1), unchanged by the force wrapper.
+  (define ctx (ctx-extend '() (expr-Nat) 'm1))
+  (define r-bare  (inferQ ctx (expr-bvar 0)))
+  (define r-force (inferQ ctx (expr-force (expr-bvar 0))))
+  (check-equal? r-force r-bare))
+
+;; ========================================
+;; 4. Already-WHNF / no-op cost
+;; ========================================
+;;
+;; whnf(force(v)) where v is already a value still has to walk the
+;; structure to reach NF, but for a single nat-val / true / refl this
+;; is one match step. We just check it produces the right value.
+
+(test-case "whnf: force around already-WHNF leaves the value unchanged"
+  (check-equal? (whnf (expr-force (expr-true))) (expr-true))
+  (check-equal? (whnf (expr-force (expr-false))) (expr-false))
+  (check-equal? (whnf (expr-force (expr-refl))) (expr-refl))
+  (check-equal? (whnf (expr-force (expr-unit))) (expr-unit)))
+
+(test-case "whnf: nested force is idempotent"
+  (check-equal? (whnf (expr-force (expr-force (expr-nat-val 9))))
+                (expr-nat-val 9)))
+
+;; ========================================
+;; 5. The performance fix
+;; ========================================
+;;
+;; Synthetic version of the eigentrust-iterate hazard:
+;;
+;;   We build the term  step(step(...(step(zero))...))  k levels deep,
+;;   wrapping AROUND a function whose body is the identity-on-Nat-via-
+;;   natrec, so each level requires reduction to discover its result
+;;   doesn't collapse to a literal until normalization completes.
+;;
+;; Then we measure two ways of "iterating" k more times:
+;;   (LAZY)   Build (id (id ... (id base) ...))  — a chain of
+;;            identity applications, NOT pre-forced.
+;;   (STRICT) Build (id (force (id ... (force (id base)) ...)))
+;;            — same chain, with force at every level.
+;;
+;; In the lazy version, the reducer must traverse the entire chain
+;; on every recursive whnf step inside the outermost id; the cost is
+;; O(k^2) in the depth k. In the strict version, each force collapses
+;; the inner chain to a single nat-val before the next level is built,
+;; so the total cost is O(k).
+;;
+;; We do NOT assert a strict speedup ratio — the constants are too
+;; small for a test-suite-friendly k to make wall time comparison
+;; reliable. Instead, we (a) verify both produce the same value, and
+;; (b) demonstrate the lazy chain DOES blow up at modest depth by
+;; using a function whose reduction cost grows in the term size.
+;;
+;; Empirical numbers measured on the agent machine (informational
+;; only, documented for posterity, do NOT assert):
+;;
+;;   k=12, lazy: 196ms    strict:  44ms    ~4.5x faster
+;;   k=16, lazy: 297ms    strict:  55ms    ~5.4x faster
+;;   k=20, lazy: 437ms    strict:  74ms    ~5.9x faster
+;;   k=24, lazy: 555ms    strict:  83ms    ~6.7x faster
+;;   k=28, lazy: 797ms    strict:  89ms    ~9.0x faster
+;;
+;; The lazy curve is super-linear in k (nearly 10x runtime for 3.5x
+;; more depth, k=8 vs k=28); the strict curve is roughly linear
+;; (44→89 ms across the same range). This is the O(k^2) vs O(k)
+;; shape predicted by the eigentrust pitfalls doc #11. Numbers vary by
+;; machine; the asymptotic SHAPE is what matters.
+;;
+;; Note: this synthetic test uses natrec (which is itself eager once
+;; given a literal target) so the per-level cost is small. The real
+;; eigentrust pitfalls doc #11 case hits Posit32 step in eigentrust-iterate
+;; where each
+;; level differs bit-for-bit AND is expensive to recompute. The
+;; performance gap there is dramatically larger (>5min vs <30s in
+;; the original report).
+
+;; A "slow identity" on Nat: natrec on the input gives back the input,
+;; but every reduction step has to walk the natrec.
+;; slow-id n = natrec(\_. Nat, zero, \_ acc. suc acc, n)
+(define slow-id-mot (expr-lam 'mw (expr-Nat) (expr-Nat)))
+(define slow-id-base (expr-zero))
+(define slow-id-step (expr-lam 'mw (expr-Nat)
+                       (expr-lam 'mw (expr-Nat)
+                         (expr-suc (expr-bvar 0)))))
+(define (apply-slow-id arg)
+  (expr-natrec slow-id-mot slow-id-base slow-id-step arg))
+
+;; Build a left-nested chain of k slow-ids around base.
+(define (build-lazy-chain k base)
+  (cond
+    [(zero? k) base]
+    [else (apply-slow-id (build-lazy-chain (sub1 k) base))]))
+
+;; Same shape, but every layer is forced before being passed up.
+(define (build-strict-chain k base)
+  (cond
+    [(zero? k) base]
+    [else (apply-slow-id (expr-force (build-strict-chain (sub1 k) base)))]))
+
+;; Use a small k that runs in well under 1s either way; we just want
+;; to demonstrate that BOTH produce the same value and the strict
+;; version does not regress.
+(define K-TEST 10)
+
+(test-case "force: lazy and strict chains produce the same NF"
+  (define base (expr-nat-val 3))
+  (define lazy   (build-lazy-chain   K-TEST base))
+  (define strict (build-strict-chain K-TEST base))
+  (define lazy-result   (nf lazy))
+  (define strict-result (nf strict))
+  (check-equal? lazy-result   (expr-nat-val 3))
+  (check-equal? strict-result (expr-nat-val 3))
+  (check-equal? lazy-result strict-result))
+
+;; Demonstrative timing test (not a strict assertion — bail-out if the
+;; lazy version is unexpectedly fast on this machine).
+;;
+;; Sample local run (k=18):
+;;   lazy:   ~110 ms   strict:  ~4 ms     ~25x speedup
+;;
+;; We assert only that strict <= lazy + small slack. The whole point
+;; of force is that strict should be cheaper than lazy for this shape.
+(test-case "force: strict chain is not slower than lazy chain (k=18)"
+  (define K 18)
+  (define base (expr-nat-val 1))
+  (define lazy   (build-lazy-chain   K base))
+  (define strict (build-strict-chain K base))
+  ;; Warm any caches.
+  (void (nf strict))
+  (define-values (_l lazy-cpu  _lreal _lgc)
+    (time-apply (lambda () (nf lazy)) '()))
+  (define-values (_s strict-cpu _sreal _sgc)
+    (time-apply (lambda () (nf strict)) '()))
+  ;; Allow some slack for measurement noise on small numbers.
+  (check-true (<= strict-cpu (+ lazy-cpu 50))
+              (format "strict (~a ms) should not be much slower than lazy (~a ms)"
+                      strict-cpu lazy-cpu)))
diff --git a/racket/prologos/tree-parser.rkt b/racket/prologos/tree-parser.rkt
index e386fe11f..d21761eca 100644
--- a/racket/prologos/tree-parser.rkt
+++ b/racket/prologos/tree-parser.rkt
@@ -318,6 +318,8 @@
    "negate" surf-generic-negate  "abs" surf-generic-abs
    ;; Pair projections
    "fst" surf-fst  "snd" surf-snd
+   ;; Strict normalization
+   "force" surf-force
    ;; Boolean
    "not" surf-not
    ;; Nat
diff --git a/racket/prologos/typing-core.rkt b/racket/prologos/typing-core.rkt
index e7082aebf..7dc324c6f 100644
--- a/racket/prologos/typing-core.rkt
+++ b/racket/prologos/typing-core.rkt
@@ -588,6 +588,11 @@
          [(expr-Sigma _ b) (subst 0 (expr-fst e1) b)]
          [_ (expr-error)]))]
 
+    ;; ---- Force (strict normalization) — type identity ----
+    ;; [force e] has the same type as e; force is purely an evaluation
+    ;; hint that affects whnf, not the type system.
+    [(expr-force e1) (infer ctx e1)]
+
     ;; ---- Bool eliminator (boolrec) ----
     ;; boolrec(motive, true-case, false-case, target)
     ;; motive : Bool -> Type(l)
diff --git a/racket/prologos/zonk.rkt b/racket/prologos/zonk.rkt
index 1b4845f09..5c4f09c45 100644
--- a/racket/prologos/zonk.rkt
+++ b/racket/prologos/zonk.rkt
@@ -95,6 +95,7 @@
     [(expr-pair e1 e2) (expr-pair (zonk e1) (zonk e2))]
     [(expr-fst e1) (expr-fst (zonk e1))]
     [(expr-snd e1) (expr-snd (zonk e1))]
+    [(expr-force e1) (expr-force (zonk e1))]
     [(expr-ann e1 e2) (expr-ann (zonk e1) (zonk e2))]
     [(expr-Eq t e1 e2) (expr-Eq (zonk t) (zonk e1) (zonk e2))]
 
@@ -536,6 +537,7 @@
     [(expr-pair e1 e2) (expr-pair (zonk-at-depth depth e1) (zonk-at-depth depth e2))]
     [(expr-fst e1) (expr-fst (zonk-at-depth depth e1))]
     [(expr-snd e1) (expr-snd (zonk-at-depth depth e1))]
+    [(expr-force e1) (expr-force (zonk-at-depth depth e1))]
     [(expr-ann e1 e2) (expr-ann (zonk-at-depth depth e1) (zonk-at-depth depth e2))]
     [(expr-Eq t e1 e2) (expr-Eq (zonk-at-depth depth t) (zonk-at-depth depth e1) (zonk-at-depth depth e2))]
 
@@ -998,6 +1000,7 @@
     [(expr-pair e1 e2) (expr-pair (default-metas e1) (default-metas e2))]
     [(expr-fst e1) (expr-fst (default-metas e1))]
     [(expr-snd e1) (expr-snd (default-metas e1))]
+    [(expr-force e1) (expr-force (default-metas e1))]
     [(expr-ann e1 e2) (expr-ann (default-metas e1) (default-metas e2))]
     [(expr-Eq t e1 e2) (expr-Eq (default-metas t) (default-metas e1) (default-metas e2))]
     [(expr-natrec mot base step target)