From 5d412504fbae9e4f2ac0e17bcc10b1600720522c Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Wed, 23 Aug 2017 14:22:11 -0400
Subject: [PATCH] add linear language examples

closes #19
---
 turnstile/examples/linear-var-assign.rkt      | 184 ---------
 turnstile/examples/linear/lin+chan.rkt        |  61 +++
 turnstile/examples/linear/lin+cons.rkt        |  80 ++++
 turnstile/examples/linear/lin+tup.rkt         | 112 ++++++
 turnstile/examples/linear/lin+var.rkt         | 118 ++++++
 turnstile/examples/linear/lin.rkt             | 349 ++++++++++++++++++
 .../tests/linear-var-assign-tests.rkt         |  63 ----
 .../examples/tests/linear/lin+chan-tests.rkt  |  18 +
 .../examples/tests/linear/lin+cons-tests.rkt  |  28 ++
 .../examples/tests/linear/lin+tup-tests.rkt   |  29 ++
 .../examples/tests/linear/lin+var-tests.rkt   |  67 ++++
 turnstile/examples/tests/linear/lin-tests.rkt |  76 ++++
 12 files changed, 938 insertions(+), 247 deletions(-)
 delete mode 100644 turnstile/examples/linear-var-assign.rkt
 create mode 100644 turnstile/examples/linear/lin+chan.rkt
 create mode 100644 turnstile/examples/linear/lin+cons.rkt
 create mode 100644 turnstile/examples/linear/lin+tup.rkt
 create mode 100644 turnstile/examples/linear/lin+var.rkt
 create mode 100644 turnstile/examples/linear/lin.rkt
 delete mode 100644 turnstile/examples/tests/linear-var-assign-tests.rkt
 create mode 100644 turnstile/examples/tests/linear/lin+chan-tests.rkt
 create mode 100644 turnstile/examples/tests/linear/lin+cons-tests.rkt
 create mode 100644 turnstile/examples/tests/linear/lin+tup-tests.rkt
 create mode 100644 turnstile/examples/tests/linear/lin+var-tests.rkt
 create mode 100644 turnstile/examples/tests/linear/lin-tests.rkt

diff --git a/turnstile/examples/linear-var-assign.rkt b/turnstile/examples/linear-var-assign.rkt
deleted file mode 100644
index ad718d0..0000000
--- a/turnstile/examples/linear-var-assign.rkt
+++ /dev/null
@@ -1,184 +0,0 @@
-#lang turnstile
-(extends "ext-stlc.rkt"
-         #:except
-         define-type-alias
-         define if begin let let* letrec λ #%app
-         ⊔ zero? = add1 sub1 not void +)
-
-(provide (for-syntax current-linear?
-                     linear-scope
-                     linear-var-in-scope?
-                     use-linear-var!)
-
-         (type-out Unit Int String Bool -o ⊗ !!)
-         #%top-interaction #%module-begin require only-in
-         begin tup let λ #%app if
-         (rename-out [λ lambda])
-
-         (typed-out [+ : (!! (-o Int Int Int))]
-                    [< : (!! (-o Int Int Bool))]
-                    [displayln : (!! (-o String Unit))]))
-
-
-(define-type-constructor -o #:arity >= 1)
-(define-type-constructor ⊗ #:arity = 2)
-(define-type-constructor !! #:arity = 1)
-
-
-(begin-for-syntax
-  (require syntax/id-set)
-  (define (sym-diff s0 . ss)
-    (for*/fold ([s0 s0])
-               ([s (in-list ss)]
-                [x (in-set s)])
-      (if (set-member? s0 x)
-          (set-remove s0 x)
-          (set-add s0 x))))
-
-
-  (define (fail/multiple-use x)
-    (raise-syntax-error #f "linear variable used more than once" x))
-  (define (fail/unused x)
-    (raise-syntax-error #f "linear variable unused" x))
-  (define (fail/unbalanced-branches x)
-    (raise-syntax-error #f "linear variable may be unused in certain branches" x))
-  (define (fail/unrestricted-fn x)
-    (raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
-
-
-  ; current-linear : (Parameter (TypeStx -> Bool))
-  (define current-linear?
-    (make-parameter (or/c -o? ⊗?)))
-
-  ; linear-type? : TypeStx -> Bool
-  (define (linear-type? t)
-    ((current-linear?) t))
-
-  ; unrestricted-type? : TypeStx -> Bool
-  (define (unrestricted-type? t)
-    (not (linear-type? t)))
-
-
-  ; linear-scope : FreeIdSet
-  ;   holds a list of all linear variables that have been used.
-  (define linear-scope
-    (immutable-free-id-set))
-
-  ; linear-var-in-scope? : Id -> Bool
-  (define (linear-var-in-scope? x)
-    (not (set-member? linear-scope x)))
-
-  ; use-linear-var! : Id -> Void
-  (define (use-linear-var! x #:fail [fail fail/multiple-use])
-    (unless (linear-var-in-scope? x)
-      (fail x))
-    (set! linear-scope (set-add linear-scope x)))
-
-  ; pop-linear-scope! : StxList -> Void
-  ;   drops from scope the linear variables in the given context
-  ;   ignores unrestricted types in the context, but checks that
-  ;   variables with linear types must be used already.
-  ;   the context is a syntax list of the form #'([x τ] ...)
-  (define (pop-linear-scope! ctx #:fail [fail fail/unused])
-    (syntax-parse ctx
-      [([X T] ...)
-       (for ([x (in-syntax #'[X ...])]
-             [t (in-syntax #'[T ...])])
-         (when (and (linear-type? t)
-                    (linear-var-in-scope? x))
-           (fail x)))]))
-
-  ; merge-linear-scope! : FreeIdSet -> Void
-  ;  ensure that the current scope and the given scope are compatible,
-  ;  e.g. when unifying the branches in a conditional
-  (define (merge-linear-scope! merge-scope #:fail [fail fail/unbalanced-branches])
-    (for ([x (in-set (sym-diff linear-scope
-                               merge-scope))])
-      (fail x)))
-
-  )
-
-
-(define-typed-variable-syntax
-  #:datum-literals [:]
-  [(_ x- : σ) ≫ ; record use when σ restricted
-   #:do [(unless (unrestricted-type? #'σ)
-           (use-linear-var! #'x-))]
-   --------
-   [⊢ x- ⇒ σ]])
-
-
-(define-typed-syntax begin
-  [(_ e ... e0) ≫
-   [⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]]
-   --------
-   [⊢ (begin- e- ... e0-) ⇒ σ]])
-
-
-(define-typed-syntax tup
-  [(_ e1 e2) ≫
-   [⊢ e1 ≫ e1- ⇒ σ1]
-   [⊢ e2 ≫ e2- ⇒ σ2]
-   --------
-   [⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]])
-
-
-(define-typed-syntax let
-  [(let ([x rhs] ...) e) ≫
-   [⊢ [rhs ≫ rhs- ⇒ σ] ...]
-   [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
-   #:do [(pop-linear-scope! #'([x- σ] ...))]
-   --------
-   [⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]])
-
-
-(define-typed-syntax λ
-  #:datum-literals (: !)
-  ; linear function
-  [(λ ([x:id : T:type] ...) e) ≫
-   #:with (σ ...) #'(T.norm ...)
-   [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
-   #:do [(pop-linear-scope! #'([x- σ] ...))]
-   --------
-   [⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]]
-
-  ; unrestricted function
-  [(λ ! ([x:id : T:type] ...) e) ≫
-   #:with (σ ...) #'(T.norm ...)
-   #:do [(define scope-prev linear-scope)]
-   [[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
-   #:do [(pop-linear-scope! #'([x- σ] ...))
-         (merge-linear-scope! scope-prev
-                              #:fail fail/unrestricted-fn)]
-   --------
-   [⊢ (λ- (x- ...) e-) ⇒ (!! (-o σ ... σ_out))]])
-
-
-(define-typed-syntax #%app
-  [(_) ≫
-   --------
-   [⊢ (#%app- void-) ⇒ Unit]]
-
-  [(#%app fun arg ...) ≫
-   [⊢ fun ≫ fun- ⇒ σ_fun]
-   #:with (~or (~-o σ_in ... σ_out)
-               (~!! (~-o σ_in ... σ_out))
-               (~post (~fail "expected linear function type")))
-   #'σ_fun
-   [⊢ [arg ≫ arg- ⇐ σ_in] ...]
-   --------
-   [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
-
-
-(define-typed-syntax if
-  [(if c e1 e2) ≫
-   [⊢ c ≫ c- ⇐ Bool]
-   #:do [(define scope-pre-branch linear-scope)]
-   [⊢ e1 ≫ e1- ⇒ σ]
-   #:do [(define scope-then linear-scope)
-         (set! linear-scope scope-pre-branch)]
-   [⊢ e2 ≫ e2- ⇐ σ]
-   #:do [(merge-linear-scope! scope-then
-                              #:fail fail/unbalanced-branches)]
-   --------
-   [⊢ (if- c- e1- e2-) ⇒ σ]])
diff --git a/turnstile/examples/linear/lin+chan.rkt b/turnstile/examples/linear/lin+chan.rkt
new file mode 100644
index 0000000..e16db31
--- /dev/null
+++ b/turnstile/examples/linear/lin+chan.rkt
@@ -0,0 +1,61 @@
+#lang turnstile/lang
+(extends "lin+tup.rkt")
+
+(provide (type-out InChan OutChan)
+         make-channel channel-put channel-get
+         thread sleep)
+
+(define-type-constructor InChan #:arity = 1)
+(define-type-constructor OutChan #:arity = 1)
+
+(begin-for-syntax
+  (current-linear-type? (or/c InChan? (current-linear-type?))))
+
+
+(define-typed-syntax make-channel
+  [(_ {ty:type}) ≫
+   #:with σ #'ty.norm
+   #:with tmp (generate-temporary)
+   --------
+   [⊢ (let ([tmp (#%app- make-channel-)])
+            (list tmp tmp))
+      ⇒ (⊗ (InChan σ) (OutChan σ))]])
+
+
+(define-typed-syntax channel-put
+  [(_ ch e) ≫
+   [⊢ ch ≫ ch- ⇒ (~OutChan σ)]
+   [⊢ e ≫ e- ⇐ σ]
+   --------
+   [⊢ (channel-put- ch- e-) ⇒ Unit]])
+
+
+(define-typed-syntax channel-get
+  [(_ ch) ≫
+   [⊢ ch ≫ ch- ⇒ (~InChan σ)]
+   #:with tmp (generate-temporary #'ch)
+   --------
+   [⊢ (let ([tmp ch-])
+            (list tmp (channel-get- tmp)))
+      ⇒ (⊗ (InChan σ) σ)]])
+
+
+(define-typed-syntax thread
+  [(_ f) ≫
+   [⊢ f ≫ f- ⇒ (~-o _)]
+   --------
+   [⊢ (void (thread- f-)) ⇒ Unit]])
+
+
+(define-typed-syntax sleep
+  [(_) ≫
+   --------
+   [⊢ (sleep-) ⇒ Unit]]
+
+  [(_ e) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   #:fail-unless (or (Int? #'σ)
+                     (Float? #'σ))
+   "invalid sleep time, expected Int or Float"
+   --------
+   [⊢ (sleep- e-) ⇒ Unit]])
diff --git a/turnstile/examples/linear/lin+cons.rkt b/turnstile/examples/linear/lin+cons.rkt
new file mode 100644
index 0000000..b6a43fe
--- /dev/null
+++ b/turnstile/examples/linear/lin+cons.rkt
@@ -0,0 +1,80 @@
+#lang turnstile/lang
+(extends "lin+tup.rkt")
+
+(provide (type-out MList MList0)
+         cons nil match-list)
+
+(define-type-constructor MList #:arity = 1)
+(define-base-type MList0)
+
+(begin-for-syntax
+  (current-linear-type? (or/c MList? MList0? (current-linear-type?))))
+
+
+(define-typed-syntax cons
+  #:datum-literals (@)
+
+  ; implicit memory location created
+  [(_ e e_rest) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
+   --------
+   [⊢ (#%app- mcons- e- e_rest-) ⇒ (MList σ)]]
+
+  ; with memory location given
+  [(_ e e_rest @ e_loc) ≫
+   [⊢ e ≫ e- ⇒ σ]
+   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
+   [⊢ e_loc ≫ e_loc- ⇐ MList0]
+   #:with tmp (generate-temporary #'e_loc)
+   --------
+   [⊢ (let- ([tmp e_loc-])
+            (set-mcar!- tmp e-)
+            (set-mcdr!- tmp e_rest-)
+            tmp)
+      ⇒ (MList σ)]])
+
+
+(define-typed-syntax nil
+  [(_ {ty:type}) ≫
+   --------
+   [⊢ '() ⇒ (MList ty.norm)]]
+  [(_) ⇐ (~MList σ) ≫
+   --------
+   [⊢ '()]])
+
+
+(define-typed-syntax match-list
+  #:datum-literals (cons nil @)
+  [(_ e_list
+      (~or [(cons x+:id xs+:id @ l+:id) e_cons+]
+           [(nil) e_nil+]) ...) ≫
+   #:with [(l x xs e_cons)] #'[(l+ x+ xs+ e_cons+) ...]
+   #:with [e_nil] #'[e_nil+ ...]
+
+   ; list
+   [⊢ e_list ≫ e_list- ⇒ (~MList σ)]
+   #:with σ_xs ((current-type-eval) #'(MList σ))
+   #:with σ_l ((current-type-eval) #'MList0)
+
+   #:mode (make-linear-branch-mode 2)
+     (; cons branch
+      #:submode (branch-nth 0)
+        ([[x ≫ x- : σ]
+          [xs ≫ xs- : σ_xs]
+          [l ≫ l- : σ_l]
+          ⊢ e_cons ≫ e_cons- ⇒ σ_out]
+         #:do [(linear-out-of-scope! #'([x- : σ] [xs- : σ_xs] [l- : σ_l]))])
+
+      ; nil branch
+      #:submode (branch-nth 1)
+        ([⊢ [e_nil ≫ e_nil- ⇐ σ_out]]))
+
+   --------
+   [⊢ (let- ([l- e_list-])
+            (if- (null? l-)
+                 e_nil-
+                 (let- ([x- (mcar- l-)]
+                        [xs- (mcdr- l-)])
+                       e_cons-)))
+      ⇒ σ_out]])
diff --git a/turnstile/examples/linear/lin+tup.rkt b/turnstile/examples/linear/lin+tup.rkt
new file mode 100644
index 0000000..476924f
--- /dev/null
+++ b/turnstile/examples/linear/lin+tup.rkt
@@ -0,0 +1,112 @@
+#lang turnstile/lang
+(extends "lin.rkt")
+
+(provide (type-out ⊗) tup let*)
+(begin-for-syntax (provide in-cad*rs
+                           list-destructure-syntax))
+
+(define-type-constructor ⊗ #:arity >= 2)
+
+(begin-for-syntax
+  (define (num-tuple-fail-msg σs xs)
+    (format "wrong number of tuple elements: expected ~a, got ~a"
+            (stx-length xs)
+            (stx-length σs)))
+
+  (current-linear-type? (or/c ⊗? (current-linear-type?))))
+
+
+(define-typed-syntax tup
+  [(_ e1 e2 ...+) ≫
+   [⊢ e1 ≫ e1- ⇒ σ1]
+   [⊢ e2 ≫ e2- ⇒ σ2] ...
+   --------
+   [⊢ (list- e1- e2- ...) ⇒ (⊗ σ1 σ2 ...)]])
+
+
+(define-typed-syntax let*
+  ; normal let* recursive bindings
+  [(_ ([x:id e_rhs] . xs) . body) ≫
+   [⊢ e_rhs ≫ e_rhs- ⇒ σ]
+   [[x ≫ x- : σ] ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ]))]
+   --------
+   [⊢ (let- ([x- e_rhs-]) e_body-) ⇒ σ_out]]
+
+  ; tuple unpacking with (let* ([(x ...) tup]) ...)
+  [(_ ([(x:id ...) e_rhs] . xs) . body) ≫
+   [⊢ e_rhs ≫ e_rhs- ⇒ (~⊗ σ ...)]
+   #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
+                 (num-tuple-fail-msg #'[σ ...] #'[x ...])
+
+   [[x ≫ x- : σ] ... ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+
+   #:with tmp (generate-temporary #'e_tup)
+   #:with destr (list-destructure-syntax #'[x- ...] #'tmp #:unsafe? #t
+                                         #'e_body-)
+   --------
+   [⊢ (let- ([tmp e_rhs-]) destr) ⇒ σ_out]]
+
+  [(_ () e) ≫
+   --------
+   [≻ e]]
+
+  [(_ () e ...+) ≫
+   --------
+   [≻ (lin:begin e ...)]])
+
+
+
+(require racket/unsafe/ops)
+
+;; generate infinite sequence of cad*r syntax, e.g.
+;;   (car e) (cadr e) (caddr e) ...
+(define-for-syntax (in-cad*rs e #:unsafe? [unsafe? #f])
+  (make-do-sequence
+   (λ ()
+     (values (λ (s)
+               (if unsafe?
+                   (quasisyntax/loc e (unsafe-car #,s))
+                   (quasisyntax/loc e (car #,s))))
+             (λ (s)
+               (if unsafe?
+                   (quasisyntax/loc e (unsafe-cdr #,s))
+                   (quasisyntax/loc e (cdr #,s))))
+             e
+             #f #f #f))))
+
+
+;; (list-destructure-syntax #'(x y z ...) #'rhs #'body)
+;;   =
+;; (let ([x (car rhs)]
+;;       [y (cadr rhs)]
+;;       [z (caddr rhs)]
+;;       ...)
+;;   body)
+(define-for-syntax (list-destructure-syntax xs rhs body #:unsafe? [unsafe? #f])
+  (with-syntax ([binds (for/list ([c (in-cad*rs rhs #:unsafe? unsafe?)]
+                                  [x (in-syntax xs)])
+                         (list x c))]
+                [body body])
+    (syntax/loc rhs
+      (let- binds body))))
+
+
+
+(module+ test
+  (begin-for-syntax
+    (require  rackunit)
+    (check-equal? (for/list ([c (in-cad*rs #'x)]
+                             [i (in-range 4)])
+                    (syntax->datum c))
+                  '[(car x)
+                    (car (cdr x))
+                    (car (cdr (cdr x)))
+                    (car (cdr (cdr (cdr x))))])
+
+    (check-equal? (syntax->datum
+                   (list-destructure-syntax #'[x y] #'lst #'z #:unsafe? #t))
+                  '(let- ([x (unsafe-car lst)]
+                          [y (unsafe-car (unsafe-cdr lst))])
+                         z))))
diff --git a/turnstile/examples/linear/lin+var.rkt b/turnstile/examples/linear/lin+var.rkt
new file mode 100644
index 0000000..040d8e6
--- /dev/null
+++ b/turnstile/examples/linear/lin+var.rkt
@@ -0,0 +1,118 @@
+#lang turnstile/lang
+(extends "lin.rkt")
+(require (only-in "lin+tup.rkt" list-destructure-syntax))
+
+(provide ⊕ var match)
+
+(define-internal-type-constructor ⊕/i)
+
+(define-syntax ⊕
+  (syntax-parser
+    [(_ (V:id t ...) ...)
+     (add-orig (mk-type #'(⊕/i- (#%app 'V t ...) ...))
+               this-syntax)]))
+
+(begin-for-syntax
+  (provide ⊕? ~⊕)
+  (define ⊕? ⊕/i?)
+
+  (define (fail/no-variant type V [src V])
+    (raise-syntax-error #f
+       (format "expected type ~a does not have variant named '~a'\n"
+               (type->str type)
+               (stx->datum V))
+       src))
+
+  (define (num-var-args-fail-msg σs xs)
+    (format "wrong number of arguments to variant: expected ~a, got ~a"
+            (stx-length σs)
+            (stx-length xs)))
+
+
+  (define (unvariant type)
+    (syntax-parse type
+      [(~⊕/i ((~literal #%plain-app) ((~literal quote) U) τ ...) ...)
+       #'[(U τ ...) ...]]))
+
+  (define-syntax ~⊕
+    (pattern-expander
+     (λ (stx)
+       (syntax-case stx ()
+         [(_ . pat)
+          (with-syntax ([(x) (generate-temporaries #'(x))])
+            #'(~and x (~⊕/i . _) (~parse pat (unvariant #'x))))]))))
+
+  (define (has-variant? type v)
+    (syntax-parse type
+      [(~⊕ [U . _] ...)
+       (for/or ([u (in-syntax #'[U ...])])
+         (eq? (stx->datum u) (stx->datum v)))]
+      [_ #f]))
+
+  (define (get-variant type v)
+    (syntax-parse type
+      [(~⊕ [U τ ...] ...)
+       (for/first ([u (in-syntax #'[U ...])]
+                   [ts (in-syntax #'[(τ ...) ...])]
+                   #:when (eq? (stx->datum u) (stx->datum v)))
+         ts)]))
+
+  (current-linear-type? (or/c ⊕? (current-linear-type?)))
+  )
+
+
+(define-typed-syntax var
+  [(_ [V:id e ...]) ⇐ σ_var ≫
+   #:when (⊕? #'σ_var)
+   #:fail-unless (has-variant? #'σ_var #'V)
+                 (fail/no-variant #'σ_var #'V this-syntax)
+   #:with [σ ...] (get-variant #'σ_var #'V)
+   #:fail-unless (stx-length=? #'[σ ...] #'[e ...])
+                 (num-var-args-fail-msg #'[σ ...] #'[e ...])
+   [⊢ e ≫ e- ⇐ σ] ...
+   --------
+   [⊢ (list 'V e- ...)]]
+
+  [(_ [V:id e ...] (~datum as) t) ≫
+   --------
+   [≻ (lin:ann (var [V e ...]) : t)]])
+
+
+
+(define-typed-syntax match
+  [(_ e_var [(V:id x:id ...) e_bra] ...) ≫
+   [⊢ e_var ≫ e_var- ⇒ σ_var]
+   #:fail-unless (⊕? #'σ_var)
+   (format "expected type ⊕, given ~a" (type->str #'σ_var))
+
+   #:mode (make-linear-branch-mode (stx-length #'[e_bra ...]))
+     (#:with ([(x- ...) e_bra- σ_bra] ...)
+      (for/list ([q (in-syntax #'([V (x ...) e_bra] ...))]
+                 [i (in-naturals)])
+        (syntax-parse/typecheck q
+         [(V (x ...) e) ≫
+          #:fail-unless (has-variant? #'σ_var #'V)
+                        (fail/no-variant #'σ_var #'V)
+
+          #:with [σ ...] (get-variant #'σ_var #'V)
+          #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
+                        (num-var-args-fail-msg #'[σ ...] #'[x ...])
+
+          #:submode (branch-nth i)
+            ([[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_bra]
+             #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+          --------
+          [≻ [(x- ...) e- σ_bra]]])))
+
+   #:with tmp (generate-temporary)
+   #:with (destr ...) (stx-map (λ (l) (apply list-destructure-syntax (stx->list l)))
+                               #'[([x- ...]
+                                   (cdr tmp)
+                                   e_bra-) ...])
+   --------
+   [⊢ (let ([tmp e_var-])
+        (case (car tmp)
+          [(V) destr] ...
+          [else (printf "~a\n" tmp)
+                (error '"unhandled case: " (car tmp))]))
+      ⇒ (⊔ σ_bra ...)]])
diff --git a/turnstile/examples/linear/lin.rkt b/turnstile/examples/linear/lin.rkt
new file mode 100644
index 0000000..f4523be
--- /dev/null
+++ b/turnstile/examples/linear/lin.rkt
@@ -0,0 +1,349 @@
+#lang turnstile
+(extends "../ext-stlc.rkt" #:except define if begin let let* letrec λ #%app)
+
+(provide (for-syntax current-linear-type?
+                     linear-type?
+                     unrestricted-type?
+
+                     linear-scope
+                     linear-in-scope?
+                     linear-use-var!
+                     linear-out-of-scope!
+                     linear-merge-scopes!
+                     linear-merge-scopes*!
+
+                     ;; TODO: should these be in turnstile/mode ?
+                     branch-nth
+                     branch-then
+                     branch-else
+
+                     make-empty-linear-mode
+                     make-fresh-linear-mode
+                     make-linear-branch-mode)
+
+         %%reset-linear-mode
+
+         (type-out Unit Int String Bool -o)
+         #%top-interaction #%module-begin require only-in
+         begin drop
+         #%app #%lin-var
+         λ (rename-out [λ lambda])
+         let letrec
+         if
+         define
+         )
+
+
+(define-type-constructor -o #:arity >= 1)
+
+
+(begin-for-syntax
+  (require syntax/id-set
+           racket/set
+           racket/generic
+           turnstile/mode)
+
+  (define (fail/multiple-use x)
+    (raise-syntax-error #f "linear variable used more than once" x))
+  (define (fail/unused x)
+    (raise-syntax-error #f "linear variable unused" x))
+  (define (fail/unbalanced-branches x)
+    (raise-syntax-error #f "linear variable may be unused in certain branches" x))
+  (define (fail/unrestricted-fn x)
+    (raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
+
+
+  ;; this parameter defines the linear-type? function.
+  ;; we defining new types that are linear, modify this
+  ;; parameter like so:
+  ;;   (current-linear-type? (or/c MYTYPE? (current-linear-type?)))
+  ;;
+  ;; current-linear-type? : (Parameter (Type -> Bool))
+  (define current-linear-type?
+    (make-parameter -o?))
+
+  ;; is the given type [linear|unrestricted]?
+  ;; Type -> Bool
+  (define (linear-type? T)
+    ((current-linear-type?) T))
+  (define (unrestricted-type? T)
+    (not ((current-linear-type?) T)))
+
+
+
+  ;; mode object to be used during linear typing.
+  ;; the field 'scope' contains a free-id-set of
+  ;; variables that have been used, and therefore
+  ;; can't be used again.
+  (struct linear-mode mode (scope))
+
+  ;; get the current scope (as described above)
+  ;; based on (current-mode)
+  (define (linear-scope)
+    (linear-mode-scope (current-mode)))
+
+  ;; is the given variable available for use?
+  ;; linear-in-scope? : Id -> Bool
+  (define (linear-in-scope? x)
+    (not (set-member? (linear-scope) x)))
+
+  ;; set the variable to be used in this scope, or raise
+  ;; an error if it's already used.
+  ;;
+  ;; linear-use-var! : Id Type -> void
+  (define (linear-use-var! x T #:fail [fail fail/multiple-use])
+    (when (linear-type? T)
+      (when (set-member? (linear-scope) x)
+        (fail x))
+      (set-add! (linear-scope) x)))
+
+
+  ;; call this with the ([x : t] ...) context after introducing variables,
+  ;; to remove those variables from the linear scope
+  ;;
+  ;; linear-out-of-scope! : Ctx -> Void
+  (define (linear-out-of-scope! ctx #:fail [fail fail/unused])
+    (syntax-parse ctx
+      #:datum-literals (:)
+      [([x : σ] ...)
+       (for ([var (in-syntax #'[x ...])]
+             [T (in-syntax #'[σ ...])] #:when (linear-type? T))
+         (if (linear-in-scope? var)
+             (fail var)
+             (set-remove! (linear-scope) var)))]))
+
+  ;; linear-merge-scopes! : (or '∪ '∩) FreeIdSet ... -> void
+  (define (linear-merge-scopes! op #:fail [fail fail/unbalanced-branches] . ss)
+    (linear-merge-scopes*! op ss #:fail fail))
+
+  ;; linear-merge-scopes*! : (or '∪ '∩) (Listof FreeIdSet) -> void
+  (define (linear-merge-scopes*! op ss #:fail [fail fail/unbalanced-branches])
+    (define s0
+      (case op
+        [(∩)
+         (let ([s0 (set-copy (car ss))])
+           (for ([s (in-list (cdr ss))])
+             (set-intersect! s0 s))
+           (for* ([s (in-list ss)]
+                  [x (in-set s)] #:when (not (set-member? s0 x)))
+             (fail x))
+           s0)]
+
+        [(∪) (apply set-union ss)]))
+
+    (set-clear! (linear-scope))
+    (set-union! (linear-scope) s0))
+
+
+
+  ;; a mode that contains submodes, for use
+  ;; in branching (if, cond, etc.)
+  (struct branch-mode mode (sub-modes))
+
+  ;; for use as `#:submode (branch-nth n)`
+  (define ((branch-nth n) bm)
+    (list-ref (branch-mode-sub-modes bm) n))
+  (define branch-then (branch-nth 0))
+  (define branch-else (branch-nth 1))
+
+  ;; creates a branch-mode with n branches (default: 2)
+  ;; which merges the linear sub-scopes during teardown.
+  ;; see 'if' syntax.
+  ;;
+  ;; make-linear-branch : Int -> BranchMode
+  (define (make-linear-branch-mode [n 2])
+    (define scopes
+      (for/list ([i (in-range n)])
+        (set-copy (linear-scope))))
+
+    (branch-mode void
+                 (λ () (linear-merge-scopes*! '∩ scopes))
+                 (for/list ([s (in-list scopes)])
+                   (linear-mode void void s))))
+
+
+  ;; creates a linear mode that disallows (on teardown) use
+  ;; of variables from outside of the current scope.
+  ;; see unrestricted λ syntax.
+  ;;
+  ;; make-fresh-linear-context : -> linear-mode?
+  (define (make-fresh-linear-mode #:fail [fail fail/unrestricted-fn])
+    (let ([ls #f])
+      (linear-mode (λ () (set! ls (set-copy (linear-scope))))
+                   (λ () (linear-merge-scopes! '∩ (linear-scope) ls #:fail fail))
+                   (linear-scope))))
+
+
+  ;; creates an empty linear mode.
+  ;;
+  ;; make-empty-linear-mode : -> LinearMode
+  (define (make-empty-linear-mode)
+    (linear-mode void void (mutable-free-id-set)))
+
+  (current-mode (make-empty-linear-mode))
+
+  )
+
+;; this function resets the mode to be an empty
+;; linear-mode. this should ONLY be used by tests
+;; that screw up the state of current-mode, and
+;; need to reset it for the next test. this is because
+;; we don't have proper backtracking facilities, so
+;; errors in the middle of inference screw up the
+;; global state
+(define-syntax %%reset-linear-mode
+  (syntax-parser
+    [(_)
+     #:do [(current-mode (make-empty-linear-mode))]
+     #'(#%app- void-)]))
+
+
+
+(define-typed-syntax begin
+  [(begin e ... e0) ≫
+   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇒ σ]]
+   --------
+   [⊢ (begin- e- ... e0-) ⇒ σ]]
+
+  [(begin e ... e0) ⇐ σ ≫
+   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇐ σ]]
+   --------
+   [⊢ (begin- e- ... e0-)]])
+
+
+
+(define-typed-syntax drop
+  [(drop e) ≫
+   [⊢ e ≫ e- ⇒ _]
+   --------
+   [⊢ (#%app- void- e-) ⇒ Unit]])
+
+
+
+(define-typed-syntax #%app
+  [(_) ≫
+   --------
+   [⊢ (#%app- void-) ⇒ Unit]]
+
+  [(#%app fun arg ...) ≫
+   [⊢ fun ≫ fun- ⇒ σ_fun]
+   #:with (~or (~-o σ_in ... σ_out)
+               (~→ σ_in ... σ_out)
+               (~post (~fail "expected linear function type")))
+          #'σ_fun
+   [⊢ [arg ≫ arg- ⇐ σ_in] ...]
+   --------
+   [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
+
+
+
+(define-typed-variable-syntax
+  #:name #%lin-var
+  [(#%var x- : σ) ≫
+   #:do [(linear-use-var! #'x- #'σ)]
+   ----------
+   [⊢ x- ⇒ σ]])
+
+
+(define-typed-syntax λ
+  #:datum-literals (: !)
+  ;; linear lambda; annotations
+  [(λ ([x:id : T:type] ...) b) ≫
+   #:with [σ ...] #'[T.norm ...]
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (λ- (x- ...) b-) ⇒ (-o σ ... σ_out)]]
+
+  ;; unrestricted lambda; annotations
+  [(λ ! ([x:id : T:type] ...) b) ≫
+   #:with [σ ...] #'[T.norm ...]
+   #:mode (make-fresh-linear-mode)
+     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+   --------
+   [⊢ (λ- (x- ...) b-) ⇒ (→ σ ... σ_out)]]
+
+  ;; linear lambda; inferred
+  [(λ (x:id ...) b) ⇐ (~-o σ ... σ_out) ≫
+   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
+                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (λ- (x- ...) b-)]]
+
+  ;; unrestricted lambda; inferred
+  [(λ (x:id ...) b) ⇐ (~→ σ ... σ_out) ≫
+   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
+                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
+   #:mode (make-fresh-linear-mode)
+     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
+      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
+   --------
+   [⊢ (λ- (x- ...) b-)]])
+
+
+
+(define-typed-syntax let
+  [(let ([x e] ...) b) ≫
+   [⊢ [e ≫ e- ⇒ σ] ...]
+   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
+   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
+   --------
+   [⊢ (let- ([x- e-] ...) b-) ⇒ σ_out]])
+
+
+
+(define-typed-syntax letrec
+  [(letrec ([b:type-bind rhs] ...) e ...) ≫
+   #:fail-when (ormap linear-type? (stx->list #'[b.type ...]))
+               (format "may not bind linear type ~a in letrec"
+                       (type->str (findf linear-type? (stx->list #'[b.type ...]))))
+   [[b.x ≫ x- : b.type] ...
+    ⊢ [rhs ≫ rhs- ⇐ b.type] ...
+       [(begin e ...) ≫ e- ⇒ σ_out]]
+   #:do [(linear-out-of-scope! #'([x- : b.type] ...))]
+   --------
+   [⊢ (letrec- ([x- rhs-] ...) e-) ⇒ σ_out]])
+
+
+
+(define-typed-syntax if
+  [(_ c e1 e2) ⇐ σ ≫
+   [⊢ c ≫ c- ⇐ Bool]
+   #:mode (make-linear-branch-mode 2)
+     ([⊢ [e1 ≫ e1- ⇐ σ] #:submode branch-then]
+      [⊢ [e2 ≫ e2- ⇐ σ] #:submode branch-else])
+   --------
+   [⊢ (if- c- e1- e2-)]]
+
+  [(_ c e1 e2) ≫
+   [⊢ c ≫ c- ⇐ Bool]
+   #:mode (make-linear-branch-mode 2)
+     ([⊢ [e1 ≫ e1- ⇒ σ1] #:submode branch-then]
+      [⊢ [e2 ≫ e2- ⇒ σ2] #:submode branch-else])
+   --------
+   [⊢ (if- c- e1- e2-) ⇒ (⊔ σ1 σ2)]])
+
+
+
+(define-typed-syntax define
+  #:datum-literals (:)
+  [(define (f [x:id : ty] ...) ret
+     e ...+) ≫
+   --------
+   [≻ (define f : (→ ty ... ret)
+        (letrec ([{f : (→ ty ... ret)}
+                  (λ ! ([x : ty] ...)
+                    (begin e ...))])
+          f))]]
+
+  [(_ x:id : τ:type e:expr) ≫
+   #:fail-when (linear-type? #'τ.norm)
+               "cannot define linear type globally"
+   #:with y (generate-temporary #'x)
+   --------
+   [≻ (begin-
+        (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
+        (define- y (ann e : τ.norm)))]])
diff --git a/turnstile/examples/tests/linear-var-assign-tests.rkt b/turnstile/examples/tests/linear-var-assign-tests.rkt
deleted file mode 100644
index 7f0038b..0000000
--- a/turnstile/examples/tests/linear-var-assign-tests.rkt
+++ /dev/null
@@ -1,63 +0,0 @@
-#lang s-exp turnstile/examples/linear-var-assign
-
-(require turnstile/rackunit-typechecking
-         (only-in racket/base quote))
-
-(check-type #t : Bool)
-(check-type 4 : Int)
-(check-type () : Unit)
-
-(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
-(check-type (tup 1 (tup 2 3)) : (⊗ Int (⊗ Int Int)) -> '(1 (2 3)))
-
-(check-type (let ([x 3] [y 4]) y) : Int -> 4)
-(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
-
-(typecheck-fail (let ([p (tup 1 2)]) ())
-                #:with-msg "p: linear variable unused")
-(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
-                #:with-msg "p: linear variable used more than once")
-
-(check-type (if #t 1 2) : Int -> 1)
-(typecheck-fail (if 1 2 3)
-                #:with-msg "expected Bool, given Int")
-(typecheck-fail (if #t 2 ())
-                #:with-msg "expected Int, given Unit")
-
-(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
-(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
-                #:with-msg "linear variable may be unused in certain branches")
-(typecheck-fail (let ([p (tup 1 ())]) (if #t p (begin p p)))
-                #:with-msg "p: linear variable used more than once")
-
-
-(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
-(check-type (λ ([x : (⊗ Int Int)]) x) : (-o (⊗ Int Int) (⊗ Int Int)))
-(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
-                #:with-msg "x: linear variable unused")
-
-(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
-            : (-o Int (⊗ Int Int)))
-
-(check-type (λ ! ([x : Int]) x) : (!! (-o Int Int)))
-(typecheck-fail (let ([p (tup 1 2)]) (λ ! ([x : Int]) p))
-                #:with-msg "linear variable may not be used by unrestricted function")
-
-
-(check-type (let ([f (λ ([x : Int] [y : Int]) y)])
-              (f 3 4))
-            : Int -> 4)
-(check-type + : (!! (-o Int Int Int)))
-(check-type (+ 1 2) : Int -> 3)
-(check-type (< 3 4) : Bool -> #t)
-
-
-(check-type (let ([×2 (λ ! ([x : Int]) (+ x x))])
-              (+ (×2 8)
-                 (×2 9)))
-            : Int -> 34)
-
-(typecheck-fail (let ([×2 (λ ([x : Int]) (+ x x))])
-                  (+ (×2 8)
-                     (×2 9)))
-                #:with-msg "×2: linear variable used more than once")
diff --git a/turnstile/examples/tests/linear/lin+chan-tests.rkt b/turnstile/examples/tests/linear/lin+chan-tests.rkt
new file mode 100644
index 0000000..8e93f19
--- /dev/null
+++ b/turnstile/examples/tests/linear/lin+chan-tests.rkt
@@ -0,0 +1,18 @@
+#lang s-exp turnstile/examples/linear/lin+chan
+(require turnstile/rackunit-typechecking)
+
+(check-type
+ (let* ([(c c-out) (make-channel {Int})])
+   (thread (λ () (channel-put c-out 5)))
+   (thread (λ () (channel-put c-out 4)))
+   (let* ([(c1 x) (channel-get c)]
+          [(c2 y) (channel-get c1)])
+     (drop c2)
+     (+ x y)))
+ : Int -> 9)
+
+(typecheck-fail
+ (let* ([(c-in c-out) (make-channel {String})])
+   (thread (λ () (channel-get c-in)))
+   (channel-get c-in))
+ #:with-msg "c-in: linear variable used more than once")
diff --git a/turnstile/examples/tests/linear/lin+cons-tests.rkt b/turnstile/examples/tests/linear/lin+cons-tests.rkt
new file mode 100644
index 0000000..917582e
--- /dev/null
+++ b/turnstile/examples/tests/linear/lin+cons-tests.rkt
@@ -0,0 +1,28 @@
+#lang s-exp turnstile/examples/linear/lin+cons
+(require turnstile/rackunit-typechecking)
+
+
+(define (length [lst : (MList Int)]) Int
+  (match-list lst
+    [(cons _ xs @ l)
+     (begin (drop l)
+            (add1 (length xs)))]
+    [(nil) 0]))
+
+(check-type (length (cons 9 (cons 8 (cons 7 (nil))))) : Int -> 3)
+
+
+
+(define (rev-append [lst : (MList String)]
+                    [acc : (MList String)]) (MList String)
+  (match-list lst
+    [(cons x xs @ l) (rev-append xs (cons x acc @ l))]
+    [(nil) acc]))
+
+(define (rev [lst : (MList String)]) (MList String)
+  (rev-append lst (nil)))
+
+
+(check-type (rev (cons "a" (cons "b" (cons "c" (nil)))))
+            : (MList String)
+            -> (cons "c" (cons "b" (cons "a" (nil)))))
diff --git a/turnstile/examples/tests/linear/lin+tup-tests.rkt b/turnstile/examples/tests/linear/lin+tup-tests.rkt
new file mode 100644
index 0000000..669c6e5
--- /dev/null
+++ b/turnstile/examples/tests/linear/lin+tup-tests.rkt
@@ -0,0 +1,29 @@
+#lang s-exp turnstile/examples/linear/lin+tup
+
+(require turnstile/rackunit-typechecking
+         (only-in racket/base quote))
+
+(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
+(check-type (tup 1 2 3) : (⊗ Int Int Int) -> '(1 2 3))
+
+(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
+(typecheck-fail (let ([p (tup 1 2)]) ())
+                #:with-msg "p: linear variable unused")
+(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
+                #:with-msg "p: linear variable used more than once")
+
+(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
+(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
+                #:with-msg "linear variable may be unused in certain branches")
+
+(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
+(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
+                #:with-msg "x: linear variable unused")
+
+(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
+            : (-o Int (⊗ Int Int)))
+
+(check-type (let* ([x 3] [y x]) y) : Int -> 3)
+(check-type (let* ([(x y) (tup 1 #f)]) x) : Int -> 1)
+(typecheck-fail (let* ([(x y) (tup (tup 1 2) 3)]) y)
+                #:with-msg "x: linear variable unused")
diff --git a/turnstile/examples/tests/linear/lin+var-tests.rkt b/turnstile/examples/tests/linear/lin+var-tests.rkt
new file mode 100644
index 0000000..170497a
--- /dev/null
+++ b/turnstile/examples/tests/linear/lin+var-tests.rkt
@@ -0,0 +1,67 @@
+#lang s-exp turnstile/examples/linear/lin+var
+(require turnstile/rackunit-typechecking)
+
+(check-type (var [left 3]) : (⊕ [left Int] [right String]))
+(check-type (var [right "a"]) : (⊕ [left Int] [right String]))
+
+(typecheck-fail (var [left 3] as (⊕ [yes] [no]))
+                #:with-msg "type \\(⊕ \\(yes\\) \\(no\\)\\) does not have variant named 'left'")
+
+(typecheck-fail (var [left 3] as (⊕ [left Int Int] [right String]))
+                #:with-msg "wrong number of arguments to variant: expected 2, got 1")
+
+(define-type-alias (Either A B) (⊕ [left A] [right B]))
+(define-type-alias (Option A) (⊕ [some A] [none]))
+
+(typecheck-fail (var [middle 3] as (Either Int Float))
+                #:with-msg "type \\(Either Int Float\\) does not have variant named 'middle'")
+
+(check-type (λ (x) x) : (→ (Either Int Float) (Either Int Float)))
+(check-type (λ (x) x) : (→ (Either Int Float) (⊕ [left Int] [right Float])))
+
+(typecheck-fail (let ([x (var [left 3] as (Either Int Int))]) 0)
+                #:with-msg "x: linear variable unused")
+
+(check-type (match (var [left 3] as (Either Int Int))
+              [(left x) x]
+              [(right y) (+ y 1)])
+            : Int ⇒ 3)
+
+(check-type (match (var [right 5] as (Either Int Int))
+              [(left x) x]
+              [(right y) (+ y 1)])
+            : Int ⇒ 6)
+
+(typecheck-fail (match (var [left 3] as (Either Int (-o Int Int)))
+                  [(left x) x]
+                  [(right f) 0])
+                #:with-msg "f: linear variable unused")
+
+(check-type (match (var [right (λ (x) (+ x x))] as (Either Int (-o Int Int)))
+              [(left x) x]
+              [(right f) (f 2)])
+            : Int ⇒ 4)
+
+(typecheck-fail (match (var [left 0] as (Either Int String))
+                  [(left x) x]
+                  [(right y) y])
+                #:with-msg "branches have incompatible types: Int and String")
+
+(typecheck-fail (match (var [some ()] as (Option Unit))
+                  [(left x) x]
+                  [(right y) y])
+                #:with-msg "type \\(Option Unit\\) does not have variant named 'left'")
+(%%reset-linear-mode)
+
+(typecheck-fail (match (var [left 0] as (Either Int Int))
+                  [(left x) x]
+                  [(right y z) y])
+                #:with-msg "wrong number of arguments to variant: expected 1, got 2")
+(%%reset-linear-mode)
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (match (var [left 0] as (Either Int Int))
+                    [(left x) (f x)]
+                    [(right y) y]))
+                #:with-msg "f: linear variable may be unused in certain branches")
+(%%reset-linear-mode)
diff --git a/turnstile/examples/tests/linear/lin-tests.rkt b/turnstile/examples/tests/linear/lin-tests.rkt
new file mode 100644
index 0000000..1132be1
--- /dev/null
+++ b/turnstile/examples/tests/linear/lin-tests.rkt
@@ -0,0 +1,76 @@
+#lang s-exp turnstile/examples/linear/lin
+(require turnstile/rackunit-typechecking
+         (only-in racket/base quote))
+
+(check-type #t : Bool)
+(check-type 4 : Int)
+(check-type () : Unit)
+
+(check-type (let ([x 3] [y 4]) y) : Int -> 4)
+
+(check-type (if #t 1 2) : Int -> 1)
+(typecheck-fail (if 1 2 3)
+                #:with-msg "expected Bool, given Int")
+(typecheck-fail (if #t 2 ())
+                #:with-msg "branches have incompatible types: Int and Unit")
+(%%reset-linear-mode)
+
+(check-type (λ ([x : Int]) x) : (-o Int Int))
+(check-type (λ ! ([x : Int]) x) : (→ Int Int))
+(check-type (λ (x) x) : (-o String String))
+(check-type (λ (x) x) : (→ String String))
+
+(check-type + : (→ Int Int Int))
+(check-type (+ 1 2) : Int -> 3)
+(check-type ((λ ([x : Int]) (+ x 1)) 4) : Int -> 5)
+
+
+(typecheck-fail (λ ([p : (-o Int Bool)]) 0)
+                #:with-msg "p: linear variable unused")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  0)
+                #:with-msg "f: linear variable unused")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (f (f 3)))
+                #:with-msg "f: linear variable used more than once")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (if #t
+                      (f 3)
+                      4))
+                #:with-msg "f: linear variable may be unused in certain branches")
+
+(typecheck-fail (let ([f (λ ([x : Int]) x)])
+                  (λ ! ([x : Int]) f))
+                #:with-msg "f: linear variable may not be used by unrestricted function")
+(%%reset-linear-mode)
+
+(check-type (let ([twice (λ ! ([x : Int]) (+ x x))])
+              (+ (twice 8)
+                 (twice 9)))
+            : Int -> 34)
+
+(check-type (let ([f (λ ([x : Int]) #t)])
+              (begin (drop f)
+                     3))
+            : Int -> 3)
+
+(check-type (letrec ([{<= : (→ Int Int Bool)}
+                      (λ (n m)
+                         (if (zero? n)
+                             #t
+                             (if (zero? m)
+                                 #f
+                                 (<= (sub1 n) (sub1 m)))))])
+              (if (<= 4 1) 999
+                  (if (<= 3 3)
+                      0
+                      888)))
+            : Int -> 0)
+
+(typecheck-fail (letrec ([{f : (-o Int Int)}
+                          (λ (x) (f x))])
+                  (f 3))
+                #:with-msg "may not bind linear type \\(-o Int Int\\) in letrec")