diff --git a/tapl/typed-lang-builder/exist.rkt b/tapl/typed-lang-builder/exist.rkt
index ee48c9a..b4ec669 100644
--- a/tapl/typed-lang-builder/exist.rkt
+++ b/tapl/typed-lang-builder/exist.rkt
@@ -17,10 +17,10 @@
 (define-typed-syntax pack
   [(pack (τ:type e) as ∃τ:type) ▶
    [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm]
-   [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: ∃τ.norm)]]])
+   [⊢ [[_ ≫ e-] ⇒ : ∃τ.norm]]])
 
 (define-typed-syntax open #:datum-literals (<= with)
   [(open [x:id <= e_packed with X:id] e)
@@ -68,8 +68,8 @@
    ;; ------------------------------
    ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
    ;;
-   [⊢ [[e_packed ≫ e_packed-] ⇒ (: (~∃ (Y) τ_body))]]
+   [⊢ [[e_packed ≫ e_packed-] ⇒ : (~∃ (Y) τ_body)]]
    [#:with τ_x (subst #'X #'Y #'τ_body)]
-   [([X : #%type ≫ X-]) ([x : τ_x ≫ x-]) ⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [([X : #%type ≫ X-]) ([x : τ_x ≫ x-]) ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e_packed-]) e-)] ⇒ (: τ_e)]]])
+   [⊢ [[_ ≫ (let- ([x- e_packed-]) e-)] ⇒ : τ_e]]])
diff --git a/tapl/typed-lang-builder/ext-stlc.rkt b/tapl/typed-lang-builder/ext-stlc.rkt
index ab4500a..a08a15d 100644
--- a/tapl/typed-lang-builder/ext-stlc.rkt
+++ b/tapl/typed-lang-builder/ext-stlc.rkt
@@ -25,17 +25,17 @@
 (define-typed-syntax #%datum
   [(#%datum . b:boolean) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . b)] ⇒ (: Bool)]]]
+   [⊢ [[_ ≫ (#%datum- . b)] ⇒ : Bool]]]
   [(#%datum . s:str) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . s)] ⇒ (: String)]]]
+   [⊢ [[_ ≫ (#%datum- . s)] ⇒ : String]]]
   [(#%datum . f) ▶
    [#:when (flonum? (syntax-e #'f))]
    --------
-   [⊢ [[_ ≫ (#%datum- . f)] ⇒ (: Float)]]]
+   [⊢ [[_ ≫ (#%datum- . f)] ⇒ : Float]]]
   [(#%datum . c:char) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . c)] ⇒ (: Char)]]]
+   [⊢ [[_ ≫ (#%datum- . c)] ⇒ : Char]]]
   [(#%datum . x) ▶
    --------
    [_ ≻ (stlc+lit:#%datum . x)]])
@@ -49,16 +49,16 @@
 
 (define-typed-syntax and
   [(and e1 e2) ▶
-   [⊢ [[e1 ≫ e1-] ⇐ (: Bool)]]
-   [⊢ [[e2 ≫ e2-] ⇐ (: Bool)]]
+   [⊢ [[e1 ≫ e1-] ⇐ : Bool]]
+   [⊢ [[e2 ≫ e2-] ⇐ : Bool]]
    --------
-   [⊢ [[_ ≫ (and- e1- e2-)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (and- e1- e2-)] ⇒ : Bool]]])
 
 (define-typed-syntax or
   [(or e ...) ▶
-   [⊢ [[e ≫ e-] ⇐ (: Bool)] ...]
+   [⊢ [[e ≫ e-] ⇐ : Bool] ...]
    --------
-   [⊢ [[_ ≫ (or- e- ...)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (or- e- ...)] ⇒ : Bool]]])
 
 (begin-for-syntax 
   (define current-join 
@@ -78,45 +78,45 @@
        ((current-join) τ τ2))]))
 
 (define-typed-syntax if
-  [(if e_tst e1 e2) ⇐ (: τ-expected) ▶
-   [⊢ [[e_tst ≫ e_tst-] ⇒ (: _)]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇐ (: τ-expected)]]
-   [⊢ [[e2 ≫ e2-] ⇐ (: τ-expected)]]
+  [(if e_tst e1 e2) ⇐ : τ-expected ▶
+   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [[e1 ≫ e1-] ⇐ : τ-expected]]
+   [⊢ [[e2 ≫ e2-] ⇐ : τ-expected]]
    --------
-   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇐ : _]]]
   [(if e_tst e1 e2) ▶
-   [⊢ [[e_tst ≫ e_tst-] ⇒ (: _)]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇒ (: τ1)]]
-   [⊢ [[e2 ≫ e2-] ⇒ (: τ2)]]
+   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
+   [⊢ [[e2 ≫ e2-] ⇒ : τ2]]
    --------
-   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇒ (: (⊔ τ1 τ2))]]])
+   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
 
 (define-base-type Unit)
 (define-primop void : (→ Unit))
 
 (define-typed-syntax begin
-  [(begin e_unit ... e) ⇐ (: τ_expected) ▶
-   [⊢ [[e_unit ≫ e_unit-] ⇒ (: _)] ...]
-   [⊢ [[e ≫ e-] ⇐ (: τ_expected)]]
+  [(begin e_unit ... e) ⇐ : τ_expected ▶
+   [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
+   [⊢ [[e ≫ e-] ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇐ : _]]]
   [(begin e_unit ... e) ▶
-   [⊢ [[e_unit ≫ e_unit-] ⇒ (: _)] ...]
-   [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇒ (: τ_e)]]])
+   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇒ : τ_e]]])
 
 (define-typed-syntax let
-  [(let ([x e] ...) e_body) ⇐ (: τ_expected) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ_x)] ...]
-   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇐ (: τ_expected)]]
+  [(let ([x e] ...) e_body) ⇐ : τ_expected ▶
+   [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
+   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇐ : _]]]
   [(let ([x e] ...) e_body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ_x)] ...]
-   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇒ (: τ_body)]]
+   [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
+   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇒ : τ_body]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇒ (: τ_body)]]])
+   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇒ : τ_body]]])
 
 ; dont need to manually transfer expected type
 ; result template automatically propagates properties
@@ -131,15 +131,15 @@
    [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
 
 (define-typed-syntax letrec
-  [(letrec ([b:type-bind e] ...) e_body) ⇐ (: τ_expected) ▶
+  [(letrec ([b:type-bind e] ...) e_body) ⇐ : τ_expected ▶
    [() ([b.x : b.type ≫ x-] ...)
-    ⊢ [[e ≫ e-] ⇐ (: b.type)] ... [[e_body ≫ e_body-] ⇐ (: τ_expected)]]
+    ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇐ : _]]]
   [(letrec ([b:type-bind e] ...) e_body) ▶
    [() ([b.x : b.type ≫ x-] ...)
-    ⊢ [[e ≫ e-] ⇐ (: b.type)] ... [[e_body ≫ e_body-] ⇒ (: τ_body)]]
+    ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇒ : τ_body]]
    --------
-   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇒ (: τ_body)]]])
+   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇒ : τ_body]]])
 
 
diff --git a/tapl/typed-lang-builder/fomega.rkt b/tapl/typed-lang-builder/fomega.rkt
index 35cd108..021b4ff 100644
--- a/tapl/typed-lang-builder/fomega.rkt
+++ b/tapl/typed-lang-builder/fomega.rkt
@@ -84,34 +84,34 @@
 
 (define-typed-syntax Λ
   [(Λ bvs:kind-ctx e) ▶
-   [([bvs.x : bvs.kind ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [([bvs.x : bvs.kind ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: (∀ ([tv- : bvs.kind] ...) τ_e))]]])
+   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
   [(inst e τ ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~∀ (tv ...) τ_body)) ⇒ (: (~∀★ k ...))]]
-   [⊢ [[τ ≫ τ-] ⇐ (: k)] ...]
+   [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
+   [⊢ [[τ ≫ τ-] ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ-inst)]]])
+   [⊢ [[_ ≫ e-] ⇒ : τ-inst]]])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
 (define-typed-syntax tyλ
   [(tyλ bvs:kind-ctx τ_body) ▶
-   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[τ_body ≫ τ_body-] ⇒ (: k_body)]]
+   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[τ_body ≫ τ_body-] ⇒ : k_body]]
    [#:fail-unless ((current-kind?) #'k_body)
     (format "not a valid type: ~a\n" (type->str #'τ_body))]
    --------
-   [⊢ [[_ ≫ (λ- (tv- ...) τ_body-)] ⇒ (: (⇒ bvs.kind ... k_body))]]])
+   [⊢ [[_ ≫ (λ- (tv- ...) τ_body-)] ⇒ : (⇒ bvs.kind ... k_body)]]])
 
 (define-typed-syntax tyapp
   [(tyapp τ_fn τ_arg ...) ▶
-   [⊢ [[τ_fn ≫ τ_fn-] ⇒ (: (~⇒ k_in ... k_out))]]
+   [⊢ [[τ_fn ≫ τ_fn-] ⇒ : (~⇒ k_in ... k_out)]]
    [#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
     (format "wrong number of arguments: expected ~a, given ~a"
             (stx-length #'[k_in ...]) (stx-length #'[τ_arg ...]))]
-   [⊢ [[τ_arg ≫ τ_arg-] ⇐ (: k_in)] ...]
+   [⊢ [[τ_arg ≫ τ_arg-] ⇐ : k_in] ...]
    --------
-   [⊢ [[_ ≫ (#%app- τ_fn- τ_arg- ...)] ⇒ (: k_out)]]])
+   [⊢ [[_ ≫ (#%app- τ_fn- τ_arg- ...)] ⇒ : k_out]]])
diff --git a/tapl/typed-lang-builder/fomega2.rkt b/tapl/typed-lang-builder/fomega2.rkt
index 5bce9c5..d152435 100644
--- a/tapl/typed-lang-builder/fomega2.rkt
+++ b/tapl/typed-lang-builder/fomega2.rkt
@@ -80,15 +80,15 @@
 
 (define-typed-syntax Λ
   [(Λ bvs:kind-ctx e) ▶
-   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: (∀ ([tv- : bvs.kind] ...) τ_e))]]])
+   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
   [(inst e τ ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~∀ (tv ...) τ_body)) ⇒ (: (~∀★ k ...))]]
-   [⊢ [[τ ≫ τ-] ⇐ (: k)] ...]
+   [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
+   [⊢ [[τ ≫ τ-] ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ-inst)]]])
+   [⊢ [[_ ≫ e-] ⇒ : τ-inst]]])
 
diff --git a/tapl/typed-lang-builder/fsub.rkt b/tapl/typed-lang-builder/fsub.rkt
index f4e8747..1ff395b 100644
--- a/tapl/typed-lang-builder/fsub.rkt
+++ b/tapl/typed-lang-builder/fsub.rkt
@@ -48,7 +48,7 @@
   [(∀ ([tv:id <: τ:type] ...) τ_body) ▶
    --------
    ; eval first to overwrite the old #%type
-   [⊢ [[_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body))] ⇒ (: (<: τ.norm ...))]]])
+   [⊢ [[_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body))] ⇒ : (<: τ.norm ...)]]])
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
@@ -79,14 +79,14 @@
    ;; environment with a syntax property using another tag: '<:
    ;; The "expose" function looks for this tag to enforce the bound,
    ;; as in TaPL (fig 28-1)
-   [([tv : #%type <: τsub ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [([tv : #%type <: τsub ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: (∀ ([tv- <: τsub] ...) τ_e))]]])
+   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- <: τsub] ...) τ_e)]]])
 (define-typed-syntax inst
   [(inst e τ:type ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~∀ ([tv <: τ_sub] ...) τ_body))]]
+   [⊢ [[e ≫ e-] ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
    [τ.norm τ⊑ τ_sub] ...
    [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ_inst)]]])
+   [⊢ [[_ ≫ e-] ⇒ : τ_inst]]])
 
diff --git a/tapl/typed-lang-builder/mlish-core.rkt b/tapl/typed-lang-builder/mlish-core.rkt
index f65eb5e..26b6b35 100644
--- a/tapl/typed-lang-builder/mlish-core.rkt
+++ b/tapl/typed-lang-builder/mlish-core.rkt
@@ -312,7 +312,7 @@
 ;;   intuitive, we arbitrarily sort the inferred tyvars lexicographically
 (define-typed-syntax define
   [(define x:id e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ)]]
+   [⊢ [[e ≫ e-] ⇒ : τ]]
    [#:with y (generate-temporary)]
    --------
    [_ ≻ (begin-
@@ -466,15 +466,15 @@
               --------
               [_ ≻ (C)]]
              ; no args but polymorphic, check expected type
-             [C:id ⇐ (: (NameExpander τ-expected-arg (... ...))) ▶
+             [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ▶
               [#:when (stx-null? #'(τ ...))]
               --------
-              [⊢ [[_ ≫ (StructName)] ⇐ (: _)]]]
+              [⊢ [[_ ≫ (StructName)] ⇐ : _]]]
              ; id with multiple expected args, HO fn
              [C:id ▶
               [#:when (not (stx-null? #'(τ ...)))]
               --------
-              [⊢ [[_ ≫ StructName] ⇒ (: (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))]]]
+              [⊢ [[_ ≫ StructName] ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
              [(C τs e_arg ...) ▶
               [#:when (brace? #'τs)] ; commit to this clause
               [#:with [X* (... ...)] #'[X ...]]
@@ -482,10 +482,10 @@
               [#:with {~! τ_X:type (... ...)} #'τs]
               [#:with (τ_in:type (... ...)) ; instantiated types
                (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))]
-              [⊢ [[e_arg* ≫ e_arg*-] ⇐ (: τ_in.norm)] (... ...)]
+              [⊢ [[e_arg* ≫ e_arg*-] ⇐ : τ_in.norm] (... ...)]
               [#:with [e_arg- ...] #'[e_arg*- (... ...)]]
               --------
-              [⊢ [[_ ≫ (StructName e_arg- ...)] ⇒ (: (Name τ_X.norm (... ...)))]]]
+              [⊢ [[_ ≫ (StructName e_arg- ...)] ⇒ : (Name τ_X.norm (... ...))]]]
              [(C . args) ▶ ; no type annotations, must infer instantiation
               [#:with StructName/ty 
                (set-stx-prop/preserved
@@ -700,7 +700,7 @@
   ;; e is a tuple
   [(match e with . clauses) ▶
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (×? #'τ_e)]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([x ... -> e_body]) #'clauses]
@@ -715,11 +715,11 @@
    --------
    [⊢ [[_ ≫ (let- ([z e-])
               (let- ([x- (acc z)] ...) e_body-))]
-       ⇒ (: ty_body)]]]
+       ⇒ : ty_body]]]
   ;; e is a list
   [(match e with . clauses) ▶
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (List? #'τ_e)]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
@@ -753,11 +753,11 @@
               (cond-
                 [(pred? z)
                  (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))]
-       ⇒ (: (⊔ ty_body ...))]]]
+       ⇒ : (⊔ ty_body ...)]]]
   ;; e is a variant
   [(match e with . clauses) ▶
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([Clause:id x:id ... 
                        (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
@@ -794,7 +794,7 @@
    [#:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))]
    ;TODO: get this working
    ;[() ([x : τ ≫ x-] ...)
-   ; ⊢ [[e_guard ≫ e_guard-] ⇐ (: Bool)] [[e_c ≫ e_c-] ⇒ τ_ec]]
+   ; ⊢ [[e_guard ≫ e_guard-] ⇐ : Bool] [[e_c ≫ e_c-] ⇒ : τ_ec]]
    ;...
    [#:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
     (stx-map 
@@ -810,7 +810,7 @@
                 [(and- (Cons? z) 
                        (let- ([x- (acc z)] ...) e_guard-))
                  (let- ([x- (acc z)] ...) e_c-)] ...))]
-       ⇒ (: (⊔ τ_ec ...))]]])
+       ⇒ : (⊔ τ_ec ...)]]])
 
 ; special arrow that computes free vars; for use with tests
 ; (because we can't write explicit forall
@@ -845,29 +845,29 @@
 
 ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
 (define-typed-syntax λ #:datum-literals (:)
-  [(λ (x:id ...) body) ⇐ (: (~?∀ (X ...) (~ext-stlc:→ τ_in ... τ_out))) ▶
+  [(λ (x:id ...) body) ⇐ : (~?∀ (X ...) (~ext-stlc:→ τ_in ... τ_out)) ▶
    [#:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
     (format "expected a function of ~a arguments, got one with ~a arguments"
             (stx-length #'[τ_in ...]) (stx-length #'[x ...]))]
    [([X : #%type ≫ X-] ...) ([x : τ_in ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ (: τ_out)]]
+    ⊢ [[body ≫ body-] ⇐ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ : _]]]
   [(λ ([x : τ_x] ...) body) ▶
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
    ;; TODO is there a way to have λs that refer to ids defined after them?
    [([X : #%type ≫ X-] ...) ([x : τ_x ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇒ (: τ_body)]]
+    ⊢ [[body ≫ body-] ⇒ : τ_body]]
    [#:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇒ (: (?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body)))]]])
+   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇒ : (?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body))]]])
 
 
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
   [(_ e_fn . e_args) ▶
    ;; compute fn type (ie ∀ and →)
-   [⊢ [[e_fn ≫ e_fn-] ⇒ (: (~?∀ Xs (~ext-stlc:→ . tyX_args)))]]
+   [⊢ [[e_fn ≫ e_fn-] ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
    ;; solve for type variables Xs
    [#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)]
    ;; instantiate polymorphic function type
@@ -894,7 +894,7 @@
                               stx)))
                          #'(∀ (unsolved-X ... Y ...) τ_out)]))]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ (: τ_out*)]]])
+   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out*]]])
 
 
 ;; cond and other conditionals
@@ -902,32 +902,32 @@
   [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
                test)
           b ... body] ...+)
-   ⇐ (: τ_expected) ▶
+   ⇐ : τ_expected ▶
    [#:with [[Bool* τ_expected* _] ...] #'[[Bool τ_expected test] ...]]
-   [⊢ [[test ≫ test-] ⇐ (: Bool*)] ...]
-   [⊢ [[(begin b ... body) ≫ body-] ⇐ (: τ_expected*)] ...]
+   [⊢ [[test ≫ test-] ⇐ : Bool*] ...]
+   [⊢ [[(begin b ... body) ≫ body-] ⇐ : τ_expected*] ...]
    --------
-   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇐ : _]]]
   [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
                test)
           b ... body] ...+) ▶
    [#:with [[Bool* _] ...] #'[[Bool test] ...]]
-   [⊢ [[test ≫ test-] ⇐ (: Bool*)] ...]
-   [⊢ [[(begin b ... body) ≫ body-] ⇒ (: τ_body)] ...]
+   [⊢ [[test ≫ test-] ⇐ : Bool*] ...]
+   [⊢ [[(begin b ... body) ≫ body-] ⇒ : τ_body] ...]
    --------
-   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇒ (: (⊔ τ_body ...))]]])
+   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇒ : (⊔ τ_body ...)]]])
 (define-typed-syntax when
   [(when test body ...) ▶
-   [⊢ [[test ≫ test-] ⇒ (: _)]]
-   [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+   [⊢ [[test ≫ test-] ⇒ : _]]
+   [⊢ [[body ≫ body-] ⇒ : _] ...]
    --------
-   [⊢ [[_ ≫ (when- test- body- ... (void-))] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (when- test- body- ... (void-))] ⇒ : Unit]]])
 (define-typed-syntax unless
   [(unless test body ...) ▶
-   [⊢ [[test ≫ test-] ⇒ (: _)]]
-   [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+   [⊢ [[test ≫ test-] ⇒ : _]]
+   [⊢ [[body ≫ body-] ⇒ : _] ...]
    --------
-   [⊢ [[_ ≫ (unless- test- body- ... (void-))] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (unless- test- body- ... (void-))] ⇒ : Unit]]])
 
 ;; sync channels and threads
 (define-type-constructor Channel)
@@ -936,31 +936,31 @@
   [(make-channel (~and tys {ty})) ▶
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (make-channel-)] ⇒ (: (Channel ty))]]])
+   [⊢ [[_ ≫ (make-channel-)] ⇒ : (Channel ty)]]])
 (define-typed-syntax channel-get
-  [(channel-get c) ⇐ (: ty) ▶
-   [⊢ [[c ≫ c-] ⇐ (: (Channel ty))]]
+  [(channel-get c) ⇐ : ty ▶
+   [⊢ [[c ≫ c-] ⇐ : (Channel ty)]]
    --------
-   [⊢ [[_ ≫ (channel-get- c-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (channel-get- c-)] ⇐ : _]]]
   [(channel-get c) ▶
-   [⊢ [[c ≫ c-] ⇒ (: (~Channel ty))]]
+   [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
    --------
-   [⊢ [[_ ≫ (channel-get- c-)] ⇒ (: ty)]]])
+   [⊢ [[_ ≫ (channel-get- c-)] ⇒ : ty]]])
 (define-typed-syntax channel-put
   [(channel-put c v) ▶
-   [⊢ [[c ≫ c-] ⇒ (: (~Channel ty))]]
-   [⊢ [[v ≫ v-] ⇐ (: ty)]]
+   [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
+   [⊢ [[v ≫ v-] ⇐ : ty]]
    --------
-   [⊢ [[_ ≫ (channel-put- c- v-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (channel-put- c- v-)] ⇒ : Unit]]])
 
 (define-base-type Thread)
 
 ;; threads
 (define-typed-syntax thread
   [(thread th) ▶
-   [⊢ [[th ≫ th-] ⇒ (: (~?∀ () (~ext-stlc:→ τ_out)))]]
+   [⊢ [[th ≫ th-] ⇒ : (~?∀ () (~ext-stlc:→ τ_out))]]
    --------
-   [⊢ [[_ ≫ (thread- th-)] ⇒ (: Thread)]]])
+   [⊢ [[_ ≫ (thread- th-)] ⇒ : Thread]]])
 
 (define-primop random : (→ Int Int))
 (define-primop integer->char : (→ Int Char))
@@ -970,15 +970,15 @@
 (define-typed-syntax number->string
   [number->string:id ▶
    --------
-   [⊢ [[_ ≫ number->string-] ⇒ (: (→ Int String))]]]
+   [⊢ [[_ ≫ number->string-] ⇒ : (→ Int String)]]]
   [(number->string n) ▶
    --------
    [_ ≻ (number->string n (ext-stlc:#%datum . 10))]]
   [(number->string n rad) ▶
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
-   [⊢ [[rad ≫ rad-] ⇐ (: Int)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [[rad ≫ rad-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (number->string- n rad)] ⇒ (: String)]]])
+   [⊢ [[_ ≫ (number->string- n rad)] ⇒ : String]]])
 (define-primop string : (→ Char String))
 (define-primop sleep : (→ Int Unit))
 (define-primop string=? : (→ String String Bool))
@@ -987,9 +987,9 @@
 (define-typed-syntax string-append
   [(string-append str ...) ▶
    [#:with [[String* _] ...] #'[[String str] ...]]
-   [⊢ [[str ≫ str-] ⇐ (: String*)] ...]
+   [⊢ [[str ≫ str-] ⇐ : String*] ...]
    --------
-   [⊢ [[_ ≫ (string-append- str- ...)] ⇒ (: String)]]])
+   [⊢ [[_ ≫ (string-append- str- ...)] ⇒ : String]]])
 
 ;; vectors
 (define-type-constructor Vector)
@@ -998,57 +998,57 @@
   [(vector (~and tys {ty})) ▶
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (vector-)] ⇒ (: (Vector ty))]]]
-  [(vector v ...) ⇐ (: (Vector ty)) ▶
+   [⊢ [[_ ≫ (vector-)] ⇒ : (Vector ty)]]]
+  [(vector v ...) ⇐ : (Vector ty) ▶
    [#:with [[ty* _] ...] #'[[ty v] ...]]
-   [⊢ [[v ≫ v-] ⇐ (: ty*)] ...]
+   [⊢ [[v ≫ v-] ⇐ : ty*] ...]
    --------
-   [⊢ [[_ ≫ (vector- v- ...)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (vector- v- ...)] ⇐ : _]]]
   [(vector v ...) ▶
-   [⊢ [[v ≫ v-] ⇒ (: ty)] ...]
+   [⊢ [[v ≫ v-] ⇒ : ty] ...]
    [#:when (same-types? #'(ty ...))]
    [#:with one-ty (stx-car #'(ty ...))]
    --------
-   [⊢ [[_ ≫ (vector- v- ...)] ⇒ (: (Vector one-ty))]]])
+   [⊢ [[_ ≫ (vector- v- ...)] ⇒ : (Vector one-ty)]]])
 (define-typed-syntax make-vector
   [(make-vector n) ▶
    --------
    [_ ≻ (make-vector n (ext-stlc:#%datum . 0))]]
   [(make-vector n e) ▶
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
-   [⊢ [[e ≫ e-] ⇒ (: ty)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [[e ≫ e-] ⇒ : ty]]
    --------
-   [⊢ [[_ ≫ (make-vector- n- e-)] ⇒ (: (Vector ty))]]])
+   [⊢ [[_ ≫ (make-vector- n- e-)] ⇒ : (Vector ty)]]])
 (define-typed-syntax vector-length
   [(vector-length e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Vector _))]]
+   [⊢ [[e ≫ e-] ⇒ : (~Vector _)]]
    --------
-   [⊢ [[_ ≫ (vector-length- e-)] ⇒ (: Int)]]])
+   [⊢ [[_ ≫ (vector-length- e-)] ⇒ : Int]]])
 (define-typed-syntax vector-ref
-  [(vector-ref e n) ⇐ (: ty) ▶
-   [⊢ [[e ≫ e-] ⇐ (: (Vector ty))]]
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
+  [(vector-ref e n) ⇐ : ty ▶
+   [⊢ [[e ≫ e-] ⇐ : (Vector ty)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇐ : _]]]
   [(vector-ref e n) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇒ (: ty)]]])
+   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇒ : ty]]])
 (define-typed-syntax vector-set!
   [(vector-set! e n v) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
-   [⊢ [[v ≫ v-] ⇐ (: ty)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [[v ≫ v-] ⇐ : ty]]
    --------
-   [⊢ [[_ ≫ (vector-set!- e- n- v-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (vector-set!- e- n- v-)] ⇒ : Unit]]])
 (define-typed-syntax vector-copy!
   [(vector-copy! dest start src) ▶
-   [⊢ [[dest ≫ dest-] ⇒ (: (~Vector ty))]]
-   [⊢ [[start ≫ start-] ⇐ (: Int)]]
-   [⊢ [[src ≫ src-] ⇐ (: (Vector ty))]]
+   [⊢ [[dest ≫ dest-] ⇒ : (~Vector ty)]]
+   [⊢ [[start ≫ start-] ⇐ : Int]]
+   [⊢ [[src ≫ src-] ⇐ : (Vector ty)]]
    --------
-   [⊢ [[_ ≫ (vector-copy!- dest- start- src-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (vector-copy!- dest- start- src-)] ⇒ : Unit]]])
 
 
 ;; sequences and for loops
@@ -1063,159 +1063,159 @@
    --------
    [_ ≻ (in-range start end (ext-stlc:#%datum . 1))]]
   [(in-range start end step) ▶
-   [⊢ [[start ≫ start-] ⇐ (: Int)]]
-   [⊢ [[end ≫ end-] ⇐ (: Int)]]
-   [⊢ [[step ≫ step-] ⇐ (: Int)]]
+   [⊢ [[start ≫ start-] ⇐ : Int]]
+   [⊢ [[end ≫ end-] ⇐ : Int]]
+   [⊢ [[step ≫ step-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (in-range- start- end- step-)] ⇒ (: (Sequence Int))]]])
+   [⊢ [[_ ≫ (in-range- start- end- step-)] ⇒ : (Sequence Int)]]])
 
 (define-typed-syntax in-naturals
  [(in-naturals) ▶
   --------
   [_ ≻ (in-naturals (ext-stlc:#%datum . 0))]]
  [(in-naturals start) ▶
-  [⊢ [[start ≫ start-] ⇐ (: Int)]]
+  [⊢ [[start ≫ start-] ⇐ : Int]]
   --------
-  [⊢ [[_ ≫ (in-naturals- start-)] ⇒ (: (Sequence Int))]]])
+  [⊢ [[_ ≫ (in-naturals- start-)] ⇒ : (Sequence Int)]]])
 
 
 (define-typed-syntax in-vector
   [(in-vector e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
+   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
    --------
-   [⊢ [[_ ≫ (in-vector- e-)] ⇒ (: (Sequence ty))]]])
+   [⊢ [[_ ≫ (in-vector- e-)] ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-list
   [(in-list e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List ty))]]
+   [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
    --------
-   [⊢ [[_ ≫ (in-list- e-)] ⇒ (: (Sequence ty))]]])
+   [⊢ [[_ ≫ (in-list- e-)] ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-lines
   [(in-lines e) ▶
-   [⊢ [[e ≫ e-] ⇐ (: String)]]
+   [⊢ [[e ≫ e-] ⇐ : String]]
    --------
-   [⊢ [[_ ≫ (in-lines- (open-input-string- e-))] ⇒ (: (Sequence String))]]])
+   [⊢ [[_ ≫ (in-lines- (open-input-string- e-))] ⇒ : (Sequence String)]]])
 
 (define-typed-syntax for
   [(for ([x:id e]...) b ... body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇒ (: _)]]
+    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (for- ([x- e-] ...) b- ... body-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (for- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
 (define-typed-syntax for*
   [(for* ([x:id e]...) b ... body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇒ (: _)]]
+    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (for*- ([x- e-] ...) b- ... body-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (for*- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
 
 (define-typed-syntax for/list
   [(for/list ([x:id e]...) body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
+   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for/list- ([x- e-] ...) body-)] ⇒ (: (List ty_body))]]])
+   [⊢ [[_ ≫ (for/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
 (define-typed-syntax for/vector
   [(for/vector ([x:id e]...) body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
+   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for/vector- ([x- e-] ...) body-)] ⇒ (: (Vector ty_body))]]])
+   [⊢ [[_ ≫ (for/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/vector
   [(for*/vector ([x:id e]...) body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
+   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for*/vector- ([x- e-] ...) body-)] ⇒ (: (Vector ty_body))]]])
+   [⊢ [[_ ≫ (for*/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/list
   [(for*/list ([x:id e]...) body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
+   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for*/list- ([x- e-] ...) body-)] ⇒ (: (List ty_body))]]])
+   [⊢ [[_ ≫ (for*/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
 (define-typed-syntax for/fold
-  [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ (: τ_expected) ▶
-   [⊢ [[init ≫ init-] ⇐ (: τ_expected)]]
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+  [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ : τ_expected ▶
+   [⊢ [[init ≫ init-] ⇐ : τ_expected]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([acc : τ_expected ≫ acc-] [x : ty ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ (: τ_expected)]]
+    ⊢ [[body ≫ body-] ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇐ : _]]]
   [(for/fold ([acc init]) ([x:id e] ...) body) ▶
-   [⊢ [[init ≫ init-] ⇒ (: τ_init)]]
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+   [⊢ [[init ≫ init-] ⇒ : τ_init]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([acc : τ_init ≫ acc-] [x : ty ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ (: τ_init)]]
+    ⊢ [[body ≫ body-] ⇐ : τ_init]]
    --------
-   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇒ (: τ_init)]]])
+   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇒ : τ_init]]])
 
 (define-typed-syntax for/hash
   [(for/hash ([x:id e]...) body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: (~× ty_k ty_v))]]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
+   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : (~× ty_k ty_v)]]
    --------
    [⊢ [[_ ≫ (for/hash- ([x- e-] ...)
               (let- ([t body-])
                 (values- (car- t) (cadr- t))))]
-       ⇒ (: (Hash ty_k ty_v))]]])
+       ⇒ : (Hash ty_k ty_v)]]])
 
 (define-typed-syntax for/sum
   [(for/sum ([x:id e]... 
              (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
      body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
-    ⊢ [[guard ≫ guard-] ⇒ (: _)] [[body ≫ body-] ⇐ (: Int)]]
+    ⊢ [[guard ≫ guard-] ⇒ : _] [[body ≫ body-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (for/sum- ([x- e-] ... #:when guard-) body-)] ⇒ (: Int)]]])
+   [⊢ [[_ ≫ (for/sum- ([x- e-] ... #:when guard-) body-)] ⇒ : Int]]])
 
 ; printing and displaying
 (define-typed-syntax printf
   [(printf str e ...) ▶
-   [⊢ [[str ≫ s-] ⇐ (: String)]]
-   [⊢ [[e ≫ e-] ⇒ (: ty)] ...]
+   [⊢ [[str ≫ s-] ⇐ : String]]
+   [⊢ [[e ≫ e-] ⇒ : ty] ...]
    --------
-   [⊢ [[_ ≫ (printf- s- e- ...)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (printf- s- e- ...)] ⇒ : Unit]]])
 (define-typed-syntax format
   [(format str e ...) ▶
-   [⊢ [[str ≫ s-] ⇐ (: String)]]
-   [⊢ [[e ≫ e-] ⇒ (: ty)] ...]
+   [⊢ [[str ≫ s-] ⇐ : String]]
+   [⊢ [[e ≫ e-] ⇒ : ty] ...]
    --------
-   [⊢ [[_ ≫ (format- s- e- ...)] ⇒ (: String)]]])
+   [⊢ [[_ ≫ (format- s- e- ...)] ⇒ : String]]])
 (define-typed-syntax display
   [(display e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: _)]]
+   [⊢ [[e ≫ e-] ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (display- e-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (display- e-)] ⇒ : Unit]]])
 (define-typed-syntax displayln
   [(displayln e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: _)]]
+   [⊢ [[e ≫ e-] ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (displayln- e-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (displayln- e-)] ⇒ : Unit]]])
 (define-primop newline : (→ Unit))
 
 (define-typed-syntax list->vector
-  [(list->vector e) ⇐ (: (~Vector ty)) ▶
-   [⊢ [[e ≫ e-] ⇐ (: (List ty))]]
+  [(list->vector e) ⇐ : (~Vector ty) ▶
+   [⊢ [[e ≫ e-] ⇐ : (List ty)]]
    --------
-   [⊢ [[_ ≫ (list->vector- e-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (list->vector- e-)] ⇐ : _]]]
   [(list->vector e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List ty))]]
+   [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
    --------
-   [⊢ [[_ ≫ (list->vector- e-)] ⇒ (: (Vector ty))]]])
+   [⊢ [[_ ≫ (list->vector- e-)] ⇒ : (Vector ty)]]])
 
 (define-typed-syntax let
   [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ▶
-   [⊢ [[e ≫ e-] ⇒ (: ty_e)] ...]
+   [⊢ [[e ≫ e-] ⇒ : ty_e] ...]
    [() ([name : (→ ty_e ... ty.norm) ≫ name-] [x : ty_e ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇐ (: ty.norm)]]
+    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇐ : ty.norm]]
    --------
    [⊢ [[_ ≫ (letrec- ([name- (λ- xs- b- ... body-)])
               (name- e- ...))]
-       ⇒ (: ty_body)]]]
+       ⇒ : ty_body]]]
   [(let ([x:id e] ...) body ...) ▶
    --------
    [_ ≻ (ext-stlc:let ([x e] ...) (begin body ...))]])
@@ -1225,72 +1225,72 @@
    [_ ≻ (ext-stlc:let* ([x e] ...) (begin body ...))]])
 
 (define-typed-syntax begin
-  [(begin body ... b) ⇐ (: τ_expected) ▶
-   [⊢ [[body ≫ body-] ⇒ (: _)] ...]
-   [⊢ [[b ≫ b-] ⇐ (: τ_expected)]]
+  [(begin body ... b) ⇐ : τ_expected ▶
+   [⊢ [[body ≫ body-] ⇒ : _] ...]
+   [⊢ [[b ≫ b-] ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (begin- body- ... b-)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (begin- body- ... b-)] ⇐ : _]]]
   [(begin body ... b) ▶
-   [⊢ [[body ≫ body-] ⇒ (: _)] ...]
-   [⊢ [[b ≫ b-] ⇒ (: τ)]]
+   [⊢ [[body ≫ body-] ⇒ : _] ...]
+   [⊢ [[b ≫ b-] ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ (begin- body- ... b-)] ⇒ (: τ)]]])
+   [⊢ [[_ ≫ (begin- body- ... b-)] ⇒ : τ]]])
 
 ;; hash
 (define-type-constructor Hash #:arity = 2)
 
 (define-typed-syntax in-hash
   [(in-hash e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Hash ty_k ty_v))]]
+   [⊢ [[e ≫ e-] ⇒ : (~Hash ty_k ty_v)]]
    --------
-   [⊢ [[_ ≫ (hash-map- e- list-)] ⇒ (: (Sequence (stlc+rec-iso:× ty_k ty_v)))]]])
+   [⊢ [[_ ≫ (hash-map- e- list-)] ⇒ : (Sequence (stlc+rec-iso:× ty_k ty_v))]]])
 
 ; mutable hashes
 (define-typed-syntax hash
   [(hash (~and tys {ty_key ty_val})) ▶
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (make-hash-)] ⇒ (: (Hash ty_key ty_val))]]]
+   [⊢ [[_ ≫ (make-hash-)] ⇒ : (Hash ty_key ty_val)]]]
   [(hash (~seq k v) ...) ▶
-   [⊢ [[k ≫ k-] ⇒ (: ty_k)] ...]
-   [⊢ [[v ≫ v-] ⇒ (: ty_v)] ...]
+   [⊢ [[k ≫ k-] ⇒ : ty_k] ...]
+   [⊢ [[v ≫ v-] ⇒ : ty_v] ...]
    [#:when (same-types? #'(ty_k ...))]
    [#:when (same-types? #'(ty_v ...))]
    [#:with ty_key (stx-car #'(ty_k ...))]
    [#:with ty_val (stx-car #'(ty_v ...))]
    --------
-   [⊢ [[_ ≫ (make-hash- (list- (cons- k- v-) ...))] ⇒ (: (Hash ty_key ty_val))]]])
+   [⊢ [[_ ≫ (make-hash- (list- (cons- k- v-) ...))] ⇒ : (Hash ty_key ty_val)]]])
 (define-typed-syntax hash-set!
   [(hash-set! h k v) ▶
-   [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
-   [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
-   [⊢ [[v ≫ v-] ⇐ (: ty_v)]]
+   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [[k ≫ k-] ⇐ : ty_k]]
+   [⊢ [[v ≫ v-] ⇐ : ty_v]]
    --------
-   [⊢ [[_ ≫ (hash-set!- h- k- v-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (hash-set!- h- k- v-)] ⇒ : Unit]]])
 (define-typed-syntax hash-ref
   [(hash-ref h k) ▶
-   [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
-   [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [[k ≫ k-] ⇐ : ty_k]]
    --------
-   [⊢ [[_ ≫ (hash-ref- h- k-)] ⇒ (: ty_v)]]]
+   [⊢ [[_ ≫ (hash-ref- h- k-)] ⇒ : ty_v]]]
   [(hash-ref h k fail) ▶
-   [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
-   [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
-   [⊢ [[fail ≫ fail-] ⇐ (: (→ ty_v))]]
+   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [[k ≫ k-] ⇐ : ty_k]]
+   [⊢ [[fail ≫ fail-] ⇐ : (→ ty_v)]]
    --------
-   [⊢ [[_ ≫ (hash-ref- h- k- fail-)] ⇒ (: ty_val)]]])
+   [⊢ [[_ ≫ (hash-ref- h- k- fail-)] ⇒ : ty_val]]])
 (define-typed-syntax hash-has-key?
   [(hash-has-key? h k) ▶
-   [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k _))]]
-   [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k _)]]
+   [⊢ [[k ≫ k-] ⇐ : ty_k]]
    --------
-   [⊢ [[_ ≫ (hash-has-key?- h- k-)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (hash-has-key?- h- k-)] ⇒ : Bool]]])
 
 (define-typed-syntax hash-count
   [(hash-count h) ▶
-   [⊢ [[h ≫ h-] ⇒ (: (~Hash _ _))]]
+   [⊢ [[h ≫ h-] ⇒ : (~Hash _ _)]]
    --------
-   [⊢ [[_ ≫ (hash-count- h-)] ⇒ (: Int)]]])
+   [⊢ [[_ ≫ (hash-count- h-)] ⇒ : Int]]])
 
 (define-base-type String-Port)
 (define-base-type Input-Port)
@@ -1303,18 +1303,18 @@
   --------
   [_ ≻ (write-string str out (ext-stlc:#%datum . 0) (string-length/tc str))]]
  [(write-string str out start end) ▶
-  [⊢ [[str ≫ str-] ⇐ (: String)]]
-  [⊢ [[out ≫ out-] ⇐ (: String-Port)]]
-  [⊢ [[start ≫ start-] ⇐ (: Int)]]
-  [⊢ [[end ≫ end-] ⇐ (: Int)]]
+  [⊢ [[str ≫ str-] ⇐ : String]]
+  [⊢ [[out ≫ out-] ⇐ : String-Port]]
+  [⊢ [[start ≫ start-] ⇐ : Int]]
+  [⊢ [[end ≫ end-] ⇐ : Int]]
   --------
-  [⊢ [[_ ≫ (begin- (write-string- str- out- start- end-) (void-))] ⇒ (: Unit)]]])
+  [⊢ [[_ ≫ (begin- (write-string- str- out- start- end-) (void-))] ⇒ : Unit]]])
 
 (define-typed-syntax string-length
  [(string-length str) ▶
-  [⊢ [[str ≫ str-] ⇐ (: String)]]
+  [⊢ [[str ≫ str-] ⇐ : String]]
   --------
-  [⊢ [[_ ≫ (string-length- str-)] ⇒ (: Int)]]])
+  [⊢ [[_ ≫ (string-length- str-)] ⇒ : Int]]])
 (define-primop make-string : (→ Int String))
 (define-primop string-set! : (→ String Int Char Unit))
 (define-primop string-ref : (→ String Int Char))
@@ -1324,13 +1324,13 @@
    [_ ≻ (string-copy!
          dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]]
   [(string-copy! dest dest-start src src-start src-end) ▶
-   [⊢ [[dest ≫ dest-] ⇐ (: String)]]
-   [⊢ [[src ≫ src-] ⇐ (: String)]]
-   [⊢ [[dest-start ≫ dest-start-] ⇐ (: Int)]]
-   [⊢ [[src-start ≫ src-start-] ⇐ (: Int)]]
-   [⊢ [[src-end ≫ src-end-] ⇐ (: Int)]]
+   [⊢ [[dest ≫ dest-] ⇐ : String]]
+   [⊢ [[src ≫ src-] ⇐ : String]]
+   [⊢ [[dest-start ≫ dest-start-] ⇐ : Int]]
+   [⊢ [[src-start ≫ src-start-] ⇐ : Int]]
+   [⊢ [[src-end ≫ src-end-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-)] ⇒ : Unit]]])
 
 (define-primop fl+ : (→ Float Float Float))
 (define-primop fl- : (→ Float Float Float))
@@ -1345,20 +1345,20 @@
 (define-primop fx->fl : (→ Int Float))
 (define-typed-syntax quotient+remainder
   [(quotient+remainder x y) ▶
-   [⊢ [[x ≫ x-] ⇐ (: Int)]]
-   [⊢ [[y ≫ y-] ⇐ (: Int)]]
+   [⊢ [[x ≫ x-] ⇐ : Int]]
+   [⊢ [[y ≫ y-] ⇐ : Int]]
    --------
    [⊢ [[_ ≫ (let-values- ([[a b] (quotient/remainder- x- y-)])
               (list- a b))]
-       ⇒ (: (stlc+rec-iso:× Int Int))]]])
+       ⇒ : (stlc+rec-iso:× Int Int)]]])
 (define-primop quotient : (→ Int Int Int))
 
 (define-typed-syntax set!
   [(set! x:id e) ▶
-   [⊢ [[x ≫ x-] ⇒ (: ty_x)]]
-   [⊢ [[e ≫ e-] ⇐ (: ty_x)]]
+   [⊢ [[x ≫ x-] ⇒ : ty_x]]
+   [⊢ [[e ≫ e-] ⇐ : ty_x]]
    --------
-   [⊢ [[_ ≫ (set!- x e-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (set!- x e-)] ⇒ : Unit]]])
 
 (define-typed-syntax provide-type
   [(provide-type ty ...) ▶
@@ -1367,7 +1367,7 @@
 
 (define-typed-syntax provide
   [(provide x:id ...) ▶
-   [⊢ [[x ≫ x-] ⇒ (: ty_x)] ...]
+   [⊢ [[x ≫ x-] ⇒ : ty_x] ...]
    ; TODO: use hash-code to generate this tmp
    [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
    --------
@@ -1390,10 +1390,10 @@
 
 (define-typed-syntax equal?
   [(equal? e1 e2) ▶
-   [⊢ [[e1 ≫ e1-] ⇒ (: ty1)]]
-   [⊢ [[e2 ≫ e2-] ⇐ (: ty1)]]
+   [⊢ [[e1 ≫ e1-] ⇒ : ty1]]
+   [⊢ [[e2 ≫ e2-] ⇐ : ty1]]
    --------
-   [⊢ [[_ ≫ (equal?- e1- e2-)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (equal?- e1- e2-)] ⇒ : Bool]]])
 
 (define-typed-syntax read-int
   [(read-int) ▶
@@ -1401,7 +1401,7 @@
    [⊢ [[_ ≫ (let- ([x (read-)])
               (cond- [(exact-integer?- x) x]
                      [else (error- 'read-int "expected an int, given: ~v" x)]))]
-       ⇒ (: Int)]]])
+       ⇒ : Int]]])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
diff --git a/tapl/typed-lang-builder/stlc+box.rkt b/tapl/typed-lang-builder/stlc+box.rkt
index c87e120..e3a9d24 100644
--- a/tapl/typed-lang-builder/stlc+box.rkt
+++ b/tapl/typed-lang-builder/stlc+box.rkt
@@ -13,20 +13,20 @@
 
 (define-typed-syntax ref
   [(ref e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ)]]
+   [⊢ [[e ≫ e-] ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ (box- e-)] ⇒ (: (Ref τ))]]])
+   [⊢ [[_ ≫ (box- e-)] ⇒ : (Ref τ)]]])
 
 (define-typed-syntax deref
   [(deref e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Ref τ))]]
+   [⊢ [[e ≫ e-] ⇒ : (~Ref τ)]]
    --------
-   [⊢ [[_ ≫ (unbox- e-)] ⇒ (: τ)]]])
+   [⊢ [[_ ≫ (unbox- e-)] ⇒ : τ]]])
 
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e) ▶
-   [⊢ [[e_ref ≫ e_ref-] ⇒ (: (~Ref τ))]]
-   [⊢ [[e ≫ e-] ⇐ (: τ)]]
+   [⊢ [[e_ref ≫ e_ref-] ⇒ : (~Ref τ)]]
+   [⊢ [[e ≫ e-] ⇐ : τ]]
    --------
-   [⊢ [[_ ≫ (set-box!- e_ref- e-)] ⇒ (: Unit)]]])
+   [⊢ [[_ ≫ (set-box!- e_ref- e-)] ⇒ : Unit]]])
 
diff --git a/tapl/typed-lang-builder/stlc+cons.rkt b/tapl/typed-lang-builder/stlc+cons.rkt
index 5c6fa0f..65a52c5 100644
--- a/tapl/typed-lang-builder/stlc+cons.rkt
+++ b/tapl/typed-lang-builder/stlc+cons.rkt
@@ -15,67 +15,67 @@
 (define-typed-syntax nil
   [(nil ~! τi:type-ann) ▶
    --------
-   [⊢ [[_ ≫ null-] ⇒ (: (List τi.norm))]]]
+   [⊢ [[_ ≫ null-] ⇒ : (List τi.norm)]]]
   ; minimal type inference
-  [nil:id ⇐ (: (~List τ)) ▶
+  [nil:id ⇐ : (~List τ) ▶
    --------
-   [⊢ [[_ ≫ null-] ⇐ (: _)]]])
+   [⊢ [[_ ≫ null-] ⇐ : _]]])
 (define-typed-syntax cons
   [(cons e1 e2) ▶
-   [⊢ [[e1 ≫ e1-] ⇒ (: τ1)]]
-   [⊢ [[e2 ≫ e2-] ⇐ (: (List τ1))]]
+   [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
+   [⊢ [[e2 ≫ e2-] ⇐ : (List τ1)]]
    --------
-   [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ (: (List τ1))]]])
+   [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ : (List τ1)]]])
 (define-typed-syntax isnil
   [(isnil e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List _))]]
+   [⊢ [[e ≫ e-] ⇒ : (~List _)]]
    --------
-   [⊢ [[_ ≫ (null?- e-)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (null?- e-)] ⇒ : Bool]]])
 (define-typed-syntax head
   [(head e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
+   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
    --------
-   [⊢ [[_ ≫ (car- e-)] ⇒ (: τ)]]])
+   [⊢ [[_ ≫ (car- e-)] ⇒ : τ]]])
 (define-typed-syntax tail
   [(tail e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (cdr- e-)] ⇒ (: τ-lst)]]])
+   [⊢ [[_ ≫ (cdr- e-)] ⇒ : τ-lst]]])
 (define-typed-syntax list
   [(list) ▶
    --------
    [_ ≻ nil]]
-  [(list x . rst) ⇐ (: (~List τ)) ▶ ; has expected type
+  [(list x . rst) ⇐ : (~List τ) ▶ ; has expected type
    --------
-   [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ : _]]]
   [(list x . rst) ▶ ; no expected type
    --------
    [_ ≻ (cons x (list . rst))]])
 (define-typed-syntax reverse
   [(reverse e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (reverse- e-)] ⇒ (: τ-lst)]]])
+   [⊢ [[_ ≫ (reverse- e-)] ⇒ : τ-lst]]])
 (define-typed-syntax length
   [(length e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (length- e-)] ⇒ (: Int)]]])
+   [⊢ [[_ ≫ (length- e-)] ⇒ : Int]]])
 (define-typed-syntax list-ref
   [(list-ref e n) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
-   [⊢ [[n ≫ n-] ⇐ (: Int)]]
+   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
+   [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ (: τ)]]])
+   [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ : τ]]])
 (define-typed-syntax member
   [(member v e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
-   [⊢ [[v ≫ v-] ⇐ (: τ)]]
+   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
+   [⊢ [[v ≫ v-] ⇐ : τ]]
    --------
-   [⊢ [[_ ≫ (member- v- e-)] ⇒ (: Bool)]]])
+   [⊢ [[_ ≫ (member- v- e-)] ⇒ : Bool]]])
diff --git a/tapl/typed-lang-builder/stlc+effect.rkt b/tapl/typed-lang-builder/stlc+effect.rkt
index 15d18b3..9fd715f 100644
--- a/tapl/typed-lang-builder/stlc+effect.rkt
+++ b/tapl/typed-lang-builder/stlc+effect.rkt
@@ -58,28 +58,41 @@
 (define-typed-syntax effect:#%app #:export-as #%app
   [(_ efn e ...) ▶
    [⊢ [[efn ≫ e_fn-]
-       ⇒ (: ty_fn ν (~locs fns ...) := (~locs fas ...) ! (~locs fds ...))
-       ⇒ (ν (~locs tyns ...) := (~locs tyas ...) ! (~locs tyds ...))]]
+       (⇒ : ty_fn
+          (⇒ ν (~locs tyns ...))
+          (⇒ := (~locs tyas ...))
+          (⇒ ! (~locs tyds ...)))
+       (⇒ ν (~locs fns ...))
+       (⇒ := (~locs fas ...))
+       (⇒ ! (~locs fds ...))]]
    [#:with (~→ τ_in ... τ_out) #'ty_fn]
-   [⊢ [[e ≫ e_arg-] ⇒ (: τ_arg ν (~locs ns ...) := (~locs as ...) ! (~locs ds ...))] ...]
+   [⊢ [[e ≫ e_arg-]
+       (⇒ : τ_arg)
+       (⇒ ν (~locs ns ...))
+       (⇒ := (~locs as ...))
+       (⇒ ! (~locs ds ...))]
+      ...]
    [#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
     "wrong number of arguments"]
    [τ_arg τ⊑ τ_in] ...
    --------
    [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)]
-       ⇒ (: τ_out
-            ν (locs fns ... tyns ... ns ... ...)
-            := (locs fas ... tyas ... as ... ...)
-            ! (locs fds ... tyds ... ds ... ...))]]])
+       (⇒ : τ_out)
+       (⇒ ν (locs fns ... tyns ... ns ... ...))
+       (⇒ := (locs fas ... tyas ... as ... ...))
+       (⇒ ! (locs fds ... tyds ... ds ... ...))]]])
 
 (define-typed-syntax λ
   [(λ bvs:type-ctx e) ▶
    [() ([bvs.x : bvs.type ≫ x-] ...) ⊢
        [[e ≫ e-]
-        ⇒ (: τ_res ν (~locs ns ...) := (~locs as ...) ! (~locs ds ...))]]
+        (⇒ : τ_res)
+        (⇒ ν (~locs ns ...))
+        (⇒ := (~locs as ...))
+        (⇒ ! (~locs ds ...))]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) e-)]
-       ⇒ (: #,(add-effects #'(→ bvs.type ... τ_res)
+       (⇒ : #,(add-effects #'(→ bvs.type ... τ_res)
                            #'(locs ns ...)
                            #'(locs as ...)
                            #'(locs ds ...)))]]])
@@ -88,31 +101,47 @@
 
 (define-typed-syntax ref
   [(ref e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ ν (~locs ns ...) := (~locs as ...) ! (~locs ds ...))]]
+   [⊢ [[e ≫ e-]
+       (⇒ : τ)
+       (⇒ ν (~locs ns ...))
+       (⇒ := (~locs as ...))
+       (⇒ ! (~locs ds ...))]]
    --------
    [⊢ [[_ ≫ (box- e-)]
-       ⇒ (: (Ref τ)
-            ν (locs #,(syntax-position stx) ns ...)
-            := (locs as ...)
-            ! (locs ds ...))]]])
+       (⇒ : (Ref τ))
+       (⇒ ν (locs #,(syntax-position stx) ns ...))
+       (⇒ := (locs as ...))
+       (⇒ ! (locs ds ...))]]])
 (define-typed-syntax deref
   [(deref e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~Ref ty) ν (~locs ns ...) := (~locs as ...) ! (~locs ds ...))]]
+   [⊢ [[e ≫ e-]
+       (⇒ : (~Ref ty))
+       (⇒ ν (~locs ns ...))
+       (⇒ := (~locs as ...))
+       (⇒ ! (~locs ds ...))]]
    --------
    [⊢ [[_ ≫ (unbox- e-)]
-       ⇒ (: ty
-            ν (locs ns ...)
-            := (locs as ...)
-            ! (locs #,(syntax-position stx) ds ...))]]])
+       (⇒ : ty)
+       (⇒ ν (locs ns ...))
+       (⇒ := (locs as ...))
+       (⇒ ! (locs #,(syntax-position stx) ds ...))]]])
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e) ▶
-   [⊢ [[e_ref ≫ e_ref-] ⇒ (: (~Ref ty1) ν (~locs ns1 ...) := (~locs as1 ...) ! (~locs ds1 ...))]]
-   [⊢ [[e ≫ e-] ⇒ (: ty2 ν (~locs ns2 ...) := (~locs as2 ...) ! (~locs ds2 ...))]]
+   [⊢ [[e_ref ≫ e_ref-]
+       (⇒ : (~Ref ty1))
+       (⇒ ν (~locs ns1 ...))
+       (⇒ := (~locs as1 ...))
+       (⇒ ! (~locs ds1 ...))]]
+   [⊢ [[e ≫ e-]
+       (⇒ : ty2)
+       (⇒ ν (~locs ns2 ...))
+       (⇒ := (~locs as2 ...))
+       (⇒ ! (~locs ds2 ...))]]
    [ty1 τ⊑ ty2]
    --------
    [⊢ [[_ ≫ (set-box!- e_ref- e-)]
-       ⇒ (: Unit
-            ν (locs ns1 ... ns2 ...)
-            := (locs #,(syntax-position stx) as1 ... as2 ...)
-            ! (locs ds1 ... ds2 ...))]]])
+       (⇒ : Unit)
+       (⇒ ν (locs ns1 ... ns2 ...))
+       (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...))
+       (⇒ ! (locs ds1 ... ds2 ...))]]])
 
diff --git a/tapl/typed-lang-builder/stlc+lit.rkt b/tapl/typed-lang-builder/stlc+lit.rkt
index d5d92b7..15fc420 100644
--- a/tapl/typed-lang-builder/stlc+lit.rkt
+++ b/tapl/typed-lang-builder/stlc+lit.rkt
@@ -34,7 +34,7 @@
 (define-typed-syntax #%datum
   [(#%datum . n:integer) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Int)]]]
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
   [(_ . x) ▶
    --------
    [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
diff --git a/tapl/typed-lang-builder/stlc+rec-iso.rkt b/tapl/typed-lang-builder/stlc+rec-iso.rkt
index e887097..c0ebad5 100644
--- a/tapl/typed-lang-builder/stlc+rec-iso.rkt
+++ b/tapl/typed-lang-builder/stlc+rec-iso.rkt
@@ -39,13 +39,13 @@
 (define-typed-syntax unfld
   [(unfld τ:type-ann e) ▶
    [#:with (~μ* (tv) τ_body) #'τ.norm]
-   [⊢ [[e ≫ e-] ⇐ (: τ.norm)]]
+   [⊢ [[e ≫ e-] ⇐ : τ.norm]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: #,(subst #'τ.norm #'tv #'τ_body))]]])
+   [⊢ [[_ ≫ e-] ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]])
 (define-typed-syntax fld
   [(fld τ:type-ann e) ▶
    [#:with (~μ* (tv) τ_body) #'τ.norm]
    [#:with τ_e (subst #'τ.norm #'tv #'τ_body)]
-   [⊢ [[e ≫ e-] ⇐ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇐ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ.norm)]]])
+   [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
diff --git a/tapl/typed-lang-builder/stlc+reco+var.rkt b/tapl/typed-lang-builder/stlc+reco+var.rkt
index 88084d6..eb894d9 100644
--- a/tapl/typed-lang-builder/stlc+reco+var.rkt
+++ b/tapl/typed-lang-builder/stlc+reco+var.rkt
@@ -37,7 +37,7 @@
           (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
           (define- y (ann e : τ.norm)))]]
   [(define x:id e) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ)]]
+   [⊢ [[e ≫ e-] ⇒ : τ]]
    [#:with y (generate-temporary #'x)]
    --------
    [_ ≻ (begin-
@@ -88,18 +88,18 @@
 ;; records
 (define-typed-syntax tup #:datum-literals (=)
   [(tup [l:id = e] ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ)] ...]
+   [⊢ [[e ≫ e-] ⇒ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ (: (× [l : τ] ...))]]])
+   [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ : (× [l : τ] ...)]]])
 (define-typed-syntax proj #:literals (quote)
   [(proj e_rec l:id) ▶
-   [⊢ [[e_rec ≫ e_rec-] ⇒ (: τ_e)]]
+   [⊢ [[e_rec ≫ e_rec-] ⇒ : τ_e]]
    [#:fail-unless (×? #'τ_e)
     (format "Expected expression ~s to have × type, got: ~a"
             (syntax->datum #'e_rec) (type->str #'τ_e))]
    [#:with τ_l (×-ref #'τ_e #'l)]
    --------
-   [⊢ [[_ ≫ (cadr- (assoc- 'l e_rec-))] ⇒ (: τ_l)]]])
+   [⊢ [[_ ≫ (cadr- (assoc- 'l e_rec-))] ⇒ : τ_l]]])
 
 (define-type-constructor ∨/internal #:arity >= 0)
 
@@ -148,7 +148,7 @@
   [(var l:id = e as τ:type) ▶
    --------
    [_ ≻ (ann (var l = e) : τ.norm)]]
-  [(var l:id = e) ⇐ (: τ) ▶
+  [(var l:id = e) ⇐ : τ ▶
    [#:fail-unless (∨? #'τ)
     (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))]
    [#:with τ_e
@@ -156,20 +156,20 @@
            (λ () (raise-syntax-error #f
                     (format "~a field does not exist" (syntax->datum #'l))
                     stx)))]
-   [⊢ [[e ≫ e-] ⇐ (: τ_e)]]
+   [⊢ [[e ≫ e-] ⇐ : τ_e]]
    --------
-   [⊢ [[_ ≫ (list- 'l e)] ⇐ (: _)]]])
+   [⊢ [[_ ≫ (list- 'l e)] ⇐ : _]]])
 
 (define-typed-syntax case
   #:datum-literals (of =>)
   [(case e [l:id x:id => e_l] ...) ▶
    [#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ (: (~∨* [l_x : τ_x] ...))]]
+   [⊢ [[e ≫ e-] ⇒ : (~∨* [l_x : τ_x] ...)]]
    [#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"]
    [#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"]
-   [() ([x : τ_x ≫ x-]) ⊢ [[e_l ≫ e_l-] ⇒ (: τ_el)]] ...
+   [() ([x : τ_x ≫ x-]) ⊢ [[e_l ≫ e_l-] ⇒ : τ_el]] ...
    --------
    [⊢ [[_ ≫
         (let- ([l_e (car- e-)])
           (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))]
-       ⇒ (: (⊔ τ_el ...))]]])
+       ⇒ : (⊔ τ_el ...)]]])
diff --git a/tapl/typed-lang-builder/stlc+sub.rkt b/tapl/typed-lang-builder/stlc+sub.rkt
index 8d16cec..64121ec 100644
--- a/tapl/typed-lang-builder/stlc+sub.rkt
+++ b/tapl/typed-lang-builder/stlc+sub.rkt
@@ -30,13 +30,13 @@
 (define-typed-syntax #%datum
   [(#%datum . n:nat) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Nat)]]]
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Nat]]]
   [(#%datum . n:integer) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Int)]]]
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
   [(#%datum . n:number) ▶
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ (: Num)]]]
+   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Num]]]
   [(#%datum . x) ▶
    --------
    [_ ≻ (ext:#%datum . x)]])
diff --git a/tapl/typed-lang-builder/stlc+tup.rkt b/tapl/typed-lang-builder/stlc+tup.rkt
index ecf37e8..0201d3e 100644
--- a/tapl/typed-lang-builder/stlc+tup.rkt
+++ b/tapl/typed-lang-builder/stlc+tup.rkt
@@ -16,20 +16,20 @@
                     (make-list (stx-length (stx-cdr stx)) covariant)))
 
 (define-typed-syntax tup
-  [(tup e ...) ⇐ (: (~× τ ...)) ▶
+  [(tup e ...) ⇐ : (~× τ ...) ▶
    [#:when (stx-length=? #'[e ...] #'[τ ...])]
-   [⊢ [[e ≫ e-] ⇐ (: τ)] ...]
+   [⊢ [[e ≫ e-] ⇐ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- e- ...)] ⇐ (: _)]]]
+   [⊢ [[_ ≫ (list- e- ...)] ⇐ : _]]]
   [(tup e ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: τ)] ...]
+   [⊢ [[e ≫ e-] ⇒ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- e- ...)] ⇒ (: (× τ ...))]]])
+   [⊢ [[_ ≫ (list- e- ...)] ⇒ : (× τ ...)]]])
 
 (define-typed-syntax proj
   [(proj e_tup n:nat) ▶
-   [⊢ [[e_tup ≫ e_tup-] ⇒ (: (~× τ ...))]]
+   [⊢ [[e_tup ≫ e_tup-] ⇒ : (~× τ ...)]]
    [#:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"]
    --------
-   [⊢ [[_ ≫ (list-ref- e_tup- n)] ⇒ (: #,(stx-list-ref #'[τ ...] (syntax-e #'n)))]]])
+   [⊢ [[_ ≫ (list-ref- e_tup- n)] ⇒ : #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]])
 
diff --git a/tapl/typed-lang-builder/stlc.rkt b/tapl/typed-lang-builder/stlc.rkt
index 88c5dc0..bc1c92a 100644
--- a/tapl/typed-lang-builder/stlc.rkt
+++ b/tapl/typed-lang-builder/stlc.rkt
@@ -29,26 +29,26 @@
 
 (define-typed-syntax λ #:datum-literals (:)
   [(λ ([x:id : τ_in:type] ...) e) ▶
-   [() ([x : τ_in.norm ≫ x-] ...) ⊢ [[e ≫ e-] ⇒ (: τ_out)]]
+   [() ([x : τ_in.norm ≫ x-] ...) ⊢ [[e ≫ e-] ⇒ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇒ (: (→ τ_in.norm ... τ_out))]]]
-  [(λ (x:id ...) e) ⇐ (: (~→ τ_in ... τ_out)) ▶
-   [() ([x : τ_in ≫ x-] ...) ⊢ [[e ≫ e-] ⇐ (: τ_out)]]
+   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇒ : (→ τ_in.norm ... τ_out)]]]
+  [(λ (x:id ...) e) ⇐ : (~→ τ_in ... τ_out) ▶
+   [() ([x : τ_in ≫ x-] ...) ⊢ [[e ≫ e-] ⇐ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇐ (: _)]]])
+   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇐ : _]]])
 
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ▶
-   [⊢ [[e_fn ≫ e_fn-] ⇒ (: (~→ τ_in ... τ_out))]]
+   [⊢ [[e_fn ≫ e_fn-] ⇒ : (~→ τ_in ... τ_out)]]
    [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
     (format "wrong number of arguments: expected ~a, given ~a"
             (stx-length #'[τ_in ...]) (stx-length #'[e_arg ...]))] 
-   [⊢ [[e_arg ≫ e_arg-] ⇐ (: τ_in)] ...]
+   [⊢ [[e_arg ≫ e_arg-] ⇐ : τ_in] ...]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ (: τ_out)]]])
+   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])
 
 (define-typed-syntax ann #:datum-literals (:)
-  [(_ e : τ:type) ▶
-   [⊢ [[e ≫ e-] ⇐ (: τ.norm)]]
+  [(ann e : τ:type) ▶
+   [⊢ [[e ≫ e-] ⇐ : τ.norm]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ.norm)]]])
+   [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
diff --git a/tapl/typed-lang-builder/sysf.rkt b/tapl/typed-lang-builder/sysf.rkt
index 40af118..52a68e9 100644
--- a/tapl/typed-lang-builder/sysf.rkt
+++ b/tapl/typed-lang-builder/sysf.rkt
@@ -16,16 +16,16 @@
 
 (define-typed-syntax Λ
   [(Λ (tv:id ...) e) ▶
-   [([tv : #%type ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ (: τ)]]
+   [([tv : #%type ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: (∀ (tv- ...) τ))]]])
+   [⊢ [[_ ≫ e-] ⇒ : (∀ (tv- ...) τ)]]])
 
 (define-typed-syntax inst
   [(inst e τ:type ...) ▶
-   [⊢ [[e ≫ e-] ⇒ (: (~∀ tvs τ_body))]]
+   [⊢ [[e ≫ e-] ⇒ : (~∀ tvs τ_body)]]
    [#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ (: τ_inst)]]]
+   [⊢ [[_ ≫ e-] ⇒ : τ_inst]]]
   [(inst e) ▶
    --------
    [_ ≻ e]])
diff --git a/tapl/typed-lang-builder/typed-lang-builder.rkt b/tapl/typed-lang-builder/typed-lang-builder.rkt
index 5ead5fe..9041580 100644
--- a/tapl/typed-lang-builder/typed-lang-builder.rkt
+++ b/tapl/typed-lang-builder/typed-lang-builder.rkt
@@ -19,6 +19,46 @@
     [pattern (~literal ...)])
   (define-splicing-syntax-class props
     [pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))])
+  (define-splicing-syntax-class ⇒-prop
+    #:datum-literals (⇒)
+    #:attributes (e-pat)
+    [pattern (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)
+             #:with e-tmp (generate-temporary)
+             #:with e-pat
+             #'(~and e-tmp
+                     (~parse
+                      (~and tag-prop.e-pat ... tag-pat)
+                      (typeof #'e-tmp #:tag 'tag)))])
+  (define-splicing-syntax-class ⇐-prop
+    #:datum-literals (⇐ :)
+    [pattern (~seq ⇐ : τ-stx)
+             #:with e-tmp (generate-temporary)
+             #:with τ-tmp (generate-temporary)
+             #:with τ-exp (generate-temporary)
+             #:with e-pat
+             #'(~and e-tmp
+                     (~parse τ-exp (get-expected-type #'e-tmp))
+                     (~parse τ-tmp (typeof #'e-tmp))
+                     (~parse
+                      (~post
+                       (~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp))
+                                          (get-orig #'e-tmp))
+                              (format "type mismatch: expected ~a, given ~a\n  expression: ~s"
+                                      (type->str #'τ-exp)
+                                      (type->str #'τ-tmp)
+                                      (syntax->datum (get-orig #'e-tmp)))))
+                      (get-orig #'e-tmp)))])
+  (define-splicing-syntax-class ⇒-props
+    #:attributes (e-pat)
+    [pattern (~seq :⇒-prop)]
+    [pattern (~seq (p:⇒-prop) ...)
+             #:with e-pat #'(~and p.e-pat ...)])
+  (define-splicing-syntax-class ⇐-props
+    #:attributes (τ-stx e-pat)
+    [pattern (~seq :⇐-prop)]
+    [pattern (~seq (p:⇐-prop))
+             #:with τ-stx #'p.τ-stx
+             #:with e-pat #'p.e-pat])
   (define-splicing-syntax-class id+props+≫
     #:datum-literals (≫)
     #:attributes ([x- 1] [ctx 1])
@@ -36,9 +76,7 @@
   (define-splicing-syntax-class inf
     #:datum-literals (⊢ ⇒ ⇐ ≫ :)
     #:attributes ([e-stx 1] [e-stx-orig 1] [e-pat 1])
-    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*] ooo:elipsis ...)
-             #:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()] ooo ...]]
-    [pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)] ooo:elipsis ...)
+    [pattern (~seq [[e-stx* ≫ e-pat*] props:⇒-props] ooo:elipsis ...)
              #:with e-tmp (generate-temporary #'e-pat*)
              #:with τ-tmp (generate-temporary 'τ)
              #:with [e-stx ...] #'[e-stx* ooo ...]
@@ -46,35 +84,19 @@
              #:with [e-pat ...]
              #'[(~post
                  (~seq
-                  (~and e-tmp
-                        (~parse τ-tmp (typeof #'e-tmp))
-                        (~parse τ-props.v (typeof #'e-tmp #:tag 'τ-props.k))
-                        ...
-                        (~parse k-props.v (typeof #'τ-tmp #:tag 'k-props.k))
-                        ...
+                  (~and props.e-pat
                         e-pat*)
                   ooo ...))]]
-    [pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)] ooo:elipsis ...)
+    [pattern (~seq [[e-stx* ≫ e-pat*] props:⇐-props] ooo:elipsis ...)
              #:with e-tmp (generate-temporary #'e-pat*)
              #:with τ-tmp (generate-temporary 'τ)
              #:with τ-exp-tmp (generate-temporary 'τ_expected)
-             #:with [e-stx ...] #'[(add-expected e-stx* τ-stx*) ooo ...]
+             #:with [e-stx ...] #'[(add-expected e-stx* props.τ-stx) ooo ...]
              #:with [e-stx-orig ...] #'[e-stx* ooo ...]
              #:with [e-pat ...]
              #'[(~post
                  (~seq
-                  (~and e-tmp
-                        (~parse τ-exp-tmp (get-expected-type #'e-tmp))
-                        (~parse τ-tmp (typeof #'e-tmp))
-                        (~parse
-                         (~post
-                          (~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp-tmp))
-                                             (get-orig #'e-tmp))
-                                 (format "type mismatch: expected ~a, given ~a\n  expression: ~s"
-                                         (type->str #'τ-exp-tmp)
-                                         (type->str #'τ-tmp)
-                                         (syntax->datum (get-orig #'e-tmp)))))
-                         (get-orig #'e-tmp))
+                  (~and props.e-pat
                         e-pat*)
                   ooo ...))]]
     )
@@ -133,13 +155,16 @@
     )
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
-    [pattern [⊢ [[pat ≫ e-stx] ⇒ (τ-props:props)]]
+    #:attributes ([pat 0] [stuff 1])
+    [pattern [⊢ [[pat* ≫ e-stx] ⇒ k v]]
+             #:with :last-clause #'[⊢ [[pat* ≫ e-stx] (⇒ k v)]]]
+    [pattern [⊢ [[pat ≫ e-stx] (⇒ k:id v) ...]]
              #:with [stuff ...]
              #'[(for/fold ([result (quasisyntax/loc this-syntax e-stx)])
-                          ([tag (in-list (list 'τ-props.k ...))]
-                           [τ (in-list (list #`τ-props.v ...))])
+                          ([tag (in-list (list 'k ...))]
+                           [τ (in-list (list #`v ...))])
                   (assign-type result τ #:tag tag))]]
-    [pattern [⊢ [[pat* ≫ e-stx] ⇐ (: τ-pat)]]
+    [pattern [⊢ [[pat* ≫ e-stx] ⇐ : τ-pat]]
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with pat
@@ -161,7 +186,7 @@
                 (error msg)]])
   (define-splicing-syntax-class pat #:datum-literals (⇐ :)
     [pattern (~seq pat)]
-    [pattern (~seq pat* ⇐ (: τ-pat))
+    [pattern (~seq pat* ⇐ : τ-pat)
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with pat