minor cleanup

- allow lone ids that default to tyvars

info.rkt

@@ -15,3 +15,4 @@
     "racket-doc"
     ))
 
+(define version "0.1")

macrotypes/examples/exist.rkt

@@ -67,8 +67,5 @@
      ;;
    #:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed)
    #:with τ_x (subst #'X #'Y #'τ_body)
-   #:with [(X-) (x-) (e-) (τ_e)]
-          (infer #'(e)
-                 #:tvctx #'([X : #%type])
-                 #:ctx   #`([x : τ_x]))
+   #:with [(_ x-) e- τ_e] (infer/ctx+erase #'(X [x : τ_x]) #'e)
    (⊢ (let- ([x- e_packed-]) e-) : τ_e)])

macrotypes/examples/fomega.rkt

@@ -1,50 +1,30 @@
 #lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
-(reuse String #%datum #:from "stlc+reco+var.rkt")
+(reuse λ #%app Int → + #:from "sysf.rkt")
+(reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
-;; Type relation:
 ;; Types:
-;; - types from sysf.rkt
-;; - String from stlc+reco+var
+;; - redefine ∀
+;; - extend kind? and kind=? to include #%type
+;; - extend sysf with tyλ and tyapp
 ;; Terms:
-;; - extend ∀ Λ inst from sysf
-;; - add tyλ and tyapp
-;; - #%datum from stlc+reco+var
+;; - extend sysf with Λ inst
 
-(provide (for-syntax current-kind?)
-         define-type-alias
-         (type-out ★ ⇒ ∀★ ∀)
-         Λ inst tyλ tyapp)
+(provide (type-out ∀) (kind-out ★ ⇒ ∀★ ∀) Λ inst tyλ tyapp)
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
-; want #%type to be equiv to★
-; => edit current-kind? so existing #%type annotations (with no #%kind tag)
-;    are treated as kinds
-; <= define ★ as rename-transformer expanding to #%type
+;; want #%type to be equiv to ★
+;; => extend current-kind? to recognize #%type
+;; <= define ★ as rename-transformer expanding to #%type
 (begin-for-syntax
   (current-kind? (λ (k) (or (#%type? k) (kind? k))))
-  ;; Try to keep "type?" backward compatible with its uses so far,
-  ;; eg in the definition of λ or previous type constuctors.
-  ;; (However, this is not completely possible, eg define-type-alias)
-  ;; So now "type?" no longer validates types, rather it's a subset.
-  ;; But we no longer need type? to validate types, instead we can use 
-  ;; (kind? (typeof t))
-  (current-type? (λ (t)
-                   (define k (typeof t))
-                   #;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
-                   (and ((current-kind?) k) (not (⇒? k))))))
-
-; must override, to handle kinds
-(define-syntax define-type-alias
-  (syntax-parser
-    [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
-     #:fail-unless ((current-kind?) #'k_τ)
-                   (format "not a valid type: ~a\n" (type->str #'τ))
-     #'(define-syntax alias 
-         (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
+  ;; well-formed types, ie not types with ⇒ kind
+  (current-type? (λ (t) (define k (kindof t))
+                   (and k ((current-kind?) k) (not (⇒? k)))))
+  ;; any valid type (includes ⇒-kinded types)
+  (current-any-type? (λ (t) (define k (kindof t))
+                       (and k ((current-kind?) k)))))
 
 (begin-for-syntax
   (define ★? #%type?)
@@ -53,10 +33,10 @@
 (define-kind-constructor ⇒ #:arity >= 1)
 (define-kind-constructor ∀★ #:arity >= 0)
 
-(define-binding-type ∀ #:bvs >= 0 #:arr ∀★)
+(define-binding-type ∀ #:arr ∀★)
 
 ;; alternative: normalize before type=?
-; but then also need to normalize in current-promote
+;; but then also need to normalize in current-promote?
 (begin-for-syntax
   (define (normalize τ)
     (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
@@ -83,44 +63,45 @@
   (define old-type=? (current-type=?))
   ; ty=? == syntax eq and syntax prop eq
   (define (type=? t1 t2)
-    (let ([k1 (typeof t1)][k2 (typeof t2)])
+    (let ([k1 (kindof t1)][k2 (kindof t2)])
       (and (or (and (not k1) (not k2))
-               (and k1 k2 ((current-type=?) k1 k2)))
+               (and k1 k2 ((current-kind=?) k1 k2)))
            (old-type=? t1 t2))))
-  (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (current-typecheck-relation type=?))
 
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
    #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
-   (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
+   (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
-  [(_ e τ ...)
+  [(_ e τ:any-type ...)
    #:with [e- τ_e] (infer+erase #'e)
    #:with (~∀ (tv ...) τ_body) #'τ_e
-   #:with (~∀★ k ...) (typeof #'τ_e)
-   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
-   #:fail-unless (typechecks? #'(k_τ ...) #'(k ...))
+   #:with (~∀★ k ...) (kindof #'τ_e)
+;   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:tag '::)
+   #:with (k_τ ...) (stx-map kindof #'(τ.norm ...))
+   #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
                  (typecheck-fail-msg/multi 
                   #'(k ...) #'(k_τ ...) #'(τ ...))
-   #:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+   #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
    (⊢ e- : τ_inst)])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
 (define-typed-syntax tyλ
   [(_ bvs:kind-ctx τ_body)
-   #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
+   #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:tag '::)
    #:fail-unless ((current-kind?) #'k_body)
                  (format "not a valid type: ~a\n" (type->str #'τ_body))
-   (⊢ (λ- tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
+   (assign-kind #'(λ- tvs- τ_body-) #'(⇒ bvs.kind ... k_body))])
 
 (define-typed-syntax tyapp
   [(_ τ_fn τ_arg ...)
-   #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
-   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
-   #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
+;   #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+   #:with [τ_fn- (~⇒ k_in ... k_out)] (infer+erase #'τ_fn #:tag '::)
+   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::)
+   #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...))
                  (string-append
                   (format 
                    "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
@@ -135,4 +116,4 @@
                   (format "Expected: ~a arguments with type(s): "
                           (stx-length #'(k_in ...)))
                   (string-join (stx-map type->str #'(k_in ...)) ", "))
-   (⊢ (#%app- τ_fn- τ_arg- ...) : k_out)])
+   (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)])

macrotypes/examples/fomega2.rkt

@@ -1,8 +1,10 @@
 #lang s-exp macrotypes/typecheck
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
-(reuse String #%datum #:from "stlc+reco+var.rkt")
+(reuse Int + #:from "sysf.rkt")
+(require (prefix-in sysf: (only-in "sysf.rkt" →- → #%app λ))
+         (only-in "sysf.rkt" ~→ →?))
+(reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt")
 
-; same as fomega.rkt except here λ and #%app works as both type and terms
+; same as fomega.rkt except λ and #%app works as both type and terms,
 ; - uses definition from stlc, but tweaks type? and kind? predicates
 ;; → is also both type and kind
 
@@ -15,36 +17,35 @@
 ;; - extend ∀ Λ inst from sysf
 ;; - #%datum from stlc+reco+var
 
-(provide define-type-alias
-         ★ ∀★ ∀
-         Λ inst)
+(provide (kind-out ★ ∀★) (type-out ∀) → λ #%app Λ inst
+         (for-syntax current-kind-eval kindcheck?))
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
+;; modify predicates to recognize → (function type) as both type and kind
 (begin-for-syntax
-  (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
-  ;; Try to keep "type?" backward compatible with its uses so far,
-  ;; eg in the definition of λ or previous type constuctors.
-  ;; (However, this is not completely possible, eg define-type-alias)
-  ;; So now "type?" no longer validates types, rather it's a subset.
-  ;; But we no longer need type? to validate types, instead we can use
-  ;;(kind? (typeof t))
-  (current-type? (λ (t) (or (type? t)
-                            (let ([k (typeof t)])
-                              (or (★? k) (∀★? k)))
-                            ((current-kind?) t)))))
+  (define old-kind? (current-kind?))
+  (current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
 
-; must override
-(define-syntax define-type-alias
-  (syntax-parser
-    [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
-     #'(define-syntax alias
-         (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
+  ;; well-formed types, eg not types with kind →
+  ;; must allow kinds as types, for →
+  (current-type? (λ (t) (define k (kindof t))
+                    (and k ((current-kind?) k) (not (→? k)))))
+
+  ;; o.w., a valid type is one with any valid kind
+  (current-any-type? (λ (t) (define k (kindof t))
+                        (and k ((current-kind?) k)))))
+
+;; extend → to serve as both type and kind
+(define-syntax (→ stx)
+  (syntax-parse stx
+    [(_ k:kind ...)                ; kind
+     (add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)]
+    [(_ . tys) #'(sysf:→ . tys)])) ; type
 
 (define-base-kind ★)
 (define-kind-constructor ∀★ #:arity >= 0)
-(define-binding-type ∀ #:bvs >= 0 #:arr ∀★)
+(define-binding-type ∀ #:arr ∀★)
 
 ;; alternative: normalize before type=?
 ; but then also need to normalize in current-promote
@@ -70,32 +71,69 @@
   (define (type-eval τ) (normalize (old-eval τ)))
   (current-type-eval type-eval)
   
-  (define old-type=? (current-type=?))
-  (define (type=? t1 t2)
-    (or (and (★? t1) (#%type? t2))
-        (and (#%type? t1) (★? t2))
-        (and (syntax-parse (list t1 t2) #:datum-literals (:)
-               [((~∀ ([tv1 : k1]) tbody1)
-                 (~∀ ([tv2 : k2]) tbody2))
-                ((current-type=?) #'k1 #'k2)]
-               [_ #t])
-             (old-type=? t1 t2))))
-  (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (define old-typecheck? (current-typecheck-relation))
+  (define (new-typecheck? t1 t2)
+    (and (kindcheck? (kindof t1) (kindof t2))
+         (old-typecheck? t1 t2)))
+  (current-typecheck-relation new-typecheck?)
+
+  ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind=
+  (define old-kind=? (current-kind=?))
+  (define (new-kind=? k1 k2)
+    (or (and (★? k1) (#%type? k2))
+        (and (#%type? k1) (★? k2))
+        (old-kind=? k1 k2)))
+  (current-kind=? new-kind=?)
+  (current-kindcheck-relation new-kind=?))
 
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
-   #:with ((tv- ...) e- τ_e)
-          (infer/ctx+erase #'bvs #'e)
-   (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
+   #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
+   (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
-  [(_ e τ ...)
-   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
-   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
-   #:when (stx-andmap 
-           (λ (t k) (or ((current-kind?) k)
-                        (type-error #:src t #:msg "not a valid type: ~a" t)))
-           #'(τ ...) #'(k_τ ...))
-   #:when (typechecks? #'(k_τ ...) #'(k ...))
-   (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))])
+  [(_ e τ:any-type ...)
+;   #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
+   #:with [e- τ_e] (infer+erase #'e)
+   #:with (~∀ (tv ...) τ_body) #'τ_e
+   #:with (~∀★ k ...) (kindof #'τ_e)
+;   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
+   #:with (k_τ ...) (stx-map kindof #'(τ.norm ...))
+   #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
+                 (typecheck-fail-msg/multi 
+                  #'(k ...) #'(k_τ ...) #'(τ ...))
+   #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
+   (⊢ e- : τ_inst)])
+
+;; extend λ to also work as a type
+(define-typed-syntax λ
+  [(_ bvs:kind-ctx τ)           ; type
+   #:with (Xs- τ- k_res) (infer/ctx+erase #'bvs #'τ #:tag '::)
+   (assign-kind #'(λ- Xs- τ-) #'(→ bvs.kind ... k_res))]
+  [(_ . rst) #'(sysf:λ . rst)]) ; term
+
+;; extend #%app to also work as a type
+(define-typed-syntax #%app
+  [(_ τ_fn τ_arg ...) ; type
+;   #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+   #:with [τ_fn- k_fn] (infer+erase #'τ_fn #:tag '::)
+   #:when (syntax-e #'k_fn) ; non-false
+   #:with (~→ k_in ... k_out ~!) #'k_fn
+   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::)
+   #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...))
+                 (string-append
+                  (format 
+                   "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+                   (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                   (syntax->datum #'τ_fn))
+                  "or wrong number of arguments:\nGiven:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(τ_arg ...))
+                        (stx-map type->str #'(k_arg ...)))
+                   "\n" #:after-last "\n")
+                  (format "Expected: ~a arguments with type(s): "
+                          (stx-length #'(k_in ...)))
+                  (string-join (stx-map type->str #'(k_in ...)) ", "))
+   (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)]
+  [(_ . rst) #'(sysf:#%app . rst)]) ; term

macrotypes/examples/fomega3.rkt

@@ -1,6 +1,8 @@
 #lang s-exp macrotypes/typecheck
 (extends "fomega.rkt" #:except tyapp tyλ)
 
+;; NOTE 2017-02-03: currently not working
+
 ; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
 ; → is both type and kind --- but reuses parts of fomega.rkt,
 ; ie removes the duplication in fomega2.rkt

macrotypes/examples/fsub.rkt

@@ -26,7 +26,7 @@
 (begin-for-syntax
   (define (expose t)
     (cond [(identifier? t)
-           (define sub (typeof t #:tag '<:))
+           (define sub (detach t '<:))
            (if sub (expose sub) t)]
           [else t]))
   (current-promote expose)
@@ -75,14 +75,13 @@
                        #:msg "Expected ∀ type, got: ~a" #'any))))]))))
 
 (define-typed-syntax Λ #:datum-literals (<:)
-  [(_ ([tv:id <: τsub:type] ...) e)
+  [(_ ([X:id <: τsub:type] ...) e)
    ;; NOTE: store the subtyping relation of tv and τsub in another
    ;; "environment", ie, a syntax property with another tag: '<:
    ;; The "expose" function looks for this tag to enforce the bound,
    ;; as in TaPL (fig 28-1)
-   #:with ((tv- ...) _ (e-) (τ_e))
-          (infer #'(e) #:tvctx #'([tv : #%type <: τsub] ...))
-   (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))])
+   #:with ((X- ...) e- τ_e) (infer/ctx #'([X :: #%type <: τsub] ...) #'e)
+   (⊢ e- : (∀ ([X- <: τsub] ...) τ_e))])
 (define-typed-syntax inst
   [(_ e τ:type ...)
    #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)

macrotypes/examples/infer.rkt

@@ -51,7 +51,7 @@
                                (for/fold ([tv-id #'tv])
                                          ([s (in-list (list 'sep ...))]
                                           [k (in-list (list #'tvk ...))])
-                                 (assign-type tv-id k #:tag s))
+                                 (attach tv-id s k))
                                'tyvar #t))] ...)
               (λ- (x ...)
                 (let-syntax 

macrotypes/examples/mlish+adhoc.rkt

@@ -383,7 +383,7 @@
                            (format "Improper use of constructor ~a; expected ~a args, got ~a"
                                    (syntax->datum #'Name) (stx-length #'(X ...))
                                    (stx-length (stx-cdr #'stx))))])]
-                       [X (make-rename-transformer (⊢ X #%type))] ...)
+                       [X (make-rename-transformer (mk-type #'X))] ...)
                       (void ty_flat ...)))))
      #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
                 (stx-map 
@@ -854,7 +854,7 @@
            (expand/df
             #'(lambda (X ...) 
                 (let-syntax 
-                 ([X (make-rename-transformer (assign-type #'X #'#%type))] ...)
+                 ([X (make-rename-transformer (mk-type #'X))] ...)
                  (let-syntax
                   ;; must have this inner macro bc body of lambda may require
                   ;; ops defined by TC to be bound
@@ -1670,7 +1670,7 @@
               (~=> TCsub ... 
                    (~TC [generic-op-expected ty-concrete-op-expected] ...)))
              _)
-            (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...)))
+            (infers/tyctx+erase #'([X :: #%type] ...) #'(TC ... (Name ty ...)))
      #:when (TCs-exist? #'(TCsub ...) #:ctx stx)
      ;; simulate as if the declared concrete-op* has TC ... predicates
      ;; TODO: fix this manual deconstruction and assembly

macrotypes/examples/mlish.rkt

@@ -447,7 +447,7 @@
                            (format "Improper use of constructor ~a; expected ~a args, got ~a"
                                    (syntax->datum #'Name) (stx-length #'(X ...))
                                    (stx-length (stx-cdr #'stx))))])]
-                       [X (make-rename-transformer (⊢ X #%type))] ...)
+                       [X (make-rename-transformer (mk-type #'X))] ...)
                       (void ty_flat ...)))))
      #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
                 (stx-map 

macrotypes/examples/stlc+overloading.rkt

@@ -106,7 +106,7 @@
 
 (define-typed-syntax signature
   [(_ (name:id α:id) τ)
-   #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ)
+   #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α :: #%type]) #'τ)
    (define ℜ (ℜ-init #'name #'τ-cod))
    (⊢ (define-syntax name
         (syntax-parser

macrotypes/examples/sysf.rkt

@@ -15,11 +15,10 @@
 
 (define-typed-syntax Λ
   [(_ (tv:id ...) e)
-   #:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv : #%type] ...) #'e)
-   (⊢ e- : (∀ (tv- ...) τ))])
+   #:with [tvs- e- τ-] (infer/ctx #'(tv ...) #'e)
+   (⊢ e- : (∀ tvs- τ-))])
 (define-typed-syntax inst
   [(_ e τ:type ...)
    #:with [e- (~∀ tvs τ_body)] (infer+erase #'e)
-   #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
-   (⊢ e- : τ_inst)]
+   (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
   [(_ e) #'e])

macrotypes/examples/tests/ext-stlc-tests.rkt

@@ -52,8 +52,8 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (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")
+(typecheck-fail (ann Bool : Int)
+                #:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)

macrotypes/examples/tests/fomega-tests.rkt

@@ -1,82 +1,86 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-type Int :: ★)
+(check-type String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(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")
+(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 (Λ ([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 (∀ ([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)))
 
-(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 ((λ ([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 (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"))
+(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)
-            : (⇒ ★ ★))
+(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))))
+(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))
+             (Λ ([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\n *expected: +★\n *given: +Int\n *expressions: 1")
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst:.*not a valid type: 1")
 
 (typecheck-fail
- (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (Λ ([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))
+  (Λ ([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))
+              (Λ ([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))
+               (Λ ([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))
+(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))
@@ -89,104 +93,125 @@
 (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))))
+(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
 ;(check-type Pair : (⇒ ★ ★ ★))
-(check-type Pair : (⇒ ★ ★ (∀★ ★)))
+(check-type Pair :: (⇒ ★ ★ (∀★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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))))
+ (Λ ([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)))))
+ (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)))))
+ ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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 :: ★]) (λ ([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 (Λ ([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))))
+            : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2)))))
 
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+(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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
+ (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)
+ ((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)))
+(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)
 
 

macrotypes/examples/tests/fomega2-tests.rkt

@@ -1,10 +1,11 @@
 #lang s-exp "../fomega2.rkt"
 (require "rackunit-typechecking.rkt")
+(require "rackunit-kindchecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-kind Int :: ★)
+(check-kind String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(check-kind (→ Int Int) :: ★)
 (typecheck-fail (→ →))
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
@@ -12,63 +13,64 @@
 ;; this should error but it doesnt
 #;(λ ([x : ★]) 1)
 
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+;(check-kind (∀ ([t :: ★]) (→ t t)) :: ★)
+(check-kind (∀ ([t :: ★]) (→ t t)) :: (∀★ ★))
+(check-kind (→ (∀ ([t :: ★]) (→ t t)) (→ Int Int)) :: ★)
 
-(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(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 ((λ ([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 (λ ([t : ★]) t) : (→ ★ ★))
-(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
-(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
-(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+;; λ as a type
+(check-kind (λ ([t :: ★]) t) :: (→ ★ ★))
+(check-kind (λ ([t :: ★] [s :: ★]) t) :: (→ ★ ★ ★))
+(check-kind (λ ([t :: ★]) (λ ([s :: ★]) t)) :: (→ ★ (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★)]) t) :: (→ (→ ★ ★) (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★ ★)]) t) :: (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-kind (λ ([arg :: ★] [res :: ★]) (→ arg res)) :: (→ ★ ★ ★))
 
-(check-type ((λ ([t : ★]) t) Int) : ★)
-(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+(check-kind ((λ ([t :: ★]) t) Int) :: ★)
+(check-type (λ ([x : ((λ ([t :: ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) "a-string"))
 
 ;; partial-apply →
-(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
-            : (→ ★ ★))
+(check-kind ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)
+            :: (→ ★ ★))
 ; f's type must have kind ★
-(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
-(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
-            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(typecheck-fail (λ ([f : ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf :: (→ ★ ★)]) (→ (tyf String) (tyf String))))
 (check-type (inst
-             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+             ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int))
             : (→ (→ Int String) (→ Int String)))
 (typecheck-fail
- (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
+ (inst (Λ ([X :: ★]) (λ ([x :: X]) x)) 1))
  ;#:with-msg "not a valid type: 1")
 
 ;; applied f too early
 (typecheck-fail (inst
-                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
-                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+                 (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)))
 (check-type ((inst
-              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int))
              (λ ([x : Int]) "int")) : (→ Int String))
 (check-type (((inst
-               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+               (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([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 (λ ([X : ★]) X))
+(define-type-alias Id (λ ([X :: ★]) X))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
 (check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
@@ -81,104 +83,105 @@
 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
 
 ;; tapl examples, p451
-(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+(define-type-alias Pair (λ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
 ;(check-type Pair : (→ ★ ★ ★))
-(check-type Pair : (→ ★ ★ (∀★ ★)))
+(check-kind Pair :: (→ ★ ★ (∀★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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 (Pair X Y))))
+ (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X :: ★][Y :: ★]) (→ X Y (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)))))
+ (inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
        Int String)
  : (→ Int String (Pair Int String)))
 ; Pair Int String value
 (check-type
- ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ ((inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
        Int String) 1 "1")
  : (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 : ★]) (→ (Pair X Y) X)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (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))))
+  (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
   Int String)
  : (→ (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))))
+   (Λ ([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)))))
+  ((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 : ★]) (→ (Pair X Y) Y)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (Pair X Y) Y)))
 (check-type
  (inst
-  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
   Int String)
  : (→ (Pair Int String) String))
 (check-type
  ((inst
-   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   (Λ ([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)))))
+  ((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 :: ★]) (λ ([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 (Λ ([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))))
+            : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2)))))
 
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+(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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
+ (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)
+ ((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)))
+(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)
 
 

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 #:no-attach-kind #:bvs = 1 #:arity = 1)
-  (define-binding-type exist2 #:bvs = 1 #:arity = 1 #:no-attach-kind)
-  (define-binding-type exist3 #:bvs = 1 #:no-attach-kind #: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")
 )

macrotypes/examples/tests/infer-tests.rkt

@@ -246,7 +246,7 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (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")
+(typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Bool")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)

macrotypes/examples/tests/mlish-tests.rkt

@@ -64,6 +64,8 @@
 (check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
 (check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil)
 
+(check-type (λ ([x : (List Int)]) x) : (→/test (List Int) (List Int)))
+
 (check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
 (check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
 
@@ -675,7 +677,7 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (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")
+(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)

macrotypes/examples/tests/rackunit-kindchecking.rkt

@@ -0,0 +1,16 @@
+#lang racket/base
+(require (for-syntax rackunit syntax/srcloc) rackunit macrotypes/typecheck
+         (only-in "../fomega2.rkt" current-kind-eval kindcheck?))
+(provide check-kind)
+
+(define-syntax (check-kind stx)
+  (syntax-parse stx #:datum-literals (⇒ ->)
+    [(_ τ tag:id k-expected)
+     #:with k (detach (expand/df #'(add-expected τ k-expected))
+                      (stx->datum #'tag))
+     #:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected))
+                   (format
+                    "Type ~a [loc ~a:~a] has kind ~a, expected ~a"
+                    (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
+                    (type->str #'k) (type->str #'k-expected))
+     #'(void)]))

macrotypes/info.rkt

@@ -1,13 +1,16 @@
 #lang info
 
 (define compile-omit-paths 
-  '("examples/tests"))
+  '("examples/fomega3.rkt"
+    "examples/tests"))
 
 (define test-include-paths
   '("examples/tests/mlish")) ; to include .mlish files
 
 (define test-omit-paths
   '("examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
+    "examples/fomega3.rkt"
+    "examples/tests/fomega3-tests.rkt"
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts

macrotypes/stx-utils.rkt

@@ -1,11 +1,17 @@
 #lang racket/base
-(require syntax/stx syntax/parse racket/list racket/format version/utils)
+(require syntax/stx syntax/parse syntax/parse/define
+         racket/list racket/format version/utils)
 (provide (all-defined-out))
 
+;; shorthands
+(define id? identifier?)
+(define free-id=? free-identifier=?)
+
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 (define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
 (define (stx-cddr stx) (stx-cdr (stx-cdr stx)))
 
+(define datum->stx datum->syntax)
 (define (stx->datum stx)
   (if (syntax? stx)
       (syntax->datum stx)
@@ -48,6 +54,7 @@
 
 (define (stx-list-ref stx i)
   (list-ref (stx->list stx) i))
+(define-simple-macro (in-stx-list stx) (in-list (stx->list stx)))
 
 (define (stx-str=? s1 s2)
   (string=? (syntax-e s1) (syntax-e s2)))
@@ -81,6 +88,27 @@
 (define (generate-temporariesss stx)
   (stx-map generate-temporariess stx))
 
+;; stx prop helpers
+
+;; ca*r : Any -> Any
+(define (ca*r v)
+  (if (cons? v) (ca*r (car v)) v))
+;; cd*r : Any -> Any
+(define (cd*r v)
+  (if (cons? v) (cd*r (cdr v)) v))
+
+;; get-stx-prop/ca*r : Syntax Key -> Val
+;; Retrieves Val at Key stx prop on Stx.
+;; If Val is a non-empty list, continue down head until non-list.
+(define (get-stx-prop/ca*r stx tag)
+  (ca*r (syntax-property stx tag)))
+
+;; get-stx-prop/cd*r : Syntax Key -> Val
+(define (get-stx-prop/cd*r stx tag)
+  (cd*r (syntax-property stx tag)))
+
+  
+
 ;; transfers properties and src loc from orig to new
 (define (transfer-stx-props new orig #:ctx [ctx new])
   (datum->syntax ctx (syntax-e new) orig orig))

macrotypes/type-constraints.rkt

@@ -161,7 +161,7 @@
 ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
 ;; looks up each X in the constraints, returning the X if it's unconstrained
 (define (lookup-Xs/keep-unsolved Xs cs)
-  (for/list ([X (in-list (stx->list Xs))])
+  (for/list ([X (in-stx-list Xs)])
     (or (lookup X cs) X)))
 
 ;; instantiate polymorphic types

turnstile/examples/exist.rkt

@@ -65,7 +65,6 @@
    ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
    ;;
   [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)]
-  #:with τ_x (subst #'X #'Y #'τ_body)
-  [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
+  [X [x ≫ x- : #,(subst #'X #'Y #'τ_body)] ⊢ e ≫ e- ⇒ τ_e]
   --------
   [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])

turnstile/examples/fomega-no-reuse-old.rkt

@@ -0,0 +1,175 @@
+#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
+
+;; this version still uses ': key for kinds
+
+;; tyλ and λ are separate forms
+
+(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?: 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
+  
+  ;; well-formed types have kind ★
+  ;; (need this for define-primop, which still uses type stx-class)
+  (current-type? (λ (t) (★? (kindof t))))
+  ;; o.w., a valid type is one with any valid kind
+  (current-any-type? (λ (t) ((current-kind?) (kindof 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 (kindof t1)][k2 (kindof t2)])
+      ; 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=?)
+  (current-typecheck-relation type=?))
+
+;; kinds ----------------------------------------------------------------------
+(define-internal-kind-constructor ★) ; defines ★-
+(define-syntax (★ stx)
+  (syntax-parse stx
+    [:id (mk-kind #'(★-))]
+    [(_ k:kind ...) (mk-kind #'(★- k.norm ...))]))
+
+(define-kind-constructor ⇒ #:arity >= 1)
+
+;; types ----------------------------------------------------------------------
+(define-kinded-syntax (define-type-alias alias:id τ:any-type) ≫
+  ------------------
+  [≻ (define-syntax- alias 
+       (make-variable-like-transformer #'τ.norm))])
+
+(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-kinded-syntax (→ ty ...+) ≫
+  [⊢ ty ≫ ty- ⇒ (~★ . _)] ...
+  --------
+  [⊢ (→- ty- ...) ⇒ ★])
+
+(define-internal-binding-type ∀) ; defines ∀-
+(define-kinded-syntax ∀ #:datum-literals (:)
+  [(_ ([tv:id : k_in:kind] ...) ty) ≫
+   [[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
+   -------
+   [⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
+
+(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-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 ...])
+  [⊢ τ_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] ...  ; ⇐ would use typechecks?
+  [⊢ τ ≫ τ- ⇒ k_τ] ... ; so use ⇒ and kindchecks?
+  #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
+                (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
+  #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+  --------
+  [⊢ e- ⇒ τ-inst])
+

turnstile/examples/fomega-no-reuse.rkt

@@ -12,7 +12,7 @@
          (typed-out [+ : (→ Int Int Int)])
          λ #%app #%datum Λ inst ann)
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
 ;; redefine:
 ;; - current-type?: well-formed types have kind ★
@@ -23,9 +23,10 @@
   
   ;; well-formed types have kind ★
   ;; (need this for define-primop, which still uses type stx-class)
-  (current-type? (λ (t) (★? (typeof t))))
+  (current-type? (λ (t) (★? (kindof t))))
   ;; o.w., a valid type is one with any valid kind
-  (current-any-type? (λ (t) ((current-kind?) (typeof t))))
+  (current-any-type? (λ (t) (define k (kindof t))
+                        (and k ((current-kind?) k))))
 
   ;; TODO: I think this can be simplified
   (define (normalize τ)
@@ -48,20 +49,19 @@
   (define old-eval (current-type-eval))
   (current-type-eval (lambda (τ) (normalize (old-eval τ))))
   
-  (define old-type=? (current-type=?))
+  (define old-typecheck? (current-typecheck-relation))
   ; ty=? == syntax eq and syntax prop eq
-  (define (type=? t1 t2)
-    (let ([k1 (typeof t1)][k2 (typeof t2)])
+  (define (new-typecheck? t1 t2)
+    (let ([k1 (kindof t1)][k2 (kindof t2)])
       ; 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=?)
-  (current-typecheck-relation (current-type=?)))
+               (and k1 k2 (kindcheck? k1 k2)))
+           (old-typecheck? t1 t2))))
+  (current-typecheck-relation new-typecheck?))
 
 ;; kinds ----------------------------------------------------------------------
-(define-internal-kind-constructor ★ #:arity >= 0) ; defines ★-
+(define-internal-kind-constructor ★) ; defines ★-
 (define-syntax (★ stx)
   (syntax-parse stx
     [:id (mk-kind #'(★-))]
@@ -75,11 +75,11 @@
   [≻ (define-syntax- alias 
        (make-variable-like-transformer #'τ.norm))])
 
-(define-base-type Int : ★)
-(define-base-type Bool : ★)
-(define-base-type String : ★)
-(define-base-type Float : ★)
-(define-base-type Char : ★)
+(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-kinded-syntax (→ ty ...+) ≫
@@ -88,15 +88,15 @@
   [⊢ (→- ty- ...) ⇒ ★])
 
 (define-internal-binding-type ∀) ; defines ∀-
-(define-kinded-syntax ∀ #:datum-literals (:)
-  [(_ ([tv:id : k_in:kind] ...) ty) ≫
-   [[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
+(define-kinded-syntax ∀
+  [(_ ctx:kind-ctx ty) ≫
+   [[ctx.x ≫ tv- :: ctx.kind] ... ⊢ ty ≫ ty- ⇒ (~★ . _)]
    -------
-   [⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]])
+   [⊢ (∀- (tv- ...) ty-) ⇒ (★ ctx.kind ...)]])
 
 (define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
-  [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
-  #:fail-unless ((current-kind?) #'k_body)
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
+  #:fail-unless ((current-kind?) #'k_body) ; better err, in terms of τ_body
                 (format "not a valid type: ~a\n" (type->str #'τ_body))
   --------
   [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
@@ -155,20 +155,16 @@
    [_ #: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]
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
   --------
-  [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+  [⊢ 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] ...
-  ;; want to use kindchecks? instead of typechecks?
-  [⊢ τ ≫ τ- ⇒ k_τ] ...
+(define-typed-syntax (inst e τ:any-type ...) ≫
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~★ k ...))]
+;  [⊢ τ ≫ τ- ⇐ k] ...     ; ⇐ would use typechecks?
+  [⊢ τ ≫ τ- ⇒ :: k_τ] ... ; so use ⇒ and kindchecks?
   #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
                 (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
-  #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
-  [⊢ e- ⇒ τ-inst])
+  [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body)])
 

turnstile/examples/fomega.rkt

@@ -1,54 +1,33 @@
 #lang turnstile/lang
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
-(reuse String #%datum #:from "stlc+reco+var.rkt")
+(reuse λ #%app Int → + #:from "sysf.rkt")
+(reuse define-type-alias #%datum String #:from "ext-stlc.rkt")
 
 ;; System F_omega
-;; Type relation:
 ;; Types:
-;; - types from sysf.rkt
-;; - String from stlc+reco+var
+;; - redefine ∀
+;; - extend sysf with tyλ and tyapp
 ;; Terms:
-;; - extend ∀ Λ inst from sysf
-;; - add tyλ and tyapp
-;; - #%datum from stlc+reco+var
+;; - extend sysf with Λ inst
 
-(provide (for-syntax current-kind?)
-         define-type-alias
-         (type-out ★ ⇒ ∀★ ∀)
-         Λ inst tyλ tyapp)
+(provide (type-out ∀) (kind-out ★ ⇒ ∀★) Λ inst tyλ tyapp)
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
-; want #%type to be equiv to★
-; => edit current-kind? so existing #%type annotations (with no #%kind tag)
-;    are treated as kinds
-; <= define ★ as rename-transformer expanding to #%type
+;; want #%type to be equiv to ★
+;; => extend current-kind? to recognize #%type
+;; <= define ★ as rename-transformer expanding to #%type
 (begin-for-syntax
   (current-kind? (λ (k) (or (#%type? k) (kind? k))))
-  ;; Try to keep "type?" backward compatible with its uses so far,
-  ;; eg in the definition of λ or previous type constuctors.
-  ;; (However, this is not completely possible, eg define-type-alias)
-  ;; So now "type?" no longer validates types, rather it's a subset.
-  ;; But we no longer need type? to validate types, instead we can use
-  ;; (kind? (typeof t))
-  (current-type? (λ (t)
-                   (define k (typeof t))
-                   #;(or (type? t) (★? (typeof t)) (∀★? (typeof t)))
-                   (and ((current-kind?) k) (not (⇒? k))))))
-
-; must override, to handle kinds
-(define-syntax define-type-alias
-  (syntax-parser
-    [(define-type-alias alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
-     #:fail-unless ((current-kind?) #'k_τ)
-                   (format "not a valid type: ~a\n" (type->str #'τ))
-     #'(define-syntax alias 
-         (syntax-parser [x:id #'τ-] [(_ . rst) #'(τ- . rst)]))]))
+  ;; any valid type (includes ⇒-kinded types)
+  (current-any-type? (λ (t) (define k (kindof t))
+                        (and k ((current-kind?) k))))
+  ;; well-formed types, ie not types with ⇒ kind
+  (current-type? (λ (t) (and ((current-any-type?) t)
+                             (not (⇒? (kindof t)))))))
 
 (begin-for-syntax
   (define ★? #%type?)
-  (define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder
+  (define-syntax ~★ (λ _ (error "~★ not implemented")))) ; placeholder
 (define-syntax ★ (make-rename-transformer #'#%type))
 (define-kind-constructor ⇒ #:arity >= 1)
 (define-kind-constructor ∀★ #:arity >= 0)
@@ -56,7 +35,7 @@
 (define-binding-type ∀ #:arr ∀★)
 
 ;; alternative: normalize before type=?
-; but then also need to normalize in current-promote
+;; but then also need to normalize in current-promote
 (begin-for-syntax
   (define (normalize τ)
     (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
@@ -77,44 +56,45 @@
       [_ τ]))
   
   (define old-eval (current-type-eval))
-  (define (type-eval τ) (normalize (old-eval τ)))
-  (current-type-eval type-eval)
+  (define (new-type-eval τ) (normalize (old-eval τ)))
+  (current-type-eval new-type-eval)
   
   (define old-type=? (current-type=?))
-  ; ty=? == syntax eq and syntax prop eq
-  (define (type=? t1 t2)
-    (let ([k1 (typeof t1)][k2 (typeof t2)])
+  ;; need to also compare kinds of types
+  (define (new-type=? t1 t2)
+    (let ([k1 (kindof t1)][k2 (kindof t2)])
+      ;; need these `not` checks bc type= does a structural stx traversal
+      ;; and may compare non-type ids (like #%plain-app)
       (and (or (and (not k1) (not k2))
-               (and k1 k2 ((current-type=?) k1 k2)))
+               (and k1 k2 ((current-kind=?) k1 k2)))
            (old-type=? t1 t2))))
-  (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  (current-typecheck-relation new-type=?))
 
 (define-typed-syntax (Λ bvs:kind-ctx e) ≫
-  [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
   --------
-  [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+  [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)])
 
-(define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
-  [⊢ τ ≫ τ- ⇐ k] ...
-  #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+;; τ.norm invokes current-type-eval while "≫ τ-" uses only local-expand
+;; (via infer fn)
+(define-typed-syntax (inst e τ:any-type ...) ≫
+  [⊢ e ≫ e- ⇒ (~∀ tvs τ_body) (⇒ :: (~∀★ k ...))]
+  [⊢ τ ≫ τ- ⇐ :: k] ...
   --------
-  [⊢ e- ⇒ τ-inst])
+  [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)])
 
-;; TODO: merge with regular λ and app?
-;; - see fomega2.rkt
-(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))
+;; - see fomega2.rkt for example with no explicit tyλ and tyapp
+(define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
+  #:fail-unless ((current-kind?) #'k_body) ; better err, in terms of τ_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 ...])
+                (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
   [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
   --------
   [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])

turnstile/examples/fomega2.rkt

@@ -1,5 +1,5 @@
 #lang turnstile/lang
-(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst)
+(extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst λ #%app →)
 (reuse String #%datum #:from "stlc+reco+var.rkt")
 
 ; same as fomega.rkt except here λ and #%app works as both type and terms
@@ -17,31 +17,42 @@
 
 (provide define-type-alias
          ★ ∀★ ∀
-         Λ inst)
+         λ #%app → Λ inst
+         (for-syntax current-kind-eval kindcheck?))
 
-(define-syntax-category kind)
+(define-syntax-category :: kind)
 
 (begin-for-syntax
-  (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
+  (define old-kind? (current-kind?))
+  (current-kind? (λ (k) (or (#%type? k) (old-kind? k))))
   ;; Try to keep "type?" backward compatible with its uses so far,
   ;; eg in the definition of λ or previous type constuctors.
   ;; (However, this is not completely possible, eg define-type-alias)
   ;; So now "type?" no longer validates types, rather it's a subset.
   ;; But we no longer need type? to validate types, instead we can use
   ;; (kind? (typeof t))
-  (current-type? (λ (t) (or (type? t)
-                            (let ([k (typeof t)])
-                              (or (★? k) (∀★? k)))
-                            ((current-kind?) t)))))
+  (current-type? (λ (t) (define k (kindof t))
+                    (and k ((current-kind?) k) (not (→? k)))))
+
+  ;; o.w., a valid type is one with any valid kind
+  (current-any-type? (λ (t) (define k (kindof t))
+                        (and k ((current-kind?) k)))))
 
 ; must override
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
+     #:with (τ- _) (infer+erase #'τ #:tag '::)
      #'(define-syntax alias
          (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
+;; extend → to serve as both type and kind
+(define-syntax (→ stx)
+  (syntax-parse stx
+    [(_ k:kind ...)                ; kind
+     (add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)]
+    [(_ . tys) #'(sysf:→ . tys)])) ; type
+
 (define-base-kind ★)
 (define-kind-constructor ∀★ #:arity >= 0)
 (define-binding-type ∀ #:arr ∀★)
@@ -70,28 +81,53 @@
   (define (type-eval τ) (normalize (old-eval τ)))
   (current-type-eval type-eval)
   
-  (define old-type=? (current-type=?))
-  (define (type=? t1 t2)
-    (or (and (★? t1) (#%type? t2))
-        (and (#%type? t1) (★? t2))
-        (and (syntax-parse (list t1 t2) #:datum-literals (:)
-               [((~∀ ([tv1 : k1]) tbody1)
-                 (~∀ ([tv2 : k2]) tbody2))
-                ((current-type=?) #'k1 #'k2)]
-               [_ #t])
-             (old-type=? t1 t2))))
-  (current-type=? type=?)
-  (current-typecheck-relation (current-type=?)))
+  ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind=
+  (define old-kind=? (current-kind=?))
+  (define (new-kind=? k1 k2)
+    (or (and (★? k1) (#%type? k2)) ; enables use of existing type defs
+        (and (#%type? k1) (★? k2))
+        (old-kind=? k1 k2)))
+  (current-kind=? new-kind=?)
+  (current-kindcheck-relation new-kind=?)
+
+  (define old-typecheck? (current-typecheck-relation))
+  (define (new-typecheck? t1 t2)
+    (syntax-parse (list t1 t2) #:datum-literals (:)
+     [((~∀ ([tv1 : k1]) tbody1)
+       (~∀ ([tv2 : k2]) tbody2))
+      (and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))]
+     [_ (old-typecheck? t1 t2)]))
+  (current-typecheck-relation new-typecheck?))
 
 (define-typed-syntax (Λ bvs:kind-ctx e) ≫
-  [[bvs.x ≫ tv- : bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
+  [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
   --------
-  [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
+  [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)])
 
-(define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
-  [⊢ τ ≫ τ- ⇐ k] ...
-  #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+(define-typed-syntax (inst e τ:any-type ...) ≫
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))]
+;  [⊢ τ ≫ τ- ⇐ :: k] ... ; doesnt work since def-typed-s ⇐ not using kindcheck?
+  #:with (k_τ ...) (stx-map kindof #'(τ.norm ...))
+  #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...))
+                (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
   --------
-  [⊢ e- ⇒ τ-inst])
+  [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body)])
 
+;; extend λ to also work as a type
+(define-kinded-syntax λ
+  [(_ bvs:kind-ctx τ) ≫                 ; type
+   [[bvs.x ≫ X- :: bvs.kind] ... ⊢ τ ≫ τ- ⇒ k_res]
+   ------------
+   [⊢ (λ- (X- ...) τ-) ⇒ (→ bvs.kind ... k_res)]]
+  [(_ . rst) ≫ --- [≻ (sysf:λ . rst)]]) ; term
+
+;; extend #%app to also work as a type
+(define-kinded-syntax #%app
+  [(_ τ_fn τ_arg ...) ≫                     ; type
+   [⊢ τ_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]]
+  [(_ . rst) ≫ --- [≻ (sysf:#%app . rst)]]) ; term

turnstile/examples/fomega3.rkt

@@ -1,6 +1,8 @@
 #lang turnstile/lang
 (extends "fomega.rkt" #:except tyapp tyλ)
 
+;; not current working 2017-02-03
+
 ; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
 ; → is both type and kind --- but reuses parts of fomega.rkt,
 ; ie removes the duplication in fomega2.rkt

turnstile/examples/fsub.rkt

@@ -26,7 +26,7 @@
 (begin-for-syntax
   (define (expose t)
     (cond [(identifier? t)
-           (define sub (typeof t #:tag '<:))
+           (define sub (detach t '<:))
            (if sub (expose sub) t)]
           [else t]))
   (current-promote expose)
@@ -34,7 +34,7 @@
   (define (sub? t1 t2)
     (stlc:sub? ((current-promote) t1) t2))
   (current-sub? sub?)
-  (current-typecheck-relation (current-sub?)))
+  (current-typecheck-relation sub?))
 
 ; quasi-kind, but must be type constructor because its arguments are types
 (define-type-constructor <: #:arity >= 0) 
@@ -79,7 +79,7 @@
   ;; environment with a syntax property using another tag: '<:
   ;; The "expose" function looks for this tag to enforce the bound,
   ;; as in TaPL (fig 28-1)
-  [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e]
+  [[tv ≫ tv- :: #%type <: τsub] ... ⊢ e ≫ e- ⇒ τ_e]
   --------
   [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)])
 (define-typed-syntax (inst e τ:type ...) ≫

turnstile/examples/infer.rkt

@@ -159,7 +159,7 @@
    #:with [X ...]
    (for/list ([X (in-list (generate-temporaries #'[x ...]))])
      (add-orig X X))
-   [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...)
+   [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...)
     ⊢ [body ≫ body- ⇒ : τ_body*]]
    #:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*)
    #:with τ_fn (some/inst/generalize #'[X- ... V ...]

turnstile/examples/mlish+adhoc.rkt

@@ -338,7 +338,7 @@
    --------
    [≻ (begin-
         (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
-        #,(quasisyntax/loc stx
+        #,(quasisyntax/loc this-syntax
             (define- g
               ;(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
               (liftedλ {Y ...} ([x : τ] ... #:where TC ...) 
@@ -387,7 +387,7 @@
                            (format "Improper use of constructor ~a; expected ~a args, got ~a"
                                    (syntax->datum #'Name) (stx-length #'(X ...))
                                    (stx-length (stx-cdr #'stx))))])]
-                       [X (make-rename-transformer (⊢ X #%type))] ...)
+                       [X (make-rename-transformer (mk-type #'X))] ...)
                       (void ty_flat ...)))))
      #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
                 (stx-map 
@@ -658,10 +658,10 @@
    [⊢ e ≫ e- ⇒ τ_e]
    #:with ([(~seq p ...) (~datum ->) e_body] ...) #'clauses
    #:with (pat ...) (stx-map ; use brace to indicate root pattern
-                     (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+                     (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc this-syntax {pp ...})]))
                      #'((p ...) ...))
    #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
-   #:with ty-expected (get-expected-type stx)
+   #:with ty-expected (get-expected-type this-syntax)
    [[x ≫ x- : ty] ... ⊢ [(add-expected e_body ty-expected) ≫ e_body- ⇒ ty_body]] ...
    #:when (check-exhaust #'(pat- ...) #'τ_e)
    ----
@@ -671,7 +671,7 @@
    [(_ e with . clauses) ≫
     #:fail-when (null? (syntax->list #'clauses)) "no clauses"
     [⊢ e ≫ e- ⇒ τ_e]
-    #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+    #:with t_expect (syntax-property this-syntax 'expected-type) ; propagate inferred type
     #:with out
     (cond
      [(×? #'τ_e) ;; e is tuple
@@ -730,7 +730,7 @@
         #:with (_ (_ (_ ConsAll) . _) ...) #'info-body
         #:fail-unless (set=? (syntax->datum #'(Clause ...))
                              (syntax->datum #'(ConsAll ...)))
-                      (type-error #:src stx
+                      (type-error #:src this-syntax
                        #:msg (string-append
                               "match: clauses not exhaustive; missing: "
                               (string-join      
@@ -842,7 +842,7 @@
            (expand/df
             #'(lambda (X ...) 
                 (let-syntax 
-                 ([X (make-rename-transformer (assign-type #'X #'#%type))] ...)
+                 ([X (make-rename-transformer (mk-type #'X))] ...)
                  (let-syntax
                   ;; must have this inner macro bc body of lambda may require
                   ;; ops defined by TC to be bound
@@ -896,7 +896,7 @@
       ⇒ (∀ Xs+ (=> TC+ ... (ext-stlc:→ ty+ ... ty-out)))]]
   [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC
    #:with (X ...) (compute-tyvars #'(ty ...))
-   #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type stx)
+   #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type this-syntax)
    --------
    [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) (add-expected body body-ty)))]]
   [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC, ignoring expected-type
@@ -904,12 +904,12 @@
    --------
    [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) body))]]
   [(_ (x:id ...+) body) ≫
-   #:with (~?∀ Xs expected) (get-expected-type stx)
+   #:with (~?∀ Xs expected) (get-expected-type this-syntax)
    #:do [(unless (→? #'expected)
-           (type-error #:src stx #:msg "λ parameters must have type annotations"))]
+           (type-error #:src this-syntax #:msg "λ parameters must have type annotations"))]
    #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected
    #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...])
-           (type-error #:src stx #:msg
+           (type-error #:src this-syntax #:msg
                        (format "expected a function of ~a arguments, got one with ~a arguments"
                                (stx-length #'[arg-ty ...] #'[x ...]))))]
    --------
@@ -922,10 +922,9 @@
    ;; TODO is there a way to have λs that refer to ids defined after them?
    #'(Λ Xs (ext-stlc:λ x+tys . body))])
 
-
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
-  [(_ e_fn . e_args) ≫
+  [(~and this-app (_ e_fn . e_args)) ≫
 ;   #:when (printf "app: ~a\n" (syntax->datum #'(e_fn . e_args)))
    ;; ) compute fn type (ie ∀ and →) 
    [⊢ e_fn ≫ e_fn- ⇒ (~and ty_fn (~∀ Xs ty_fnX))]
@@ -939,7 +938,7 @@
         (syntax-parse #'(e_args tyX_args)
           [((e_arg ...) (τ_inX ... _))
            #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
-           (mk-app-err-msg stx #:expected #'(τ_inX ...) 
+           (mk-app-err-msg #'this-app #:expected #'(τ_inX ...) 
                            #:note "Wrong number of arguments.")
            #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
            #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
@@ -949,13 +948,13 @@
       ;; no typeclasses, duplicate code for now --------------------------------
       [(~ext-stlc:→ . tyX_args) 
        ;; ) solve for type variables Xs
-       (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+       (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app))
        ;; ) instantiate polymorphic function type
        (syntax-parse (inst-types/cs #'Xs #'cs #'tyX_args)
         [(τ_in ... τ_out) ; concrete types
          ;; ) arity check
          #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
-                       (mk-app-err-msg stx #:expected #'(τ_in ...)
+                       (mk-app-err-msg #'this-app #:expected #'(τ_in ...)
                         #:note "Wrong number of arguments.")
          ;; ) compute argument types; re-use args expanded during solve
          #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
@@ -967,7 +966,7 @@
          #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
          ;; ) typecheck args
          #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                       (mk-app-err-msg stx 
+                       (mk-app-err-msg #'this-app
                         #:given #'(τ_arg ...)
                         #:expected 
                         (stx-map 
@@ -986,13 +985,13 @@
                            (syntax-parse #'τ_out
                              [(~?∀ (Y ...) τ_out)
                               (unless (→? #'τ_out)
-                                (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+                                (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn))
                               #'(∀ (unsolved-X ... Y ...) τ_out)]))
          (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])]
       ;; handle type class constraints ----------------------------------------
       [(~=> TCX ... (~ext-stlc:→ . tyX_args))
        ;; ) solve for type variables Xs
-       (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+       (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app))
        ;; ) instantiate polymorphic function type
        (syntax-parse (inst-types/cs #'Xs #'cs #'((TCX ...) tyX_args))
          [((TC ...) (τ_in ... τ_out)) ; concrete types
@@ -1005,7 +1004,7 @@
                          (with-handlers 
                            ([exn:fail:syntax:unbound? 
                              (lambda (e)
-                               (type-error #:src stx
+                               (type-error #:src #'this-app
                                 #:msg 
                                 (format 
                                  (string-append
@@ -1028,9 +1027,12 @@
                                  (stx-map 
                                    (lambda (X ty-solved)
                                      (string-append (type->str X) " : " (type->str ty-solved)))
-                                   #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))])
+                                   #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))]
+                            [(lambda _ #t)
+                             (lambda (e) (displayln "other exn")(displayln e)
+                             (error 'lookup))])
                          (lookup-op o tys)))
-                       (stx-map (lambda (o) (format-id stx "~a" o #:source stx)) gen-ops)
+                       (stx-map (lambda (o) (format-id #'this-app "~a" o #:source #'this-app)) gen-ops)
                        (stx-map
                          (syntax-parser
                            [(~∀ _ (~ext-stlc:→ ty_in ... _)) #'(ty_in ...)])
@@ -1038,7 +1040,7 @@
                    #'((generic-op ...) ...) #'((ty-concrete-op ...) ...) #'(TC ...))
           ;; ) arity check
           #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
-                        (mk-app-err-msg stx #:expected #'(τ_in ...)
+                        (mk-app-err-msg #'this-app #:expected #'(τ_in ...)
                                         #:note "Wrong number of arguments.")
           ;; ) compute argument types; re-use args expanded during solve
           #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
@@ -1050,7 +1052,7 @@
           #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
           ;; ) typecheck args
           #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                        (mk-app-err-msg stx 
+                        (mk-app-err-msg #'this-app
                          #:given #'(τ_arg ...)
                          #:expected 
                          (stx-map 
@@ -1069,14 +1071,14 @@
                            (syntax-parse #'τ_out
                              [(~?∀ (Y ...) τ_out)
                               (unless (→? #'τ_out)
-                                (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+                                (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn))
                               #'(∀ (unsolved-X ... Y ...) τ_out)]))
           (⊢ ((#%app- e_fn- op ...) e_arg- ...) : τ_out*)])])])]]
   [(_ e_fn . e_args) ≫ ; err case; e_fn is not a function
    [⊢ e_fn ≫ e_fn- ⇒ τ_fn]
    --------
    [#:error 
-    (type-error #:src stx 
+    (type-error #:src #'this-app
                 #:msg (format "Expected expression ~a to have → type, got: ~a"
                               (syntax->datum #'e_fn) (type->str #'τ_fn)))]])
 
@@ -1658,10 +1660,10 @@
   [(_ (Name ty ...) [generic-op concrete-op] ...) ≫
    [⊢ (Name ty ...) ≫ 
       (~=> TC ... (~TC [generic-op-expected ty-concrete-op-expected] ...)) ⇒ _]
-   #:when (TCs-exist? #'(TC ...) #:ctx stx)
+   #:when (TCs-exist? #'(TC ...) #:ctx this-syntax)
    #:fail-unless (set=? (syntax->datum #'(generic-op ...)) 
                         (syntax->datum #'(generic-op-expected ...)))
-                 (type-error #:src stx
+                 (type-error #:src this-syntax
                   #:msg (format "Type class instance ~a incomplete, missing: ~a"
                           (syntax->datum #'(Name ty ...))
                           (string-join
@@ -1711,15 +1713,15 @@
                 (~=> TCsub ... 
                      (~TC [generic-op-expected ty-concrete-op-expected] ...)))
            _)
-           (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...)))
+           (infers/tyctx+erase #'(X ...) #'(TC ... (Name ty ...)))
    ;; this produces #%app bad stx err, so manually call infer for now
-   ;; [([X ≫ X- : #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫
+   ;; [([X ≫ X- :: #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫
    ;;                                (TC+ ... 
    ;;                                 (~=> TCsub ... 
    ;;                                  (~TC [generic-op-expected ty-concrete-op-expected] ...)))
    ;;                                ⇒ _]
    ;; #:with Xs+ #'(X- ...)
-   #:when (TCs-exist? #'(TCsub ...) #:ctx stx)
+   #:when (TCs-exist? #'(TCsub ...) #:ctx this-syntax)
    ;; simulate as if the declared concrete-op* has TC ... predicates
    ;; TODO: fix this manual deconstruction and assembly
    #:with ((app fa (lam _ ei ty_fn)) ...) #'(ty-concrete-op-expected ...)
@@ -1727,7 +1729,7 @@
           (stx-map (current-type-eval) #'((app fa (lam Xs+ ei (=> TC+ ... ty_fn))) ...))
    #:fail-unless (set=? (syntax->datum #'(generic-op ...)) 
                         (syntax->datum #'(generic-op-expected ...)))
-                 (type-error #:src stx
+                 (type-error #:src this-syntax
                   #:msg (format "Type class instance ~a incomplete, missing: ~a"
                           (syntax->datum #'(Name ty ...))
                           (string-join

turnstile/examples/mlish.rkt

@@ -86,9 +86,7 @@
   ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
   ;; finds the free Xs in the type
   (define (find-free-Xs Xs ty)
-    (for/list ([X (in-list (stx->list Xs))]
-               #:when (stx-contains-id? ty X))
-      X))
+    (for/list ([X (in-stx-list Xs)] #:when (stx-contains-id? ty X)) X))
 
   ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
   ;;   stx = the application stx = (#%app e_fn e_arg ...)
@@ -104,8 +102,9 @@
     (syntax-parse tyXs
       [(τ_inX ... τ_outX)
        ;; generate initial constraints with expected type and τ_outX
-       #:with (~?∀ Vs expected-ty) (and (get-expected-type stx)
-                                        ((current-type-eval) (get-expected-type stx)))
+       #:with (~?∀ Vs expected-ty)
+              (and (get-expected-type stx)
+                   ((current-type-eval) (get-expected-type stx)))
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
              (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
@@ -114,8 +113,8 @@
          [(_ e_fn . args)
           (define-values (as- cs)
               (for/fold ([as- null] [cs initial-cs])
-                        ([a (in-list (syntax->list #'args))]
-                         [tyXin (in-list (syntax->list #'(τ_inX ...)))])
+                        ([a (in-stx-list #'args)]
+                         [tyXin (in-stx-list #'(τ_inX ...))])
                 (define ty_in (inst-type/cs Xs cs tyXin))
                 (define/with-syntax [a- ty_a]
                   (infer+erase (if (empty? (find-free-Xs Xs ty_in))
@@ -149,7 +148,7 @@
   (define (covariant-Xs? ty)
     (syntax-parse ((current-type-eval) ty)
       [(~?∀ Xs ty)
-       (for/and ([X (in-list (syntax->list #'Xs))])
+       (for/and ([X (in-stx-list #'Xs)])
          (covariant-X? X #'ty))]))
 
   ;; find-X-variance : Id Type [Variance] -> Variance
@@ -186,7 +185,7 @@
          (for/list ([arg-variance (in-list (get-arg-variances #'tycons))])
            (variance-compose ctxt-variance arg-variance)))
        (for/fold ([acc (make-list (length Xs) irrelevant)])
-                 ([τ (in-list (syntax->list #'[τ ...]))]
+                 ([τ (in-stx-list #'[τ ...])]
                   [τ-ctxt-variance (in-list τ-ctxt-variances)])
          (map variance-join
               acc
@@ -422,7 +421,7 @@
                            (format "Improper use of constructor ~a; expected ~a args, got ~a"
                                    (syntax->datum #'Name) (stx-length #'(X ...))
                                    (stx-length (stx-cdr #'stx))))])]
-                       [X (make-rename-transformer (⊢ X #%type))] ...)
+                       [X (make-rename-transformer (mk-type #'X))] ...)
                       (void ty_flat ...)))))
      #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
                 (stx-map 
@@ -701,10 +700,10 @@
    [⊢ e ≫ e- ⇒ τ_e]
    #:with ([(~seq p ...) -> e_body] ...) #'clauses
    #:with (pat ...) (stx-map ; use brace to indicate root pattern
-                     (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+                     (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc this-syntax {pp ...})]))
                      #'((p ...) ...))
    #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
-   #:with ty-expected (get-expected-type stx)
+   #:with ty-expected (get-expected-type this-syntax)
    [[x ≫ x- : ty] ... ⊢ (add-expected e_body ty-expected) ≫ e_body- ⇒ ty_body] ...
    #:when (check-exhaust #'(pat- ...) #'τ_e)
    --------
@@ -716,7 +715,7 @@
    #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ e ≫ e- ⇒ τ_e]
    #:when (×? #'τ_e)
-   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with t_expect (get-expected-type this-syntax) ; propagate inferred type
    #:with ([x ... -> e_body]) #'clauses
    #:with (~× ty ...) #'τ_e
    #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
@@ -733,7 +732,7 @@
    #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ e ≫ e- ⇒ τ_e]
    #:when (List? #'τ_e)
-   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with t_expect (get-expected-type this-syntax) ; propagate inferred type
    #:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
                  (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
             -> e_body] ...+)
@@ -770,7 +769,7 @@
    #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ e ≫ e- ⇒ τ_e]
    #:when (and (not (×? #'τ_e)) (not (List? #'τ_e)))
-   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with t_expect (get-expected-type this-syntax) ; propagate inferred type
    #:with ([Clause:id x:id ... 
                       (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
                       -> e_c_un] ...+) ; un = unannotated with expected ty
@@ -780,7 +779,7 @@
    #:with (_ (_ (_ ConsAll) . _) ...) #'info-body
    #:fail-unless (set=? (syntax->datum #'(Clause ...))
                         (syntax->datum #'(ConsAll ...)))
-   (type-error #:src stx
+   (type-error #:src this-syntax
                #:msg (string-append
                       "match: clauses not exhaustive; missing: "
                       (string-join      
@@ -851,22 +850,21 @@
    #:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
    (format "expected a function of ~a arguments, got one with ~a arguments"
            (stx-length #'[τ_in ...]) (stx-length #'[x ...]))
-   [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]]
+   [(X ...) ([x ≫ x- : τ_in] ...) ⊢ [body ≫ body- ⇐ τ_out]]
    --------
    [⊢ (λ- (x- ...) body-)]]
   [(λ ([x : τ_x] ...) body) ⇐ (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
    #:with [X ...] (compute-tyvars #'(τ_x ...))
-   [([X ≫ X- : #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ #%type] ...]
+   [[X ≫ X- :: #%type] ... ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...]
    [τ_in τ⊑ τ_x- #:for x] ...
    ;; TODO is there a way to have λs that refer to ids defined after them?
-   [([V ≫ V- : #%type] ... [X- ≫ X-- : #%type] ...) ([x ≫ x- : τ_x-] ...)
-    ⊢ body ≫ body- ⇐ τ_out]
+   [(V ... X- ...) ([x ≫ x- : τ_x-] ...) ⊢ body ≫ body- ⇐ τ_out]
    --------
    [⊢ (λ- (x- ...) body-)]]
   [(λ ([x : τ_x] ...) body) ≫
    #:with [X ...] (compute-tyvars #'(τ_x ...))
    ;; TODO is there a way to have λs that refer to ids defined after them?
-   [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_x] ...) ⊢ body ≫ body- ⇒ τ_body]
+   [([X ≫ X- :: #%type] ...) ([x ≫ x- : τ_x] ...) ⊢ body ≫ body- ⇒ τ_body]
    #:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])
    #:with τ_fn (add-orig #'(?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body))
                          #`(→ #,@(stx-map get-orig #'[τ_x* ...]) #,(get-orig #'τ_body)))
@@ -880,7 +878,7 @@
    ;; compute fn type (ie ∀ and →)
    [⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))]
    ;; solve for type variables Xs
-   #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)
+   #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
    ;; instantiate polymorphic function type
    #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
    #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
@@ -896,13 +894,13 @@
                      (syntax-parse #'τ_out
                        [(~?∀ (Y ...) τ_out)
                         #:fail-unless (→? #'τ_out)
-                        (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+                        (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
                         (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
                           (unless (covariant-X? X #'τ_out)
                             (raise-syntax-error
                              #f
-                             (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
-                             stx)))
+                             (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+                             this-syntax)))
                         #'(∀ (unsolved-X ... Y ...) τ_out)]))
    --------
    [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out*]])

turnstile/examples/stlc+effect.rkt

@@ -80,7 +80,7 @@
    --------
    [⊢ (#%app- box- e-)
        (⇒ : (Ref τ))
-       (⇒ ν (locs #,(syntax-position stx) ns ...))
+       (⇒ ν (locs #,(syntax-position this-syntax) ns ...))
        (⇒ := (locs as ...))
        (⇒ ! (locs ds ...))]])
 (define-typed-syntax deref
@@ -95,7 +95,7 @@
        (⇒ : ty)
        (⇒ ν (locs ns ...))
        (⇒ := (locs as ...))
-       (⇒ ! (locs #,(syntax-position stx) ds ...))]])
+       (⇒ ! (locs #,(syntax-position this-syntax) ds ...))]])
 (define-typed-syntax := #:literals (:=)
   [(_ e_ref e) ≫
    [⊢ e_ref ≫ e_ref-
@@ -112,6 +112,6 @@
    [⊢ (#%app- set-box!- e_ref- e-)
        (⇒ : Unit)
        (⇒ ν (locs ns1 ... ns2 ...))
-       (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...))
+       (⇒ := (locs #,(syntax-position this-syntax) as1 ... as2 ...))
        (⇒ ! (locs ds1 ... ds2 ...))]])
 

turnstile/examples/stlc+rec-iso.rkt

@@ -23,7 +23,6 @@
   [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)])
 (define-typed-syntax (fld τ:type-ann e) ≫
   #:with (~μ (tv) τ_body) #'τ.norm
-  #:with τ_e (subst #'τ.norm #'tv #'τ_body)
-  [⊢ e ≫ e- ⇐ τ_e]
+  [⊢ e ≫ e- ⇐ #,(subst #'τ.norm #'tv #'τ_body)]
   --------
   [⊢ e- ⇒ τ.norm])

turnstile/examples/stlc+reco+sub.rkt

@@ -49,4 +49,4 @@
          #'([l τl] ...))]
        [_ #f])))
   (current-sub? sub?)
-  (current-typecheck-relation (current-sub?)))
+  (current-typecheck-relation sub?))

turnstile/examples/stlc+reco+var.rkt

@@ -122,7 +122,7 @@
    (∨-ref #'τ #'l #:else
           (λ () (raise-syntax-error #f
                    (format "~a field does not exist" (syntax->datum #'l))
-                   stx)))
+                   this-syntax)))
    [⊢ e ≫ e- ⇐ τ_e]
    --------
    [⊢ (list- 'l e)]])

turnstile/examples/stlc+sub.rkt

@@ -52,6 +52,7 @@
         (Top? τ2)))
   (define current-sub? (make-parameter sub?))
   (current-typecheck-relation sub?)
+
   (define (subs? τs1 τs2)
     (and (stx-length=? τs1 τs2)
          (stx-andmap (current-sub?) τs1 τs2)))

turnstile/examples/stlc+union+case.rkt

@@ -99,7 +99,5 @@
   (current-typecheck-relation sub?)
   (define (subs? τs1 τs2)
     (and (stx-length=? τs1 τs2)
-         (stx-andmap (current-sub?) τs1 τs2)))
-  
-  )
+         (stx-andmap (current-sub?) τs1 τs2))))
                    

turnstile/examples/sysf.rkt

@@ -14,17 +14,14 @@
 (define-binding-type ∀)
 
 (define-typed-syntax (Λ (tv:id ...) e) ≫
-  [([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ]
+  [[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ]
   --------
   [⊢ e- ⇒ (∀ (tv- ...) τ)])
 
 (define-typed-syntax inst
   [(_ e τ:type ...) ≫
    [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
-   #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
    --------
-   [⊢ e- ⇒ τ_inst]]
-  [(_ e) ≫
-   --------
-   [≻ e]])
+   [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
+  [(_ e) ≫ --- [≻ e]])
 

turnstile/examples/tests/ext-stlc-tests.rkt

@@ -52,8 +52,8 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (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")
+(typecheck-fail (ann Bool : Int)
+                #:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)

turnstile/examples/tests/fomega-no-reuse-tests-old.rkt

@@ -0,0 +1,213 @@
+#lang s-exp "../fomega-no-reuse-old.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; similar to fomega-tests.rkt, but with ': kind key
+
+(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.*expressions: 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)

turnstile/examples/tests/fomega-no-reuse-tests.rkt

@@ -1,84 +1,84 @@
 #lang s-exp "../fomega-no-reuse.rkt"
 (require "rackunit-typechecking.rkt")
 
-;; identical to fomega-tests.rkt
+;; mostly identical to fomega-tests.rkt
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-type Int :: ★)
+(check-type String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(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")
+(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 (Λ ([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 (∀ ([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)))
 
-(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 ((λ ([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 (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"))
+(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)
-            : (⇒ ★ ★))
+(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))))
+(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))
+             (Λ ([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.*expressions: 1")
+(typecheck-fail ; TODO: fix err msg: "given an invalid expression"
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst:.*not a valid type: 1") 
 
 (typecheck-fail
- (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (Λ ([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))
+  (Λ ([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))
+              (Λ ([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))
+               (Λ ([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))
+(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))
@@ -91,104 +91,104 @@
 (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))))
+(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
-;(check-type Pair : (⇒ ★ ★ ★))
-(check-type Pair : (⇒ ★ ★ (★ ★)))
+;(check-type Pair :: (⇒ ★ ★ ★))
+(check-type Pair :: (⇒ ★ ★ (★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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))))
+ (Λ ([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)))))
+ (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)))))
+ ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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 :: ★]) (λ ([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 (Λ ([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))))
+            : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2)))))
 
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+(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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
+ (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)
+ ((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)))
+(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)
 
 

turnstile/examples/tests/fomega-tests.rkt

@@ -1,82 +1,84 @@
 #lang s-exp "../fomega.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+;; ok to conflate check-kind and check-type bc
+;; kindcheck? does not require special cases
+(check-type Int :: ★)
+(check-type String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(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")
+(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 (Λ ([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 (∀ ([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)))
 
-(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 ((λ ([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 (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"))
+(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)
-            : (⇒ ★ ★))
+(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))))
+(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))
+             (Λ ([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")
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "inst:.*not a valid type: 1")
 
 (typecheck-fail
- (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (Λ ([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))
+  (Λ ([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))
+              (Λ ([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))
+               (Λ ([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))
+(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))
@@ -89,104 +91,104 @@
 (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))))
+(define-type-alias Pair (tyλ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
 ;(check-type Pair : (⇒ ★ ★ ★))
-(check-type Pair : (⇒ ★ ★ (∀★ ★)))
+(check-type Pair :: (⇒ ★ ★ (∀★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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))))
+ (Λ ([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)))))
+ (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)))))
+ ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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)))
+ (Λ ([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))))
+  (Λ ([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))))
+   (Λ ([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)))))
+  ((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 :: ★]) (λ ([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 (Λ ([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))))
+            : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2)))))
 
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+(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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
+ (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)
+ ((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)))
+(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)
 
 

turnstile/examples/tests/fomega2-tests.rkt

@@ -1,74 +1,76 @@
 #lang s-exp "../fomega2.rkt"
 (require "rackunit-typechecking.rkt")
+(require "rackunit-kindchecking.rkt")
 
-(check-type Int : ★)
-(check-type String : ★)
+(check-kind Int :: ★)
+(check-kind String :: ★)
 (typecheck-fail →)
-(check-type (→ Int Int) : ★)
+(check-kind (→ Int Int) :: ★)
 (typecheck-fail (→ →))
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
 
 ;; this should error but it doesnt
-#;(λ ([x : ★]) 1)
+#;(λ ([x :: ★]) 1)
 
-;(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+;(check-type (∀ ([t :: ★]) (→ t t)) :: ★)
+(check-kind (∀ ([t :: ★]) (→ t t)) :: (∀★ ★))
+(check-kind (→ (∀ ([t :: ★]) (→ t t)) (→ Int Int)) :: ★)
 
-(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(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 ((λ ([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 (λ ([t : ★]) t) : (→ ★ ★))
-(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
-(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
-(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
-(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+;; tests for λ as a type
+(check-kind (λ ([t :: ★]) t) :: (→ ★ ★))
+(check-kind (λ ([t :: ★] [s :: ★]) t) :: (→ ★ ★ ★))
+(check-kind (λ ([t :: ★]) (λ ([s :: ★]) t)) :: (→ ★ (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★)]) t) :: (→ (→ ★ ★) (→ ★ ★)))
+(check-kind (λ ([t :: (→ ★ ★ ★)]) t) :: (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-kind (λ ([arg :: ★] [res :: ★]) (→ arg res)) :: (→ ★ ★ ★))
 
-(check-type ((λ ([t : ★]) t) Int) : ★)
-(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
-(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
-(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+(check-kind ((λ ([t :: ★]) t) Int) :: ★)
+(check-type (λ ([x : ((λ ([t :: ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t :: ★]) t) Int)]) (+ 1 x)) "a-string"))
 
 ;; partial-apply →
-(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
-            : (→ ★ ★))
+(check-kind ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)
+            :: (→ ★ ★))
 ; f's type must have kind ★
-(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
-(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
-            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(typecheck-fail (λ ([f : ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf :: (→ ★ ★)]) (→ (tyf String) (tyf String))))
 (check-type (inst
-             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+             ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int))
             : (→ (→ Int String) (→ Int String)))
 (typecheck-fail
- (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
- ;#:with-msg "not a valid type: 1")
+ (inst (Λ ([X :: ★]) (λ ([x : X]) x)) 1)
+ #:with-msg "not a valid type: 1")
 
 ;; applied f too early
 (typecheck-fail (inst
-                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
-                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+                 (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int)))
 (check-type ((inst
-              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([res :: ★]) (→ arg res))) Int))
              (λ ([x : Int]) "int")) : (→ Int String))
 (check-type (((inst
-               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
-              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+               (Λ ([tyf :: (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg :: ★]) (λ ([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 (λ ([X : ★]) X))
+(define-type-alias Id (λ ([X :: ★]) X))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
 (check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
@@ -81,104 +83,104 @@
 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
 
 ;; tapl examples, p451
-(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+(define-type-alias Pair (λ ([A :: ★] [B :: ★]) (∀ ([X :: ★]) (→ (→ A B X) X))))
 
-;(check-type Pair : (→ ★ ★ ★))
-(check-type Pair : (→ ★ ★ (∀★ ★)))
+;(check-type Pair :: (→ ★ ★ ★))
+(check-type Pair :: (→ ★ ★ (∀★ ★)))
 
-(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+(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 (Pair X Y))))
+ (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X :: ★][Y :: ★]) (→ X Y (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)))))
+ (inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
        Int String)
  : (→ Int String (Pair Int String)))
 ; Pair Int String value
 (check-type
- ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ ((inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y)))))
        Int String) 1 "1")
  : (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 : ★]) (→ (Pair X Y) X)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (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))))
+  (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
   Int String)
  : (→ (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))))
+   (Λ ([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)))))
+  ((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 : ★]) (→ (Pair X Y) Y)))
+ (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X :: ★][Y :: ★]) (→ (Pair X Y) Y)))
 (check-type
  (inst
-  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
   Int String)
  : (→ (Pair Int String) String))
 (check-type
  ((inst
-   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   (Λ ([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)))))
+  ((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)))
+;; 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 (Λ ([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))))
+            : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2)))))
 
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
-            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+(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-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)
+(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))
+(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))
+(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))))
+(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 ((λ ([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))
+ (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)
+ ((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)))
+(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)
 
 

turnstile/examples/tests/mlish-tests.rkt

@@ -295,7 +295,7 @@
    [Nil -> 3])
  : Int ⇒ 6)
             
-;; check expected-type propagation for other match paterns
+;; check expected-type propagation for other match patterns
 
 (define-type (Option A)
   (None)
@@ -450,6 +450,13 @@
 
 (define (ok [a : A] → (Result A B))
   (Ok a))
+
+;; Cannot infer concrete type for B in (Result A B).
+;; Need expected type (see (inst result-if-1 ...) example below)
+(typecheck-fail
+ (λ ([a : Int]) (ok (Cons a Nil)))
+ #:with-msg "Could not infer instantiation of polymorphic function ok")
+
 (define (error [b : B] → (Result A B))
   (Error b))
 
@@ -512,6 +519,7 @@
             : (→ (→ Int (Result (List Int) (List String)))
                  (→ String (Result (List Int) (List String)))
                  (Result (List Int) (List String))))
+
 (check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
              (λ ([a : Int])    (ok (Cons a Nil)))
              (λ ([b : String]) (error (Cons b Nil))))
@@ -671,7 +679,7 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (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")
+(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)

turnstile/examples/tests/rackunit-kindchecking.rkt

@@ -0,0 +1,18 @@
+#lang racket/base
+(require (for-syntax rackunit syntax/srcloc) rackunit macrotypes/typecheck
+         (only-in "../fomega2.rkt" current-kind-eval kindcheck?))
+(provide check-kind)
+
+;; Note: this file is separate from macrotypes/examples/test/rackunit-kindcheck
+;; because each one uses different defs of current-kind-eval and kindcheck?
+(define-syntax (check-kind stx)
+  (syntax-parse stx #:datum-literals (⇒ ->)
+    [(_ τ tag:id k-expected)
+     #:with k (detach (expand/df #'(add-expected τ k-expected))
+                      (stx->datum #'tag))
+     #:fail-unless (kindcheck? #'k ((current-kind-eval) #'k-expected))
+                   (format
+                    "Type ~a [loc ~a:~a] has kind ~a, expected ~a"
+                    (syntax->datum #'τ) (syntax-line #'τ) (syntax-column #'τ)
+                    (type->str #'k) (type->str #'k-expected))
+     #'(void)]))

turnstile/examples/tests/rackunit-typechecking.rkt

@@ -19,19 +19,20 @@
      (string-join (map add-escs (string-split givens ", ")) ".*"))))
 
 (define-syntax (check-type stx)
-  (syntax-parse stx #:datum-literals (: ⇒ ->)
+  (syntax-parse stx #:datum-literals (⇒ ->)
     ;; duplicate code to avoid redundant expansions
-    [(_ e : τ-expected (~or ⇒ ->) v)
+    [(_ e tag:id τ-expected (~or ⇒ ->) v)
      #:with e+ (expand/df #'(add-expected e τ-expected))
-     #:with τ (typeof #'e+)
+     #:with τ (detach #'e+ (stx->datum #'tag))
      #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
                    (format
                     "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
                     (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
                     (type->str #'τ) (type->str #'τ-expected))
      (syntax/loc stx (check-equal? e+ (add-expected v τ-expected)))]
-    [(_ e : τ-expected)
-     #:with τ (typeof (expand/df #'(add-expected e τ-expected)))
+    [(_ e tag:id τ-expected)
+     #:with e+ (expand/df #'(add-expected e τ-expected))
+     #:with τ (detach #'e+ (stx->datum #'tag))
      #:fail-unless
      (typecheck? #'τ ((current-type-eval) #'τ-expected))
      (format

turnstile/examples/trivial.rkt

@@ -120,7 +120,7 @@
            ((current-type=?) t1 #'t2*)]
           [_ #f])))
   (current-type=? new-type=?)
-  (current-typecheck-relation (current-type=?))
+  (current-typecheck-relation new-type=?)
 
   ;; current-type?
   ;; TODO: disabling type validation for now
@@ -282,7 +282,7 @@
                   [x:id : ty])) ...)
       . es) ≫
    #:with (X ...) (generate-temporaries #'(x ...))
-   [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...) 
+   [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...) 
     ⊢ (begin . es) ≫ e- ⇒ τ_out]
    ;; TODO: investigate why this extra syntax-local-introduce is needed?
    #:with τ_out* (syntax-local-introduce #'τ_out)
@@ -344,7 +344,7 @@
    #:with Bs** (prune-Bs #'Bs*)
 ;   #:when (begin (displayln "checking Cs:")
 ;                 (pretty-print (syntax->datum #'Cs*)))
-   #:with remaining-Cs (check-Cs #'Cs* stx)
+   #:with remaining-Cs (check-Cs #'Cs* this-syntax)
 ;   #:when (printf "remaining Cs: ~a\n"
 ;                  (syntax->datum #'remaining-Cs))
    #:with ty-out**

turnstile/info.rkt

@@ -5,8 +5,9 @@
 
 (define compile-omit-paths 
   '("examples/rosette"
+    "examples/fomega3.rkt"
     "examples/tests"
-    "examples/trivial.rkt"))
+    "examples/trivial.rkt")) ; needs typed racket
 
 (define test-include-paths
   '("examples/tests/mlish")) ; to include .mlish files
@@ -16,6 +17,8 @@
     "examples/tests/rosette"             ; needs rosette
     "examples/tests/trivial-test.rkt"    ; needs typed/racket
     "examples/tests/mlish/sweet-map.rkt" ; needs sweet-exp
+    "examples/fomega3.rkt"
+    "examples/tests/fomega3-tests.rkt"
     "examples/tests/mlish/bg/README.md"))
 
 (define test-timeouts

turnstile/scribblings/reference.scrbl

@@ -34,7 +34,7 @@ and then press Control-@litchar{\}.
 
 @; define-typed-syntax---------------------------------------------------------
 @defform*[
-  #:literals (≫ ⊢ ⇒ ⇐ ≻ : --------)
+  #:literals (≫ ⊢ ⇒ ⇐ ≻ --------)
   ((define-typed-syntax (name-id . pattern) ≫
      premise ...
      --------
@@ -50,7 +50,7 @@ and then press Control-@litchar{\}.
           premise ...
           --------
           ⇐-conclusion]
-         [expr-pattern ⇐ key type-pattern ≫
+         [expr-pattern ⇐ key pattern ≫
           premise ...
           --------
           ⇐-conclusion]]
@@ -70,48 +70,86 @@ and then press Control-@litchar{\}.
             type-relation
             (code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
    [ctx (ctx-elem ...)]
-   [ctx-elem (code:line [id ≫ id : type-template] ooo ...)]
+   [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)
+             (code:line id ooo ...)]
    [tc (code:line tc-elem ooo ...)]
    [tc-elem [expr-template ≫ expr-pattern ⇒ type-pattern]
-             [expr-template ≫ expr-pattern ⇒ key type-pattern]
-             [expr-template ≫ expr-pattern (⇒ key type-pattern) ooo ...]
+             [expr-template ≫ expr-pattern ⇒ key pattern]
+             [expr-template ≫ expr-pattern (⇒ key pattern) ooo ...]
              [expr-template ≫ expr-pattern ⇐ type-template]
-             [expr-template ≫ expr-pattern ⇐ key type-template]
-             [expr-template ≫ expr-pattern (⇐ key type-template) ooo ...]]
+             [expr-template ≫ expr-pattern ⇐ key template]
+             [expr-template ≫ expr-pattern (⇐ key template) ooo ...]]
    [type-relation (code:line [type-template τ= type-template] ooo ...)
                   (code:line [type-template τ= type-template #:for expr-template] ooo ...)
                   (code:line [type-template τ⊑ type-template] ooo ...)
                   (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)]
    [conclusion [⊢ expr-template ⇒ type-template]
-               [⊢ expr-template ⇒ key type-template]
-               [⊢ expr-template (⇒ key type-template) ooo ...]
+               [⊢ expr-template ⇒ key template]
+               [⊢ expr-template (⇒ key template) ooo ...]
                [≻ expr-template]
                [#:error expr-template]]
    [⇐-conclusion [⊢ expr-template]]
    [ooo ...])
  ]{
 
-Defines a macro that additionally performs typechecking. It uses
-@racket[syntax-parse] @tech:stx-pats and @tech:pat-directives and
- additionally allows writing type-judgement-like clauses that interleave
- typechecking and macro expansion.
+Generates a macro definition that also performs type checking. The macro is
+generated from @racket[syntax-parse] @tech:stx-pats and @tech:pat-directives,
+along with type-judgement-like clauses that interleave typechecking and macro
+expansion.  The resulting macro type checks its surface syntax as part of macro
+expansion and the resulting type is attached to the expanded expression.
 
-Type checking is computed as part of macro expansion and the resulting type is
-attached to an expanded expression. In addition, Turnstile supports
-bidirectional type checking clauses. For example @racket[[⊢ e ≫ e- ⇒ τ]]
-declares that expression @racket[e] expands to @racket[e-] and has type
-@racket[τ], where @racket[e] is the input and, @racket[e-] and @racket[τ]
-outputs. Syntactically, @racket[e] is a syntax template position and
-@racket[e-] @racket[τ] are syntax pattern positions.
+@; ----------------------------------------------------------------------------
+@bold{Premises}
 
-A programmer may use the generalized form @racket[[⊢ e ≫ e- (⇒ key τ) ...]] to
-specify propagation of arbitrary values, associated with any number of
-keys. For example, a type and effect system may wish to additionally propagate
-source locations of allocations and mutations. When no key is specified,
-@litchar{:}, i.e., the "type" key, is used.  Dually, one may write @racket[[⊢ e
+@italic{Bidirectional judgements}
+
+Turnstile @racket[define-typed-syntax] rules use bidirectional type checking
+judgements:
+@itemlist[
+  @item{@racket[[⊢ e ≫ e- ⇒ τ]] declares that expression @racket[e] expands to
+@racket[e-] and has type @racket[τ], where @racket[e] is the input and,
+@racket[e-] and @racket[τ] outputs. Syntactically, @racket[e] is a syntax
+template position and @racket[e-] and @racket[τ] are syntax pattern positions.}
+
+  @item{Dually, one may write @racket[[⊢ e
 ≫ e- ⇐ τ]] to check that @racket[e] has type @racket[τ]. Here, both @racket[e]
 and @racket[τ] are inputs (templates) and only @racket[e-] is an
-output (pattern).
+output (pattern).}]
+
+Each bidirectional arrow has a generalized form that associates a key with a
+value, e.g., @racket[[⊢ e ≫ e- (⇒ key pat) ...]]. A programmer may use this
+generalized form to specify propagation of arbitrary values, associated with
+any number of keys. For example, a type and effect system may wish to
+additionally propagate source locations of allocations and mutations. When no
+key is specified, @litchar{:}, i.e., the "type" key, is used.
+
+@italic{Contexts}
+
+A context may be specified to the left of the turnstile. A context element has
+shape @racket[[⊢ x ≫ x- key pat ... ...]] where @racket[x-] is a pattern
+matching the expansion of @racket[x] and the interleaved @racket[key ...] and
+@racket[pat ...] are arbitrary key-value pairs, e.g. a @litchar{:} key and type
+pattern.
+
+A context has @racket[let*] semantics where each binding is in scope for
+subsequent parts of the context. This means type and term variables may be in
+the same context (if properly ordered). In addition, Turnstile allows writing
+two separate contexts, grouped by parens, where bindings in first are in scope
+for the second. This is often convenient for scenarios that Racket's pattern
+language cannot express, e.g., when there two distinct groups of bindings, a
+pattern @racket[x ... y ...] will not work as expected.
+
+For convenience, lone identifiers written to the left of the turnstile are
+automatically treated as type variables.
+
+@; ----------------------------------------------------------------------------
+@bold{Conclusion}
+
+Bidirectional judgements below the conclusion line invert their inputs and
+outputs so that both positions in @racket[[⊢ e- ⇒ τ]] are syntax templates and
+means that @racket[e-] is the output of the generated macro and it has type τ
+attached. The generalized key-value form of the bidirectional judgements may
+also be used in the conclusion.
 
 The @racket[≻] conclusion form is useful in many scenarios where the rule being
 implemented may not want to attach type information. E.g.,
@@ -180,6 +218,13 @@ attach type information to the top-level @tt{x} identifier, so the
 
 ]}
 
+@; ----------------------------------------------------------------------------
+@bold{Note}
+
+@racket[define-typed-syntax] is generated by
+@racket[define-syntax-category]. See @racket[define-syntax-category] for more
+information.
+
 @defform[(define-typerule ....)]{Alias for @racket[define-typed-syntax].}
 @defform[(define-syntax/typecheck ....)]{Alias for @racket[define-typed-syntax].}
 
@@ -203,10 +248,30 @@ When not specified, @racket[op-id] is @racket[typed-op-id] suffixed with
 @litchar{-} (see @secref{racket-}).}
 
 @; define-syntax-category -----------------------------------------------------
-@defform[(define-syntax-category name-id)]{
+@defform*[((define-syntax-category name-id)
+           (define-syntax-category key1 name-id)
+           (define-syntax-category key1 name-id key2))]{
+
 Defines a new "category" of syntax by defining a series of forms and functions.
 Turnstile pre-declares @racket[(define-syntax-category type)], which in turn
- defines the following forms and functions:
+defines the forms and functions below.
+
+Each category of syntax is associated with two keys: @racket[key1] is used when
+attaching values in the category to other syntax, e.g., attaching types to
+terms, and @racket[key2] is used for attaching an additional syntax property to
+values in the category, e.g. using @racket[#%type] to indicate well-formedness.
+
+If no keys are specified, @racket[key1] is @litchar{:} and @racket[key2] is
+@litchar{::}. If only @racket[key1] is given, then @racket[key2] is
+@racket[key1] appended to itself.
+
+Defining another category, e.g., @racket[(define-syntax-category kind)],
+defines a separate set of forms and functions, e.g.,
+@racket[define-kinded-syntax], @racket[define-base-kind], @racket[kind=?], etc.
+
+@; ----------------------------------------------------------------------------
+@italic{The following forms and functions are automatically defined by a
+@racket[(define-syntax-category type)] declaration:}
 
 @margin-note{It's not important to immediately understand all these
 definitions. Some, like @racket[type?] and @racket[mk-type], are
@@ -216,35 +281,48 @@ are probably @racket[define-typed-syntax], and the type-defining forms
 @racket[define-binding-type].}
 
  @itemlist[
- @item{@racket[define-typed-syntax], as described above.
-   Uses @racket[current-typecheck-relation] for typechecking.}
+
+ @item{@racket[define-typed-syntax], as described above. Uses
+@racket[current-typecheck-relation] @racket[current-type-eval] for
+typechecking, and uses @litchar{:} as the key when an explicit key is not specificed in type judgements.}
+
  @item{@defform*[((define-base-type base-type-name-id)
-                  (define-base-type base-type-name-id : kind))]{
+                  (define-base-type base-type-name-id key tag))]{
    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[τ].}]}
 
-  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.}}
+  Types defined with @racket[define-base-type] are automatically tagged with a
+@racket[key2]-keyed (as specified in the @racket[define-syntax-category]
+declaration) @racket[#%type] syntax property, unless second form above is used,
+in which case the specified @tt{tag} is attached to the type using the
+specified @tt{key}.}
+
+ @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types, each using the default key.}}
+
  @item{
   @defform[(define-type-constructor name-id option ...)
             #:grammar
            ([option (code:line #:arity op n)
                     (code:line #:arg-variances expr)
                     (code:line #:extra-info stx)])]{
-    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.
-                  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[τ].}]
+    Defines a type constructor (that does not bind type variables).
+    Defining a type constructor @racket[τ] subsequently defines:
+  @itemlist[
+
+    @item{@racket[τ], a macro for constructing an instance of type @racket[τ],
+          with the specified arity.  Validates inputs and expands to
+          @racket[τ-], attaching @racket[#%type] at @tt{key2}.}
+
+    @item{@racket[τ-], an internal macro that expands to the internal
+          (i.e., fully expanded) type representation. Does not validate inputs
+          or attach any extra properties. 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[τ].}]
 
   The @racket[#:arity] argument specifies the valid shapes
     for the type. For example
@@ -274,16 +352,18 @@ are probably @racket[define-typed-syntax], and the type-defining forms
                          (list covariant))])))]
     
     The @racket[#:extra-info] argument is useful for attaching additional
-    metainformation to types, for example to implement pattern matching.}}
+    metainformation to types, for example to communicate accessors to a pattern
+    matching form.}}
  @item{
   @defform[(define-internal-type-constructor name-id option ...)
             #:grammar
-           ([option (code:line #:arity op n)
-                    (code:line #:arg-variances expr)
+           ([option (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.}}
+
+  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
@@ -311,12 +391,10 @@ are probably @racket[define-typed-syntax], and the type-defining forms
  @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)
+           ([option (code:line #:arr kindcon)
                     (code:line #:arg-variances expr)
                     (code:line #:extra-info stx)])]{
-  Analogous to @racket[define-internal-type-constructor].}}
+  Analogous to @racket[define-internal-type-constructor], but for binding types.}}
 @item{
 @defform[(type-out ty-id)]{
 A @racket[provide]-spec that, given @racket[ty-id], provides @racket[ty-id], 
@@ -326,7 +404,7 @@ and provides @racket[for-syntax] a predicate @racket[ty-id?] and a @tech:pat-exp
  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
+immediately before attaching 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.
@@ -420,6 +498,13 @@ equality, but includes alpha-equivalence.
       syntax objects with shape @racket[(b:type-bind ...)].}}
  @item{@defthing[type-ann stx-class]{A syntax class recognizing
        syntax objects with shape @racket[{τ:type}] where the braces are required.}}
+
+ @item{@defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{
+Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e] using @tt{key1}.}}
+
+ @item{@defproc[(typeof [e expr-stx]) type-stx]{
+Phase 1 function returning type of @racket[e], at @tt{key1}.}}
+
  ]
 }
 
@@ -460,13 +545,14 @@ Reuses @racket[name]s from @racket[base-lang].}
 
 To help avoid name conflicts, Turnstile re-provides all Racket bindings with a
 @litchar{-} suffix. These bindings are automatically used in some cases, e.g.,
-@racket[define-primop], but in general are useful for avoiding name conflicts.
+@racket[define-primop], but in general are useful for avoiding name conflicts,
+particularly for commonly used macros like @racket[#%app].
 
 @; Sec: turnstile/lang ----------------------------------------------
 @section[#:tag "turnstilelang"]{@hash-lang[] @racketmodname[turnstile]/lang}
 
 Languages implemented using @hash-lang[] @racketmodname[turnstile]
-must additionally provide @racket[#%module-begin] and other forms required by
+must manually provide @racket[#%module-begin] and other forms required by
 Racket. 
 
 For convenience, Turnstile additionally supplies @hash-lang[]
@@ -482,18 +568,30 @@ 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.
 
-@defproc[(assign-type [e syntax?] [τ syntax?]) syntax?]{
-Phase 1 function that calls @racket[current-type-eval] on @racket[τ] and attaches it to @racket[e]}
-
-@defproc[(typeof [e expr-stx]) type-stx]{
-Phase 1 function returning type of @racket[e].}
-
 @defproc[(infer [es (listof expr-stx)]
                 [#:ctx ctx (listof bindings) null]
-                [#:tvctx tvctx (listof tyvar-bindings) null]) (list tvs xs es τs)]{
-Phase 1 function expanding a list of expressions, in the given contexts and computes their types.
- Returns the expanded expressions, their types, and expanded identifiers from the
- contexts, e.g. @racket[(infer (list #'(+ x 1)) #:ctx ([x : Int]))].}
+                [#:tvctx tvctx (listof tyvar-bindings) null]
+                [#:tag tag symbol? ':])
+                (list tvs xs es τs)]{
+
+Phase 1 function expanding a list of expressions, in the given contexts and
+computes their types. Returns the expanded expressions, their types, and
+expanded identifiers from the contexts, e.g.
+
+@racket[(infer (list #'(+ x 1)) #:ctx ([x : Int]))]
+
+might return
+
+@racket[(list '() (list #'x-) (list #'(#%plain-app x- 1))(list #'Int))].
+
+The context elements have the same shape as in @racket[define-typed-syntax].
+The contexts use @racket[let*] semantics, where each binding is in scope for
+subsequent bindings.
+
+Use the @tt{tag} keyword argument to specify the key for the
+returned "type". The default key is @litchar{:}. For example, a programmer may
+want to specify a @litchar{::} key when using @racket[infer] to compute the
+kinds on types.}
 
 @defproc[(subst [τ type-stx]
                 [x id]

turnstile/turnstile.rkt

@@ -5,9 +5,9 @@
          define-typed-syntax define-syntax-category
          (rename-out [define-typed-syntax define-typerule]
                      [define-typed-syntax define-syntax/typecheck])
-         (for-syntax syntax-parse/typed-syntax
+         (for-syntax syntax-parse/typecheck
                      (rename-out
-                      [syntax-parse/typed-syntax syntax-parse/typecheck])))
+                      [syntax-parse/typecheck syntax-parse/typed-syntax])))
 
 (require (except-in (rename-in
                      macrotypes/typecheck
@@ -25,16 +25,18 @@
   ;;   xs-   ; a stx-list of the expanded versions of variables in the ctx
   ;;   es*-  ; a nested list a depth given by the depth argument, with the same structure
   ;;         ; as es*, containing the expanded es*, with the types attached
-  (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*)
+  (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*
+                       #:tag [tag (current-tag)])
     (define flat (stx-flatten/depth-lens depth))
     (define es (lens-view flat es*))
     (define origs (lens-view flat origs*))
     (define/with-syntax [tvxs- xs- es- _]
-      (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs)))
-    (define es*- (lens-set flat es* #'es-))
+      (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag))
+    (define es*- (lens-set flat es* #`es-))
     (list #'tvxs- #'xs- es*-))
   ;; infers/depths
-  (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*)
+  (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*
+                         #:tag [tag (current-tag)])
     (define flat (stx-flatten/depth-lens clause-depth))
     (define tvctxs/ctxs/ess/origss
       (lens-view flat tvctxs/ctxs/ess/origss*))
@@ -42,7 +44,7 @@
       (for/list ([tvctx/ctx/es/origs (in-list (stx->list tvctxs/ctxs/ess/origss))])
         (match-define (list tvctx ctx es origs)
           (stx->list tvctx/ctx/es/origs))
-        (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs)))
+        (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs #:tag tag)))
     (define res
       (lens-set flat tvctxs/ctxs/ess/origss* tcs))
     res)
@@ -92,44 +94,45 @@
   (define-splicing-syntax-class ⇒-prop
     #:datum-literals (⇒)
     #:attributes (e-pat)
-    [pattern (~or (~seq ⇒ tag-pat ; implicit : tag
-                        (~parse tag #':) (tag-prop:⇒-prop) ...)
+    [pattern (~or (~seq ⇒ tag-pat ; implicit tag
+                          (~parse tag #',(current-tag))
+                          (tag-prop:⇒-prop) ...)
                   (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
              #:with e-tmp (generate-temporary)
              #:with e-pat
              #'(~and e-tmp
                      (~parse
                       (~and tag-prop.e-pat ... tag-pat)
-                      (typeof #'e-tmp #:tag 'tag)))])
+                      (detach #'e-tmp `tag)))])
   (define-splicing-syntax-class ⇒-prop/conclusion
     #:datum-literals (⇒)
     #:attributes (tag tag-expr)
-    [pattern (~or (~seq ⇒ tag-stx 
-                        (~parse tag #':)
-                        (~parse (tag-prop.tag ...) #'())
-                        (~parse (tag-prop.tag-expr ...) #'()))
+    [pattern (~or (~seq ⇒ tag-stx ; implicit tag
+                          (~parse tag #',(current-tag))
+                          (~parse (tag-prop.tag ...) #'())
+                          (~parse (tag-prop.tag-expr ...) #'()))
                   (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
              #:with tag-expr
              (for/fold ([tag-expr #'#`tag-stx])
-                       ([k (in-list (syntax->list #'[tag-prop.tag ...]))]
-                        [v (in-list (syntax->list #'[tag-prop.tag-expr ...]))])
+                       ([k (in-stx-list #'[tag-prop.tag ...])]
+                        [v (in-stx-list #'[tag-prop.tag-expr ...])])
                (with-syntax ([tag-expr tag-expr] [k k] [v v])
-                 #'(assign-type tag-expr #:tag 'k v)))])
+                 #'(attach tag-expr `k ((current-ev) v))))])
   (define-splicing-syntax-class ⇐-prop
-    #:datum-literals (⇐ :)
+    #:datum-literals (⇐)
     #:attributes (τ-stx e-pat)
-    [pattern (~or (~seq ⇐ τ-stx)
-                  (~seq ⇐ : τ-stx))
+    [pattern (~or (~seq ⇐ τ-stx (~parse tag #',(current-tag)))
+                  (~seq ⇐ tag:id τ-stx))
              #:with e-tmp (generate-temporary)
              #:with τ-tmp (generate-temporary)
              #:with τ-exp (generate-temporary)
              #:with e-pat
-             #'(~and e-tmp
+             #`(~and e-tmp
                      (~parse τ-exp (get-expected-type #'e-tmp))
-                     (~parse τ-tmp (typeof #'e-tmp))
+                     (~parse τ-tmp (detach #'e-tmp `tag))
                      (~parse
                       (~post
-                       (~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp))
+                       (~fail #:when (and (not (check? #'τ-tmp #'τ-exp))
                                           (get-orig #'e-tmp))
                               (typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp)))
                       (get-orig #'e-tmp)))])
@@ -153,6 +156,12 @@
   (define-splicing-syntax-class id+props+≫
     #:datum-literals (≫)
     #:attributes ([x- 1] [ctx 1])
+    [pattern (~seq (~and X:id (~not _:elipsis)))
+             #:with [x- ...] #'[_]
+             #:with [ctx ...] #'[[X :: #%type]]]
+    [pattern (~seq X:id ooo:elipsis)
+             #:with [x- ...] #'[_ ooo]
+             #:with [ctx ...] #'[[X :: #%type] ooo]]
     [pattern (~seq [x:id ≫ x--:id props:props])
              #:with [x- ...] #'[x--]
              #:with [ctx ...] #'[[x props.stuff ...]]]
@@ -165,7 +174,7 @@
              #:with [x- ...] #'[ctx1.x- ... ...]
              #:with [ctx ...] #'[ctx1.ctx ... ...]])
   (define-syntax-class tc-elem
-    #:datum-literals (⊢ ⇒ ⇐ ≫ :)
+    #:datum-literals (⊢ ⇒ ⇐ ≫)
     #:attributes (e-stx e-stx-orig e-pat)
     [pattern [e-stx ≫ e-pat* props:⇒-props]
              #:with e-stx-orig #'e-stx
@@ -198,9 +207,9 @@
                    (define max-d (apply max 0 ds))]
              #:with depth (add1 max-d)
              #:with [[es-stx* es-stx-orig* es-pat*] ...]
-             (for/list ([tc-es-stx (in-list (syntax->list #'[tc.es-stx ...]))]
-                        [tc-es-stx-orig (in-list (syntax->list #'[tc.es-stx-orig ...]))]
-                        [tc-es-pat (in-list (syntax->list #'[tc.es-pat ...]))]
+             (for/list ([tc-es-stx (in-stx-list #'[tc.es-stx ...])]
+                        [tc-es-stx-orig (in-stx-list #'[tc.es-stx-orig ...])]
+                        [tc-es-pat (in-stx-list #'[tc.es-pat ...])]
                         [d (in-list ds)])
                (list
                 (add-lists tc-es-stx (- max-d d))
@@ -226,58 +235,59 @@
               #'[ooo ...])
              #:with tvctxs/ctxs/ess/origs
              (with-depth
-              #'[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
+              #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
               #'[ooo ...])
              #:with pat
-             #'(~post
+             #`(~post
                 (~post
                  (~parse
                   tcs-pat
-                  (infers/depths 'clause-depth 'tc.depth #'tvctxs/ctxs/ess/origs))))]
+                  (infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs
+                                 #:tag (current-tag)))))]
     )
   (define-splicing-syntax-class clause
     #:attributes (pat)
-    #:datum-literals (τ⊑ τ=)
+    #:datum-literals (τ⊑ τ=) ; TODO: drop the τ in τ⊑ and τ=
     [pattern :tc-clause]
     [pattern [a τ⊑ b]
              #:with pat
              #'(~post
-                (~fail #:unless (typecheck? #'a #'b)
+                (~fail #:unless (check? #'a #'b)
                        (typecheck-fail-msg/1/no-expr #'b #'a)))]
     [pattern [a τ⊑ b #:for e]
              #:with pat
              #'(~post
-                (~fail #:unless (typecheck? #'a #'b)
+                (~fail #:unless (check? #'a #'b)
                        (typecheck-fail-msg/1 #'b #'a #'e)))]
     [pattern (~seq [a τ⊑ b] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
+                (~fail #:unless (checks? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
     [pattern (~seq [a τ⊑ b #:for e] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
+                (~fail #:unless (checks? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
     [pattern [a τ= b]
              #:with pat
              #'(~post
-                (~fail #:unless ((current-type=?) #'a #'b)
+                (~fail #:unless ((current=?) #'a #'b)
                        (typecheck-fail-msg/1/no-expr #'b #'a)))]
     [pattern [a τ= b #:for e]
              #:with pat
              #'(~post
-                (~fail #:unless ((current-type=?) #'a #'b)
+                (~fail #:unless ((current=?) #'a #'b)
                        (typecheck-fail-msg/1 #'b #'a #'e)))]
     [pattern (~seq [a τ= b] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (types=? #'[a ooo] #'[b ooo])
+                (~fail #:unless (=s? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]
     [pattern (~seq [a τ= b #:for e] ooo:elipsis)
              #:with pat
              #'(~post
-                (~fail #:unless (types=? #'[a ooo] #'[b ooo])
+                (~fail #:unless (=s? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
     [pattern (~seq #:when condition:expr)
              #:with pat
@@ -296,7 +306,7 @@
              #'(~post (~fail #:unless condition message))]
     )
   (define-syntax-class last-clause
-    #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
+    #:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
     #:attributes ([pat 0] [stuff 1] [body 0])
     ;; ⇒ conclusion
     [pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
@@ -304,21 +314,25 @@
              #:with [stuff ...] #'[]
              #:with body:expr
              (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
-                       ([k (in-list (syntax->list #'[props.tag ...]))]
-                        [v (in-list (syntax->list #'[props.tag-expr ...]))])
+                       ([k (in-stx-list #'[props.tag ...])]
+                        [v (in-stx-list #'[props.tag-expr ...])])
                (with-syntax ([body body] [k k] [v v])
-                 #'(assign-type body #:tag 'k v)))]
+                 #`(attach body `k ((current-ev) v))))]
     ;; ⇒ conclusion, implicit pat
     [pattern (~or [⊢ e-stx props:⇒-props/conclusion]
                   [⊢ [e-stx props:⇒-props/conclusion]])
              #:with :last-clause #'[⊢ [_ ≫ e-stx . props]]]
     ;; ⇐ conclusion
-    [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))]
-             #:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
-    [pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
-                  [⊢ pat* ≫ e-stx ⇐ : τ-pat]
-                  [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
-                  [⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
+    [pattern [⊢ (~and e-stx (~not [_ ≫ . rst]))] ;; TODO: this current tag isnt right?
+             #:with :last-clause #`[⊢ [_ ≫ e-stx ⇐ #,(datum->stx #'h (current-tag)) _]]]
+    [pattern (~or [⊢ pat* (~seq ≫ e-stx
+                                ⇐ τ-pat ; implicit tag
+                                  (~parse tag #',(current-tag)))]
+                  [⊢ pat* ≫ e-stx ⇐ tag:id τ-pat] ; explicit tag
+                  [⊢ [pat* (~seq ≫ e-stx
+                                 ⇐ τ-pat ; implicit tag
+                                   (~parse tag #',(current-tag)))]]
+                  [⊢ [pat* ≫ e-stx ⇐ tag:id τ-pat]]) ; explicit tag
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with pat
@@ -330,7 +344,7 @@
                      (~parse τ-pat #'τ))
              #:with [stuff ...] #'[]
              #:with body:expr
-             #'(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]
+                    #'(attach (quasisyntax/loc this-syntax e-stx) `tag #`τ)]
     ;; macro invocations
     [pattern [≻ e-stx]
              #:with :last-clause #'[_ ≻ e-stx]]
@@ -346,11 +360,12 @@
              #:with body:expr
              ;; should never get here
              #'(error msg)])
-  (define-splicing-syntax-class pat #:datum-literals (⇐ :)
+  (define-splicing-syntax-class pat #:datum-literals (⇐)
     [pattern (~seq pat)
              #:attr transform-body identity]
-    [pattern (~or (~seq pat* left:⇐ τ-pat)
-                  (~seq pat* left:⇐ : τ-pat))
+    [pattern (~or (~seq pat* left:⇐ τ-pat ; implicit tag
+                        (~parse tag #',(current-tag)))
+                  (~seq pat* left:⇐ tag:id τ-pat)) ; explicit tag
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with b (generate-temporary 'body)
@@ -363,11 +378,10 @@
                      (~parse τ-pat #'τ))
              #:attr transform-body
              (lambda (body)
-               #`(let ([b #,body])
-                   (when (and (typeof b)
-                              (not (typecheck? (typeof b) #'τ)))
-                     (raise-⇐-expected-type-error #'left b #'τ (typeof b)))
-                   (assign-type b #'τ)))])
+               #`(let* ([b #,body][ty-b (detach b `tag)])
+                   (when (and ty-b (not (check? ty-b #'τ)))
+                     (raise-⇐-expected-type-error #'left b #'τ ty-b))
+                   (attach b `tag #'τ)))])
   (define-syntax-class rule #:datum-literals (≫)
     [pattern [pat:pat ≫
               clause:clause ...
@@ -388,62 +402,59 @@
 (require (for-meta 1 'syntax-classes)
          (for-meta 2 'syntax-classes))
 
-(define-syntax define-typed-syntax
-  (lambda (stx)
-    (syntax-parse stx
-      ;; single-clause def
-      [(def (name:id . pats) . rst)
-       ;; cannot always bind name as pat var, eg #%app, so replace with _
-       #:with r:rule #'[(_ . pats) . rst]
-       #'(-define-typed-syntax name r.norm)]
-      ;; multi-clause def
-      [(def name:id
-         (~and (~seq kw-stuff ...) :stxparse-kws)
-         rule:rule
-         ...+)
-       #'(-define-typed-syntax
-          name
-          kw-stuff ...
-          rule.norm
-          ...)])))
-
 (begin-for-syntax
-  (define-syntax syntax-parse/typed-syntax
-    (lambda (stx)
-      (syntax-parse stx
-        [(stxparse
-          stx-expr
+  (define-syntax syntax-parse/typecheck
+    (syntax-parser
+      [(_ stx-expr
           (~and (~seq kw-stuff ...) :stxparse-kws)
-          rule:rule
-          ...)
-         #'(syntax-parse
-               stx-expr
-             kw-stuff ...
-             rule.norm
-             ...)]))))
+          rule:rule ...)
+       #'(syntax-parse stx-expr kw-stuff ... rule.norm ...)])))
+
+;; macrotypes/typecheck.rkt already defines (-define-syntax-category type);
+;; - just add the "def-named-syntax" part of the def-stx-cat macro below
+;; TODO: eliminate code dup with def-named-stx in define-stx-cat below?
+(define-syntax define-typed-syntax
+  (syntax-parser
+    ;; single-clause def
+    [(_ (rulename:id . pats) . rst)
+     ;; using #'rulename as patvar may cause problems, eg #%app, so use _
+     #'(define-typed-syntax rulename [(_ . pats) . rst])]
+    ;; multi-clause def
+    ;; - let stx-parse/tychk match :rule (dont double-match)
+    [(_ rulename:id
+        (~and (~seq kw-stuff ...) :stxparse-kws)
+        rule ...+)
+     #'(define-syntax (rulename stx)
+         (parameterize ([current-check-relation (current-typecheck-relation)]
+                        [current-ev (current-type-eval)]
+                        [current-tag (type-key1)])
+           (syntax-parse/typecheck stx kw-stuff ... rule ...)))]))
 
 (define-syntax define-syntax-category
- (lambda (stx)
-   (syntax-parse stx
-    [(_ name:id)
+  (syntax-parser
+    [(_ name:id)        ; default key1 = ': for types
+     #'(define-syntax-category : name)]
+    [(_ key:id name:id) ; default key2 = ':: for kinds
+     #`(define-syntax-category key name #,(mkx2 #'key))]
+    [(_ key1:id name:id key2:id)
      #:with def-named-syntax (format-id #'name "define-~aed-syntax" #'name)
-     #:with check-relation (format-id #'name "current-~acheck-relation" #'name)
+     #:with new-check-rel (format-id #'name "current-~acheck-relation" #'name)
+     #:with new-eval (format-id #'name "current-~a-eval" #'name)
      #'(begin
-        (-define-syntax-category name)
-        (define-syntax (def-named-syntax stx)
-          (syntax-parse stx
+        (-define-syntax-category key1 name key2)
+        (define-syntax def-named-syntax
+          (syntax-parser
             ;; 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
+            [(_ (rulename:id . pats) . rst)
+             ;; #'rulename as a pat var may cause problems, eg #%app, so use _
+             #'(def-named-syntax rulename [(_ . pats) . rst])]
+            ;; 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 (... ...))))])))])))
+              rule (... ...+)) ; let stx-parse/tychk match :rule stxcls
+            #'(define-syntax (rulename stx)
+                (parameterize ([current-check-relation (new-check-rel)]
+                               [current-ev (new-eval)]
+                               [current-tag 'key1])
+                  (syntax-parse/typecheck stx kw-stuff (... ...)
+                    rule (... ...))))])))]))