diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
index 251aaa5..91c89ff 100644
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@@ -11,7 +11,6 @@
 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
 (require (only-in "stlc+rec-iso.rkt" ~× ×?))
-(provide → define-type)
 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
@@ -25,13 +24,15 @@
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
 
+(provide → →/test match2 define-type)
+
 ;; ML-like language
 ;; - top level recursive functions
 ;; - user-definable algebraic datatypes
 ;; - pattern matching
 ;; - (local) type inference
 
-;; type inference constraint solving
+  ;; type inference constraint solving
 (begin-for-syntax 
   (define (compute-constraint τ1-τ2)
     (syntax-parse τ1-τ2
@@ -193,11 +194,9 @@
          (⊢ g : ty_fn_expected #;(∀ Ys (ext-stlc:→ τ+orig ...)))))
       (define g
         (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
-;
-;; internal form used to expand many types at once under the same context
-(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
 
-;; define-type --------------------------------------------------
+;; define-type -----------------------------------------------
+;; TODO: should validate τ as part of define-type definition (before it's ever used)
 (define-syntax (define-type stx)
   (syntax-parse stx
     [(_ Name:id . rst)
@@ -217,6 +216,10 @@
                          (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
      #:with RecName (generate-temporary #'Name)
      #:with NameExpander (format-id #'Name "~~~a" #'Name)
+     #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
+     #:with NameDelayed (format-id #'Name "~a-delayed" #'Name)
+     #:with NameForced (format-id #'NameDelayed "~a-force" #'NameDelayed)
+     #:with NameForcedExpander (format-id #'NameForced "~~~a" #'NameForced)
      #:with (StructName ...) (generate-temporaries #'(Cons ...))
      #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
      #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
@@ -224,11 +227,25 @@
      #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
                                      #'(StructName ...) #'((fld ...) ...))
      #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+     #:with (Y ...) (generate-temporaries #'(X ...))
      ;; types, but using RecName instead of Name
      #:with ((τ/rec ...) ...) (subst #'RecName #'Name #'((τ ...) ...))
-     #:with (Y ...) (generate-temporaries #'(X ...))
      #`(begin
+;         (define NameDelayed (lambda () (error "types not allowed at runtime")))
+         ; TODO: use define-type-constructor for delayed form as well,
+         ;; to get proper pattern expanders, etc
+         ;; (define-syntax (Name stx) 
+         ;;   (syntax-parse stx
+         ;;     [(_ Y ...) (add-orig (mk-type #'(delay NameDelayed Y ...)) stx)]))
+         (define-syntax (NameExtraInfo stx)
+           (syntax-parse stx
+             [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
          (define-type-constructor Name
+           #:arity = #,(stx-length #'(X ...))
+           #:extra-info 'NameExtraInfo
+;           #:extra-info (X ...) (('Cons 'StructName Cons? [acc τ] ...) ...)
+           #:no-provide)
+         #;(define-type-constructor Name
            #:arity = #,(stx-length #'(X ...))
            #:extra-info (X ...) 
              (λ (RecName) 
@@ -263,6 +280,7 @@
               #:with τ-expected (syntax-property #'C 'expected-type)
               #:fail-unless (syntax-e #'τ-expected)
                             (type-error #:src stx #:msg "cannot infer type of ~a; add annotations" #'C)
+;              #:with (_ (~datum delay) (_ () _ τ-expected-arg (... ...))) ((current-type-eval) #'τ-expected)
               #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
               #'(C {τ-expected-arg (... ...)})]
              [_:id 
@@ -316,12 +334,12 @@
         [{(~datum _)} #'()]
         [{(~literal stlc+cons:nil)}  #'()]
         [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
-         #:with ((~literal #%plain-lambda) (RecName) 
-                 ((~literal let-values) ()
-                  ((~literal let-values) ()
-                   . info-body)))
-                 (get-extra-info #'ty)
-                #'()]
+         ;; #:with ((~literal #%plain-lambda) (RecName) 
+         ;;         ((~literal let-values) ()
+         ;;          ((~literal let-values) ()
+         ;;           . info-body)))
+         #:when (get-extra-info #'ty)
+         #'()]
         ;; comma tup syntax always has parens
 ;        [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
         [{(~and ps (p1 (unq p) ...))}
@@ -333,10 +351,11 @@
       [((~datum _) ty) #'()]
       [((~or (~literal stlc+cons:nil)) ty) #'()]
       [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
-       #:with ((~literal #%plain-lambda) (RecName) 
-               ((~literal let-values) ()
-                ((~literal let-values) ()
-                 . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
+       #:with (_ (_ ((~literal quote) C) . _) ...)
+       ;; ((~literal #%plain-lambda) (RecName) 
+       ;;         ((~literal let-values) ()
+       ;;          ((~literal let-values) ()
+       ;;           . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
               (get-extra-info #'ty)
        #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
        #'()]
@@ -360,19 +379,19 @@
        #:with (~List t) #'ty
        (unifys #'([p t] [ps ty]))]
       [((Name p ...) ty)
-        #:with ((~literal #%plain-lambda) (RecName) 
-                ((~literal let-values) ()
-                 ((~literal let-values) ()
-                  . info-body)))
-               (get-extra-info #'ty)
-        #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
-        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+        ;; #:with ((~literal #%plain-lambda) (RecName) 
+        ;;         ((~literal let-values) ()
+        ;;          ((~literal let-values) ()
+        ;;           . info-body)))
+       ;; (get-extra-info #'ty)
+;        #:with (_ (_ ((~literal quote) ConsAll) . _) ...) (get-extra-info #'ty)
+;        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
         #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...)
                (stx-findf
-                   (syntax-parser
-                     [((~literal #%plain-app) 'C . rst)
-                      (equal? (syntax->datum #'Name) (syntax->datum #'C))])
-                 #'info-unfolded)
+                 (syntax-parser
+                  [(_ 'C . rst) 
+                   (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+                 (stx-cdr (get-extra-info #'ty)))
         (unifys #'([p τ] ...))]
       [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) #'()]))
   (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys))
@@ -384,12 +403,12 @@
         [{(~datum _)} #'_]
         [{(~literal stlc+cons:nil)}  (syntax/loc p (list))]
         [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
-         #:with ((~literal #%plain-lambda) (RecName) 
-                 ((~literal let-values) ()
-                  ((~literal let-values) ()
-                   . info-body)))
-                 (get-extra-info ty)
-                (compile-pat #'(A) ty)]
+         ;; #:with ((~literal #%plain-lambda) (RecName) 
+         ;;         ((~literal let-values) ()
+         ;;          ((~literal let-values) ()
+         ;;           . info-body)))
+         #:when (get-extra-info ty)
+         (compile-pat #'(A) ty)]
         ;; comma tup stx always has parens
         ;; comma tup syntax always has parens
 ;        [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
@@ -402,11 +421,11 @@
      [(~literal stlc+cons:nil) ; nil
       #'(list)]
      [A:id ; disambiguate 0-arity constructors (that don't need parens)
-      #:with ((~literal #%plain-lambda) (RecName) 
-              ((~literal let-values) ()
-               ((~literal let-values) ()
-                . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
-              (get-extra-info ty)
+      ;; #:with ((~literal #%plain-lambda) (RecName) 
+      ;;         ((~literal let-values) ()
+      ;;          ((~literal let-values) ()
+      ;;           . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
+       #:with (_ (_ ((~literal quote) C) . _) ...) (get-extra-info ty)
        #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
       (compile-pat #'(A) ty)]
      [x:id p]
@@ -435,19 +454,19 @@
       #:with ps- (compile-pat #'ps ty)
       #'(cons p- ps-)]
      [(Name . pats)
-      #:with ((~literal #%plain-lambda) (RecName) 
-              ((~literal let-values) ()
-               ((~literal let-values) ()
-                . info-body)))
-             (get-extra-info ty)
-      #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
-      #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+      ;; #:with ((~literal #%plain-lambda) (RecName) 
+      ;;         ((~literal let-values) ()
+      ;;          ((~literal let-values) ()
+      ;;           . info-body)))
+      ;;        (get-extra-info ty)
+      ;; #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+      ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
       #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...)
              (stx-findf
-                 (syntax-parser
-                   [((~literal #%plain-app) 'C . rst)
-                    (equal? (syntax->datum #'Name) (syntax->datum #'C))])
-               #'info-unfolded)
+               (syntax-parser
+                [(_ 'C . rst) 
+                 (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+               (stx-cdr (get-extra-info ty)))
       #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
       (syntax/loc p (StructName p- ...))]))
 
@@ -494,13 +513,14 @@
                    (syntax->list #'((p ...) ...)))])])]
      [else ; algebraic datatypes
       (syntax-parse (get-extra-info ty)
-        [((~literal #%plain-lambda) (RecName) 
+        [#;((~literal #%plain-lambda) (RecName) 
            ((~literal let-values) ()
              ((~literal let-values) ()
               . (((~literal #%plain-app)  
                   ((~literal quote) C) 
                   ((~literal quote) Cstruct)
                   . rst) ...))))
+         (_ (_ ((~literal quote) C) ((~literal quote) Cstruct) . rst) ...)
          (syntax-parse pats
            [((Cpat _ ...) ...)
             (define Cs (syntax->datum #'(C ...)))
@@ -522,7 +542,6 @@
     (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
   )
 
-(provide match2)
 (define-syntax (match2 stx)
  (syntax-parse stx #:datum-literals (with)
    [(_ e with . clauses)
@@ -530,11 +549,16 @@
     #:with [e- τ_e] (infer+erase #'e)
     (syntax-parse #'clauses #:datum-literals (->)
      [([(~seq p ...) -> e_body] ...)
-      #:with (pat ...) (stx-map (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
-                            #'((p ...) ...)) ; use brace to indicate root pattern
+      #:with (pat ...) (stx-map ; use brace to indicate root pattern
+                         (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+                         #'((p ...) ...)) 
       #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
       ;; #:with ((~and ctx ([x ty] ...)) ...) (stx-map (lambda (p) (get-ctx p #'τ_e)) #'(pat ...))
-      #:with ([(x- ...) e_body- ty_body] ...) (stx-map infer/ctx+erase #'(ctx ...) #'(e_body ...))
+      #:with ty-expected (get-expected-type stx)
+      #:with ([(x- ...) e_body- ty_body] ...) 
+             (stx-map 
+               infer/ctx+erase 
+               #'(ctx ...) #'((add-expected e_body ty-expected) ...))
       ;; #:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...))
       #:fail-unless (same-types? #'(ty_body ...))
                     (string-append "branches have different types, given: "
@@ -602,13 +626,15 @@
              (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
              -> e_c_un] ...) ; un = unannotated with expected ty
         ;; len #'clauses maybe > len #'info, due to guards
-        #:with ((~literal #%plain-lambda) (RecName) 
-                ((~literal let-values) ()
-                 ((~literal let-values) ()
-                  . info-body)))
-               (get-extra-info #'τ_e)
-        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
-        #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+        ;; #:with ((~literal #%plain-lambda) (RecName) 
+        ;;         ((~literal let-values) ()
+        ;;          ((~literal let-values) ()
+        ;;           . info-body)))
+        ;;        (get-extra-info #'τ_e)
+        ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+        #:with info-body (get-extra-info #'τ_e)
+        #:with info-unfolded #'info-body
+        #:with (_ (_ ((~literal quote) ConsAll) . _) ...) #'info-body
         #:fail-unless (set=? (syntax->datum #'(Clause ...))
                              (syntax->datum #'(ConsAll ...)))
                       (type-error #:src stx
@@ -627,7 +653,7 @@
                       (syntax-parser
                         [((~literal #%plain-app) 'C . rst)
                          (equal? Cl (syntax->datum #'C))])
-                    #'info-unfolded))
+                    (stx-cdr #'info-unfolded))) ; drop leading #%app
                 (syntax->datum #'(Clause ...)))
         ;; this commented block experiments with expanding to unsafe ops
         ;; #:with ((acc ...) ...) (stx-map 
@@ -660,7 +686,6 @@
     [(_ . rst) (syntax-property #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))]))
 ; special arrow that computes free vars; for use with tests
 ; (because we can't write explicit forall
-(provide →/test)
 (define-syntax →/test 
   (syntax-parser
     [(_ (~and Xs (X:id ...)) . rst)
@@ -730,8 +755,7 @@
         #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
     [else
      ;; ) solve for type variables Xs
-     (define/with-syntax ((e_arg1- ...) tys-solved) 
-       (solve #'Xs #'tyX_args stx))
+     (define/with-syntax ((e_arg1- ...) tys-solved) (solve #'Xs #'tyX_args stx))
      ;; ) instantiate polymorphic function type
      (syntax-parse (inst-types #'tys-solved #'Xs #'tyX_args)
       [(τ_in ... τ_out) ; concrete types
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 4b49f5f..bc39f2e 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -68,6 +68,11 @@
 (define (stx-drop stx n)
   (drop (syntax->list stx) n))
 
+(define (generate-temporariess stx)
+  (stx-map generate-temporaries stx))
+(define (generate-temporariesss stx)
+  (stx-map generate-temporariess stx))
+
 ;; based on make-variable-like-transformer from syntax/transformer,
 ;; but using (#%app id ...) instead of ((#%expression id) ...)
 (define (make-variable-like-transformer ref-stx)
diff --git a/tapl/tests/mlish/bg/monad.mlish b/tapl/tests/mlish/bg/monad.mlish
index 5d0adde..cbea739 100644
--- a/tapl/tests/mlish/bg/monad.mlish
+++ b/tapl/tests/mlish/bg/monad.mlish
@@ -114,9 +114,9 @@
 ;; check match2 nested datatype bug
 (check-type
     (match bq-tails-result with
-     [None -> (None {Int})]
+     [None -> None]
      [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4))
 (check-type
     (match2 bq-tails-result with
-     [None -> (None {Int})]
+     [None -> None]
      [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4))
diff --git a/tapl/tests/mlish/loop.mlish b/tapl/tests/mlish/loop.mlish
new file mode 100644
index 0000000..5d3f63f
--- /dev/null
+++ b/tapl/tests/mlish/loop.mlish
@@ -0,0 +1,108 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; datatype with no self-reference
+(define-type (Test X)
+  (A X) 
+  (B X X))
+
+(check-type (A 1) : (Test Int))
+(check-type (B 1 2) : (Test Int))
+
+(check-type
+    (match (A 1) with
+     [A x -> x]
+     [B x y -> (+ x y)]) : Int -> 1)
+
+(check-type
+    (match (B 1 2) with
+     [A x -> x]
+     [B x y -> (+ x y)]) : Int -> 3)
+
+;; datatype with self-reference
+(define-type (Rec X)
+  N
+  (C X (Rec X)))
+
+(check-type N : (Rec Int) -> N)
+(check-type (N {Int}) : (Rec Int) -> (N {Int}))
+(check-type (C 1 N) : (Rec Int) -> (C 1 N))
+
+(check-type
+    (match (N {Int}) with
+     [N -> 0]
+     [C x xs -> x]) : Int -> 0)
+
+(check-type
+    (match (C 1 N) with
+     [N -> 0]
+     [C x xs -> x]) : Int -> 1)
+
+;; mutually referential datatypes
+(define-type (Loop1 X)
+  (L1 (Loop2 X)))
+(define-type (Loop2 X)
+  (L2 (Loop1 X)))
+
+(define (looping-f [x : (Loop1 Y)] -> (Loop1 Y)) x)
+
+(define-type (ListA X)
+  NA
+  (CA X (ListB X)))
+(define-type (ListB X)
+  NB
+  (CB X (ListA X)))
+
+;; TODO: error should occur here
+(define-type (ListC X)
+  NC
+  (CC X (ListA X X))) ; misapplication of ListA type constructor
+
+(check-type NC : (ListC Int))
+(typecheck-fail (CC 1 NA)) ; and not here
+
+;; (define (g [x : (ListA Int Int)] -> Int) 0)
+
+(typecheck-fail (CA 1 NA))
+(check-type (CA 1 NB) : (ListA Int))
+(check-type (CA 1 (CB 2 NA)) : (ListA Int))
+(typecheck-fail (CA 1 (CB 2 NB)))
+(typecheck-fail (CB 1 NB))
+(check-type (CB 1 NA) : (ListB Int))
+(check-type (CB 1 (CA 2 NB)) : (ListB Int))
+(typecheck-fail (CB 1 (CA 2 NA)))
+
+(check-type
+    (match (CA 1 NB) with
+     [NA -> 0]
+     [CA x xs -> x]) : Int -> 1)
+
+(check-type
+    (match (CA 1 (CB 2 NA)) with
+     [NA -> 0]
+     [CA x xs ->
+      (match xs with
+       [NB -> 3]
+       [CB x xs -> x])]) : Int -> 2)
+
+;; "real world" mutually referential datatypes
+(define-type (BankersDeque A)
+  [BD Int (List A) Int (List A)])
+
+(define-type (ImplicitCatDeque A)
+  [Shallow (BankersDeque A)]
+  [Deep (BankersDeque A)
+        (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
+        (BankersDeque A)
+        (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
+        (BankersDeque A)])
+
+(define-type (CmpdElem A)
+  [Simple (BankersDeque A)]
+  [Cmpd (BankersDeque A) 
+        (ImplicitCatDeque 
+          (BankersDeque (CmpdElem (BankersDeque A)))) (BankersDeque A)])
+
+(define (id (icd : (ImplicitCatDeque Int)) → (ImplicitCatDeque Int))
+  icd)
+
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
index 34b5921..2f79776 100644
--- a/tapl/tests/mlish/polyrecur.mlish
+++ b/tapl/tests/mlish/polyrecur.mlish
@@ -109,7 +109,7 @@
         (BankersDeque A)])
 
 
-(typecheck-fail
+#;(typecheck-fail
   (λ ([icd : (ImplicitCatDeque A)]) icd)
   #:with-msg 
   "type constructor ImplicitCatDeque expects 1 args, given 2")
diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt
index abca30d..4e22fa5 100644
--- a/tapl/tests/run-all-mlish-tests.rkt
+++ b/tapl/tests/run-all-mlish-tests.rkt
@@ -1,36 +1,24 @@
-#lang racket
+#lang racket/base
+(require racket/match racket/system racket/port)
 
 (match-define (list i1 o1 id1 err1 f1)
   (process "time racket run-mlish-tests1.rkt"))
-(match-define (list i1b o1b id1b err1b f1b)
-  (process "time racket run-mlish-tests1b.rkt"))
 (match-define (list i2 o2 id2 err2 f2)
   (process "time racket run-mlish-tests2.rkt"))
 (match-define (list i3 o3 id3 err3 f3)
-  (process "time racket mlish/bg/basics.mlish"))
-(match-define (list i3b o3b id3b err3b f3b)
-  (process "time racket mlish/bg/basics2.mlish"))
-(match-define (list i3c o3c id3c err3c f3c)
   (process "time racket run-mlish-tests3.rkt"))
 (match-define (list i4 o4 id4 err4 f4)
   (process "time racket run-mlish-tests4.rkt"))
 
-(displayln "----- General tests and queens: ---------------------------------")
+(displayln "----- General MLish tests: --------------------------------------")
 (write-string (port->string err1))
 (write-string (port->string i1))
-(displayln "----- Shootout tests: -------------------------------------------")
-(write-string (port->string err1b))
-(write-string (port->string i1b))
-(displayln "----- RW OCaml tests: -------------------------------------------")
+(displayln "----- Shootout and RW OCaml tests: ------------------------------")
 (write-string (port->string err2))
 (write-string (port->string i2))
 (displayln "----- Ben's tests: ----------------------------------------------")
 (write-string (port->string err3))
 (write-string (port->string i3))
-(write-string (port->string err3b))
-(write-string (port->string i3b))
-(write-string (port->string err3c))
-(write-string (port->string i3c))
 (displayln "----- Okasaki / polymorphic recursion tests: --------------------")
 (write-string (port->string err4))
 (write-string (port->string i4))
@@ -38,51 +26,12 @@
 (close-input-port i1)
 (close-output-port o1)
 (close-input-port err1)
-(close-input-port i1b)
-(close-output-port o1b)
-(close-input-port err1b)
 (close-input-port i2)
 (close-output-port o2)
 (close-input-port err2)
 (close-input-port i3)
 (close-output-port o3)
 (close-input-port err3)
-(close-input-port i3b)
-(close-output-port o3b)
-(close-input-port err3b)
-(close-input-port i3c)
-(close-output-port o3c)
-(close-input-port err3c)
 (close-input-port i4)
 (close-output-port o4)
 (close-input-port err4)
-
-;; (require "mlish-tests.rkt")
-;; (require "mlish/queens.mlish")
-;; (require "mlish/trees.mlish")
-;; (require "mlish/chameneos.mlish")
-;; (require "mlish/ack.mlish")
-;; (require "mlish/ary.mlish")
-;; (require "mlish/fannkuch.mlish")
-;; (require "mlish/fasta.mlish")
-;; (require "mlish/fibo.mlish")
-;; (require "mlish/hash.mlish")
-;; ;(require "mlish/heapsort.mlish")
-;; (require "mlish/knuc.mlish")
-;; (require "mlish/matrix.mlish")
-;; (require "mlish/nbody.mlish")
-
-;; ;; from rw ocaml
-;; (require "mlish/term.mlish")
-;; (require "mlish/find.mlish")
-;; (require "mlish/alex.mlish")
-;; (require "mlish/inst.mlish")
-;; (require "mlish/result.mlish")
-
-;; ;; bg
-;; (require "mlish/bg/basics.mlish")
-;; (require "mlish/bg/huffman.mlish")
-;; (require "mlish/bg/lambda.rkt")
-
-;; ;; okasaki, polymorphic recursion
-;; (require "mlish/polyrecur.mlish")
diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt
index 4487582..c486d39 100644
--- a/tapl/tests/run-mlish-tests1.rkt
+++ b/tapl/tests/run-mlish-tests1.rkt
@@ -1,8 +1,10 @@
 #lang racket/base
 (require "mlish-tests.rkt")
-(require "mlish/queens.mlish")
+;(require "mlish/queens.mlish")
 (require "mlish/listpats.mlish")
 (require "mlish/match2.mlish")
+(require "mlish/polyrecur.mlish")
+(require "mlish/loop.mlish")
 
 ;; (require "mlish/trees.mlish")
 ;; (require "mlish/chameneos.mlish")
diff --git a/tapl/tests/run-mlish-tests1b.rkt b/tapl/tests/run-mlish-tests1b.rkt
deleted file mode 100644
index 64e8300..0000000
--- a/tapl/tests/run-mlish-tests1b.rkt
+++ /dev/null
@@ -1,15 +0,0 @@
-#lang racket/base
-;; (require "mlish-tests.rkt")
-;(require "mlish/queens.mlish")
-(require "mlish/trees-tests.mlish")
-(require "mlish/chameneos.mlish")
-(require "mlish/ack.mlish")
-(require "mlish/ary.mlish")
-(require "mlish/fannkuch.mlish")
-(require "mlish/fasta.mlish")
-(require "mlish/fibo.mlish")
-(require "mlish/hash.mlish")
-;(require "mlish/heapsort.mlish")
-(require "mlish/knuc.mlish")
-(require "mlish/matrix.mlish")
-(require "mlish/nbody.mlish")
diff --git a/tapl/tests/run-mlish-tests2.rkt b/tapl/tests/run-mlish-tests2.rkt
index dc856d4..7cc65dd 100644
--- a/tapl/tests/run-mlish-tests2.rkt
+++ b/tapl/tests/run-mlish-tests2.rkt
@@ -1,4 +1,21 @@
 #lang racket/base
+
+(require "mlish/queens.mlish")
+
+;; shootout tests
+(require "mlish/trees-tests.mlish")
+(require "mlish/chameneos.mlish")
+(require "mlish/ack.mlish")
+(require "mlish/ary.mlish")
+(require "mlish/fannkuch.mlish")
+(require "mlish/fasta.mlish")
+(require "mlish/fibo.mlish")
+(require "mlish/hash.mlish")
+;(require "mlish/heapsort.mlish")
+(require "mlish/knuc.mlish")
+(require "mlish/matrix.mlish")
+(require "mlish/nbody.mlish")
+
 ;; from rw ocaml
 (require "mlish/term.mlish")
 (require "mlish/find.mlish")
diff --git a/tapl/tests/run-mlish-tests3.rkt b/tapl/tests/run-mlish-tests3.rkt
index 50806bd..048d497 100644
--- a/tapl/tests/run-mlish-tests3.rkt
+++ b/tapl/tests/run-mlish-tests3.rkt
@@ -1,5 +1,7 @@
 #lang racket/base
 ;; bg
+(require "mlish/bg/basics.mlish")
+(require "mlish/bg/basics2.mlish")
 (require "mlish/bg/huffman.mlish")
 (require "mlish/bg/lambda.mlish")
 (require "mlish/bg/monad.mlish")
diff --git a/tapl/tests/run-mlish-tests4.rkt b/tapl/tests/run-mlish-tests4.rkt
index ade7b0b..4e8cc2d 100644
--- a/tapl/tests/run-mlish-tests4.rkt
+++ b/tapl/tests/run-mlish-tests4.rkt
@@ -1,5 +1,5 @@
 #lang racket/base
 
 ;; okasaki tests
-(require "mlish/polyrecur.mlish")
+;(require "mlish/polyrecur.mlish")
 (require "mlish/bg/okasaki.mlish")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index cab80dc..c0b602f 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -6,9 +6,9 @@
               "stx-utils.rkt")
   (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
   (for-meta 3 racket/base syntax/parse racket/syntax)
-  racket/bool racket/provide racket/require racket/match)
+  racket/bool racket/provide racket/require racket/match racket/promise)
 (provide
- symbol=? match
+ symbol=? match delay
  (except-out (all-from-out racket/base) #%module-begin)
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
@@ -431,9 +431,9 @@
     (syntax-parse t
       [((~literal #%plain-app) internal-id
         ((~literal #%plain-lambda) bvs
-         ((~literal #%expression) extra-info-to-extract) . rst))
-       #'extra-info-to-extract]
-      [_ #'void]))
+         ((~literal #%expression) ((~literal quote) extra-info-macro)) . tys))
+       (expand/df #'(extra-info-macro . tys))]
+      [_ #f]))
   (define (get-tyargs ty)
     (syntax-parse ty
       [((~literal #%plain-app) internal-id
@@ -493,9 +493,10 @@
          #:defaults ([bvs-op #'=][bvs-n #'0]))
         (~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon))
          #:defaults ([tycon #'void]))
-        (~optional (~seq #:extra-info extra-bvs extra-info)
+        #;(~optional (~seq #:extra-info extra-bvs extra-info)
                    #:defaults ([extra-bvs #'()]
                                [extra-info #'void]))
+        (~optional (~seq #:extra-info extra-info) #:defaults ([extra-info #'void]))
         (~optional (~and #:no-provide (~parse no-provide? #'#t)))
         )
      #:with #%kind (format-id #'kind "#%~a" #'kind)
@@ -580,14 +581,14 @@
                #:with k_result (if #,(attribute has-annotations?)
                                    #'(tycon k_arg (... ...))
                                    #'#%kind)
-               #:with extra-info-inst
-                      (if (stx-null? #'extra-bvs)
-                          #'extra-info
-                          (substs #'τs- #'extra-bvs #'extra-info))
+               ;; #:with extra-info-inst
+               ;;        (if (stx-null? #'extra-bvs)
+               ;;            #'extra-info
+               ;;            (substs #'τs- #'extra-bvs #'extra-info))
                (add-orig
                 (assign-type 
                   (syntax/loc stx 
-                    (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) 
+                    (τ-internal (λ bvs- (#%expression extra-info) . τs-))) 
                   #'k_result)
                 #'(τ . args))]
              ;; else fail with err msg