From 98568ceb9984222f42a0f41bb27b28d9aae737b7 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 13 Oct 2016 21:21:05 -0400
Subject: [PATCH] add define-internal-type-constructor and
 define-internal-binding-type

- add fomega-no-reuse example
---
 macrotypes/typecheck.rkt                      |  26 ++-
 turnstile/examples/fomega-no-reuse.rkt        | 165 ++++++++++++++
 .../examples/tests/fomega-no-reuse-tests.rkt  | 213 ++++++++++++++++++
 turnstile/examples/tests/run-all-tests.rkt    |   1 +
 turnstile/scribblings/reference.scrbl         |  25 +-
 5 files changed, 422 insertions(+), 8 deletions(-)
 create mode 100644 turnstile/examples/fomega-no-reuse.rkt
 create mode 100644 turnstile/examples/tests/fomega-no-reuse-tests.rkt

diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index f201e1c..c290c8b 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -688,7 +688,9 @@
               (syntax/loc stx 
                 (τ-internal* (λ () (#%expression extra-info) . args)))]))
          ; this is the actual constructor
-         (define-syntax (τ stx)
+         #,@(if (attribute no-attach-kind?)
+               #'()
+          #'((define-syntax (τ stx)
            (syntax-parse stx
              [(_ . args)
               #:fail-unless (op (stx-length #'args) n)
@@ -708,7 +710,7 @@
                #:msg
                  (string-append
                   "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
-                 #'τ stx #'op #'n)])))]))
+                 #'τ stx #'op #'n)])))))]))
 
 ;; Form for defining *binding* types, kinds, etc.
 ;; The def uses pattern vars "τ" and "kind" but this form is not restricted to
@@ -817,7 +819,9 @@
               (syntax/loc stx 
                 (τ-internal* (λ bvs (#%expression extra-info) . args)))]))
          ; this is the actual constructor
-         (define-syntax (τ stx)
+         #,@(if (attribute no-attach-kind?)
+               #'()
+               #`((define-syntax (τ stx)
            (syntax-parse stx
              [(_ (~or (bv:id (... ...))
                       (~and (~fail #:unless #,(attribute has-annotations?))
@@ -833,20 +837,23 @@
                             (format "wrong number of arguments, expected ~a ~a"
                                     'op 'n)
               #:with (bvs- τs- _) (infers/ctx+erase #'bvs+ks #'args)
+              ;; the args are validated on the next line, rather than above
+              ;; to ensure enough stx-parse progress so we get a proper err msg,
+              ;; ie, "invalid type" instead of "improper tycon usage"
               #:with (~! (~var _ kind) (... ...)) #'τs-
               #:with ([tv (~datum :) k_arg] (... ...)) #'bvs+ks
               #:with k_result (if #,(attribute has-annotations?)
                                   #'(kindcon k_arg (... ...))
                                   #'#%kind)
-;              #:with ty-out (expand/df #'(τ- bvs- . τs-))
-              #:with ty-out #'(τ- bvs- . τs-)
-              (add-orig (assign-type #'ty-out #'k_result) stx)]
+              (add-orig
+               (assign-type #'(τ- bvs- . τs-) #'k_result)
+               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)])))]))
+                          #'τ stx #'op #'n)])))))]))
 
 ; examples:
 ; (define-syntax-category type)
@@ -867,6 +874,7 @@
      #:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
      #:with define-binding-name (format-id #'name "define-binding-~a" #'name)
      #:with define-internal-name-cons (format-id #'name "define-internal-~a-constructor" #'name)
+     #:with define-internal-binding-name (format-id #'name "define-internal-binding-~a" #'name)
      #:with name-ann (format-id #'name "~a-ann" #'name)
      #:with name=? (format-id #'name "~a=?" #'name)
      #:with names=? (format-id #'names "~a=?" #'names)
@@ -971,6 +979,10 @@
            (syntax-parser
              [(_ (~var x id) . rst)
               #'(define-basic-checked-stx x : name #:no-attach-kind . rst)]))
+         (define-syntax define-internal-binding-name
+           (syntax-parser
+             [(_ (~var x id) . rst)
+              #'(define-binding-checked-stx x : name #:no-attach-kind . rst)]))
          (define-syntax define-name-cons
            (syntax-parser
              [(_ (~var x id) . rst)
diff --git a/turnstile/examples/fomega-no-reuse.rkt b/turnstile/examples/fomega-no-reuse.rkt
new file mode 100644
index 0000000..193dab8
--- /dev/null
+++ b/turnstile/examples/fomega-no-reuse.rkt
@@ -0,0 +1,165 @@
+#lang turnstile/lang
+
+;; System F_omega, without reusing rules from other languages
+;; - try to avoid using built-in "kind" system (ie #%type)
+;;   - not quite there: define-primop and typed-out still use current-type?
+;; - use define-internal- forms instead
+
+;; example suggested by Alexis King
+
+(provide define-type-alias
+         ★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp
+         (typed-out [+ : (→ Int Int Int)])
+         λ #%app #%datum Λ inst ann)
+
+(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
+(begin-for-syntax
+  ;; need this for define-primop (which still uses type stx-class)
+  (current-type? (λ (t) (★? (typeof t))))
+
+  ;; TODO: I think this can be simplified
+  (define (normalize τ)
+    (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
+      [x:id #'x]
+      [(#%plain-app 
+        (#%plain-lambda (tv ...) τ_body) τ_arg ...)
+       (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+      [(#%plain-lambda (x ...) . bodys)
+       #:with bodys_norm (stx-map normalize #'bodys)
+       (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)]
+      [(#%plain-app x:id . args)
+       #:with args_norm (stx-map normalize #'args)
+       (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)]
+      [(#%plain-app . args)
+       #:with args_norm (stx-map normalize #'args)
+       #:with res (normalize #'(#%plain-app . args_norm))
+       (transfer-stx-props #'res τ #:ctx τ)]
+      [_ τ]))
+  (define old-eval (current-type-eval))
+  (current-type-eval (lambda (τ) (normalize (old-eval τ))))
+  
+  (define old-type=? (current-type=?))
+  ; 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
+               (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 ----------------------------------------------------------------------
+(define-internal-kind-constructor ★ #:arity >= 0) ; defines ★-
+(define-syntax (★ stx)
+  (syntax-parse stx
+    [:id (mk-kind #'(★-))]
+    [(_ k:kind ...) (mk-kind #'(★- k.norm ...))]))
+
+(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-syntax- alias 
+       (make-variable-like-transformer #'τ-))])
+
+(define-base-type Int : ★)
+(define-base-type Bool : ★)
+(define-base-type String : ★)
+(define-base-type Float : ★)
+(define-base-type Char : ★)
+
+(define-internal-type-constructor →) ; defines →-
+(define-typed-syntax (→ ty ...+) ≫
+  [⊢ ty ≫ ty- ⇒ (~★ . _)] ...
+  --------
+  [⊢ (→- ty- ...) ⇒ ★])
+
+(define-internal-binding-type ∀) ; defines ∀-
+(define-typed-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) ≫
+  [[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 ...) ≫
+  [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
+  #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
+                (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
+  [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
+  --------
+  [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])
+
+;; terms ----------------------------------------------------------------------
+(define-typed-syntax λ #:datum-literals (:)
+  [(_ ([x:id : τ_in:type] ...) e) ≫
+   [[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out]
+   -------
+   [⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
+  [(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
+   [[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]
+   ---------
+   [⊢ (λ- (x- ...) e-)]])
+
+(define-typed-syntax (#%app e_fn e_arg ...) ≫
+  [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
+  #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+                (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+  [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+  --------
+  [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])
+
+(define-typed-syntax (ann e (~datum :) τ:type) ≫
+  [⊢ e ≫ e- ⇐ τ.norm]
+  --------
+  [⊢ e- ⇒ τ.norm])
+
+(define-typed-syntax #%datum
+  [(_ . b:boolean) ≫
+   --------
+   [⊢ (#%datum- . b) ⇒ Bool]]
+  [(_ . s:str) ≫
+   --------
+   [⊢ (#%datum- . s) ⇒ String]]
+  [(_ . f) ≫
+   #:when (flonum? (syntax-e #'f))
+   --------
+   [⊢ (#%datum- . f) ⇒ Float]]
+  [(_ . c:char) ≫
+   --------
+   [⊢ (#%datum- . c) ⇒ Char]]
+  [(_ . n:integer) ≫
+   --------
+   [⊢ (#%datum- . n) ⇒ Int]]
+  [(_ . x) ≫
+   --------
+   [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
+
+(define-typed-syntax (Λ bvs:kind-ctx e) ≫
+  [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
+  --------
+  [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+
+(define-typed-syntax (inst e τ ...) ≫
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))]
+  [⊢ τ ≫ τ- ⇐ k] ...
+  #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+  --------
+  [⊢ e- ⇒ τ-inst])
+
diff --git a/turnstile/examples/tests/fomega-no-reuse-tests.rkt b/turnstile/examples/tests/fomega-no-reuse-tests.rkt
new file mode 100644
index 0000000..6a25710
--- /dev/null
+++ b/turnstile/examples/tests/fomega-no-reuse-tests.rkt
@@ -0,0 +1,213 @@
+#lang s-exp "../fomega-no-reuse.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; identical to fomega-tests.rkt
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
+                (∀ ([X : (★ ★)]) (→ X X)))
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+           : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
+(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+
+(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+            : (⇒ ★ ★))
+;; f's type must have kind ★
+(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+            (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+(check-type (inst
+             (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+             (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+            : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst: type mismatch: expected ★, given Int\n *expression: 1")
+
+(typecheck-fail
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
+;; applied f too early
+(typecheck-fail
+ (inst
+  (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+  (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ #:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
+(check-type ((inst
+              (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+              (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1)
+ #:with-msg "not a valid type: 1")
+(define-type-alias Id (tyλ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (⇒ ★ ★ ★))
+(check-type Pair : (⇒ ★ ★ (★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String)
+ : (→ Int String (tyapp Pair Int String)))
+;; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String) 1 "1")
+ : (tyapp Pair Int String))
+;; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
+;; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+  Int String)
+ : (→ (tyapp Pair Int String) Int))
+;; apply fst
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : Int ⇒ 1)
+;; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  Int String)
+ : (→ (tyapp Pair Int String) String))
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : String ⇒ "1")
+
+;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+             (Λ ([s : ★]) (λ ([y : s]) y)))
+             : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/turnstile/examples/tests/run-all-tests.rkt b/turnstile/examples/tests/run-all-tests.rkt
index fe602d0..e4f267d 100644
--- a/turnstile/examples/tests/run-all-tests.rkt
+++ b/turnstile/examples/tests/run-all-tests.rkt
@@ -26,6 +26,7 @@
 (require "fomega-tests.rkt")
 (require "fomega2-tests.rkt")
 (require "fomega3-tests.rkt")
+(require "fomega-no-reuse-tests.rkt")
 
 ;; these are not ported to turnstile yet
 ;; see macrotypes/examples/tests/run-all-tests.rkt
diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl
index 5b257fb..8173615 100644
--- a/turnstile/scribblings/reference.scrbl
+++ b/turnstile/scribblings/reference.scrbl
@@ -150,7 +150,12 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
     Defines a type constructor that does not bind type variables.
     Defining a type constructor @racket[τ] defines:
   @itemlist[@item{@racket[τ], a macro for constructing an instance of type
-                  @racket[τ], with the specified arity.}
+                  @racket[τ], with the specified arity.
+                  Validates inputs and expands to @racket[τ-], attaching kind.}
+            @item{@racket[τ-], an internal macro that expands to the internal
+                  (i.e., fully expanded) type representation. Does not validate
+                  inputs or attach kinds. This macro is useful when creating
+                  a separate kind system, see @racket[define-internal-type-constructor].}
             @item{@racket[τ?], a phase 1 predicate recognizing type @racket[τ].}
             @item{@racket[~τ], a phase 1 @tech:pat-expander recognizing type @racket[τ].}]
 
@@ -183,6 +188,15 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
     
     The @racket[#:extra-info] argument is useful for attaching additional
     metainformation to types, for example to implement pattern matching.}}
+ @item{
+  @defform[(define-internal-type-constructor name-id option ...)
+            #:grammar
+           ([option (code:line #:arity op n)
+                    (code:line #:arg-variances expr)
+                    (code:line #:extra-info stx)])]{
+  Like @racket[define-type-constructor], except the surface macro is not defined.
+  Use this form, for example, when creating a separate kind system so that
+  you can still use other Turnstile conveniences like pattern expanders.}}
  @item{
   @defform[(define-binding-type name-id option ...)
             #:grammar
@@ -207,6 +221,15 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
     on the type variables. The @racket[#:arr] argument is an "arrow" that "saves"
     the annotations after a type is expanded and annotations are erased,
     analogous to how → "saves" the type annotations on a lambda.}}
+ @item{
+  @defform[(define-internal-binding-type name-id option ...)
+            #:grammar
+           ([option (code:line #:arity op n)
+                    (code:line #:bvs op n)
+                    (code:line #:arr kindcon)
+                    (code:line #:arg-variances expr)
+                    (code:line #:extra-info stx)])]{
+  Analogous to @racket[define-internal-type-constructor].}}
 @item{
 @defform[(type-out ty-id)]{
 A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id],