diff --git a/racket/prologos/pretty-print.rkt b/racket/prologos/pretty-print.rkt
index fb95900e7..74d0ff970 100644
--- a/racket/prologos/pretty-print.rkt
+++ b/racket/prologos/pretty-print.rkt
@@ -346,7 +346,7 @@
     [(expr-String) "String"]
     [(expr-string val) (format "~s" val)]
     ;; Map
-    [(expr-Map k v) (format "(Map ~a ~a)" (pp-expr k names) (pp-expr v names))]
+    [(expr-Map k v) (format "[Map ~a ~a]" (pp-expr k names) (pp-expr v names))]
     [(expr-champ c)
      (let ([entries (champ-entries c)])
        (if (null? entries)
@@ -371,30 +371,30 @@
     [(expr-map-keys m) (format "[map-keys ~a]" (pp-expr m names))]
     [(expr-map-vals m) (format "[map-vals ~a]" (pp-expr m names))]
     ;; Set
-    [(expr-Set a) (format "(Set ~a)" (pp-expr a names))]
+    [(expr-Set a) (format "[Set ~a]" (pp-expr a names))]
     [(expr-hset c)
      (let ([keys (champ-keys c)])
        (if (null? keys)
            "#{}"
            (format "#{~a}" (string-join (map (lambda (k) (pp-expr k names)) keys) " "))))]
-    [(expr-set-empty a) (format "(set-empty ~a)" (pp-expr a names))]
-    [(expr-set-insert s a) (format "(set-insert ~a ~a)" (pp-expr s names) (pp-expr a names))]
-    [(expr-set-member s a) (format "(set-member? ~a ~a)" (pp-expr s names) (pp-expr a names))]
-    [(expr-set-delete s a) (format "(set-delete ~a ~a)" (pp-expr s names) (pp-expr a names))]
-    [(expr-set-size s) (format "(set-size ~a)" (pp-expr s names))]
-    [(expr-set-union s1 s2) (format "(set-union ~a ~a)" (pp-expr s1 names) (pp-expr s2 names))]
-    [(expr-set-intersect s1 s2) (format "(set-intersect ~a ~a)" (pp-expr s1 names) (pp-expr s2 names))]
-    [(expr-set-diff s1 s2) (format "(set-diff ~a ~a)" (pp-expr s1 names) (pp-expr s2 names))]
-    [(expr-set-to-list s) (format "(set-to-list ~a)" (pp-expr s names))]
+    [(expr-set-empty a) (format "[set-empty ~a]" (pp-expr a names))]
+    [(expr-set-insert s a) (format "[set-insert ~a ~a]" (pp-expr s names) (pp-expr a names))]
+    [(expr-set-member s a) (format "[set-member? ~a ~a]" (pp-expr s names) (pp-expr a names))]
+    [(expr-set-delete s a) (format "[set-delete ~a ~a]" (pp-expr s names) (pp-expr a names))]
+    [(expr-set-size s) (format "[set-size ~a]" (pp-expr s names))]
+    [(expr-set-union s1 s2) (format "[set-union ~a ~a]" (pp-expr s1 names) (pp-expr s2 names))]
+    [(expr-set-intersect s1 s2) (format "[set-intersect ~a ~a]" (pp-expr s1 names) (pp-expr s2 names))]
+    [(expr-set-diff s1 s2) (format "[set-diff ~a ~a]" (pp-expr s1 names) (pp-expr s2 names))]
+    [(expr-set-to-list s) (format "[set-to-list ~a]" (pp-expr s names))]
 
     ;; PVec
-    [(expr-PVec a) (format "(PVec ~a)" (pp-expr a names))]
+    [(expr-PVec a) (format "[PVec ~a]" (pp-expr a names))]
     [(expr-rrb r)
      (let ([elems (reverse (rrb-fold r (lambda (v acc) (cons (pp-expr v names) acc)) '()))])
        (if (null? elems)
            "@[]"
            (string-append "@[" (string-join elems " ") "]")))]
-    [(expr-pvec-empty a) (format "@[] : (PVec ~a)" (pp-expr a names))]
+    [(expr-pvec-empty a) (format "@[] : [PVec ~a]" (pp-expr a names))]
     [(expr-pvec-push v x) (format "[pvec-push ~a ~a]" (pp-expr v names) (pp-expr x names))]
     [(expr-pvec-fold f init vec) (format "[pvec-fold ~a ~a ~a]" (pp-expr f names) (pp-expr init names) (pp-expr vec names))]
     [(expr-pvec-map f vec) (format "[pvec-map ~a ~a]" (pp-expr f names) (pp-expr vec names))]
@@ -435,9 +435,9 @@
     ;; Transient Builders
     [(expr-transient c) (format "[transient ~a]" (pp-expr c names))]
     [(expr-persist c) (format "[persist! ~a]" (pp-expr c names))]
-    [(expr-TVec a) (format "(TVec ~a)" (pp-expr a names))]
-    [(expr-TMap k v) (format "(TMap ~a ~a)" (pp-expr k names) (pp-expr v names))]
-    [(expr-TSet a) (format "(TSet ~a)" (pp-expr a names))]
+    [(expr-TVec a) (format "[TVec ~a]" (pp-expr a names))]
+    [(expr-TMap k v) (format "[TMap ~a ~a]" (pp-expr k names) (pp-expr v names))]
+    [(expr-TSet a) (format "[TSet ~a]" (pp-expr a names))]
     [(expr-trrb _) "~trrb[...]"]
     [(expr-tchamp _) "~tchamp{...}"]
     [(expr-thset _) "~thset#{...}"]
diff --git a/racket/prologos/tests/test-implicit-map-02.rkt b/racket/prologos/tests/test-implicit-map-02.rkt
index 2c9dbbf26..4ea306b9f 100644
--- a/racket/prologos/tests/test-implicit-map-02.rkt
+++ b/racket/prologos/tests/test-implicit-map-02.rkt
@@ -180,7 +180,7 @@
       "def m : [Map Keyword [PVec Keyword]]\n"
       "  :tags @[:admin :active]\n"
       "eval m.tags\n")))
-  (check-equal? result "@[:admin :active] : (PVec Keyword)"))
+  (check-equal? result "@[:admin :active] : [PVec Keyword]"))
 
 (test-case "e2e/ws: implicit map with computed value"
   (define result
diff --git a/racket/prologos/tests/test-map.rkt b/racket/prologos/tests/test-map.rkt
index e121ba30c..c8980e909 100644
--- a/racket/prologos/tests/test-map.rkt
+++ b/racket/prologos/tests/test-map.rkt
@@ -185,7 +185,7 @@
   (check-equal? (pp-expr (expr-Keyword) '()) "Keyword" "pp Keyword")
   (check-equal? (pp-expr (expr-keyword 'name) '()) ":name" "pp :name")
   (check-equal? (pp-expr (expr-Map (expr-Keyword) (expr-Nat)) '())
-                "(Map Keyword Nat)" "pp Map Keyword Nat")
+                "[Map Keyword Nat]" "pp Map Keyword Nat")
   (check-equal? (pp-expr (expr-map-assoc (expr-champ champ-empty)
                                           (expr-keyword 'x) (expr-zero)) '())
                 "[map-assoc {} :x 0N]" "pp map-assoc"))
@@ -241,7 +241,7 @@
                  [current-module-definitions-content (hasheq)])
     (let ([result (process-string "(def m <(Map Keyword Nat)> (map-assoc (map-empty Keyword Nat) :age (suc (suc zero))))\n(eval (map-get m :age))")])
       (check-equal? (length result) 2)
-      (check-true (string-contains? (car result) "m : (Map Keyword Nat) defined"))
+      (check-true (string-contains? (car result) "m : [Map Keyword Nat] defined"))
       (check-equal? (cadr result) "2N : Nat"))))
 
 (test-case "surface: defn with map parameter"
diff --git a/racket/prologos/tests/test-pretty-print-pvec.rkt b/racket/prologos/tests/test-pretty-print-pvec.rkt
new file mode 100644
index 000000000..522416ee7
--- /dev/null
+++ b/racket/prologos/tests/test-pretty-print-pvec.rkt
@@ -0,0 +1,108 @@
+#lang racket/base
+
+;;;
+;;; Tests for pretty-printing of type-applied forms (eigentrust pitfalls doc #14)
+;;;
+;;; The reader accepts type applications written as `[T A]` (e.g.,
+;;; `[PVec Rat]`, `[List Rat]`, `[Map Keyword Nat]`), per the Prologos
+;;; syntax convention that `[]` is the universal functional/type-context
+;;; delimiter and `()` is reserved for parser keywords (match, the, def,
+;;; relational goals).
+;;;
+;;; Pre-fix, the pretty-printer produced `(PVec Rat)`, `(Set Nat)`, etc.
+;;; — a cosmetic divergence between read and printed syntax. This test
+;;; locks in the post-fix behavior: type applications round-trip with the
+;;; `[T A]` form.
+;;;
+
+(require rackunit
+         "../syntax.rkt"
+         "../pretty-print.rkt")
+
+;; ========================================
+;; Type-application forms — primary fix
+;; ========================================
+
+(test-case "pp: PVec Nat -> [PVec Nat]"
+  (check-equal? (pp-expr (expr-PVec (expr-Nat)) '())
+                "[PVec Nat]"))
+
+(test-case "pp: PVec Bool -> [PVec Bool]"
+  (check-equal? (pp-expr (expr-PVec (expr-Bool)) '())
+                "[PVec Bool]"))
+
+(test-case "pp: PVec of fvar (e.g., Rat) -> [PVec Rat]"
+  ;; Rat isn't a primitive expr-* form; using fvar 'Rat exercises the
+  ;; same code path as the eigentrust pitfalls doc observation.
+  (check-equal? (pp-expr (expr-PVec (expr-fvar 'Rat)) '())
+                "[PVec Rat]"))
+
+(test-case "pp: Set Nat -> [Set Nat]"
+  (check-equal? (pp-expr (expr-Set (expr-Nat)) '())
+                "[Set Nat]"))
+
+(test-case "pp: Map Keyword Nat -> [Map Keyword Nat]"
+  (check-equal? (pp-expr (expr-Map (expr-Keyword) (expr-Nat)) '())
+                "[Map Keyword Nat]"))
+
+(test-case "pp: TVec Nat -> [TVec Nat]"
+  (check-equal? (pp-expr (expr-TVec (expr-Nat)) '())
+                "[TVec Nat]"))
+
+(test-case "pp: TMap Keyword Nat -> [TMap Keyword Nat]"
+  (check-equal? (pp-expr (expr-TMap (expr-Keyword) (expr-Nat)) '())
+                "[TMap Keyword Nat]"))
+
+(test-case "pp: TSet Nat -> [TSet Nat]"
+  (check-equal? (pp-expr (expr-TSet (expr-Nat)) '())
+                "[TSet Nat]"))
+
+;; ========================================
+;; Nested type applications — composition with [T A] form
+;; ========================================
+
+(test-case "pp: nested Map of PVec -> [Map Keyword [PVec Nat]]"
+  (check-equal? (pp-expr (expr-Map (expr-Keyword)
+                                   (expr-PVec (expr-Nat)))
+                         '())
+                "[Map Keyword [PVec Nat]]"))
+
+(test-case "pp: nested PVec of Set -> [PVec [Set Nat]]"
+  (check-equal? (pp-expr (expr-PVec (expr-Set (expr-Nat))) '())
+                "[PVec [Set Nat]]"))
+
+;; ========================================
+;; pvec-empty annotation form — uses [PVec ~a]
+;; ========================================
+
+(test-case "pp: pvec-empty annotation uses [PVec ~a]"
+  (check-equal? (pp-expr (expr-pvec-empty (expr-Nat)) '())
+                "@[] : [PVec Nat]"))
+
+;; ========================================
+;; Set/PVec/TVec operation forms — also use [op ...]
+;; ========================================
+
+(test-case "pp: set-empty -> [set-empty Nat]"
+  (check-equal? (pp-expr (expr-set-empty (expr-Nat)) '())
+                "[set-empty Nat]"))
+
+(test-case "pp: set-insert -> [set-insert s a]"
+  (check-equal? (pp-expr (expr-set-insert (expr-fvar 's) (expr-fvar 'a)) '())
+                "[set-insert s a]"))
+
+(test-case "pp: set-member -> [set-member? s a]"
+  (check-equal? (pp-expr (expr-set-member (expr-fvar 's) (expr-fvar 'a)) '())
+                "[set-member? s a]"))
+
+;; ========================================
+;; Cross-check with already-correct forms (regression guard)
+;; ========================================
+
+(test-case "pp: Vec already uses [Vec ...] (regression guard)"
+  (check-equal? (pp-expr (expr-Vec (expr-Nat) (expr-suc (expr-zero))) '())
+                "[Vec Nat 1N]"))
+
+(test-case "pp: simple application uses [f x] (regression guard)"
+  (check-equal? (pp-expr (expr-app (expr-fvar 'f) (expr-zero)) '())
+                "[f 0N]"))
diff --git a/racket/prologos/tests/test-pvec.rkt b/racket/prologos/tests/test-pvec.rkt
index 50f3d40a8..353d32312 100644
--- a/racket/prologos/tests/test-pvec.rkt
+++ b/racket/prologos/tests/test-pvec.rkt
@@ -196,7 +196,7 @@
 ;; ========================================
 
 (test-case "pretty-print: PVec type"
-  (check-equal? (pp-expr (expr-PVec (expr-Nat)) '()) "(PVec Nat)"))
+  (check-equal? (pp-expr (expr-PVec (expr-Nat)) '()) "[PVec Nat]"))
 
 (test-case "pretty-print: rrb value"
   (check-equal? (pp-expr (expr-rrb rrb-empty) '()) "@[]"))
diff --git a/racket/prologos/tests/test-set.rkt b/racket/prologos/tests/test-set.rkt
index b8dbd18e5..71a79a2f5 100644
--- a/racket/prologos/tests/test-set.rkt
+++ b/racket/prologos/tests/test-set.rkt
@@ -241,7 +241,7 @@
 ;; ========================================
 
 (test-case "pretty-print: Set type"
-  (check-equal? (pp-expr (expr-Set (expr-Nat)) '()) "(Set Nat)"))
+  (check-equal? (pp-expr (expr-Set (expr-Nat)) '()) "[Set Nat]"))
 
 (test-case "pretty-print: hset value"
   (check-equal? (pp-expr (expr-hset champ-empty) '()) "#{}"))
@@ -332,7 +332,7 @@
                  [current-module-definitions-content (hasheq)])
     (let ([result (process-string "(def s <(Set Nat)> (set-insert (set-empty Nat) (suc (suc zero))))\n(eval (set-member? s (suc (suc zero))))")])
       (check-equal? (length result) 2)
-      (check-true (string-contains? (car result) "s : (Set Nat) defined"))
+      (check-true (string-contains? (car result) "s : [Set Nat] defined"))
       (check-equal? (cadr result) "true : Bool"))))
 
 ;; ========================================