From 28fa5dd0335a2469ed7b43187f44cdd89da415b7 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 14 Oct 2016 14:16:49 -0400
Subject: [PATCH] split def-kinded-stx from def-typed-stx; split any-type? from
 type?

- the former prevents using current-typecheck-relation at type/kind level
- the latter differentiates "well-formed" types (star)
  from valid types (any kind)
- move define-*ed-syntax and *-eval into define-syntax-category
- turnstile must wrap define-stx-category to define new define-*ed-syntax
- add any-*? pred and any-* stx class in def-stx-category
- fixes #44
- fixes #45
---
 macrotypes/examples/ext-stlc.rkt              |  4 +-
 macrotypes/examples/tests/ext-stlc-tests.rkt  |  4 +-
 macrotypes/examples/tests/infer-tests.rkt     |  4 +-
 macrotypes/examples/tests/mlish-tests.rkt     |  4 +-
 macrotypes/examples/tests/stlc+lit-tests.rkt  |  8 +-
 .../examples/tests/stlc+occurrence-tests.rkt  |  8 +-
 macrotypes/typecheck.rkt                      | 87 +++++++++++--------
 turnstile/examples/ext-stlc.rkt               |  4 +-
 turnstile/examples/fomega-no-reuse.rkt        | 41 +++++----
 turnstile/examples/stlc+union.rkt             |  2 +-
 turnstile/examples/tests/ext-stlc-tests.rkt   |  4 +-
 .../examples/tests/fomega-no-reuse-tests.rkt  |  2 +-
 turnstile/examples/tests/mlish-tests.rkt      |  4 +-
 turnstile/examples/tests/stlc+lit-tests.rkt   |  8 +-
 turnstile/scribblings/reference.scrbl         | 85 +++++++++++-------
 turnstile/turnstile.rkt                       | 31 ++++++-
 16 files changed, 185 insertions(+), 115 deletions(-)

diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt
index 96eacc8..eca5f17 100644
--- a/macrotypes/examples/ext-stlc.rkt
+++ b/macrotypes/examples/ext-stlc.rkt
@@ -42,14 +42,14 @@
 ;; τ.norm in 1st case causes "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
-    [(_ alias:id τ:type)
+    [(_ alias:id τ:any-type)
      #'(define-syntax- alias
          (make-variable-like-transformer #'τ))]
     [(_ (f:id x:id ...) ty)
      #'(define-syntax- (f stx)
          (syntax-parse stx
            [(_ x ...)
-            #:with τ:type #'ty
+            #:with τ:any-type #'ty
             #'τ.norm]))]))
 
 (define-typed-syntax define
diff --git a/macrotypes/examples/tests/ext-stlc-tests.rkt b/macrotypes/examples/tests/ext-stlc-tests.rkt
index ddc56b5..c8594a1 100644
--- a/macrotypes/examples/tests/ext-stlc-tests.rkt
+++ b/macrotypes/examples/tests/ext-stlc-tests.rkt
@@ -50,8 +50,8 @@
                 #:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
-(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
-(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
 (typecheck-fail (ann Int : Int)
                 #:with-msg "ann: type mismatch: expected Int, given #%type\n *expression: Int")
 
diff --git a/macrotypes/examples/tests/infer-tests.rkt b/macrotypes/examples/tests/infer-tests.rkt
index e91c1d7..525bd27 100644
--- a/macrotypes/examples/tests/infer-tests.rkt
+++ b/macrotypes/examples/tests/infer-tests.rkt
@@ -244,8 +244,8 @@
 (typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
-(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
-(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
 (typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
 
 ; let
diff --git a/macrotypes/examples/tests/mlish-tests.rkt b/macrotypes/examples/tests/mlish-tests.rkt
index 50f39f7..c455d80 100644
--- a/macrotypes/examples/tests/mlish-tests.rkt
+++ b/macrotypes/examples/tests/mlish-tests.rkt
@@ -673,8 +673,8 @@
 (typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
-(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
-(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
 (typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
 
 ; let
diff --git a/macrotypes/examples/tests/stlc+lit-tests.rkt b/macrotypes/examples/tests/stlc+lit-tests.rkt
index edb867a..dfcbc3b 100644
--- a/macrotypes/examples/tests/stlc+lit-tests.rkt
+++ b/macrotypes/examples/tests/stlc+lit-tests.rkt
@@ -55,7 +55,7 @@
 
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
 
-(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
+(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a well-formed type")
diff --git a/macrotypes/examples/tests/stlc+occurrence-tests.rkt b/macrotypes/examples/tests/stlc+occurrence-tests.rkt
index 5797b57..ba85f08 100644
--- a/macrotypes/examples/tests/stlc+occurrence-tests.rkt
+++ b/macrotypes/examples/tests/stlc+occurrence-tests.rkt
@@ -237,16 +237,16 @@
 (typecheck-fail
  (λ ([x : (∪ Int Boolean)])
     (test (1 ? x) #t #f))
- #:with-msg "not a valid type")
+ #:with-msg "not a well-formed type")
 (typecheck-fail
  (test (1 ? 1) #t #f)
- #:with-msg "not a valid type")
+ #:with-msg "not a well-formed type")
 (typecheck-fail
  (test (1 ? 1) #t #f)
- #:with-msg "not a valid type")
+ #:with-msg "not a well-formed type")
 (typecheck-fail
  (test (#f ? #t) #t #f)
- #:with-msg "not a valid type")
+ #:with-msg "not a well-formed type")
 
 ;; -----------------------------------------------------------------------------
 ;; --- Subtypes should not be collapsed
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index c290c8b..9ed4b8a 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -64,6 +64,7 @@
   (define (mk-- id) (format-id id "~a-" id))
   (define (mk-~ id) (format-id id "~~~a" id))
   (define (mk-#% id) (format-id id "#%~a" id))
+  (define (mk-param id) (format-id id "current-~a" id))
   (define-for-syntax (mk-? id) (format-id id "~a?" id))
   (define-for-syntax (mk-~ id) (format-id id "~~~a" id))
   ;; drop-file-ext : String -> String
@@ -401,21 +402,6 @@
     (syntax-parse (infer es #:tvctx ctx)
       [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
 
-  ; extra indirection, enables easily overriding type=? with sub?
-  ; to add subtyping, without changing any other definitions
-  ; - must be here (instead of stlc) due to rackunit-typechecking
-  (define current-typecheck-relation (make-parameter #f))
-
-  ;; convenience fns for current-typecheck-relation
-  (define (typecheck? t1 t2)
-    ((current-typecheck-relation) t1 t2))
-  (define (typechecks? τs1 τs2)
-    (and (= (stx-length τs1) (stx-length τs2))
-         (stx-andmap typecheck? τs1 τs2)))
-  
-  (define current-type-eval (make-parameter #f))
-  (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
-
   (define current-promote (make-parameter (λ (t) t)))
 
   ;; term expansion
@@ -429,22 +415,6 @@
   (define (expand/df e)
     (local-expand e 'expression null))
 
-  ;; type eval
-  ;; - default-type-eval == full expansion == canonical type representation
-  ;; - must expand because:
-  ;;   - checks for unbound identifiers (ie, undefined types)
-  ;;   - checks for valid types, ow can't distinguish types and terms
-  ;;     - could parse types but separate parser leads to duplicate code
-  ;;   - later, expanding enables reuse of same mechanisms for kind checking
-  ;;     and type application
-  (define (default-type-eval τ)
-    ; TODO: optimization: don't expand if expanded
-    ; currently, this causes problems when
-    ; combining unexpanded and expanded types to create new types
-    (add-orig (expand/df τ) τ))
-
-  (current-type-eval default-type-eval)
-
   ;; typecheck-fail-msg/1 : Type Type Stx -> String
   (define (typecheck-fail-msg/1 τ_expected τ_given expression)
     (format "type mismatch: expected ~a, given ~a\n  expression: ~s"
@@ -862,12 +832,21 @@
   (syntax-parse stx
     [(_ name:id)
      #:with names (format-id #'name "~as" #'name)
-     #:with #%tag (format-id #'name "#%~a" #'name)
+     #:with #%tag (mk-#% #'name)
      #:with #%tag? (mk-? #'#%tag)
      #:with is-name? (mk-? #'name)
+     #:with any-name (format-id #'name "any-~a" #'name)
+     #:with any-name? (mk-? #'any-name)
      #:with name-ctx (format-id #'name "~a-ctx" #'name)
      #:with name-bind (format-id #'name "~a-bind" #'name)
-     #:with current-is-name? (format-id #'is-name? "current-~a" #'is-name?)
+     #:with current-is-name? (mk-param #'is-name?)
+     #:with current-any-name? (mk-param #'any-name?)
+     #:with current-namecheck-relation (format-id #'name "current-~acheck-relation" #'name)
+     #:with namecheck? (format-id #'name "~acheck?" #'name)
+     #:with namechecks? (format-id #'name "~achecks?" #'name)
+     #:with current-name-eval (format-id #'name "current-~a-eval" #'name)
+     #:with default-name-eval (format-id #'name "default-~a-eval" #'name)
+     #:with name-evals (format-id #'name "~a-evals" #'name)
      #:with mk-name (format-id #'name "mk-~a" #'name)
      #:with define-base-name (format-id #'name "define-base-~a" #'name)
      #:with define-base-names (format-id #'name "define-base-~as" #'name)
@@ -878,15 +857,19 @@
      #:with name-ann (format-id #'name "~a-ann" #'name)
      #:with name=? (format-id #'name "~a=?" #'name)
      #:with names=? (format-id #'names "~a=?" #'names)
-     #:with current-name=? (format-id #'name=? "current-~a" #'name=?)
+     #:with current-name=? (mk-param #'name=?)
      #:with same-names? (format-id #'name "same-~as?" #'name)
      #:with name-out (format-id #'name "~a-out" #'name)
      #'(begin
          (define #%tag void)
          (begin-for-syntax
            (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag)))
+           ;; is-name?, eg type?, corresponds to "well-formed" types
            (define (is-name? t) (#%tag? (typeof t)))
            (define current-is-name? (make-parameter is-name?))
+           ;; any-name? corresponds to any type and defaults to is-name?
+           (define (any-name? t) (is-name? t))
+           (define current-any-name? (make-parameter any-name?))
            (define (mk-name t) (assign-type t #'#%tag))
            (define-syntax-class name
              #:attributes (norm)
@@ -894,6 +877,15 @@
               #:with norm ((current-type-eval) #'τ)
               #:with k (typeof #'norm)
               #:fail-unless ((current-is-name?) #'norm)
+              (format "~a (~a:~a) not a well-formed ~a: ~a"
+                      (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
+                      'name (type->str #'τ))))
+           (define-syntax-class any-name
+             #:attributes (norm)
+             (pattern τ
+              #:with norm ((current-type-eval) #'τ)
+              #:with k (typeof #'norm)
+              #:fail-unless ((current-any-name?) #'norm)
               (format "~a (~a:~a) not a valid ~a: ~a"
                       (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
                       'name (type->str #'τ))))
@@ -943,14 +935,37 @@
                    [_ (and (stx-pair? t1) (stx-pair? t2)
                            (names=? t1 t2))])))
            (define current-name=? (make-parameter name=?))
-           (current-typecheck-relation name=?)
            (define (names=? τs1 τs2)
              (and (stx-length=? τs1 τs2)
                   (stx-andmap (current-name=?) τs1 τs2)))
+           ; extra indirection, enables easily overriding type=? with sub?
+           ; to add subtyping, without changing any other definitions
+           (define current-namecheck-relation (make-parameter name=?))
+           ;; convenience fns for current-typecheck-relation
+           (define (namecheck? t1 t2)
+             ((current-namecheck-relation) t1 t2))
+           (define (namechecks? τs1 τs2)
+             (and (= (stx-length τs1) (stx-length τs2))
+                  (stx-andmap namecheck? τs1 τs2)))
            (define (same-names? τs)
              (define τs-lst (syntax->list τs))
              (or (null? τs-lst)
-                 (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst)))))
+                 (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst))))
+           ;; type eval
+           ;; - default-type-eval == full expansion == canonical type representation
+           ;; - must expand because:
+           ;;   - checks for unbound identifiers (ie, undefined types)
+           ;;   - checks for valid types, ow can't distinguish types and terms
+           ;;     - could parse types but separate parser leads to duplicate code
+           ;;   - later, expanding enables reuse of same mechanisms for kind checking
+           ;;     and type application
+           (define (default-name-eval τ)
+             ; TODO: optimization: don't expand if expanded
+             ; currently, this causes problems when
+             ; combining unexpanded and expanded types to create new types
+             (add-orig (expand/df τ) τ))
+           (define current-name-eval (make-parameter default-name-eval))
+           (define (name-evals τs) #`#,(stx-map (current-name-eval) τs)))
          ;; helps with providing defined types
          (define-syntax name-out
            (make-provide-transformer
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
index 1302385..cdc10a8 100644
--- a/turnstile/examples/ext-stlc.rkt
+++ b/turnstile/examples/ext-stlc.rkt
@@ -41,14 +41,14 @@
 ;; τ.norm in 1st case causes "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
-    [(_ alias:id τ:type)
+    [(_ alias:id τ:any-type)
      #'(define-syntax- alias
          (make-variable-like-transformer #'τ))]
     [(_ (f:id x:id ...) ty)
      #'(define-syntax- (f stx)
          (syntax-parse stx
            [(_ x ...)
-            #:with τ:type #'ty
+            #:with τ:any-type #'ty
             #'τ.norm]))]))
 
 (define-typed-syntax define
diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt
index 193dab8..034ea1f 100644
--- a/turnstile/examples/fomega-no-reuse.rkt
+++ b/turnstile/examples/fomega-no-reuse.rkt
@@ -15,12 +15,17 @@
 (define-syntax-category kind)
 
 ;; redefine:
-;; - current-type? - recognizes types with ★ kind only
-;; - current-type-eval - reduce tylams and tyapps
-;; - current-type=? - must check for any kind annotations
+;; - current-type?: well-formed types have kind ★
+;; - current-any-type?: valid types have any valid kind
+;; - current-type-eval: reduce tylams and tyapps
+;; - current-type=?: must compare kind annotations as well
 (begin-for-syntax
-  ;; need this for define-primop (which still uses type stx-class)
+  
+  ;; well-formed types have kind ★
+  ;; (need this for define-primop, which still uses type stx-class)
   (current-type? (λ (t) (★? (typeof t))))
+  ;; o.w., a valid type is one with any valid kind
+  (current-any-type? (λ (t) ((current-kind?) (typeof t))))
 
   ;; TODO: I think this can be simplified
   (define (normalize τ)
@@ -47,11 +52,12 @@
   ; ty=? == syntax eq and syntax prop eq
   (define (type=? t1 t2)
     (let ([k1 (typeof t1)][k2 (typeof t2)])
-      (and (or (and (not k1) (not k2)) ; need this bc there's no current-kindcheck-rel
+      ; the extra `and` and `or` clauses are bc type=? is a structural
+      ; traversal on stx objs, so not all sub stx objs will have a "type"-stx
+      (and (or (and (not k1) (not k2))
                (and k1 k2 ((current-kind=?) k1 k2)))
            (old-type=? t1 t2))))
   (current-type=? type=?)
-  ;; TODO: add current-kindcheck-rel
   (current-typecheck-relation (current-type=?)))
 
 ;; kinds ----------------------------------------------------------------------
@@ -64,13 +70,10 @@
 (define-kind-constructor ⇒ #:arity >= 1)
 
 ;; types ----------------------------------------------------------------------
-(define-typed-syntax (define-type-alias alias:id τ) ≫
-  [⊢ τ ≫ τ- ⇒ k_τ]
-  #:fail-unless ((current-kind?) #'k_τ)
-                (format "not a valid type: ~a\n" (type->str #'τ))
+(define-kinded-syntax (define-type-alias alias:id τ:any-type) ≫
   ------------------
   [≻ (define-syntax- alias 
-       (make-variable-like-transformer #'τ-))])
+       (make-variable-like-transformer #'τ.norm))])
 
 (define-base-type Int : ★)
 (define-base-type Bool : ★)
@@ -79,26 +82,26 @@
 (define-base-type Char : ★)
 
 (define-internal-type-constructor →) ; defines →-
-(define-typed-syntax (→ ty ...+) ≫
+(define-kinded-syntax (→ ty ...+) ≫
   [⊢ ty ≫ ty- ⇒ (~★ . _)] ...
   --------
   [⊢ (→- ty- ...) ⇒ ★])
 
 (define-internal-binding-type ∀) ; defines ∀-
-(define-typed-syntax ∀ #:datum-literals (:)
+(define-kinded-syntax ∀ #:datum-literals (:)
   [(_ ([tv:id : k_in:kind] ...) ty) ≫
    [[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
    -------
    [⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
 
-(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
+(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
   [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
   #:fail-unless ((current-kind?) #'k_body)
                 (format "not a valid type: ~a\n" (type->str #'τ_body))
   --------
   [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
 
-(define-typed-syntax (tyapp τ_fn τ_arg ...) ≫
+(define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫
   [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
   #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
                 (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
@@ -156,9 +159,15 @@
   --------
   [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
 
+;; TODO: what to do when a def-typed-stx needs both
+;; current-typecheck-relation and current-kindcheck-relation
 (define-typed-syntax (inst e τ ...) ≫
   [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
-  [⊢ τ ≫ τ- ⇐ k] ...
+;  [⊢ τ ≫ τ- ⇐ k] ...
+  ;; want to use kindchecks? instead of typechecks?
+  [⊢ τ ≫ τ- ⇒ k_τ] ...
+  #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
+                (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
   [⊢ e- ⇒ τ-inst])
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
index 5a65764..c30d7ca 100644
--- a/turnstile/examples/stlc+union.rkt
+++ b/turnstile/examples/stlc+union.rkt
@@ -31,7 +31,7 @@
 
 (define-syntax define-named-type-alias
   (syntax-parser
-    [(define-named-type-alias Name:id τ:type)
+    [(define-named-type-alias Name:id τ:any-type)
      #'(define-syntax Name
          (make-variable-like-transformer (add-orig #'τ #'Name)))]
     [(define-named-type-alias (f:id x:id ...) ty) ; dont expand yet
diff --git a/turnstile/examples/tests/ext-stlc-tests.rkt b/turnstile/examples/tests/ext-stlc-tests.rkt
index 704f6d4..881819e 100644
--- a/turnstile/examples/tests/ext-stlc-tests.rkt
+++ b/turnstile/examples/tests/ext-stlc-tests.rkt
@@ -50,8 +50,8 @@
                 #:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
-(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
-(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
 (typecheck-fail (ann Int : Int)
                 #:with-msg "ann: type mismatch: expected Int, given #%type\n *expression: Int")
 
diff --git a/turnstile/examples/tests/fomega-no-reuse-tests.rkt b/turnstile/examples/tests/fomega-no-reuse-tests.rkt
index 6a25710..1a7fd6b 100644
--- a/turnstile/examples/tests/fomega-no-reuse-tests.rkt
+++ b/turnstile/examples/tests/fomega-no-reuse-tests.rkt
@@ -54,7 +54,7 @@
             : (→ (→ Int String) (→ Int String)))
 (typecheck-fail
  (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
- #:with-msg "inst: type mismatch: expected ★, given Int\n *expression: 1")
+ #:with-msg "inst: type mismatch.*expected:.*★.*given:.*Int.*expressions: 1")
 
 (typecheck-fail
  (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
diff --git a/turnstile/examples/tests/mlish-tests.rkt b/turnstile/examples/tests/mlish-tests.rkt
index 39c0ffe..d05641e 100644
--- a/turnstile/examples/tests/mlish-tests.rkt
+++ b/turnstile/examples/tests/mlish-tests.rkt
@@ -669,8 +669,8 @@
 (typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
 ;ann errs
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
-(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
-(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
 (typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
 
 ; let
diff --git a/turnstile/examples/tests/stlc+lit-tests.rkt b/turnstile/examples/tests/stlc+lit-tests.rkt
index c0afec6..3475eb6 100644
--- a/turnstile/examples/tests/stlc+lit-tests.rkt
+++ b/turnstile/examples/tests/stlc+lit-tests.rkt
@@ -54,10 +54,10 @@
 
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
 
-(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
-(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
+(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a well-formed type")
+(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a well-formed type")
 
 (typecheck-fail
  (ann (ann 5 : Int) : (→ Int))
diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl
index 8173615..ae54178 100644
--- a/turnstile/scribblings/reference.scrbl
+++ b/turnstile/scribblings/reference.scrbl
@@ -112,8 +112,6 @@ Dually, one may write @racket[[⊢ e ≫ e- ⇐ τ]] to check that @racket[e] ha
 @racket[τ]. Here, both @racket[e] and @racket[τ] are inputs (templates) and only
  @racket[e-] is an output (pattern).}
 
-@defform[(define-typerule ....)]{An alias for @racket[define-typed-syntax].}
-
 @defform*[((define-primop typed-op-id τ)
            (define-primop typed-op-id : τ)
            (define-primop typed-op-id op-id τ)
@@ -135,11 +133,18 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
  use any forms other than @racket[define-base-type] and
  @racket[define-type-constructor] in conjunction with @racket[define-typed-syntax]. The other forms are considered "low-level" and are automatically used by @racket[define-typed-syntax].
  @itemlist[
- @item{@defform[(define-base-type base-type-name-id)]{
-   Defines a base type. A @racket[(define-base-type τ)] additionally defines:
+ @item{@racket[define-typed-syntax], as described above.
+   Uses @racket[current-typecheck-relation] for typechecking.}
+ @item{@defform[(define-typerule ....)]{An alias for @racket[define-typed-syntax].}}
+ @item{@defform*[((define-base-type base-type-name-id)
+                  (define-base-type base-type-name-id : kind))]{
+   Defines a base type. @racket[(define-base-type τ)] in turn defines:
   @itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].}
             @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
-            @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]}}
+            @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]}
+
+  The second form is useful when implementing your own kind system.
+   @racket[#%type] is used as the @tt{kind} when it's not specified.}
  @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types.}}
  @item{
   @defform[(define-type-constructor name-id option ...)
@@ -235,6 +240,33 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
 A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id], 
 and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-expander @racket[~ty-id].}}
 
+@item{@defparam[current-type-eval type-eval type-eval]{
+ A phase 1 parameter for controlling "type evaluation". A @racket[type-eval]
+function consumes and produces syntax. It is typically used to convert a type
+into a canonical representation. The @racket[(current-type-eval)] is called
+immediately before attacing a type to a syntax object, i.e., by
+@racket[assign-type].
+
+ It defaults to full expansion, i.e., @racket[(lambda (stx) (local-expand stx 'expression null))], and also stores extra surface syntax information used for error reporting.
+
+One should extend @racket[current-type-eval] if canonicalization of types
+depends on combinations of different types, e.g., type lambdas and type application in F-omega. }}
+
+@item{@defparam[current-typecheck-relation type-pred type-pred]{
+ A phase 1 parameter for controlling type checking, used by @racket[define-type-syntax].
+  A @racket[type-pred] function consumes
+ two types and returns true if they "type check". It defaults to @racket[type=?] though it does not have to be a symmetric relation.
+Useful for reusing rules that differ only in the type check operation, e.g.,
+ equality vs subtyping.}}
+
+@item{@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 function that calls
+ @racket[current-typecheck-relation].}}
+
+@item{@defproc[(typechecks? [τs1 (or/c (list/c type?) (stx-list/c type?))]
+                      [τs2 (or/c (list/c type?) (stx-list/c type?))]) boolean?]{
+Phase 1 function mapping @racket[typecheck?] over lists of types, pairwise. @racket[τs1] and @racket[τs2]
+must have the same length.}}
+
  @item{@defproc[(type=? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 equality
 predicate for types that computes structural, @racket[free-identifier=?]
 equality, but includes alpha-equivalence.
@@ -270,15 +302,28 @@ equality, but includes alpha-equivalence.
     A phase 1 parameter for computing type equality. Is initialized to @racket[type=?].}}
  @item{@defidform[#%type]{The default "kind" used to validate types.}}
  @item{@defproc[(#%type? [x Any]) boolean?]{Phase 1 predicate recognizing @racket[#%type].}}
- @item{@defproc[(type? [x Any]) boolean?]{A phase 1 predicate used to validate types.
+ @item{@defproc[(type? [x Any]) boolean?]{A phase 1 predicate recognizing well-formed types.
     Checks that @racket[x] is a syntax object and has syntax propety @racket[#%type].}}
  @item{@defparam[current-type? type-pred type-pred]{A phase 1 parameter, initialized to @racket[type?],
-    used to validate types. Useful when reusing type rules in different languages.}}
+    used to recognize well-formed types.
+    Useful when reusing type rules in different languages. For example,
+    System F-omega may define this to recognize types with "star" kinds.}}
+ @item{@defproc[(any-type? [x Any]) boolean?]{A phase 1 predicate recognizing valid types.
+    Defaults to @racket[type?].}}
+ @item{@defparam[current-any-type? type-pred type-pred]{A phase 1 parameter,
+    initialized to @racket[any-type?],
+    used to validate (not necessarily well-formed) types.
+    Useful when reusing type rules in different languages. For example,
+    System F-omega may define this to recognize types with a any valid kind,
+    whereas @racket[current-type?] would recognize types with only the "star" kind.}}
  @item{@defproc[(mk-type [stx syntax?]) type?]{
     Phase 1 function that marks a syntax object as a type by attaching @racket[#%type].
   Useful for defining your own type with arbitrary syntax that does not fit with
     @racket[define-base-type] or @racket[define-type-constructor].}}
  @item{@defthing[type stx-class]{A syntax class that calls @racket[current-type?]
+    to validate well-formed types.
+  Binds a @racket[norm] attribute to the type's expanded representation.}}
+ @item{@defthing[any-type stx-class]{A syntax class that calls @racket[current-any-type?]
     to validate types.
   Binds a @racket[norm] attribute to the type's expanded representation.}}
  @item{@defthing[type-bind stx-class]{A syntax class recognizing
@@ -335,32 +380,6 @@ necessary to call these directly, since @racket[define-typed-syntax] and other
 forms already do so, but some type systems may require extending some
 functionality.
 
-@defparam[current-type-eval type-eval type-eval]{
- A phase 1 parameter for controlling "type evaluation". A @racket[type-eval]
-function consumes and produces syntax. It is typically used to convert a type
-into a canonical representation. The @racket[(current-type-eval)] is called
-immediately before attacing a type to a syntax object, i.e., by
-@racket[assign-type].
-
- It defaults to full expansion, i.e., @racket[(lambda (stx) (local-expand stx 'expression null))], and also stores extra surface syntax information used for error reporting.
-
-One should extend @racket[current-type-eval] if canonicalization of types
-depends on combinations of different types, e.g., type lambdas and type application in F-omega. }
-
-@defparam[current-typecheck-relation type-pred type-pred]{
- A phase 1 parameter for controlling type checking. A @racket[type-pred] function consumes
- two types and returns true if they "type check". It defaults to @racket[type=?] though it does not have to be a symmetric relation.
-Useful for reusing rules that differ only in the type check operation, e.g.,
- equality vs subtyping.}
-
-@defproc[(typecheck? [τ1 type?] [τ2 type?]) boolean?]{A phase 1 function that calls
- @racket[current-typecheck-relation].}
-
-@defproc[(typechecks? [τs1 (or/c (list/c type?) (stx-list/c type?))]
-                      [τs2 (or/c (list/c type?) (stx-list/c type?))]) boolean?]{
-Phase 1 function mapping @racket[typecheck?] over lists of types, pairwise. @racket[τs1] and @racket[τs2]
-must have the same length.}
-
 @defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{
 Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e]}
 
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index 43fcf4e..d345217 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -1,13 +1,15 @@
 #lang racket/base
 
-(provide (except-out (all-from-out macrotypes/typecheck) -define-typed-syntax)
-         define-typed-syntax
+(provide (except-out (all-from-out macrotypes/typecheck) 
+                     -define-typed-syntax -define-syntax-category)
+         define-typed-syntax define-syntax-category
          (rename-out [define-typed-syntax define-typerule])
          (for-syntax syntax-parse/typed-syntax))
 
 (require (except-in (rename-in
                      macrotypes/typecheck
                      [define-typed-syntax -define-typed-syntax]
+                     [define-syntax-category -define-syntax-category]
                      )
                     #%module-begin))
 
@@ -418,3 +420,28 @@
              rule.norm
              ...)]))))
 
+(define-syntax define-syntax-category
+ (lambda (stx)
+   (syntax-parse stx
+    [(_ name:id)
+     #:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name)
+     #:with check-relation (format-id #'name "current-~acheck-relation" #'name)
+     #'(begin
+        (-define-syntax-category name)
+        (define-syntax (def-named-syntax stx)
+          (syntax-parse stx
+            ;; single-clause def
+           [(_ (rulename:id . pats) . rst)
+            ;; cannot bind name as pat var, eg #%app, so replace with _
+            #:with r #'[(_ . pats) . rst]
+            #'(define-syntax (rulename stxx)
+                (parameterize ([current-typecheck-relation (check-relation)])
+                  (syntax-parse/typed-syntax stxx r)))]
+           ;; multi-clause def
+           [(_ rulename:id
+              (~and (~seq kw-stuff (... ...)) :stxparse-kws)
+              rule:rule (... ...+))
+            #'(define-syntax (rulename stxx)
+                (parameterize ([current-typecheck-relation (check-relation)])
+                  (syntax-parse/typed-syntax stxx kw-stuff (... ...)
+                    rule (... ...))))])))])))