diff --git a/graph/graph/__DEBUG_graph__.rkt b/graph/graph/__DEBUG_graph__.rkt
index 76c5675a..3957b88d 100644
--- a/graph/graph/__DEBUG_graph__.rkt
+++ b/graph/graph/__DEBUG_graph__.rkt
@@ -34,6 +34,7 @@
 ((λget owner name) (get g streets cadr houses car))
 (get g streets … houses … owner name)
 ((λget streets … houses … owner name) g)
+(let ([f (λget streets … houses … owner name)]) f)
 ;(map: (λget houses … owner name) (get g streets))
 
 
diff --git a/graph/graph/graph4.lp2.rkt b/graph/graph/graph4.lp2.rkt
index aa4f7875..287823cd 100644
--- a/graph/graph/graph4.lp2.rkt
+++ b/graph/graph/graph4.lp2.rkt
@@ -89,12 +89,12 @@ otherwise throw an error:
              [(_ v:expr c…r:c…r other-fields …)
               #`(get v c…r.reverse-expanded … other-fields …)]
              [(_ v:expr (~literal …) other-fields …)
-              #;#'((map:: T
-                          (result-get T other-fields …)
-                          (has-get T other-fields …)
-                          (λget other-fields …))
-                   v)
-              #'((λ #:∀ (T) ([l : (Listof (has-get T other-fields …))])
+              #'((curry-map T
+                            (result-get T other-fields …)
+                            (has-get T other-fields …)
+                            (λget other-fields …))
+                 v)
+              #;#'((λ #:∀ (T) ([l : (Listof (has-get T other-fields …))])
                    : (Listof (result-get T other-fields …))
                    ((inst map
                           (result-get T other-fields …)
@@ -207,7 +207,8 @@ The type for the function generated by @tc[λget] mirrors the cases from
                   "variant.lp2.rkt"
                   "graph3.lp2.rkt"
                   "../type-expander/multi-id.lp2.rkt"
-                  "../type-expander/type-expander.lp2.rkt")
+                  "../type-expander/type-expander.lp2.rkt"
+                  "map1.rkt")
          (provide get
                   λget
                   has-get
diff --git a/graph/graph/map.rkt b/graph/graph/map.rkt
index 5e6f2c66..d16723c9 100644
--- a/graph/graph/map.rkt
+++ b/graph/graph/map.rkt
@@ -1,29 +1,197 @@
-#lang typed/racket
+#lang debug typed/racket
 
-(require (for-syntax syntax/parse)
+(require (for-syntax racket/syntax
+                     syntax/stx
+                     syntax/parse
+                     syntax/parse/experimental/template
+                     "../lib/low-untyped.rkt")
          "../lib/low.rkt"
-         "map1.rkt")
+         "map1.rkt"
+         "graph4.lp2.rkt"
+         "../type-expander/type-expander.lp2.rkt")
 
 (provide map:)
 
 (begin-for-syntax
   (define-syntax-class lam
-    (pattern (~or (~literal λ) (~literal lambda)))))
+    (pattern (~or (~literal λ) (~literal lambda))))
+  (define-syntax-class mapp
+    (pattern (~or (~literal map) (~literal map:)))))
 
+(define-for-syntax (remove-identities stx)
+  (syntax-parse stx
+    [() #'()]
+    [((~or (~lit identity) (~lit values) (~lit compose)) . rest)
+     (remove-identities #'rest)]
+    [([(~literal compose) . fs] . rest)
+     (define/with-syntax cleaned-fs (remove-identities #'fs))
+     (syntax-parse #'cleaned-fs
+       [() (remove-identities #'rest)]
+       [(one-f) #`(one-f . #,(remove-identities #'rest))]
+       [some-fs #`((compose . some-fs) . #,(remove-identities #'rest))])]
+    [(f . rest)
+     #`(f . #,(remove-identities #'rest))]))
+
+;; TODO: check that we don't bork the literals identity, values and compose
+;; inside macros or function calls, or alter them in any other way, e.g.
+;;     (map: (compose identity (λ (values) (+ values 1)) identity) '(1 2 3))
+;; or
+;;     (define (calltwice f) (λ (x) (f (f x))))
+;;     (map: (compose (calltwice identity)) '(1 2 3))
+;; Although a poor variable name choice, the two occurences of "values" in the
+;; first example shouldn't be altered, and the λ itself shouldn't be touched.
+;; In the second one, everything inside the calltwice function call should be
+;; left intact.
+(define-for-syntax (remove-identities1 stx)
+  (syntax-parse (remove-identities #`(#,stx))
+    [() #'identity]
+    [(f) #'f]))
+
+(begin-for-syntax
+  (define-syntax-class map-info
+    (pattern (_ #:in in-type
+                #:out out-type
+                #:∀ (∀-type …)
+                #:arg-funs ([arg-fun
+                             param-fun
+                             (~optional (~and auto-in #:auto-in))
+                             fun-in fun-out] …)
+                #:funs [fun …]))))
+
+(define-for-syntax (:map* stx* stx-&l… stx-out)
+  (if (stx-null? stx*)
+      '()
+      (syntax-parse (:map (stx-car stx*) stx-&l… stx-out)
+        [info:map-info
+         (let ([r (:map* (stx-cdr stx*) stx-&l… #'info.in-type)]
+               [auto (attribute info.auto-in)])
+           (if (and (not (null? auto)) (car auto) (not (null? r)))
+               (syntax-parse (car r)
+                 [r-info:map-info
+                  (let ([intact #'([info.arg-fun
+                                    info.param-fun
+                                    info.fun-in ;;;
+                                    info.fun-out] …)]
+                        [replaced #'([info.arg-fun
+                                      info.param-fun
+                                      r-info.out-type ;;info.fun-in ;;;
+                                      info.fun-out] …)])
+                    (cons #`(info #:in info.in-type
+                                  #:out info.out-type
+                                  #:∀ (info.∀-type …)
+                                  #:arg-funs (#,(stx-car replaced)
+                                              #,@(stx-cdr intact))
+                                  #:funs [info.fun …])
+                          r))])
+               (cons #'info r)))])))
+
+(define-for-syntax (:map stx stx-&l… stx-out)
+  (define/with-syntax (&l …) stx-&l…)
+  (define/with-syntax out stx-out)
+  (syntax-parse (remove-identities1 stx)
+    [(~literal car)
+     #'(info #:in (Pairof out Any) #:out out #:∀ ()
+             #:arg-funs () #:funs (car))]
+    [(~literal cdr)
+     #'(info #:in (Pairof Any out) #:out out #:∀ ()
+             #:arg-funs () #:funs (cdr))]
+    ;; TODO: should remove `identity` completely, doing (map identity l) is
+    ;; useless appart for constraining the type, but it's an ugly way to do so.
+    [(~literal identity)
+     #'(info #:in out #:out out #:∀ ()
+             #:arg-funs () #:funs (identity))]
+    [((~literal compose) f …)
+     (syntax-parse (:map* #'(f …) #'(&l …) #'out)
+       [(~and (_ … first:map-info) (last:map-info . _) (:map-info …))
+        #'(info #:in first.in-type
+                #:out last.out-type
+                #:∀ (∀-type … …)
+                #:arg-funs ([arg-fun param-fun fun-in fun-out] … …)
+                #:funs (fun … …))])]
+    [((~literal curry) :mapp f)
+     (syntax-parse (internal-map: #'f #'(&l …) #'out)
+       [(i:map-info . code)
+        #'(info #:in (Listof i.in-type)
+                #:out (Listof out)
+                #:∀ [i.∀-type …]; i.out-type
+                #:arg-funs [(i.arg-fun i.param-fun i.fun-in i.fun-out) …]
+                #:funs [(code i.fun … _)])])]
+    [(~literal length)
+     (define-temp-ids "&~a" f)
+     (define-temp-ids "~a/in" f)
+     #'(info #:in f/in #:out out #:∀ (f/in)
+             #:arg-funs ([(λ ([l : (Listof Any)]) (length l))
+                          &f
+                          #:auto-in f/in
+                          out])
+             #:funs (&f))]
+    [f
+     (define-temp-ids "&~a" f)
+     (define-temp-ids "~a/in" f)
+     #'(info #:in f/in #:out out #:∀ (f/in)
+             #:arg-funs ([f &f #:auto-in f/in out]) #:funs (&f))]))
+
+(define-syntax apply-compose
+  (syntax-rules ()
+    [(_ [] [a …]) (values a …)]
+    [(_ [f0 . f] [a …]) (apply-compose f [(f0 a …)])]))
+
+(define-for-syntax (internal-map: stx-f stx-&l… stx-out)
+  (define/with-syntax f stx-f)
+  (define/with-syntax (&l …) stx-&l…)
+  (define/with-syntax out stx-out)
+  (syntax-parse (:map #'f #'(&l …) #'out)
+    [(~and i :map-info)
+     (cons #'i
+           #'(let ()
+               (: map1 (∀ [out ∀-type …]
+                          (→ (→ fun-in fun-out) …
+                             (Listof in-type)
+                             (Listof out-type))))
+               (define (map1 param-fun … &l …)
+                 (if (or (null? &l) …)
+                     '()
+                     (cons (apply-compose [fun …] [(car &l) …])
+                           (map1 param-fun … (cdr &l) …))))
+               map1))]));(map1 arg-fun … . ls)
+
+;; TODO: inefficient at compile-time: we run (:map #'f #'Out) twice.
+;; Plus it could cause some bugs because of differing #'Out.
 (define-syntax (map: stx)
   (syntax-parse stx
-    [(_ (~literal car) l) #'((curry-map A A (Pairof A Any) car) l)]
-    [(_ (~literal cdr) l) #'((curry-map B B (Pairof Any B) cdr) l)]
-    ;; TODO: add caar etc.
-    [(_ ((~literal values)) l) #'l]
-    [(_ ((~literal compose)) l) #'l]
-    [(_ ((~literal compose) f0 . fs) l) #'(map: f0 (map: (compose . fs) l))]
-    [(_ ((~literal curry) map: f) l)
-     #''_]
-    [(_ f . ls)
-     #'(map f . ls)]))
+    [(_ (~optional (~and norun (~literal norun))) f l …)
+     (define-temp-ids "&~a" (l …))
+     (syntax-parse (internal-map: #'f #'(&l …) #'Out)
+       [(:map-info . code)
+        (if (attribute norun)
+            #'(ann '(code arg-fun … l …) Any)
+            #'(code arg-fun … l …))])]))
 
-(module* test typed/racket
+(map: add1 '(1 2 3))
+(map: (compose add1) '(1 2 3))
+(map: (∘ identity add1) '(1 2 3))
+(map: (∘ add1 identity) '(1 2 3))
+(map: (∘ number->string add1) '(1 2 9))
+(map: (∘ string-length number->string add1) '(1 2 9))
+(map: car '((1 2) (2) (9 10 11)))
+(map: (∘ add1 car) '((1 2) (2) (9 10 11)))
+(map: (∘ string-length number->string add1 car cdr)
+      '((1 2) (2 3) (9 10 11)))
+(map: identity '(1 2 3))
+(map: values '(1 2 3))
+(map: (compose) '(1 2 3))
+(map: (compose identity) '(1 2 3))
+(map: (∘ identity values identity values) '(1 2 3))
+(map: (∘ length (curry map add1)) '((1 2) (3)))
+
+(map: (curry map add1) '((1 2) (3)))
+
+(define (numlist [x : Number]) (list x))
+(map: (∘ (curry map add1) numlist) '(1 2 3))
+(map: (∘ (curry map add1) (λ ([x : Number]) (list x))) '(1 2 3))
+
+
+#|(module* test typed/racket
   (require (submod "..")
            "../lib/low.rkt")
   
@@ -53,4 +221,253 @@
                  '(2 3 4))
   (check-equal?: (map: + '(1 2 3) '(4 5 6))
                  : (Listof Number)
-                 '(5 7 9)))
\ No newline at end of file
+                 '(5 7 9)))|#
+
+
+
+
+
+
+#|
+(map: (compose F (curry map add1)) '((1 2) (3)))
+
+Problem: in the code above, the input type of `F` has to be the return type of
+`(curry map add1)`, i.e. `(Listof B)`. The return type of `F` may depend on its
+input type (e.g. wrapping a value), so the type information flows leftwards
+inside `compose`.
+
+However, if F is a destructuring operation, like `car` or `cdr`, it may impose
+constraints on the return type of the function immediately to its right, meaning
+that the type information flows rightwards.
+
+It seems difficult to reconcile these two cases without writing a complex
+algorithm.
+
+Worst-case scenario:
+
+         +-- constrains to the right
+         v                                  v-- constrains to the right
+(compose car complex-calculation (curry map car))
+             ^                   ^-- gives a (Listof ?) to the left
+             +-- constrained on both sides
+
+Maybe we could cover most common cases by first getting the type for the handled
+cases which impose constraints to the right and/or give a type to the left, and
+then use these types instead of the ∀, to fill in the holes for other functions.
+
+EDIT: that's what we did, using the #:auto-in
+|#
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#|
+(define-for-syntax (map-infer-types stx)
+  (syntax-parse stx
+    [(_ (~literal car))
+     (values #'(A B)
+             #'(Pairof A B))]
+    [(_ (~literal cdr)) #'(Pairof Any T)]
+    [(_ T (~literal values)) #'T]
+    [(_ T ((~literal compose))) #'T]
+    [(_ T ((~literal compose) f0 . fs))
+     #'(map-element (map-element T f0) (compose . fs))]
+    [(_ T ((~literal curry) (~or (~literal map:) (~literal map)) f) l)
+     #''_]
+    ;; get
+    [(_ f . ls)
+     ;; TODO:
+     #'T]))
+
+(define-type-expander (map-element stx)
+  (syntax-parse stx
+    [(_ T:id (~literal car)) #'(Pairof T Any)]
+    [(_ T:id (~literal cdr)) #'(Pairof Any T)]
+    [(_ T (~literal values)) #'T]
+    [(_ T ((~literal compose))) #'T]
+    [(_ T ((~literal compose) f0 . fs))
+     #'(map-element (map-element T f0) (compose . fs))]
+    [(_ T ((~literal curry) (~or (~literal map:) (~literal map)) f) l)
+     #''_]
+    ;; get
+    [(_ f . ls)
+     ;; TODO:
+     #'T]))
+
+
+(define-type-expander (map-result stx)
+  (syntax-parse stx
+    [(_ T:id (~literal car)) #'T]
+    [(_ T:id (~literal cdr)) #'T]))
+
+(define-syntax (map: stx)
+  (syntax-parse stx
+    [(_ (~literal car) l) #'((curry-map A A (Pairof A Any) car) l)]
+    [(_ (~literal cdr) l) #'((curry-map B B (Pairof Any B) cdr) l)]
+    ;; TODO: add caar etc.
+    [(_ ((~literal values)) l) #'l]
+    [(_ ((~literal compose)) l) #'l]
+    [(_ ((~literal compose) f0 . fs) l) #'(map: f0 (map: (compose . fs) l))]
+    [(_ ((~literal curry) (~or (~literal map:) (~literal map)) f) l)
+     #''_]
+    [(_ ((~literal λget) field-or-accessor …) l)
+     #'(get l (… …) field-or-accessor …)]
+    [(_ f . ls)
+     #'(map f . ls)]))
+
+
+
+|#
+
+
+
+
+
+
+
+
+
+#|
+
+#;#'(let ()      
+      (: map2 (∀ (poly-types …) (→ function-types …
+                                   (Listof (Listof A))
+                                   (Listof (Listof D)))))
+      (define (map2 f … l)
+        (if (null? l)
+            '()
+            (cons (map1 f … (car l))
+                  (map2 f … (cdr l)))))
+      (map2 f … l))
+
+; (map: (curry map add1) '((1 2 3) (4 5))) =>
+; (map: (curry map: add1) '((1 2 3) (4 5))) =>
+(let ()
+  (: map2 (∀ (A C) (→ (→ A C)
+                      (Listof (Listof A))
+                      (Listof (Listof C)))))
+  (define (map2 f l)
+    (if (null? l) '() (cons (map f (car l)) (map2 f (cdr l)))))
+  (map2 add1 '((1 2 3) (4 5))))
+
+;; TODO:
+; (map: (compose (curry map (compose list add1))
+;                (curry map (compose add1 add1)))
+;       '((1 2 3) (4 5)))
+; =>
+#;???
+
+; (map: (curry map (compose number->string add1)) '((1 2 3) (4 5))) =>
+; (map: (curry map: (compose number->string add1)) '((1 2 3) (4 5))) =>
+(let ()
+  (: map2 (∀ (A C D) (→ (→ A C)
+                        (→ C D)
+                        (Listof (Listof A))
+                        (Listof (Listof D)))))
+  (define (map2 f g l)
+    (if (null? l)
+        '()
+        (cons ;(map1 f g (car l))
+         ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+         (let ()
+           (: map1 (∀ (A C D) (→ (→ A C)
+                                 (→ C D)
+                                 (Listof A)
+                                 (Listof D))))
+           (define (map1 f g l)
+             (if (null? l) '() (cons (g (f (car l))) (map1 f g (cdr l)))))
+           (map1 f g (car l)))
+         ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+         (map2 f g (cdr l)))))
+  (map2 add1 number->string '((1 2 3) (4 5))))
+
+; (map: add1 '(1 2 3))
+(let ()
+  (: map1 (∀ (A C) (→ (→ A C)
+                      (Listof A)
+                      (Listof C))))
+  (define (map1 f l)
+    (if (null? l) '() (cons (f (car l)) (map1 f (cdr l)))))
+  (map1 add1 '(1 2 3)))
+
+; (map: car '((1 a) (2 b) (3 c)))
+(let ()
+  (: map1 (∀ (A B) (→ (→ (Pairof A B) A)
+                      (Listof (Pairof A B))
+                      (Listof A))))
+  (define (map1 f l)
+    (if (null? l) '() (cons (f (car l)) (map1 f (cdr l)))))
+  (map1 car
+        '((1 a) (2 b) (3 c))))
+
+; (map: (curry map car) '([(1 a) (2 b)] [(3 c)]))
+; (map: (curry map: car) '([(1 a) (2 b)] [(3 c)]))
+(let ()
+  (: map1 (∀ (A B) (→ (→ (Pairof A B) A)
+                      (Listof (Pairof A B))
+                      (Listof A))))
+  (define (map1 f l)
+    (if (null? l) '() (cons (f (car l)) (map1 f (cdr l)))))
+  
+  (: map2 (∀ (A B) (→ (→ (Pairof A B) A)
+                      (Listof (Listof (Pairof A B)))
+                      (Listof (Listof A)))))
+  (define (map2 f l)
+    (if (null? l) '() (cons (map1 f (car l)) (map2 f (cdr l)))))
+  
+  (map2 car
+        '([(1 a) (2 b)] [(3 c)])))
+
+; (map: (curry map (curry map car)) '([(1 a) (2 b)] [(3 c)]))
+; (map: (curry map (curry map: car)) '([(1 a) (2 b)] [(3 c)]))
+; (map: (curry map: (curry map car)) '([(1 a) (2 b)] [(3 c)]))
+; (map: (curry map: (curry map: car)) '([(1 a) (2 b)] [(3 c)]))
+(let ()
+  (: map3 (∀ (A B) (→ ;(→ (Pairof A B) A)
+                    (Listof (Listof (Listof (Pairof A B))))
+                    (Listof (Listof (Listof A))))))
+  (define (map3 #|f|# l)
+    (if (null? l)
+        '()
+        (cons (let ()
+                (: map2 (∀ (A B) (→ ;(→ (Pairof A B) A)
+                                  (Listof (Listof (Pairof A B)))
+                                  (Listof (Listof A)))))
+                (define (map2 #|f|# l)
+                  (if (null? l)
+                      '()
+                      (cons (let ()
+                              (: map1 (∀ (A B) (→ ;(→ (Pairof A B) A)
+                                                (Listof (Pairof A B))
+                                                (Listof A))))
+                              (define (map1 #|f|# l)
+                                (if (null? l)
+                                    '()
+                                    (cons (#|f|#car (car l))
+                                          (map1 #|f|# (cdr l)))))
+                              (map1 #|f|# (car l)))
+                            (map2 #|f|# (cdr l)))))
+                (map2 #|f|# (car l)))
+              (map3 #|f|# (cdr l)))))
+  (map3 ;car
+   '([[(1 a) (2 b)] [(3 c)]] [[(4 d)]])))
+
+;(define-syntax-rule (inst-∀ T …)
+
+
+|#
\ No newline at end of file
diff --git a/graph/graph/map1.rkt b/graph/graph/map1.rkt
index b078844b..7b241756 100644
--- a/graph/graph/map1.rkt
+++ b/graph/graph/map1.rkt
@@ -1,7 +1,8 @@
 #lang typed/racket
 
 (require (for-syntax syntax/parse
-                     "../lib/low-untyped.rkt"))
+                     "../lib/low-untyped.rkt")
+         "../type-expander/type-expander.lp2.rkt")
 
 (provide curry-map)
 
@@ -22,6 +23,9 @@
   (syntax-parse stx
     [(_ TVar Result-Type Element-Type f:curry-map-rec)
      (if (attribute f.bottom?)
+         ;; We use (ann λ type) instead of (λ #:∀ …) because as of version
+         ;; 6.3.0.8--2015-12-17(0d633fe/a), the latter doesn't work if put in a
+         ;; let's binding clause: (let ([f (λ #:∀ …)]) f) fails to typecheck.
          #'(ann (λ (l) ((inst map Result-Type Element-Type) f l))
                 (∀ (TVar) (→ (Listof Element-Type)
                              (Listof Result-Type))))
diff --git a/graph/lib/low.rkt b/graph/lib/low.rkt
index 5fba8daa..4e30e133 100644
--- a/graph/lib/low.rkt
+++ b/graph/lib/low.rkt
@@ -9,11 +9,20 @@
 ;; raco pkg install alexis-util
 ;; or:
 ;; raco pkg install threading
-(require alexis/util/threading)
+(require alexis/util/threading
+         (for-syntax racket/syntax
+                     syntax/parse))
 
 (define-syntax-rule (~>_ clause ... expr) (~> expr clause ...))
+(define-syntax (<~ stx)
+  (syntax-parse stx
+    [(_ expr clause ...)
+     (define/with-syntax (r-clause ...) (reverse (syntax->list #'(clause ...))))
+     #'(~> expr r-clause ...)]))
 
-(provide ~>_ ~> ~>> _ (rename-out [_ ♦]))
+(define-syntax-rule (<~_ clause ... expr) (<~ expr clause ...))
+
+(provide <~ <~_ ~>_ ~> ~>> _ (rename-out [_ ♦] [<~_ <~♦] [~>_ ~>♦]))
 
 ;; ==== low/typed-untyped-module.rkt ====
 
@@ -596,7 +605,7 @@
 (define (check-duplicate-identifiers ids)
   (if (check-duplicate-identifier (my-in-syntax ids)) #t #f))
 
-(require/typed racket/syntax [generate-temporary (→ Syntax Identifier)])
+(require/typed racket/syntax [generate-temporary (→ Any Identifier)])
 
 (require syntax/parse/define)
 (provide define-simple-macro)
@@ -619,7 +628,8 @@
   
   (require/typed racket/syntax
                  [format-id (→ Syntax String (U String Identifier) *
-                               Identifier)])
+                               Identifier)]
+                 [(generate-temporary generate-temporary2) (→ Any Identifier)])
   (require (only-in racket/syntax define/with-syntax)
            (only-in syntax/stx stx-map)
            (for-syntax racket/base
@@ -780,7 +790,9 @@
          (define/with-syntax pat-dotted ((attribute base.make-dotted) #'pat))
          
          (define/with-syntax format-temp-ids*
-           ((attribute base.wrap) #'(compose car (curry format-temp-ids format))
+           ((attribute base.wrap) #'(compose car
+                                             (curry format-temp-ids format)
+                                             generate-temporary)
                                   (λ (x deepest?)
                                     (if deepest?
                                         x
@@ -823,14 +835,14 @@
        (define/with-syntax pat (format-id #'base (syntax-e #'format)))
        (define/with-syntax pat-dotted ((attribute base.make-dotted) #'pat))
        (define/with-syntax format-temp-ids*
-           ((attribute base.wrap) #'(λ (x)
-                                      (car (format-temp-ids
-                                            (string-append format "~a")
-                                            "")))
-                                  (λ (x deepest?)
-                                    (if deepest?
-                                        x
-                                        #`(curry stx-map #,x)))))
+         ((attribute base.wrap) #'(λ (x)
+                                    (car (format-temp-ids
+                                          (string-append format "~a")
+                                          "")))
+                                (λ (x deepest?)
+                                  (if deepest?
+                                      x
+                                      #`(curry stx-map #,x)))))
        (syntax-cons-property
         #'(define/with-syntax pat-dotted
             (format-temp-ids* #'base))
@@ -892,15 +904,25 @@
   
   (check-equal? (fubar) '((1 . a) (2 . b) (3 . c))))
 
-#|
-(define-template-metafunction (t/gen-temp stx)
-  (syntax-parse stx
-    [(_ . id:id)
-     #:with (temp) (generate-temporaries #'(id))
-     #'temp]
-    [(_ id:id ...)
-     (generate-temporaries #'(id ...))]))
-|#
+(module m-t/gen-temp racket
+  (require syntax/parse
+           syntax/parse/experimental/template)
+  
+  (provide t/gen-temp)
+  
+  (define-template-metafunction (t/gen-temp stx)
+    (syntax-parse stx
+      [(_ id:id)
+       #:with (temp) (generate-temporaries #'(id))
+       #'temp]
+      #|[(_ . id:id)
+       #:with (temp) (generate-temporaries #'(id))
+       #'temp]
+      [(_ id:id ...)
+       (generate-temporaries #'(id ...))]|#)))
+
+(require 'm-t/gen-temp)
+(provide (rename-out [t/gen-temp &]))
 
 ;; ==== syntax.rkt ====
 
@@ -936,11 +958,75 @@
                [stx-car (∀ (A B) (→ (Syntaxof (Pairof A B)) A))]
                [stx-cdr (∀ (A B) (→ (Syntaxof (Pairof A B)) B))])
 |#
-(: stx-car (∀ (A B) (→ (Syntaxof (Pairof A B)) A)))
-(define (stx-car p) (car (syntax-e p)))
+(: stx-car (∀ (A B)
+              (case→ (→ (Syntaxof (Pairof A B)) A)
+                     ;; TODO: Not typesafe!
+                     (→ (U (Syntaxof (Listof A)) (Listof A)) A))))
+(define (stx-car p) (car (if (syntax? p) (syntax-e p) p)))
 
-(: stx-cdr (∀ (A B) (→ (Syntaxof (Pairof A B)) B)))
-(define (stx-cdr p) (cdr (syntax-e p)))
+(: stx-cdr (∀ (A B)
+              (case→ (→ (Syntaxof (Pairof A B)) B)
+                     ;; TODO: Not typesafe!
+                     (→ (U (Syntaxof (Listof A)) (Listof A)) (Listof A)))))
+(define (stx-cdr p) (cdr (if (syntax? p) (syntax-e p) p)))
+
+(: stx-null? (→ Any Boolean : (U (Syntaxof Null) Null)))
+(define (stx-null? v)
+  ((make-predicate (U (Syntaxof Null) Null)) v))
+
+(: stx-foldl
+   (∀ (E F G Acc)
+      (case→ (→ (→ E Acc Acc)
+                Acc
+                (U (Syntaxof (Listof E)) (Listof E))
+                Acc)
+             (→ (→ E F Acc Acc)
+                Acc
+                (U (Syntaxof (Listof E)) (Listof E))
+                (U (Syntaxof (Listof F)) (Listof F))
+                Acc)
+             (→ (→ E F G Acc Acc)
+                Acc
+                (U (Syntaxof (Listof E)) (Listof E))
+                (U (Syntaxof (Listof F)) (Listof F))
+                (U (Syntaxof (Listof G)) (Listof G))
+                Acc))))
+(define stx-foldl
+  (case-lambda
+    [(f acc l)
+     (if (stx-null? l)
+         acc
+         (stx-foldl f (f (stx-car l) acc) (stx-cdr l)))]
+    [(f acc l l2)
+     (if (or (stx-null? l) (stx-null? l2))
+         acc
+         (stx-foldl f
+                    (f (stx-car l) (stx-car l2) acc)
+                    (stx-cdr l)
+                    (stx-cdr l2)))]
+    [(f acc l l2 l3)
+     (if (or (stx-null? l) (stx-null? l2) (stx-null? l3))
+         acc
+         (stx-foldl f
+                    (f (stx-car l) (stx-car l2) (stx-car l3) acc)
+                    (stx-cdr l)
+                    (stx-cdr l2)
+                    (stx-cdr l3)))]))
+
+(module m-stx-untyped racket
+  (require syntax/stx)
+  (provide stx-cons stx-drop-last)
+  
+  ;(: stx-cons (∀ (A B) (→ A B (Syntaxof (Pairof A B)))))
+  (define (stx-cons a b) #`(#,a . #,b))
+  
+  ;(: stx-drop-last (∀ (A) (→ (Syntaxof (Listof A)) (Syntaxof (Listof A)))))
+  (define (stx-drop-last l)
+    (if (and (stx-pair? l) (stx-pair? (stx-cdr l)))
+        (stx-cons (stx-car l) (stx-drop-last (stx-cdr l)))
+        #'())))
+
+(require 'm-stx-untyped)
 
 ; (require/typed racket/base [(assoc assoc3)
 ;                             (∀ (a b) (→ Any (Listof (Pairof a b))
diff --git a/graph/type-expander/type-expander.lp2.rkt b/graph/type-expander/type-expander.lp2.rkt
index 29b4df15..90226112 100644
--- a/graph/type-expander/type-expander.lp2.rkt
+++ b/graph/type-expander/type-expander.lp2.rkt
@@ -385,7 +385,7 @@ them.
          (pattern [id:id (~optional (~seq :colon type:expr)) default:expr]
                   #:with tvars tvars
                   #:with (expanded ...)
-                  (template ([id (?@ : (tmpl-expand-type tvars type))
+                  (template ([id (?? (?@ : (tmpl-expand-type tvars type)))
                               default])))
          (pattern (~var kw (new-kw-formal tvars))
                   #:with (expanded ...) #'(kw.expanded ...)))