diff --git a/macrotypes/examples/tests/general-tests.rkt b/macrotypes/examples/tests/general-tests.rkt
index 5fa6e70..a490944 100644
--- a/macrotypes/examples/tests/general-tests.rkt
+++ b/macrotypes/examples/tests/general-tests.rkt
@@ -15,9 +15,9 @@
   (define-type-constructor -> #:arity > 0)
   (define-binding-type mu #:arity = 1 #:bvs = 1)
   (define-binding-type forall #:bvs = 1 #:arity = 1)
-  (define-binding-type exist #:extra-info void #:bvs = 1 #:arity = 1)
-  (define-binding-type exist2 #:bvs = 1 #:arity = 1 #:extra-info void)
-  (define-binding-type exist3 #:bvs = 1 #:extra-info void #:arity = 1)
+  (define-binding-type exist #:arr void #:bvs = 1 #:arity = 1)
+  (define-binding-type exist2 #:bvs = 1 #:arity = 1 #:arr void)
+  (define-binding-type exist3 #:bvs = 1 #:arr void #:arity = 1)
   
   (check-stx-err
    (define-binding-type exist4 #:bvs = 1 #:no-attach- #:arity = 1)
@@ -32,5 +32,11 @@
    #:with-msg "expected more terms")
   (check-stx-err
    (define-binding-type exist6 #:bvs = 1 #:bvs = 1)
-   #:with-msg "bad syntax") ; TODO: how to improve this?
+   #:with-msg "too many occurrences of #:bvs keyword")
+  (check-stx-err
+   (define-binding-type exist6 #:arity = 1 #:arity = 1)
+   #:with-msg "too many occurrences of #:arity keyword")
+  (check-stx-err
+   (define-binding-type exist6 #:arr void #:arr void)
+   #:with-msg "too many occurrences of #:arr keyword")
 )
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index 8020d5e..b4b391a 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -457,24 +457,33 @@
              [(_ (~var x id) (... ...))
               #'(begin (define-base-type x) (... ...))]))
          ;; type constructors -------------------------------------------------
+         ;; internal-type-constructor defines:
+         ;; - internal id identifying the constructor
+         ;; - predicate recognizing the internal id
+         ;; - expanded shape of type
+         ;; - pattern expander recognizing the shape
+         ;; - internal contructor τ-
+         ;; internal-type-constructor does no checks:
+         ;; - does not check arity
+         ;; - does not check that inputs are valid types
+         ;; - does not attach a kind to itself
          (define-syntax define-internal-type-constructor
            (syntax-parser
 ;             [(_ (~var x id) . rst)
 ;              #'(define-basic-checked-stx x key2 type #:no-attach-kind . rst)]))
             [(_ (~var τ id)
                 (~or
-                 (~optional ; arity
-                  (~seq #:arity op n:exact-nonnegative-integer)
-                  #:defaults ([op #'=] [n #'1]))
-                 (~optional ; arg-variances
+                 (~optional ; variances
                   (~seq #:arg-variances arg-variances-stx:expr)
+                  #:name "#:arg-variances keyword"
                   #:defaults
                   ([arg-variances-stx
                     #`(λ (stx-id)
-                        (for/list ([arg (in-stx-list (stx-cdr stx-id))])
-                          invariant))]))
+                        (for/list ([_ (in-stx-list (stx-cdr stx-id))])
+                                  invariant))]))
                  (~optional ; extra-info
                   (~seq #:extra-info extra-info)
+                  #:name "#:extra-info keyword"
                   #:defaults ([extra-info #'void]))) (... ...))
 ;              #:with #%kind (mk-#% #'kind)
              #:with τ? (mk-? #'τ)
@@ -495,14 +504,14 @@
                         #'(~and expanded-τ 
                                 (~Any
                                  (~literal/else τ-internal
-                                   (format "Expected ~a type, got: ~a"
-                                           'τ (type->str #'expanded-τ))
+                                   (format "Expected ~a ~a, got: ~a"
+                                           'τ 'name (type->str #'expanded-τ))
                                    #'expanded-τ)
                                  . pat))])))
-                  (define arg-variances arg-variances-stx))
+                  (define arg-vars arg-variances-stx))
                 (define τ-internal
                   (λ _ (raise (exn:fail:type:runtime
-                               (format "~a: Cannot use ~a at run time" 'τ 'kind)
+                               (format "~a: Cannot use ~a at run time" 'τ 'name)
                                (current-continuation-marks)))))
                 ; τ- is an internal constructor:
                 ; It does not validate inputs and does not attach a kind,
@@ -511,58 +520,56 @@
                 (define-syntax (τ- stx)
                   (syntax-parse stx
                     [(_ . args)
-                    #:fail-unless (op (stx-length #'args) n)
-                                  (format "wrong number of arguments, expected ~a ~a"
-                                          'op 'n)
-                     #:with τ-internal*
-                     (add-arg-variances #'τ-internal
-                                        (arg-variances #'(τ . args)))
+                     #:with τ* (add-arg-variances #'τ-internal (arg-vars stx))
                      (syntax/loc stx 
-                       (τ-internal*
-                        (λ () (#%expression extra-info) . args)))]
-                   [_ ;; else fail with err msg
-                    (type-error 
-                     #:src stx
-                     #:msg
-                     (string-append
-                      "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
-                     #'τ stx #'op #'n)])))]))
+                       (τ* (λ () (#%expression extra-info) . args)))])))]))
          (define-syntax define-type-constructor
            (syntax-parser
-            [(_ (~var τ id) . options)
+            [(_ (~var τ id)
+                ;; TODO: allow any order of kws between τ and τ-
+                (~optional ; arity
+                 (~seq #:arity op n:exact-nonnegative-integer)
+                 #:defaults ([op #'=] [n #'1]))
+                 . (~and other-options (~not (#:arity . _))))
              #:with τ- (mk-- #'τ)
              #'(begin
-                 (define-internal-type-constructor τ . options)
+                 (define-internal-type-constructor τ . other-options)
 ;                 #'(define-basic-checked-stx x key2 type . rst)]))
                  (define-syntax (τ stx)
                    (syntax-parse stx
-                    [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
+;                    [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
                     [(_ . args)
+                     #:fail-unless (op (stx-length #'args) n)
+                                   (format
+                                    "wrong number of arguments, expected ~a ~a"
+                                    'op 'n)
                      #:with ([arg- _] (... (... ...))) (infers+erase #'args #:tag 'key2)
                      ;; args are validated on the next line rather than above
                      ;; to ensure enough stx-parse progress for proper err msg,
                      ;; ie, "invalid type" instead of "improper tycon usage"
                      #:with (~! (~var _ type) (... (... ...))) #'(arg- (... (... ...)))
-                     (add-orig (mk-type #'(τ- arg- (... (... ...)))) stx)])))]))
+                     (add-orig (mk-type #'(τ- arg- (... (... ...)))) stx)]
+                    [_ ;; else fail with err msg
+                     (type-error #:src stx
+                      #:msg
+                      (string-append
+                       "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
+                      #'τ stx #'op #'n)])))]))
          (define-syntax define-internal-binding-type
            (syntax-parser
             [(_ (~var τ id)
                 (~or
-                 (~optional ; arity, here it's body exprs
-                  (~seq #:arity op n:exact-nonnegative-integer)
-                  #:defaults ([op #'=] [n #'1]))
-                 (~optional ; bvs, number of type vars to bind
-                  (~seq #:bvs bvs-op bvs-n:exact-nonnegative-integer)
-                  #:defaults ([bvs-op #'>=][bvs-n #'0]))
                  (~optional ; variances
                   (~seq #:arg-variances arg-variances-stx:expr)
+                  #:name "#:arg-variances keyword"
                   #:defaults
                   ([arg-variances-stx
                     #`(λ (stx-id)
-                        (for/list ([arg (in-stx-list (stx-cdr stx-id))])
+                        (for/list ([arg (in-stx-list (stx-cddr stx-id))])
                           invariant))]))
                  (~optional ; extra-info
-                  (~seq #:extra-info extra-info) 
+                  (~seq #:extra-info extra-info)
+                  #:name "#:extra-info keyword"
                   #:defaults ([extra-info #'void]))) (... ...))
              #:with τ? (mk-? #'τ)
              #:with τ- (mk-- #'τ)
@@ -606,9 +613,7 @@
                               ;;                  (detach #'expanded-τ))
                               ;;          (~parse pat
                               ;;                  #'[([tv k] (... (... ...))) rst]))
-                                    (~parse
-                                     pat
-                                     #'[bvs rst]))]
+                              (~parse pat #'[bvs rst]))]
                      ;; TODO: fix this to handle has-annotations?
                      ;; the difference with the first case is that here
                      ;; the body is ungrouped, ie,
@@ -618,16 +623,15 @@
                       #'(~and expanded-τ
                               (~Any/bvs 
                                (~literal/else τ-internal
-                                              (format "Expected ~a type, got: ~a"
-                                                      'τ (type->str #'expanded-τ))
+                                              (format "Expected ~a ~a, got: ~a"
+                                                      'τ 'name (type->str #'expanded-τ))
                                               #'expanded-τ)
-                               bvs-pat
-                               . pat))])))
-                 (define arg-variances arg-variances-stx))
+                               bvs-pat . pat))])))
+                 (define arg-vars arg-variances-stx))
                  ; end define-internal-binding-type begin-for-stx -------------
                 (define τ-internal
                   (λ _ (raise (exn:fail:type:runtime
-                               (format "~a: Cannot use ~a at run time" 'τ 'kind)
+                               (format "~a: Cannot use ~a at run time" 'τ 'name)
                                (current-continuation-marks)))))
                 ; τ- is an internal constructor:
                 ; Tt does not validate inputs and does not attach a kind,
@@ -636,44 +640,47 @@
                 (define-syntax (τ- stx)
                   (syntax-parse stx
                     [(_ bvs . args)
-                     #:fail-unless (bvs-op (stx-length #'bvs) bvs-n)
-                                   (format "wrong number of type vars, expected ~a ~a"
-                                           'bvs-op 'bvs-n)
-                     #:fail-unless (op (stx-length #'args) n)
-                                   (format "wrong number of arguments, expected ~a ~a"
-                                           'op 'n)
-                     #:with τ-internal* (add-arg-variances
-                                         #'τ-internal
-                                         (arg-variances #'(τ- . args))) ; drop bvs
-                     (syntax/loc stx 
-                       (τ-internal* (λ bvs (#%expression extra-info) . args)))]
-                    ;; else fail with err msg
-                    [_
-                     (type-error 
-                      #:src stx
-                      #:msg
-                      (string-append
-                       "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
-                      #'τ stx #'op #'n)])))]))
+                     #:with τ* (add-arg-variances #'τ-internal (arg-vars stx))
+                     (syntax/loc stx
+                       (τ* (λ bvs (#%expression extra-info) . args)))])))]))
          (define-syntax define-binding-type
            (syntax-parser
              [(_ (~var τ id)
-                 (~optional
-                  (~seq #:arr (~and kindcon (~parse has-annotations? #'#t)))
-                  #:defaults ([kindcon #'void])) ; default kindcon should never be used
-                 . other-options)
+                 (~or ;; TODO: allow any order of kws between τ and τ-
+                  (~optional ; arity, ie body exprs
+                   (~seq #:arity op n:exact-nonnegative-integer)
+                   #:name "#:arity keyword"
+                   #:defaults ([op #'=] [n #'1]))
+                  (~optional ; bvs, ie num bindings tyvars
+                   (~seq #:bvs bvs-op bvs-n:exact-nonnegative-integer)
+                   #:name "#:bvs keyword" 
+                   #:defaults ([bvs-op #'>=][bvs-n #'0]))
+                  (~optional ; arr, ie constructor for kind annotations
+                   (~seq #:arr (~and kindcon (~parse has-annotations? #'#t)))
+                   #:name "#:arr keyword"
+                   #:defaults ([kindcon #'void]))) ; dont use kindcon default
+                  (... ...)
+                 . (~and other-options
+                         (~not ((~or #:arity #:bvs #:arr) . _))))
 ;              #'(define-binding-checked-stx x key2 type . rst)])))]))
               #:with τ- (mk-- #'τ)
               #`(begin
                  (define-internal-binding-type τ . other-options)
                  (define-syntax (τ stx)
                    (syntax-parse stx
-                    [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
-                    [(_ (~or (bv:id (... (... ...)))
-                             (~and (~fail #:unless #,(attribute has-annotations?))
-                                   ([_ (~datum key2) _] (... (... ...)))
-                                   bvs+ann))
+;                    [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error
+                    [(_ (~and bvs
+                              (~or (bv:id (... (... ...)))
+                                   (~and (~fail #:unless #,(attribute has-annotations?))
+                                         ([_ (~datum key2) _] (... (... ...)))
+                                         bvs+ann)))
                         . args)
+                     #:fail-unless (bvs-op (stx-length #'bvs) bvs-n)
+                                   (format "wrong number of type vars, expected ~a ~a"
+                                           'bvs-op 'bvs-n)
+                     #:fail-unless (op (stx-length #'args) n)
+                                   (format "wrong number of arguments, expected ~a ~a"
+                                           'op 'n)
                      #:with bvs+ks (if #,(attribute has-annotations?)
                                        #'bvs+ann
                                        #'([bv key2 #%tag] (... (... ...))))
@@ -688,7 +695,13 @@
                                          #'#%tag)
                      (add-orig
                       (attach #'(τ- bvs- . τs-) 'key2 ((current-type-eval) #'k_result))
-                      stx)])))])))]))
+                      stx)]
+                    [_
+                     (type-error #:src stx
+                      #:msg
+                      (string-append
+                       "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
+                      #'τ stx #'op #'n)])))])))]))
 
 ;; end define-syntax-category -------------------------------------------------
 ;; ----------------------------------------------------------------------------
diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt
index 1716695..8f9183c 100644
--- a/turnstile/examples/fomega-no-reuse.rkt
+++ b/turnstile/examples/fomega-no-reuse.rkt
@@ -64,7 +64,7 @@
   (current-check-relation type=?))
 
 ;; kinds ----------------------------------------------------------------------
-(define-internal-kind-constructor ★ #:arity >= 0) ; defines ★-
+(define-internal-kind-constructor ★) ; defines ★-
 (define-syntax (★ stx)
   (syntax-parse stx
     [:id (mk-kind #'(★-))]
@@ -84,7 +84,7 @@
 (define-base-type Float : ★)
 (define-base-type Char : ★)
 
-(define-internal-type-constructor → #:arity >= 0) ; defines →-
+(define-internal-type-constructor →) ; defines →-
 (define-kinded-syntax (→ ty ...+) ≫
   [⊢ ty ≫ ty- ⇒ (~★ . _)] ...
   --------
diff --git a/turnstile/examples/stlc+reco+sub.rkt b/turnstile/examples/stlc+reco+sub.rkt
index 2a64009..efdc9a6 100644
--- a/turnstile/examples/stlc+reco+sub.rkt
+++ b/turnstile/examples/stlc+reco+sub.rkt
@@ -49,4 +49,5 @@
          #'([l τl] ...))]
        [_ #f])))
   (current-sub? sub?)
-  (current-typecheck-relation (current-sub?)))
+  (current-typecheck-relation sub?)
+  (current-check-relation sub?))
diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt
index 658dbdb..964080a 100644
--- a/turnstile/examples/stlc+union+case.rkt
+++ b/turnstile/examples/stlc+union+case.rkt
@@ -97,9 +97,8 @@
        [_ #f])))
   (current-sub? sub?)
   (current-typecheck-relation sub?)
+  (current-check-relation sub?)
   (define (subs? τs1 τs2)
     (and (stx-length=? τs1 τs2)
-         (stx-andmap (current-sub?) τs1 τs2)))
-  
-  )
+         (stx-andmap (current-sub?) τs1 τs2))))
                    
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
index c30d7ca..f23d0c8 100644
--- a/turnstile/examples/stlc+union.rkt
+++ b/turnstile/examples/stlc+union.rkt
@@ -124,6 +124,7 @@
        [_ #f])))
   (define current-sub? (make-parameter sub?))
   (current-typecheck-relation sub?)
+  (current-check-relation sub?)
   (define (subs? τs1 τs2)
     (and (stx-length=? τs1 τs2)
          (stx-andmap (current-sub?) τs1 τs2)))