diff --git a/macrotypes/examples/stlc+lit.rkt b/macrotypes/examples/stlc+lit.rkt
index 66e4041..05fd9db 100644
--- a/macrotypes/examples/stlc+lit.rkt
+++ b/macrotypes/examples/stlc+lit.rkt
@@ -15,14 +15,15 @@
 
 (define-base-type Int)
 
+;; Using τ.norm leads to a "not valid type" error when file is compiled
 (define-syntax define-primop
   (syntax-parser #:datum-literals (:)
-    [(_ op:id : τ:type)
+    [(_ op:id : τ)
      #:with op/tc (generate-temporary #'op)
      #'(begin
          (provide (rename-out [op/tc op]))
          (define-primop op/tc op : τ))]
-    [(_ op/tc op : τ)
+    [(_ op/tc op : τ:type)
      #'(begin
          #;(define-syntax op/tc (make-rename-transformer (assign-type #'op #'τ)))
          ; rename transformer doesnt seem to expand at the right time
diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt
index bf4710a..e8876cc 100644
--- a/macrotypes/examples/stlc+reco+var.rkt
+++ b/macrotypes/examples/stlc+reco+var.rkt
@@ -18,10 +18,11 @@
 ;; - define-type-alias
 
 (provide define-type-alias)
+;; Using τ.norm leads to a "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ:type)
-     #'(define-syntax alias (make-variable-like-transformer #'τ.norm) #;(syntax-parser [x:id #'τ.norm]))]
+     #'(define-syntax alias (make-variable-like-transformer #'τ))]
     [(_ (f:id x:id ...) ty)
      #'(define-syntax (f stx)
          (syntax-parse stx
diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
index c496706..e03f967 100644
--- a/macrotypes/stx-utils.rkt
+++ b/macrotypes/stx-utils.rkt
@@ -107,5 +107,5 @@
        ref-stx]
       [(id . args)
        (let ([stx* (list* '#%app #'id (cdr (syntax-e stx)))])
-         (datum->syntax stx stx* stx))])))
+         (datum->syntax stx stx* stx stx))])))
 
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index ba223ab..bef04ae 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -595,7 +595,10 @@
          (define-syntax τ
            (syntax-parser
              ;[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))]))
-             [(~var _ id) (add-orig (assign-type #'(τ-internal) #'#%tag) #'τ)])))]))
+             [(~var _ id) 
+              (add-orig 
+               (assign-type 
+                (syntax/loc this-syntax (τ-internal)) #'#%tag) #'τ)])))]))
 
 ; I use identifiers "τ" and "kind" but this form is not restricted to them.
 ; E.g., τ can be #'★ and kind can be #'#%kind (★'s type)
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index edc0933..ae35c85 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -93,11 +93,6 @@
 
 (define-base-type Stx)
 
-#;(define-typed-syntax syntax
-  [(_ template) ≫
-   --------
-   [⊢ [[_ ≫ (syntax- template)] ⇒ : Stx]]])
-
 ;; ----------------------------------------------------------------------------
 ;; BV stuff
 
@@ -105,10 +100,14 @@
 (define-base-type BV) ; represents actual bitvectors
 
 ; a predicate recognizing bv's of a certain size
+#;(define-syntax BVPred 
+  (make-variable-like-transformer 
+   ((current-type-eval) #'(→ BV Bool))))
 (define-type-alias BVPred (→ BV Bool))
 
 ;; TODO: fix me --- need subtyping?
-(define-syntax Nat (make-rename-transformer #'Int))
+;(define-syntax Nat (make-rename-transformer #'Int))
+(define-type-alias Nat Int)
 
 ;; TODO: support higher order case --- need intersect types?
 ;(define-rosette-primop bv : (→ Int BVPred BV)
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
index 40674c8..d6e4215 100644
--- a/turnstile/examples/stlc+lit.rkt
+++ b/turnstile/examples/stlc+lit.rkt
@@ -15,14 +15,15 @@
 
 (define-base-type Int)
 
+;; Using τ.norm leads to a "not valid type" error when file is compiled
 (define-syntax define-primop
   (syntax-parser #:datum-literals (:)
-    [(define-primop op:id : τ:type)
+    [(define-primop op:id : τ)
      #:with op/tc (generate-temporary #'op)
      #`(begin-
          (provide- #,(syntax/loc this-syntax (rename-out- [op/tc op])))
          (define-primop op/tc op : τ))]
-    [(define-primop op/tc op : τ)
+    [(define-primop op/tc op : τ:type)
      #'(begin-
          ; rename transformer doesnt seem to expand at the right time
          ; - op still has no type in #%app
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
index 3cb2539..69dfb40 100644
--- a/turnstile/examples/stlc+reco+var.rkt
+++ b/turnstile/examples/stlc+reco+var.rkt
@@ -18,10 +18,11 @@
 ;; - define-type-alias
 
 (provide define-type-alias)
+;; Using τ.norm leads to a "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
     [(define-type-alias alias:id τ:type)
-     #'(define-syntax alias (make-variable-like-transformer #'τ.norm))]
+     #'(define-syntax alias (make-variable-like-transformer #'τ))]
     [(define-type-alias (f:id x:id ...) ty)
      #'(define-syntax (f stx)
          (syntax-parse stx
diff --git a/turnstile/examples/tests/run-all-tests.rkt b/turnstile/examples/tests/run-all-tests.rkt
index e2ed66d..930686c 100644
--- a/turnstile/examples/tests/run-all-tests.rkt
+++ b/turnstile/examples/tests/run-all-tests.rkt
@@ -27,11 +27,13 @@
 (require "fomega2-tests.rkt")
 (require "fomega3-tests.rkt")
 
-(require macrotypes/examples/tests/stlc+occurrence-tests)
-(require macrotypes/examples/tests/stlc+overloading-tests)
+;; these are not ported to turnstile yet
+;; see macrotypes/examples/tests/run-all-tests.rkt
+;(require macrotypes/examples/tests/stlc+occurrence-tests)
+;(require macrotypes/examples/tests/stlc+overloading-tests)
 
 ;; type inference
-(require macrotypes/examples/tests/infer-tests)
+;(require macrotypes/examples/tests/infer-tests)
 (require "tlb-infer-tests.rkt")
 
 ;; type and effects