diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index a7b687f..dbe2f88 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -31,7 +31,7 @@
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+     #:with (τ- k_τ) (infer+erase #'τ)
      #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
      #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
@@ -81,14 +81,13 @@
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
    #:with ((tv- ...) e- τ_e)
-          (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+          (infer/ctx+erase #'bvs #'e)
    (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
   [(_ e τ ...)
    #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
-   #:with ([τ- k_τ] ...)
-          (infers+erase #'(τ ...) #:expand (current-type-eval))
+   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
    #:when (stx-andmap
            (λ (t k) (or ((current-kind?) k)
                         (type-error #:src t #:msg "not a valid type: ~a" t)))
@@ -100,15 +99,14 @@
 ;; - see fomega2.rkt
 (define-typed-syntax tyλ
   [(_ bvs:kind-ctx τ_body)
-   #:with (tvs- τ_body- k_body)
-          (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+   #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
    #:when ((current-kind?) #'k_body)
    (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
 
 (define-typed-syntax tyapp #:export-as tyapp
   [(_ τ_fn τ_arg ...)
    #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
-   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
+   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
    #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
                  (string-append
                   (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
index a81d0c2..5640f5d 100644
--- a/tapl/fomega2.rkt
+++ b/tapl/fomega2.rkt
@@ -1,5 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ; same as fomega.rkt except here λ and #%app works as both type and terms
@@ -34,64 +34,37 @@
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+     #:with (τ- k_τ) (infer+erase #'τ)
      #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
-(begin-for-syntax
-  (define sysf:type-eval (current-type-eval))
-  ;; extend type-eval to handle tyapp
-  ;; - requires manually handling all other forms
-  (define (type-eval τ)
-    (beta (sysf:type-eval τ)))
-  (define (beta τ)
-    (syntax-parse τ
-      [((~literal #%plain-app) τ_fn τ_arg ...)
-       #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
-       ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
-      [((~literal #%plain-lambda) (x ...) τ_body ...)
-       #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
-       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
-      [((~literal #%plain-app) arg ...)
-       #:with (arg+ ...) (stx-map beta #'(arg ...))
-       (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
-      [_ τ]))
-  (current-type-eval type-eval))
-
 (define-base-kind ★)
 (define-kind-constructor ∀★ #:arity >= 0)
+(define-type-constructor ∀ #:bvs >= 0 #:arr ∀★)
 
-(define-typed-syntax ∀ #:export-as ∀
-  [(_ bvs:kind-ctx τ_body)
-   ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
-   #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
-   ; expand so kind gets overwritten
-   (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
+;; alternative: normalize before type=?
+; but then also need to normalize in current-promote
 (begin-for-syntax
-  (define-syntax ~∀
-    (pattern-expander
-     (syntax-parser #:datum-literals (:)
-       [(_ ([tv:id : k] ...) τ)
-        #:with ∀τ (generate-temporary)
-        #'(~and ∀τ
-                (~parse (~sysf:∀ (tv ...) τ) #'∀τ)
-                (~parse (~∀★ k ...) (typeof #'∀τ)))]
-       [(_ . args)
-        #:with ∀τ (generate-temporary)
-        #'(~and ∀τ
-                (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
-                (~parse (~∀★ k (... ...)) (typeof #'∀τ))
-                (~parse args #'(([tv k] (... ...)) τ)))])))
-  (define-syntax ~∀*
-    (pattern-expander
-     (syntax-parser #:datum-literals (<:)
-       [(_ . args)
-        #'(~or
-           (~∀ . args)
-           (~and any (~do
-                      (type-error
-                       #:src #'any
-                       #:msg "Expected ∀ type, got: ~a" #'any))))])))
-  (define sysf:type=? (current-type=?))
+  (define (normalize τ)
+    (syntax-parse τ
+      [x:id #'x]
+      [((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
+       (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+      [((~literal #%plain-lambda) (x ...) . bodys)
+       #:with bodys_norm (stx-map normalize #'bodys)
+       (syntax-track-origin #'(#%plain-lambda (x ...) . bodys_norm) τ #'plain-lambda)]
+      [((~literal #%plain-app) x:id . args)
+       #:with args_norm (stx-map normalize #'args)
+       (syntax-track-origin #'(#%plain-app x . args_norm) τ #'#%plain-app)]
+      [((~literal #%plain-app) . args)
+       #:with args_norm (stx-map normalize #'args)
+       (syntax-track-origin (normalize #'(#%plain-app . args_norm)) τ #'#%plain-app)]
+      [_ τ]))
+  
+  (define old-eval (current-type-eval))
+  (define (type-eval τ) (normalize (old-eval τ)))
+  (current-type-eval type-eval)
+  
+  (define old-type=? (current-type=?))
   (define (type=? t1 t2)
     (or (and (★? t1) (#%type? t2))
         (and (#%type? t1) (★? t2))
@@ -100,20 +73,20 @@
                  (~∀ ([tv2 : k2]) tbody2))
                 ((current-type=?) #'k1 #'k2)]
                [_ #t])
-             (sysf:type=? t1 t2))))
+             (old-type=? t1 t2))))
   (current-type=? type=?)
   (current-typecheck-relation (current-type=?)))
 
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
    #:with ((tv- ...) e- τ_e)
-          (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+          (infer/ctx+erase #'bvs #'e)
    (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
   [(_ e τ ...)
-   #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
-   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
+   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
+   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
    #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
                                    (type-error #:src t #:msg "not a valid type: ~a" t)))
                       #'(τ ...) #'(k_τ ...))
diff --git a/tapl/fomega3.rkt b/tapl/fomega3.rkt
index dd219f4..7a405bd 100644
--- a/tapl/fomega3.rkt
+++ b/tapl/fomega3.rkt
@@ -30,24 +30,3 @@
                             (let ([k (typeof t)])
                               (or (★? k) (∀★? k)))
                             ((current-kind?) t)))))
-
-;; extend to handle #%app and λ used as both terms and types
-(begin-for-syntax
-  (define sysf:type-eval (current-type-eval))
-  ;; extend type-eval to handle tyapp
-  ;; - requires manually handling all other forms
-  (define (type-eval τ)
-    (beta (sysf:type-eval τ)))
-  (define (beta τ)
-    (syntax-parse τ
-      [((~literal #%plain-app) τ_fn τ_arg ...)
-       #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
-       ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
-      [((~literal #%plain-lambda) (x ...) τ_body ...)
-       #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
-       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
-      [((~literal #%plain-app) arg ...)
-       #:with (arg+ ...) (stx-map beta #'(arg ...))
-       (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
-      [_ τ]))
-  (current-type-eval type-eval))
\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 1d20234..6ebc9c1 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -197,12 +197,12 @@
 
   ;; basic infer function with no context:
   ;; infers the type and erases types in an expression
-  (define (infer+erase e #:expand [expand-fn expand/df])
-    (define e+ (expand-fn e))
+  (define (infer+erase e)
+    (define e+ (expand/df e))
     (list e+ (typeof e+)))
   ;; infers the types and erases types in multiple expressions
-  (define (infers+erase es #:expand [expand-fn expand/df])
-    (stx-map (λ (e) (infer+erase e #:expand expand-fn)) es))
+  (define (infers+erase es)
+    (stx-map infer+erase es))
 
   ;; This is the main "infer" function. All others are defined in terms of this.
   ;; It should be named infer+erase but leaving it for now for backward compat.
@@ -211,8 +211,7 @@
   ;; octx + tag = some other context (and an associated tag)
   ;; eg bounded quantification in Fsub
   (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
-                 #:octx [octx tvctx] #:tag [tag 'unused]
-                 #:expand [expand-fn expand/df])
+                 #:octx [octx tvctx] #:tag [tag 'unused])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with ([tv : k] ...) tvctx
@@ -233,7 +232,7 @@
           ((~literal #%plain-lambda) xs+
            ((~literal let-values) () ((~literal let-values) ()
             ((~literal #%expression) e+) ... (~literal void))))))))
-       (expand-fn
+       (expand/df
         #`(λ (tv ...)
             (let-syntax ([tv (make-rename-transformer
                               (assign-type
@@ -260,11 +259,11 @@
   ;; shorter names
   ; ctx = type env for bound vars in term e, etc
   ; can also use for bound tyvars in type e
-  (define (infer/ctx+erase ctx e #:expand [expand-fn expand/df])
-    (syntax-parse (infer (list e) #:ctx ctx #:expand expand-fn)
+  (define (infer/ctx+erase ctx e)
+    (syntax-parse (infer (list e) #:ctx ctx)
       [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
-  (define (infers/ctx+erase ctx es #:expand [expand-fn expand/df])
-    (stx-cdr (infer es #:ctx ctx #:expand expand-fn)))
+  (define (infers/ctx+erase ctx es)
+    (stx-cdr (infer es #:ctx ctx)))
   ; tyctx = kind env for bound type vars in term e
   (define (infer/tyctx+erase ctx e)
     (syntax-parse (infer (list e) #:tvctx ctx)
@@ -459,13 +458,13 @@
               #:fail-unless (op (stx-length #'args) n)
                             (format "wrong number of arguments, expected ~a ~a" 'op 'n)
               #:with (bvs- τs- _)
-                     (infers/ctx+erase #'bvs #'args ;#'([bv : #%kind] (... ...)) #'args
-                                       #:expand (current-type-eval))
+                     (infers/ctx+erase #'bvs #'args) ;#'([bv : #%kind] (... ...)) #'args
+;                                       #:expand (current-type-eval))
                #:with (~! (~var _ kind) (... ...)) #'τs-
                #:with ([tv (~datum :) k_arg] (... ...)) #'bvs
-               #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
+;               #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
                #:with k_result (if #,(attribute has-annotations?)
-                                   #'(tycon k_arg+ (... ...))
+                                   #'(tycon k_arg (... ...))
                                    #'#%kind)
                (assign-type #'(τ-internal (λ bvs- void . τs-)) #'k_result)]
              ;; else fail with err msg