diff --git a/collects/syntax/parse/debug.rkt b/collects/syntax/parse/debug.rkt
index 5b556bffc4..f24074a9ec 100644
--- a/collects/syntax/parse/debug.rkt
+++ b/collects/syntax/parse/debug.rkt
@@ -39,7 +39,7 @@
                        [(name ...) (map attr-name attrs)]
                        [(depth ...) (map attr-depth attrs)])
            #'(let ([fh (lambda (fs) fs)])
-               (app-argu parser x x (ps-empty x x) null fh fh #f
+               (app-argu parser x x (ps-empty x x) #f fh fh #f
                          (lambda (fh . attr-values)
                            (map vector '(name ...) '(depth ...) attr-values))
                          argu)))))]))
diff --git a/collects/syntax/parse/experimental/splicing.rkt b/collects/syntax/parse/experimental/splicing.rkt
index c2c3cc792d..b6e026df95 100644
--- a/collects/syntax/parse/experimental/splicing.rkt
+++ b/collects/syntax/parse/experimental/splicing.rkt
@@ -49,9 +49,8 @@
                               (cdr result))))
                      ((error)
                       (let ([es
-                             (list* (expect:message (cadr result))
-                                    (expect:thing pr (get-description param ...) #f rl)
-                                    es)])
+                             (es-add-message (cadr result)
+                                             (es-add-thing pr (get-description param ...) #f rl es))])
                         (fh (failure pr es))))))))))
          (define-syntax name
            (stxclass 'name (arity (length '(param ...)) (length '(param ...)) '() '())
diff --git a/collects/syntax/parse/private/parse.rkt b/collects/syntax/parse/private/parse.rkt
index a39175dbf6..a0ed55ba09 100644
--- a/collects/syntax/parse/private/parse.rkt
+++ b/collects/syntax/parse/private/parse.rkt
@@ -76,7 +76,7 @@
                 (define (parser x cx pr es fh0 cp0 rl success)
                   (if (predicate x)
                       (success fh0)
-                      (let ([es (cons (expect:thing pr 'description #t rl) es)])
+                      (let ([es (es-add-thing pr 'description #t rl es)])
                         (fh0 (failure pr es)))))))]))
 
 (define-syntax (parser/rhs stx)
@@ -150,7 +150,7 @@
                (let* ([x (datum->syntax #f expr)]
                       [cx x]
                       [pr (ps-empty x x)]
-                      [es null]
+                      [es #f]
                       [fh0 (syntax-patterns-fail x)])
                  (parameterize ((current-syntax-context x))
                    def ...
@@ -260,7 +260,7 @@ Conventions:
             (syntax-parameterize ((this-context-syntax
                                    (syntax-rules ()
                                      [(tbs) (ps-context-syntax pr)])))
-              (let ([es (cons (expect:thing pr description 'transparent? rl) es)]
+              (let ([es (es-add-thing pr description 'transparent? rl es)]
                     [pr (if 'transparent? pr (ps-add-opaque pr))])
                 (with ([fail-handler fh0]
                        [cut-prompt cp0])
@@ -398,7 +398,7 @@ Conventions:
                       [(alternative ...) alternatives])
           #`(let* ([ctx0 #,context]
                    [pr (ps-empty x ctx0)]
-                   [es null]
+                   [es #f]
                    [cx x]
                    [fh0 (syntax-patterns-fail ctx0)])
               (parameterize ((current-syntax-context ctx0))
@@ -470,12 +470,12 @@ Conventions:
         #`(let ([d (if (syntax? x) (syntax-e x) x)])
             (if (equal? d (quote datum))
                 k
-                (fail (failure pr (cons (expect:atom 'datum) es)))))]
+                (fail (failure pr (es-add-atom 'datum es)))))]
        [#s(pat:literal attrs literal input-phase lit-phase)
         #`(if (and (identifier? x)
                    (free-identifier=? x (quote-syntax literal) input-phase lit-phase))
               k
-              (fail (failure pr (cons (expect:literal (quote-syntax literal)) es))))]
+              (fail (failure pr (es-add-literal (quote-syntax literal) es))))]
        [#s(pat:action attrs action subpattern)
         #'(parse:A x cx action pr es (parse:S x cx subpattern pr es k))]
        [#s(pat:head attrs head tail)
@@ -549,7 +549,7 @@ Conventions:
                   (parse:S datum scx subpattern pr es k))
                 (fail (failure pr es))))]
        [#s(pat:describe attrs pattern description transparent? role)
-        #`(let ([es (cons (expect:thing pr description transparent? role) es)]
+        #`(let ([es (es-add-thing pr description transparent? role es)]
                 [pr (if 'transparent? pr (ps-add-opaque pr))])
             (parse:S x cx pattern pr es k))]
        [#s(pat:delimit attrs pattern)
@@ -575,7 +575,7 @@ Conventions:
           #'(let ([x* (datum->syntax cx x cx)])
               (if (predicate x*)
                   (let-attributes (name-attr ...) k)
-                  (let ([es (cons (expect:thing pr 'description #t role) es)])
+                  (let ([es (es-add-thing pr 'description #t role es)])
                     (fail (failure pr es))))))])]))
 
 ;; (disjunct ???-pattern success (pre:expr ...) (id:id ...)) : expr[Ans]
@@ -616,7 +616,7 @@ Conventions:
                 (let ([pr* (if (syntax? c)
                                (ps-add-stx pr c)
                                pr)]
-                      [es* (cons (expect:message message) es)])
+                      [es* (es-add-message message es)])
                   (fail (failure pr* es*)))
                 k))]
        [#s(action:parse _ pattern expr)
@@ -669,7 +669,7 @@ Conventions:
     [(parse:H x cx rest-x rest-cx rest-pr head pr es k)
      (syntax-case #'head ()
        [#s(hpat:describe _ pattern description transparent? role)
-        #`(let ([es* (cons (expect:thing pr description transparent? role) es)]
+        #`(let ([es* (es-add-thing pr description transparent? role es)]
                 [pr (if 'transparent? pr (ps-add-opaque pr))])
             (parse:H x cx rest-x rest-cx rest-pr pattern pr es*
                      (let ([rest-pr (if 'transparent? rest-pr (ps-pop-opaque rest-pr))])
@@ -867,7 +867,7 @@ Conventions:
                                   head es loop-k)
                         ...)
                    (cond [(< rel-rep (rep:min-number rel-repc))
-                          (let ([es (cons (expectation-of-reps/too-few rel-rep rel-repc) es)])
+                          (let ([es (expectation-of-reps/too-few es rel-rep rel-repc)])
                             (fail (failure loop-pr es)))]
                          ...
                          [else
@@ -912,7 +912,7 @@ Conventions:
          [_  #`(parse:H x cx x* cx* pr* head pr es
                         (if (< rep (rep:max-number repc))
                             (let ([rep (add1 rep)]) k*)
-                            (let ([es (cons (expectation-of-reps/too-many rep repc) es)])
+                            (let ([es (expectation-of-reps/too-many es rep repc)])
                               (fail (failure pr* es)))))]))]))
 
 ;; (rep:initial-value RepConstraint) : expr
@@ -962,26 +962,23 @@ Conventions:
 
 ;; ----
 
-(define-syntax-rule (expectation-of-message message)
-  (expect:message message))
-
 (define-syntax expectation-of-reps/too-few
   (syntax-rules ()
-    [(_ rep #s(rep:once name too-few-msg too-many-msg))
-     (expect:message (or too-few-msg (name->too-few/once name)))]
-    [(_ rep #s(rep:optional name too-many-msg _))
+    [(_ es rep #s(rep:once name too-few-msg too-many-msg))
+     (es-add-message (or too-few-msg (name->too-few/once name)) es)]
+    [(_ es rep #s(rep:optional name too-many-msg _))
      (error 'syntax-parse "INTERNAL ERROR: impossible (too-few)")]
-    [(_ rep #s(rep:bounds min max name too-few-msg too-many-msg))
-     (expect:message (or too-few-msg (name->too-few name)))]))
+    [(_ es rep #s(rep:bounds min max name too-few-msg too-many-msg))
+     (es-add-message (or too-few-msg (name->too-few name)) es)]))
 
 (define-syntax expectation-of-reps/too-many
   (syntax-rules ()
-    [(_ rep #s(rep:once name too-few-msg too-many-msg))
-     (expect:message (or too-many-msg (name->too-many name)))]
-    [(_ rep #s(rep:optional name too-many-msg _))
-     (expect:message (or too-many-msg (name->too-many name)))]
-    [(_ rep #s(rep:bounds min max name too-few-msg too-many-msg))
-     (expect:message (or too-many-msg (name->too-many name)))]))
+    [(_ es rep #s(rep:once name too-few-msg too-many-msg))
+     (es-add-message (or too-many-msg (name->too-many name)) es)]
+    [(_ es rep #s(rep:optional name too-many-msg _))
+     (es-add-message (or too-many-msg (name->too-many name)) es)]
+    [(_ es rep #s(rep:bounds min max name too-few-msg too-many-msg))
+     (es-add-message (or too-many-msg (name->too-many name)) es)]))
 
 ;; ====
 
diff --git a/collects/syntax/parse/private/residual.rkt b/collects/syntax/parse/private/residual.rkt
index f5682ce155..f0ffd4456e 100644
--- a/collects/syntax/parse/private/residual.rkt
+++ b/collects/syntax/parse/private/residual.rkt
@@ -215,13 +215,12 @@
                      (loop (cdr x) cx (add1 i))
                      (let* ([pr (ps-add-cdr pr i)]
                             [pr (ps-add-car pr)]
-                            [es (cons (expect:thing pr desc #t rl) es)])
+                            [es (es-add-thing pr desc #t rl es)])
                        (values 'fail (failure pr es))))]
                 [else ;; not null, because stx->list failed
                  (let ([pr (ps-add-cdr pr i)]
                        #|
                        ;; Don't extend es! That way we don't get spurious "expected ()"
                        ;; that *should* have been cancelled out by ineffable pair failures.
-                       [es (cons (expect:atom '()) es)]
                        |#)
                    (values 'fail (failure pr es)))])))))
diff --git a/collects/syntax/parse/private/runtime-progress.rkt b/collects/syntax/parse/private/runtime-progress.rkt
index 4d04e932d9..5faf58f33c 100644
--- a/collects/syntax/parse/private/runtime-progress.rkt
+++ b/collects/syntax/parse/private/runtime-progress.rkt
@@ -1,7 +1,5 @@
 #lang racket/base
 (require racket/list
-         unstable/struct
-         syntax/stx
          "minimatch.rkt")
 (provide ps-empty
          ps-add-car
@@ -13,9 +11,7 @@
          ps-add-unpstruct
          ps-add-opaque
 
-         invert-ps
          ps-pop-opaque
-         ps->stx+index
          ps-context-syntax
          ps-difference
 
@@ -25,7 +21,30 @@
          (struct-out expect:atom)
          (struct-out expect:literal)
          (struct-out expect:message)
-         (struct-out expect:disj))
+         (struct-out expect:disj)
+
+         es-add-thing
+         es-add-message
+         es-add-atom
+         es-add-literal)
+
+;; FIXME: add phase to expect:literal
+
+;; == Failure ==
+
+#|
+A Failure is (failure PS ExpectStack)
+
+A FailureSet is one of
+  - Failure
+  - (cons FailureSet FailureSet)
+
+A FailFunction = (FailureSet -> Answer)
+|#
+(define-struct failure (progress expectstack) #:prefab)
+
+
+;; == Progress ==
 
 #|
 Progress (PS) is a non-empty list of Progress Frames (PF).
@@ -86,45 +105,13 @@ Interpretation: later frames are applied first.
 ;; ps-context-syntax : Progress -> syntax
 (define (ps-context-syntax ps)
   ;; Bottom frame is always syntax
-  (car (reverse ps)))
-
-;; ps->stx+index : Progress -> (values stx nat)
-;; Gets the innermost stx that should have a real srcloc, and the offset
-;; (number of cdrs) within that where the progress ends.
-(define (ps->stx+index ps)
-  (define (interp ps)
-    (match ps
-      [(cons (? syntax? stx) _) stx]
-      [(cons 'car parent)
-       (let* ([d (interp parent)]
-              [d (if (syntax? d) (syntax-e d) d)])
-         (cond [(pair? d) (car d)]
-               [(vector? d) (vector->list d)]
-               [(box? d) (unbox d)]
-               [(prefab-struct-key d) (struct->list d)]
-               [else (error 'ps->stx+index "INTERNAL ERROR: unexpected: ~e" d)]))]
-      [(cons (? exact-positive-integer? n) parent)
-       (for/fold ([stx (interp parent)]) ([i (in-range n)])
-         (stx-cdr stx))]
-      [(cons 'post parent)
-       (interp parent)]))
-  (let ([ps (ps-truncate-opaque ps)])
-    (match ps
-      [(cons (? syntax? stx) _)
-       (values stx 0)]
-      [(cons 'car parent)
-       (values (interp ps) 0)]
-      [(cons (? exact-positive-integer? n) parent)
-       (values (interp parent) n)]
-      [(cons 'post parent)
-       (ps->stx+index parent)])))
+  (last ps))
 
 ;; ps-difference : PS PS -> nat
 ;; Returns N s.t. B = (ps-add-cdr^N A)
 (define (ps-difference a b)
   (define (whoops)
-    (error 'ps-difference "~e is not an extension of ~e"
-           (progress->sexpr b) (progress->sexpr a)))
+    (error 'ps-difference "~e is not an extension of ~e" a b))
   (match (list a b)
     [(list (cons (? exact-positive-integer? na) pa)
            (cons (? exact-positive-integer? nb) pb))
@@ -137,29 +124,7 @@ Interpretation: later frames are applied first.
      (unless (equal? a b) (whoops))
      0]))
 
-;; ps-truncate-opaque : PS -> PS
-(define (ps-truncate-opaque ps)
-  (let/ec return
-    (let loop ([ps ps])
-      (cond [(null? ps)
-             null]
-            [(eq? (car ps) 'opaque)
-             ;; Tricky! We only jump after loop returns,
-             ;; so jump closest to end wins.
-             (return (loop (cdr ps)))]
-            [else
-             ;; Either (loop _) jumps, or it is identity
-             (loop (cdr ps))
-             ps]))))
-
-;; An Inverted PS (IPS) is a PS inverted for easy comparison.
-;; An IPS may not contain any 'opaque frames.
-
-;; invert-ps : PS -> IPS
-(define (invert-ps ps)
-  (reverse (ps-truncate-opaque ps)))
-
-;; ps-pop-opaque : PS -> IPS
+;; ps-pop-opaque : PS -> PS
 ;; Used to continue with progress from opaque head pattern.
 (define (ps-pop-opaque ps)
   (match ps
@@ -169,43 +134,40 @@ Interpretation: later frames are applied first.
      ps*]
     [_ (error 'ps-pop-opaque "opaque marker not found: ~e" ps)]))
 
-;; ==== Failure ====
 
-;; A Failure is (failure PS ExpectStack)
-
-;; A FailureSet is one of
-;;   - Failure
-;;   - (cons FailureSet FailureSet)
-
-;; FailFunction = (FailureSet -> Answer)
-
-(define-struct failure (progress expectstack) #:prefab)
-
-;; == Expectations
-
-;; FIXME: add phase to expect:literal
+;; == Expectations ==
 
 #|
-An ExpectStack is (listof Expect)
-
-An Expect is one of
-  - (make-expect:thing ??? string boolean string/#f)
-  * (make-expect:message string)
-  * (make-expect:atom atom)
-  * (make-expect:literal identifier)
-  * (make-expect:disj (non-empty-listof Expect))
+An ExpectStack (during parsing) is one of
+  - (make-expect:thing Progress string boolean string/#f ExpectStack)
+  * (make-expect:message string ExpectStack)
+  * (make-expect:atom atom ExpectStack)
+  * (make-expect:literal identifier ExpectStack)
 
 The *-marked variants can only occur at the top of the stack.
 
-expect:thing frame contains representation of term:
-  - during parsing, represent as progress
-  - during reporting, convert to stx
+Goal during parsing is to minimize/consolidate allocations.
+
+During reporting, the representation changes somewhat:
+
+An ExpectStack (during reporting) is (listof Expect)
+An Expect is one of
+  - (expect:thing (cons syntax nat) string #t string/#f _)
+  * (expect:message string _)
+  * (expect:atom atom _)
+  * (expect:literal identifier _)
+  - (expect:disj (non-empty-listof Expect) _)
+
+That is, next link always ignored (replace with #f for sake of equal? cmp)
+and expect:thing term represented as syntax with index.
+
+Goal during reporting is ease of manipulation.
 |#
-(define-struct expect:thing (term description transparent? role) #:prefab)
-(define-struct expect:message (message) #:prefab)
-(define-struct expect:atom (atom) #:prefab)
-(define-struct expect:literal (literal) #:prefab)
-(define-struct expect:disj (expects) #:prefab)
+(struct expect:thing (term description transparent? role next) #:prefab)
+(struct expect:message (message next) #:prefab)
+(struct expect:atom (atom next) #:prefab)
+(struct expect:literal (literal next) #:prefab)
+(struct expect:disj (expects next) #:prefab)
 
 (define (expect? x)
   (or (expect:thing? x)
@@ -214,40 +176,18 @@ expect:thing frame contains representation of term:
       (expect:literal? x)
       (expect:disj? x)))
 
+(define (es-add-thing ps description transparent? role next)
+  (if description
+      (expect:thing ps description transparent? role next)
+      next))
 
-;; ==== Debugging
+(define (es-add-message message next)
+  (if message
+      (expect:message message next)
+      next))
 
-(provide failureset->sexpr
-         failure->sexpr
-         expectstack->sexpr
-         expect->sexpr)
+(define (es-add-atom atom next)
+  (expect:atom atom next))
 
-(define (failureset->sexpr fs)
-  (let ([fs (flatten fs)])
-    (case (length fs)
-      ((1) (failure->sexpr (car fs)))
-      (else `(union ,@(map failure->sexpr fs))))))
-
-(define (failure->sexpr f)
-  (match f
-    [(failure progress expectstack)
-     `(failure ,(progress->sexpr progress)
-               #:expected ,(expectstack->sexpr expectstack))]))
-
-(define (expectstack->sexpr es)
-  (map expect->sexpr es))
-
-(define (expect->sexpr e)
-  (match e
-    [(expect:thing term description transparent? role)
-     (expect:thing '<Term> description transparent? role)]
-    [else e]))
-
-(define (progress->sexpr ps)
-  (for/list ([pf (in-list (invert-ps ps))])
-    (match pf
-      [(? syntax? stx) 'stx]
-      ['car 'car]
-      ['post 'post]
-      [(? exact-positive-integer? n) n]
-      ['opaque 'opaque])))
+(define (es-add-literal literal next)
+  (expect:literal literal next))
diff --git a/collects/syntax/parse/private/runtime-report.rkt b/collects/syntax/parse/private/runtime-report.rkt
index 77963a9659..1e11438033 100644
--- a/collects/syntax/parse/private/runtime-report.rkt
+++ b/collects/syntax/parse/private/runtime-report.rkt
@@ -1,5 +1,7 @@
 #lang racket/base
 (require racket/list
+         syntax/stx
+         unstable/struct
          "minimatch.rkt"
          (except-in syntax/parse/private/residual
                     syntax-patterns-fail)
@@ -9,7 +11,11 @@
          maximal-failures
 
          exn:syntax-parse?
-         exn:syntax-parse-info)
+         exn:syntax-parse-info
+
+         invert-ps
+         ps->stx+index
+         )
 
 #|
 TODO: given (expect:thing _ D _ R) and (expect:thing _ D _ #f),
@@ -91,7 +97,7 @@ complicated.
            (let ([frame-stx
                   (let-values ([(x cx) (stx-list-drop/cx stx stx index)])
                     (datum->syntax cx x cx))])
-             (cond [(equal? frame-expect (expect:atom '()))
+             (cond [(equal? frame-expect (expect:atom '() #f))
                     (syntax-case frame-stx ()
                       [(one . more)
                        (report "unexpected term" #'one)]
@@ -113,18 +119,18 @@ complicated.
 ;; prose-for-expect : Expect -> string
 (define (prose-for-expect e)
   (match e
-    [(expect:thing ??? description transparent? role)
+    [(expect:thing stx+index description transparent? role _)
      (if role
          (format "expected ~a for ~a" description role)
          (format "expected ~a" description))]
-    [(expect:atom atom)
+    [(expect:atom atom _)
      (format "expected the literal ~a~s~a"
              (if (symbol? atom) "symbol `" "")
              atom
              (if (symbol? atom) "'" ""))]
-    [(expect:literal literal)
+    [(expect:literal literal _)
      (format "expected the identifier `~s'" (syntax-e literal))]
-    [(expect:message message)
+    [(expect:message message _)
      (format "~a" message)]))
 
 ;; == Do Report ==
@@ -170,55 +176,32 @@ complicated.
 
 ;; == Expectation simplification ==
 
-;; normalize-expectstack : ExpectStack -> ExpectStack
-(define (normalize-expectstack es)
-  (convert-expectstack
-   (filter-expectstack
-    (truncate-opaque-expectstack es))))
-
-;; truncate-opaque-expectstack : ExpectStack -> ExpectStack
-;; Eliminates expectations on top of opaque (ie, transparent=#f) frames.
-(define (truncate-opaque-expectstack es)
-  (let/ec return
-    (let loop ([es es])
-      (match es
-        ['() '()]
-        [(cons (expect:thing ps description '#f role) rest-es)
-         ;; Tricky! If multiple opaque frames, multiple "returns",
-         ;; but innermost one called first, so jumps past the rest.
-         ;; Also, flip opaque to transparent for sake of equality.
-         (return (cons (expect:thing ps description #t role) (loop rest-es)))]
-        [(cons (expect:thing ps description '#t role) rest-es)
-         (cons (expect:thing ps description #t role) (loop rest-es))]
-        [(cons expect rest-es)
-         (cons expect (loop rest-es))]))))
-
-;; convert-expectstack : ExpectStack -> ExpectStack
-;; Converts expect:thing term rep from progress to (cons stx index).
-(define (convert-expectstack es)
+;; normalize-expectstack : ExpectStack(parsing) -> ExpectStack(reporting)
+;; Converts internal-chaining to list, converts expect:thing term rep,
+;; and truncates expectstack after opaque (ie, transparent=#f) frames.
+(define (normalize-expectstack es [truncate-opaque? #t])
   (define (convert-ps ps)
     (let-values ([(stx index) (ps->stx+index ps)])
       (cons stx index)))
-  (map (lambda (expect)
-         (match expect
-           [(expect:thing ps de tr? rl)
-            (expect:thing (convert-ps ps) de tr? rl)]
-           [_ expect]))
-       es))
-
-;; filter-expectstack : ExpectStack -> ExpectStack
-;; Eliminates missing (ie, #f) messages and descriptions
-;; FIXME: Change parsing code to avoid useless frame allocations?
-;;   Or are they worth retaining for debugging?
-(define (filter-expectstack es)
-  (filter (lambda (expect)
-            (match expect
-              [(expect:thing _ '#f _ _)
-               #f]
-              [(expect:message '#f)
-               #f]
-              [_ #t]))
-          es))
+  (let/ec return
+    (let loop ([es es])
+      (match es
+        ['#f '()]
+        [(expect:thing ps desc tr? role rest-es)
+         (cond [(and truncate-opaque? (not tr?))
+                ;; Tricky! If multiple opaque frames, multiple 'return' calls,
+                ;; but innermost one called first, so jumps past the rest.
+                ;; Also, flip opaque to transparent for sake of equality.
+                (return
+                 (cons (expect:thing (convert-ps ps) desc #t role #f) (loop rest-es)))]
+               [else
+                (cons (expect:thing (convert-ps ps) desc tr? role #f) (loop rest-es))])]
+        [(expect:message message rest-es)
+         (cons (expect:message message #f) (loop rest-es))]
+        [(expect:atom atom rest-es)
+         (cons (expect:atom atom #f) (loop rest-es))]
+        [(expect:literal literal rest-es)
+         (cons (expect:literal literal #f) (loop rest-es))]))))
 
 #|
 Simplification dilemma
@@ -257,7 +240,7 @@ So we go with option 2.
              (let* ([frames (map car ress)])
                (list (list (if (singleton? frames)
                                (car frames)
-                               (expect:disj frames)))))]
+                               (expect:disj frames #f)))))]
             [else ress])))
   ;; singleton? : list -> boolean
   (define (singleton? res)
@@ -303,6 +286,28 @@ If ps1 = ps2 then both must "blame" the same term,
 ie (ps->stx+index ps1) = (ps->stx+index ps2).
 |#
 
+;; An Inverted PS (IPS) is a PS inverted for easy comparison.
+;; An IPS may not contain any 'opaque frames.
+
+;; invert-ps : PS -> IPS
+(define (invert-ps ps)
+  (reverse (ps-truncate-opaque ps)))
+
+;; ps-truncate-opaque : PS -> PS
+(define (ps-truncate-opaque ps)
+  (let/ec return
+    (let loop ([ps ps])
+      (cond [(null? ps)
+             null]
+            [(eq? (car ps) 'opaque)
+             ;; Tricky! We only jump after loop returns,
+             ;; so jump closest to end wins.
+             (return (loop (cdr ps)))]
+            [else
+             ;; Either (loop _) jumps, or it is identity
+             (loop (cdr ps))
+             ps]))))
+
 ;; maximal/progress : (listof (cons A IPS)) -> (listof (listof A))
 ;; Returns a list of equivalence sets.
 (define (maximal/progress items)
@@ -387,9 +392,78 @@ ie (ps->stx+index ps1) = (ps->stx+index ps2).
         [ips (cdr a+ips)])
     (cons a (cdr ips))))
 
+;; ps->stx+index : Progress -> (values stx nat)
+;; Gets the innermost stx that should have a real srcloc, and the offset
+;; (number of cdrs) within that where the progress ends.
+(define (ps->stx+index ps)
+  (define (interp ps)
+    (match ps
+      [(cons (? syntax? stx) _) stx]
+      [(cons 'car parent)
+       (let* ([d (interp parent)]
+              [d (if (syntax? d) (syntax-e d) d)])
+         (cond [(pair? d) (car d)]
+               [(vector? d) (vector->list d)]
+               [(box? d) (unbox d)]
+               [(prefab-struct-key d) (struct->list d)]
+               [else (error 'ps->stx+index "INTERNAL ERROR: unexpected: ~e" d)]))]
+      [(cons (? exact-positive-integer? n) parent)
+       (for/fold ([stx (interp parent)]) ([i (in-range n)])
+         (stx-cdr stx))]
+      [(cons 'post parent)
+       (interp parent)]))
+  (let ([ps (ps-truncate-opaque ps)])
+    (match ps
+      [(cons (? syntax? stx) _)
+       (values stx 0)]
+      [(cons 'car parent)
+       (values (interp ps) 0)]
+      [(cons (? exact-positive-integer? n) parent)
+       (values (interp parent) n)]
+      [(cons 'post parent)
+       (ps->stx+index parent)])))
+
 (define (rmap f xs)
   (let rmaploop ([xs xs] [accum null])
     (cond [(pair? xs)
            (rmaploop (cdr xs) (cons (f (car xs)) accum))]
           [else
            accum])))
+
+
+;; ==== Debugging
+
+(provide failureset->sexpr
+         failure->sexpr
+         expectstack->sexpr
+         expect->sexpr)
+
+(define (failureset->sexpr fs)
+  (let ([fs (flatten fs)])
+    (case (length fs)
+      ((1) (failure->sexpr (car fs)))
+      (else `(union ,@(map failure->sexpr fs))))))
+
+(define (failure->sexpr f)
+  (match f
+    [(failure progress expectstack)
+     `(failure ,(progress->sexpr progress)
+               #:expected ,(expectstack->sexpr expectstack))]))
+
+(define (expectstack->sexpr es)
+  (map expect->sexpr (normalize-expectstack es #f)))
+
+(define (expect->sexpr e)
+  (match e
+    [(expect:thing stx+index description transparent? role _)
+     (expect:thing '<Term> description transparent? role '_)]
+    [else e]))
+
+(define (progress->sexpr ps)
+  (for/list ([pf (in-list (reverse ps))])
+    (match pf
+      [(? syntax? stx) 'stx]
+      ['car 'car]
+      ['post 'post]
+      [(? exact-positive-integer? n) n]
+      ['opaque 'opaque])))