diff --git a/macrotypes/examples/fomega.rkt b/macrotypes/examples/fomega.rkt
index f6c3b4a..9fe72b5 100644
--- a/macrotypes/examples/fomega.rkt
+++ b/macrotypes/examples/fomega.rkt
@@ -1,5 +1,5 @@
 #lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
diff --git a/macrotypes/examples/fomega2.rkt b/macrotypes/examples/fomega2.rkt
index 4b14f5b..27aef1d 100644
--- a/macrotypes/examples/fomega2.rkt
+++ b/macrotypes/examples/fomega2.rkt
@@ -1,5 +1,5 @@
 #lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ; same as fomega.rkt except here λ and #%app works as both type and terms
diff --git a/macrotypes/examples/stlc+effect.rkt b/macrotypes/examples/stlc+effect.rkt
index 4d78077..c6a452e 100644
--- a/macrotypes/examples/stlc+effect.rkt
+++ b/macrotypes/examples/stlc+effect.rkt
@@ -1,5 +1,5 @@
 #lang s-exp macrotypes/typecheck
-(extends "stlc+box.rkt" #:except ref deref := #%app λ)
+(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ)
 
 (provide (for-syntax get-new-effects))
 
diff --git a/macrotypes/examples/stlc+reco+var.rkt b/macrotypes/examples/stlc+reco+var.rkt
index d69ace5..bf4710a 100644
--- a/macrotypes/examples/stlc+reco+var.rkt
+++ b/macrotypes/examples/stlc+reco+var.rkt
@@ -1,6 +1,6 @@
 #lang s-exp macrotypes/typecheck
-(extends "stlc+tup.rkt" #:except × ×? tup proj
-                        #:rename [~× ~stlc:×])
+(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*)
+(require (only-in "stlc+tup.rkt" [~× ~stlc:×]))
 (provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*))
 
 
@@ -30,6 +30,7 @@
 (define-typed-syntax define
   [(define x:id e)
    #:with (e- τ) (infer+erase #'e)
+
    #:with y (generate-temporary)
    #'(begin-
        (define-syntax x (make-rename-transformer (⊢ y : τ)))
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index 8440e25..ba223ab 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -43,14 +43,19 @@
 (define-syntax (mb stx)
   (syntax-parse stx
     [(_ . stuff)
-     #'(#%module-begin
+     (syntax/loc this-syntax
+       (#%module-begin
         (provide #%module-begin #%top-interaction #%top require) ; useful racket forms
-        . stuff)]))
+        . stuff))]))
 
 (struct exn:fail:type:runtime exn:fail:user ())
 
+;; drop-file-ext : String -> String
 (define-for-syntax (drop-file-ext filename)
   (car (string-split filename ".")))
+;; extract-filename : PathString -> String
+(define-for-syntax (extract-filename f)
+  (path->string (path-replace-suffix (file-name-from-path f) "")))
 
 (begin-for-syntax
   (define-syntax-parameter stx (syntax-rules ())))
@@ -78,29 +83,35 @@
 (define-syntax extends
   (syntax-parser
     [(_ base-lang
-        (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) #:defaults ([(x 1) null]))
-        (~optional (~seq #:rename [old new] ...) #:defaults ([(old 1) null][(new 1) null]))
-        (~optional (~seq #:prefix p ...) #:defaults ([(p 1) null])))
-     #:with pre (or (let ([dat (syntax-e #'base-lang)])
-                      (and (string? dat)
-                           (string->symbol (drop-file-ext dat))))
-                    #'base-lang)                    
-     #:with pre: (format-id #'pre "~a:" #'pre)
+        (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) 
+                   #:defaults ([(x 1) null]))
+        (~optional (~seq #:rename [old new] ...) 
+                   #:defaults ([(old 1) null][(new 1) null])))
+     #:with pre: 
+            (let ([pre (or (let ([dat (syntax-e #'base-lang)])
+                             (and (string? dat) (extract-filename dat)))
+                           #'base-lang)])
+              (format-id #'base-lang "~a:" pre))
      #:with internal-pre (generate-temporary)
-     #:with non-excluded-imports #'(except-in base-lang p ... x ... old ...)
+     #:with non-excluded-imports #'(except-in base-lang x ... old ...)
      #:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define)))
      #:with not-conflicted? #'(λ (n) (and (not (conflicted? n)) n))
      #`(begin
-         (require (prefix-in pre: (only-in base-lang p ... x ...))) ; prefixed
-         (require (rename-in (only-in base-lang old ...) [old new] ...))
-         (require (filtered-in not-conflicted? non-excluded-imports))
-         (require (filtered-in ; conflicted names, with (internal) prefix
+         #,(syntax/loc this-syntax
+             (require (prefix-in pre: base-lang))) ; prefixed
+         #,(syntax/loc this-syntax
+            (require (rename-in (only-in base-lang old ...) [old new] ...)))
+         #,(syntax/loc this-syntax
+             (require (filtered-in not-conflicted? non-excluded-imports)))
+         #,(syntax/loc this-syntax
+             (require (filtered-in ; conflicted names, with (internal) prefix
                    (let ([conflicted-pre (symbol->string (syntax->datum #'internal-pre))])
                      (λ (name) (and (conflicted? name)
                                     (string-append conflicted-pre name))))
-                   non-excluded-imports))
-         (provide (filtered-out
-                   (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+                   non-excluded-imports)))
+         #,(quasisyntax/loc this-syntax
+             (provide (filtered-out
+                   (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")]
                           [int-pre-str #,(symbol->string (syntax->datum #'internal-pre))]
                           [pre-str-len (string-length pre-str)]
                           [int-pre-str-len (string-length int-pre-str)]
@@ -116,20 +127,23 @@
                              name))
                        (and (not (member out-name excluded)) out-name)))
                    (all-from-out base-lang))
-                  ))]))
+                  )))]))
 (define-syntax reuse
   (syntax-parser
     [(_ (~or x:id [old:id new:id]) ... #:from base-lang)
-     #:with pre (or (let ([dat (syntax-e #'base-lang)])
-                      (and (string? dat)
-                           (string->symbol (drop-file-ext dat))))
-                    #'base-lang)                    
-     #:with pre: (format-id #'pre "~a:" #'pre)
+     #:with pre: 
+            (let ([pre (or (let ([dat (syntax-e #'base-lang)])
+                             (and (string? dat) (extract-filename dat)))
+                           #'base-lang)])
+              (format-id #'base-lang "~a:" pre))
      #`(begin
-         (require (rename-in (only-in base-lang old ...) [old new] ...))
-         (require (prefix-in pre: (only-in base-lang x ...)))
-         (provide (filtered-out
-                   (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+         #,(syntax/loc this-syntax
+             (require (rename-in (only-in base-lang old ...) [old new] ...)))
+         #,(syntax/loc this-syntax
+             (require (prefix-in pre: (only-in base-lang x ...))))
+         #,(quasisyntax/loc this-syntax
+             (provide (filtered-out
+                   (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")]
                           [pre-str-len (string-length pre-str)]
                           [drop-pre (λ (s) (substring s pre-str-len))]
                           [excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))]
@@ -142,7 +156,7 @@
                        (and (not (member out-name excluded))
                             (member out-name origs)
                             out-name)))
-                   (all-from-out base-lang))))]))
+                   (all-from-out base-lang)))))]))
 
 (define-syntax add-expected
   (syntax-parser
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
index ac045ba..9e313c0 100644
--- a/turnstile/examples/fomega.rkt
+++ b/turnstile/examples/fomega.rkt
@@ -1,5 +1,5 @@
 #lang turnstile
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
index b35593b..c953b86 100644
--- a/turnstile/examples/fomega2.rkt
+++ b/turnstile/examples/fomega2.rkt
@@ -1,5 +1,5 @@
 #lang turnstile
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ~∀* ∀? Λ inst)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ; same as fomega.rkt except here λ and #%app works as both type and terms
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
index 7919f07..ee408a4 100644
--- a/turnstile/examples/infer.rkt
+++ b/turnstile/examples/infer.rkt
@@ -1,5 +1,5 @@
 #lang turnstile
-(extends "ext-stlc.rkt" #:except #%app λ)
+(extends "ext-stlc.rkt" #:except #%app λ ann)
 (reuse inst #:from "sysf.rkt")
 (require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ))
 (reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt")
diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt
index 3d3a7fb..e365c4c 100644
--- a/turnstile/examples/stlc+effect.rkt
+++ b/turnstile/examples/stlc+effect.rkt
@@ -1,5 +1,5 @@
 #lang turnstile
-(extends "stlc+box.rkt" #:except ref deref := #%app λ)
+(extends "stlc+box.rkt" #:except ref Ref ~Ref ~Ref* Ref? deref := #%app λ)
 
 ;; Simply-Typed Lambda Calculus, plus mutable references
 ;; Types:
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
index 6d5746c..3cb2539 100644
--- a/turnstile/examples/stlc+reco+var.rkt
+++ b/turnstile/examples/stlc+reco+var.rkt
@@ -1,6 +1,6 @@
 #lang turnstile
-(extends "stlc+tup.rkt" #:except × ×? tup proj
-                        #:rename [~× ~stlc:×])
+(extends "stlc+tup.rkt" #:except × ×? tup proj ~× ~×*)
+(require (only-in "stlc+tup.rkt" [~× ~stlc:×]))
 (provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*))