diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt
index eca5f17..637c8cb 100644
--- a/macrotypes/examples/ext-stlc.rkt
+++ b/macrotypes/examples/ext-stlc.rkt
@@ -119,14 +119,14 @@
   [(_ e_unit ... e)
    #:with ([e_unit- _] ...) (infers+erase #'(e_unit ...))
    #:with (e- τ) (infer+erase #'e)
-   (⊢ (begin- e_unit- ... e-) : τ)])
+   (⊢/no-teval (begin- e_unit- ... e-) : τ)])
 
 (define-typed-syntax ann #:datum-literals (:)
   [(_ e : ascribed-τ:type)
    #:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
    #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
    (typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e)
-   (⊢ e- : ascribed-τ)])
+   (⊢/no-teval e- : ascribed-τ.norm)])
 
 (define-typed-syntax let
   [(_ ([x e] ...) e_body)
@@ -137,7 +137,7 @@
    #:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type
                      (typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
    (typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body)
-   (⊢ (let- ([x- e-] ...) e_body-) : τ_body)])
+   (⊢/no-teval (let- ([x- e-] ...) e_body-) : τ_body)])
 
 ; dont need to manually transfer expected type
 ; result template automatically propagates properties
@@ -157,4 +157,4 @@
           (infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body))
    #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
    (typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...))
-   (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
+   (⊢/no-teval (letrec- ([x- e-] ...) e_body-) : τ_body)])
diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt
index 0f00879..9849f34 100644
--- a/macrotypes/examples/infer.rkt
+++ b/macrotypes/examples/infer.rkt
@@ -31,6 +31,74 @@
     [(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
 
 (begin-for-syntax
+;; redefine all inferX functions to use 'env prop --------------------
+  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null])
+    (syntax-parse ctx #:datum-literals (:)
+      [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
+       #:with ([tv (~seq sep:id tvk) ...] ...) tvctx
+       #:with (e ...) es
+       #:with
+       ((~literal #%plain-lambda) tvs+
+        ((~literal let-values) () ((~literal let-values) ()
+         ((~literal #%expression)
+          ((~literal #%plain-lambda) xs+
+           ((~literal let-values) () ((~literal let-values) ()
+            ((~literal #%expression) e+) ... (~literal void))))))))
+       (expand/df
+        #`(λ- (tv ...)
+            (let-syntax ([tv (make-rename-transformer
+                              (set-stx-prop/preserved
+                               (for/fold ([tv-id #'tv])
+                                         ([s (in-list (list 'sep ...))]
+                                          [k (in-list (list #'tvk ...))])
+                                 (assign-type tv-id k #:tag s))
+                               'tyvar #t))] ...)
+              (λ- (x ...)
+                (let-syntax 
+                  ([x 
+                    (syntax-parser 
+                     [i:id
+                      (if (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+                          (if (get-expected-type #'i)
+                              (add-env 
+                                (assign-type #'x (get-expected-type #'i)) 
+                                #`((x #,(get-expected-type #'i))))
+                              (raise
+                               (exn:fail:type:infer
+                                 (format "~a (~a:~a): could not infer type of ~a; add annotation(s)"
+                                         (syntax-source #'x) (syntax-line #'x) (syntax-column #'x)
+                                         (syntax->datum #'x))
+                                 (current-continuation-marks))))
+                          (assign-type #'x #'τ))]
+                     [(o . rst) ; handle if x used in fn position
+                      #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+                      (raise (exn:fail:type:infer
+                                 (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)"
+                                         (syntax-source #'o) (syntax-line #'o) (syntax-column #'o)
+                                         (syntax->datum #'o))
+                               (current-continuation-marks)))
+                      #:with app (datum->syntax #'o '#%app)
+                      (datum->syntax this-syntax
+                                     (list* #'app (assign-type #'x #'τ) #'rst)
+                                     this-syntax)])] ...)
+                  (#%expression e) ... void)))))
+       (list #'tvs+ #'xs+ #'(e+ ...)
+              (stx-map typeof #'(e+ ...)))]
+      [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
+
+  (define (infer/ctx+erase ctx e)
+    (syntax-parse (infer (list e) #:ctx ctx)
+      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+  (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)
+      [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+  (define (infers/tyctx+erase ctx es)
+    (syntax-parse (infer es #:tvctx ctx)
+      [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
+
   ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
   ;; finds the free Xs in the type
   (define (find-free-Xs Xs ty)
diff --git a/macrotypes/examples/stlc+box.rkt b/macrotypes/examples/stlc+box.rkt
index e1d2503..0002382 100644
--- a/macrotypes/examples/stlc+box.rkt
+++ b/macrotypes/examples/stlc+box.rkt
@@ -20,7 +20,7 @@
 (define-typed-syntax deref
   [(_ e)
    #:with [e- (~Ref τ)] (infer+erase #'e)
-   (⊢ (unbox- e-) : τ)])
+   (⊢/no-teval (unbox- e-) : τ)])
 (define-typed-syntax := #:literals (:=)
   [(_ e_ref e)
    #:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref)
diff --git a/macrotypes/examples/stlc+cons.rkt b/macrotypes/examples/stlc+cons.rkt
index 674bcef..89694c4 100644
--- a/macrotypes/examples/stlc+cons.rkt
+++ b/macrotypes/examples/stlc+cons.rkt
@@ -50,7 +50,7 @@
    ;; propagate up inferred types of variables
    #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
    #:with result-cons (add-env #'(cons- e1- e2-) #'env)
-   (⊢ result-cons : τ_list)])
+   (⊢/no-teval result-cons : τ_list)])
 (define-typed-syntax isnil
   [(_ e)
    #:with [e- (~List _)] (infer+erase #'e)
@@ -58,12 +58,12 @@
 (define-typed-syntax head
   [(_ e)
    #:with [e- (~List τ)] (infer+erase #'e)
-   (⊢ (car- e-) : τ)])
+   (⊢/no-teval (car- e-) : τ)])
 (define-typed-syntax tail
   [(_ e)
    #:with [e- τ_lst] (infer+erase #'e)
    #:when (List? #'τ_lst)
-   (⊢ (cdr- e-) : τ_lst)])
+   (⊢/no-teval (cdr- e-) : τ_lst)])
 (define-typed-syntax list
   [(_) #'nil]
   [(_ x . rst) ; has expected type
@@ -77,7 +77,7 @@
   [(_ e)
    #:with (e- τ-lst) (infer+erase #'e)
    #:when (List? #'τ-lst)
-   (⊢ (reverse- e-) : τ-lst)])
+   (⊢/no-teval (reverse- e-) : τ-lst)])
 (define-typed-syntax length
   [(_ e)
    #:with (e- τ-lst) (infer+erase #'e)
@@ -87,7 +87,7 @@
   [(_ e n)
    #:with (e- (ty)) (⇑ e as List)
    #:with n- (⇑ n as Int)
-   (⊢ (list-ref- e- n-) : ty)])
+   (⊢/no-teval (list-ref- e- n-) : ty)])
 (define-typed-syntax member
   [(_ v e)
    #:with (e- (ty)) (⇑ e as List)
diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt
index 770a607..6a34fc3 100644
--- a/macrotypes/examples/stlc.rkt
+++ b/macrotypes/examples/stlc.rkt
@@ -32,4 +32,4 @@
    #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
                  (typecheck-fail-msg/multi 
                   #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
-   (⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
+   (⊢/no-teval (#%app- e_fn- e_arg- ...) : τ_out)])
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index ac57bf2..813d264 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -191,6 +191,10 @@
     (syntax-parse stx #:datum-literals (:)
       [(_ e : τ) #'(assign-type #`e #`τ)]
       [(_ e τ) #'(⊢ e : τ)]))
+  (define-syntax (⊢/no-teval stx)
+    (syntax-parse stx #:datum-literals (:)
+      [(_ e : τ) #'(fast-assign-type #`e #`τ)]
+      [(_ e τ) #'(⊢/no-teval e : τ)]))
 
   ;; Actual type assignment function.
   ;; assign-type Type -> Syntax
@@ -198,8 +202,10 @@
   ;; - eval here so all types are stored in canonical form
   ;; - syntax-local-introduce fixes marks on types
   ;;   which didnt get marked bc they were syntax properties
+  (define (fast-assign-type e τ #:tag [tag ':])
+    (set-stx-prop/preserved e tag (syntax-local-introduce τ)))
   (define (assign-type e τ #:tag [tag ':])
-    (set-stx-prop/preserved e tag (syntax-local-introduce ((current-type-eval) τ))))
+    (fast-assign-type e ((current-type-eval) τ) #:tag tag))
 
   (define (add-expected-type e τ)
     (if (and (syntax? τ) (syntax-e τ))
@@ -314,10 +320,8 @@
 
   ;; 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.
-  ;; ctx = vars and their types
+  ;; ctx = vars and their types (or other props, denoted with "sep")
   ;; tvctx = tyvars and their kinds
-  ;; octx + tag = some other context (and an associated tag)
-  ;; eg bounded quantification in Fsub
   (define (infer es #:ctx [ctx null] #:tvctx [tvctx null])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
@@ -348,39 +352,10 @@
                                  (assign-type tv-id k #:tag s))
                                'tyvar #t))] ...)
               (λ (x ...)
-                (let-syntax 
-                  ([x 
-                    (syntax-parser 
-                     [i:id
-                      (if (and (identifier? #'τ) (free-identifier=? #'x #'τ))
-                          (if (get-expected-type #'i)
-                              (add-env 
-                                (assign-type #'x (get-expected-type #'i)) 
-                                #`((x #,(get-expected-type #'i))))
-                              (raise
-                               (exn:fail:type:infer
-                                 (format "~a (~a:~a): could not infer type of ~a; add annotation(s)"
-                                         (syntax-source #'x) (syntax-line #'x) (syntax-column #'x)
-                                         (syntax->datum #'x))
-                                 (current-continuation-marks))))
-                          (assign-type #'x #'τ))]
-                     [(o . rst) ; handle if x used in fn position
-                      #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ))
-                      (raise (exn:fail:type:infer
-                                 (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)"
-                                         (syntax-source #'o) (syntax-line #'o) (syntax-column #'o)
-                                         (syntax->datum #'o))
-                               (current-continuation-marks)))
-                      #:with app (datum->syntax #'o '#%app)
-                      (datum->syntax this-syntax
-                                     (list* #'app (assign-type #'x #'τ) #'rst)
-                                     this-syntax)])] ...)
-                  (#%expression e) ... void)))))
-       (list #'tvs+ #'xs+ #'(e+ ...)
-             (stx-map ; need this check when combining #%type and kinds
-              (λ (t) (or (false? t)
-                         (syntax-local-introduce t)))
-              (stx-map typeof #'(e+ ...))))]
+               (let-syntax 
+                ([x (make-variable-like-transformer (assign-type #'x #'τ))] ...)
+                 (#%expression e) ... void)))))
+       (list #'tvs+ #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
       [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
 
   ;; fns derived from infer ---------------------------------------------------