diff --git a/graph-lib/graph/__DEBUG_graph__.rkt b/graph-lib/graph/__DEBUG_graph__.rkt
index 1806a6d8..87edac86 100644
--- a/graph-lib/graph/__DEBUG_graph__.rkt
+++ b/graph-lib/graph/__DEBUG_graph__.rkt
@@ -18,15 +18,18 @@
 (define-tagged tabc t [a 1] [b 'b] [c "c"])
 |#
 
-(require (submod "graph3.lp2.rkt" test))
-(require "graph3.lp2.rkt")
-(require "graph4.lp2.rkt")
-(require "map.rkt")
-(require "structure.lp2.rkt")
-(require "variant.lp2.rkt")
-(require "../lib/low.rkt")
-(require "../type-expander/type-expander.lp2.rkt")
+(require "__DEBUG_require.rkt")
 
+;; (map: (compose (curry map identity) (λget houses …)) (get g streets))
+;; (map: (compose (λget houses …) (λ #:∀ (A) ([x : A]) x)) (get g streets))
+;; (map: (compose (λget houses …) (curry map (λget owner))) (get g streets))
+;; => TODO: Crashes ../type-expander/type-expander.lp2.rkt:90:7: syntax-local-bind-syntaxes: contract violation
+;  expected: (listof identifier?)
+;  given: (#<syntax:/home/georges/phc/racket/graph-lib/graph/map.rkt:130:18 (has-get Out houses …)>)
+;  argument position: 1st
+;  other arguments...:
+
+#|
 (get '((1 2) (3)) … …)
 (structure-get (cadr (force g)) people)
 (get g people)
@@ -37,6 +40,7 @@
 ((λ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-lib/graph/__DEBUG_require.rkt b/graph-lib/graph/__DEBUG_require.rkt
new file mode 100644
index 00000000..af07347a
--- /dev/null
+++ b/graph-lib/graph/__DEBUG_require.rkt
@@ -0,0 +1,19 @@
+#lang typed/racket
+
+(require (submod "graph3.lp2.rkt" test))
+(require "graph3.lp2.rkt")
+(require "graph4.lp2.rkt")
+(require "map.rkt")
+(require "structure.lp2.rkt")
+(require "variant.lp2.rkt")
+(require "../lib/low.rkt")
+(require "../type-expander/type-expander.lp2.rkt")
+
+(provide (all-from-out (submod "graph3.lp2.rkt" test)
+                       "graph3.lp2.rkt"
+                       "graph4.lp2.rkt"
+                       "map.rkt"
+                       "structure.lp2.rkt"
+                       "variant.lp2.rkt"
+                       "../lib/low.rkt"
+                       "../type-expander/type-expander.lp2.rkt"))
\ No newline at end of file
diff --git a/graph-lib/graph/map.rkt b/graph-lib/graph/map.rkt
index 0f936097..d0bb59c7 100644
--- a/graph-lib/graph/map.rkt
+++ b/graph-lib/graph/map.rkt
@@ -5,12 +5,15 @@
                      syntax/parse
                      syntax/parse/experimental/template
                      "../lib/low-untyped.rkt")
+         (for-meta 2
+                   racket/base
+                   racket/syntax)
          "../lib/low.rkt"
          "map1.rkt"
          "graph4.lp2.rkt"
          "../type-expander/type-expander.lp2.rkt")
 
-(provide map:)
+(provide map: apply-compose) ;; TODO: move apply-compose to lib/low.rkt
 
 (begin-for-syntax
   (define-syntax-class lam
@@ -50,6 +53,7 @@
 (begin-for-syntax
   (define-syntax-class map-info
     (pattern (_ #:in in-type
+                #:in-∀ [in-∀ …]
                 #:out out-type
                 #:∀ (∀-type …)
                 #:arg-funs ([arg-fun
@@ -58,12 +62,21 @@
                              fun-in fun-out] …)
                 #:funs [fun …]))))
 
-(define-for-syntax (:map* stx* stx-&ls stx-out)
+(begin-for-syntax
+  (define-syntax (mk-info stx)
+    (syntax-case stx ()
+      [(_ . rest-stx)
+       (begin
+         (define/with-syntax whole-stx (syntax/loc stx (info . rest-stx)))
+         #'(syntax-parse #`whole-stx
+             [i:map-info #'i]))])))
+
+(define-for-syntax (:map* stx* stx-&ls stx-out stx-out-∀)
   (if (stx-null? stx*)
       '()
-      (syntax-parse (:map (stx-car stx*) stx-&ls stx-out)
+      (syntax-parse (:map (stx-car stx*) stx-&ls stx-out stx-out-∀)
         [info:map-info
-         (let ([r (:map* (stx-cdr stx*) stx-&ls #'info.in-type)]
+         (let ([r (:map* (stx-cdr stx*) stx-&ls #'info.in-type #'[info.in-∀ …])]
                [auto (attribute info.auto-in)])
            (if (and (not (null? auto)) (car auto) (not (null? r)))
                (syntax-parse (car r)
@@ -76,88 +89,102 @@
                                       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 …])
+                    (cons (mk-info #:in info.in-type
+                                   #:in-∀ [info.in-∀ …]
+                                   #: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-&ls stx-out)
+(define-for-syntax (:map stx stx-&ls stx-out stx-out-∀)
   (define/with-syntax (&l …) stx-&ls)
   (define/with-syntax out stx-out)
+  (define/with-syntax (out-∀ …) stx-out-∀)
   (syntax-parse (remove-identities1 stx)
     [(~literal car)
-     #'(info #:in (Pairof out Any) #:out out #:∀ ()
-             #:arg-funs () #:funs (car))]
+     #'(info #:in (Pairof out Any) #:in-∀ [] #:out out #:∀ []
+             #:arg-funs [] #:funs [car])]
     [(~literal cdr)
-     #'(info #:in (Pairof Any out) #:out out #:∀ ()
-             #:arg-funs () #:funs (cdr))]
+     #'(info #:in (Pairof Any out) #:in-∀ [] #: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))]
+     #'(info #:in out #:in-∀ [] #:out out #:∀ []
+             #:arg-funs [] #:funs [identity])]
     [((~literal compose) f …)
-     (syntax-parse (:map* #'(f …) #'(&l …) #'out)
+     (syntax-parse (:map* #'(f …) #'(&l …) #'out #'[out-∀ …])
        [(~and (_ … rightmost:map-info) (leftmost:map-info . _) (:map-info …))
         #'(info #:in rightmost.in-type
+                #:in-∀ [rightmost.in-∀ …];; ??
                 #:out leftmost.out-type
-                #:∀ (∀-type … …)
-                #:arg-funs ([arg-fun param-fun fun-in fun-out] … …)
-                #:funs (fun … …))])]
+                #:∀ [∀-type … …]
+                #:arg-funs [(arg-fun param-fun fun-in fun-out) … …]
+                #:funs [fun … …])])]
     [((~literal curry) :mapp f)
-     (syntax-parse (internal-map: #'f #'(&l …) #'out)
+     (syntax-parse (internal-map: #'f #'(&l …) #'out #'[out-∀ …])
        [(i:map-info . code)
-        #'(info #:in (Listof i.in-type)
+        #`(info #:in (Listof i.in-type)
+                #:in-∀ [i.in-∀ …];; ??
                 #: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 … _)])])]
+                #:funs [#,(syntax/loc #'f (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))
+     #'(info #:in f/in #:in-∀ [f/in] #:out out #:∀ [f/in] ;;??
+             #:arg-funs [((λ ([l : (Listof Any)]) (length l))
                           &f
                           #:auto-in f/in
-                          out])
-             #:funs (&f))]
+                          out)]
+             #:funs [&f])]
+    [((~literal λget) pat …)
+     #'(info #:in (has-get out pat …)
+             #:in-∀ [out-∀ …]
+             #:out (result-get out pat …)
+             #:∀ []
+             #:arg-funs []
+             #:funs [(get _ pat …)])]
     [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))]))
+     #'(info #:in f/in #:in-∀ [f/in] #:out out #:∀ [f/in] ;;??
+             #:arg-funs [(f &f #:auto-in f/in out)] #:funs [&f])]))
 
 (define-syntax (apply-compose stx)
   (syntax-parse stx
     [(_ [] [a …])
      #'(values a …)]
-    [(_ [f … (f-last x … (~literal _) y …)] [a …])
-     #'(apply-compose [f …] [(f-last x … a … y …)])]
+    [(_ [f … (~and loc (f-last x … (~literal _) y …))] [a …])
+     #`(apply-compose [f …] [#,(syntax/loc #'loc (f-last x … a … y …))])]
     [(_ [f … f-last] [a …])
-     #'(apply-compose [f …] [(f-last a …)])]))
+     #`(apply-compose [f …] [#,(syntax/loc #'f-last (f-last a …))])]))
 
-(define-for-syntax (internal-map: stx-f stx-&ls stx-out)
+(define-for-syntax (internal-map: stx-f stx-&ls stx-out stx-out-∀)
   (define/with-syntax f stx-f)
   (define/with-syntax (&l …) stx-&ls)
   (define/with-syntax out stx-out)
-  (syntax-parse (:map #'f #'(&l …) #'out)
+  (define/with-syntax (out-∀ …) stx-out-∀)
+  (syntax-parse (:map #'f #'(&l …) #'out #'[out-∀ …])
     [(~and i :map-info)
+     (define/with-syntax map1 (generate-temporary #'map))
      (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)
+           (template
+            (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.
@@ -165,7 +192,7 @@
   (syntax-parse stx
     [(_ (~optional (~and norun (~literal norun))) f l …)
      (define-temp-ids "&~a" (l …))
-     (syntax-parse (internal-map: #'f #'(&l …) #'Out)
+     (syntax-parse (internal-map: #'f #'(&l …) #'Out #'[Out])
        [(:map-info . code)
         (if (attribute norun)
             #'(ann '(code arg-fun … l …) Any)
@@ -239,54 +266,54 @@
   ;; the map: identifier with a contract, so the identifier seen outside the
   ;; module is not the same as the one used in the syntax-parse ~literal clause.
   
-  #;(begin
-    (check-equal?: (map: (curry map add1) '((1 2 3) (4 5)))
-                   : (Listof (Listof Number))
-                   '((2 3 4) (5 6)))
-    #;(check-equal?: (map: (curry map: add1) '((1 2 3) (4 5)))
+  #|(begin
+      (check-equal?: (map: (curry map add1) '((1 2 3) (4 5)))
                      : (Listof (Listof Number))
                      '((2 3 4) (5 6)))
-    
-    (check-equal?: (map: (curry map (compose number->string add1))
-                         '((1 2 3) (4 5)))
-                   : (Listof (Listof String))
-                   '(("2" "3" "4") ("5" "6")))
-    #;(check-equal?: (map: (curry map: (compose number->string add1))
+      #;(check-equal?: (map: (curry map: add1) '((1 2 3) (4 5)))
+                       : (Listof (Listof Number))
+                       '((2 3 4) (5 6)))
+      
+      (check-equal?: (map: (curry map (compose number->string add1))
                            '((1 2 3) (4 5)))
                      : (Listof (Listof String))
                      '(("2" "3" "4") ("5" "6")))
-    
-    (check-equal?: (map: add1 '(1 2 3))
-                   : (Listof Number)
-                   '(2 3 4))
-    
-    (check-equal?: (map: car '((1 a) (2 b) (3 c)))
-                   : (Listof Number)
-                   '(1 2 3))
-    
-    (check-equal?: (map: (curry map car) '([(1 a) (2 b)] [(3 c)]))
-                   : (Listof Number)
-                   '((1 a) (3 c)))
-    #;(check-equal?: (map: (curry map: car) '([(1 a) (2 b)] [(3 c)]))
+      #;(check-equal?: (map: (curry map: (compose number->string add1))
+                             '((1 2 3) (4 5)))
+                       : (Listof (Listof String))
+                       '(("2" "3" "4") ("5" "6")))
+      
+      (check-equal?: (map: add1 '(1 2 3))
+                     : (Listof Number)
+                     '(2 3 4))
+      
+      (check-equal?: (map: car '((1 a) (2 b) (3 c)))
+                     : (Listof Number)
+                     '(1 2 3))
+      
+      (check-equal?: (map: (curry map car) '([(1 a) (2 b)] [(3 c)]))
                      : (Listof Number)
                      '((1 a) (3 c)))
-    
-    (check-equal?: (map: (curry map (curry map car))
-                         '([((1 a) (2 b)) ((3 c))] [((4))]))
-                   : (Listof (Listof (Listof Number)))
-                   '([(1 2) (3)] [(4)]))
-    #;(check-equal?: (map: (curry map (curry map: car))
+      #;(check-equal?: (map: (curry map: car) '([(1 a) (2 b)] [(3 c)]))
+                       : (Listof Number)
+                       '((1 a) (3 c)))
+      
+      (check-equal?: (map: (curry map (curry map car))
                            '([((1 a) (2 b)) ((3 c))] [((4))]))
                      : (Listof (Listof (Listof Number)))
                      '([(1 2) (3)] [(4)]))
-    #;(check-equal?: (map: (curry map: (curry map car))
-                           '([((1 a) (2 b)) ((3 c))] [((4))]))
-                     : (Listof (Listof (Listof Number)))
-                     '([(1 2) (3)] [(4)]))
-    #;(check-equal?: (map: (curry map: (curry map: car))
-                           '([((1 a) (2 b)) ((3 c))] [((4))]))
-                     : (Listof (Listof (Listof Number)))
-                     '([(1 2) (3)] [(4)])))
+      #;(check-equal?: (map: (curry map (curry map: car))
+                             '([((1 a) (2 b)) ((3 c))] [((4))]))
+                       : (Listof (Listof (Listof Number)))
+                       '([(1 2) (3)] [(4)]))
+      #;(check-equal?: (map: (curry map: (curry map car))
+                             '([((1 a) (2 b)) ((3 c))] [((4))]))
+                       : (Listof (Listof (Listof Number)))
+                       '([(1 2) (3)] [(4)]))
+      #;(check-equal?: (map: (curry map: (curry map: car))
+                             '([((1 a) (2 b)) ((3 c))] [((4))]))
+                       : (Listof (Listof (Listof Number)))
+                       '([(1 2) (3)] [(4)])))|#
   
   (check-equal?: (map: car '((1 b x) (2 c) (3 d)))
                  : (Listof Number)
@@ -427,3 +454,5 @@ EDIT: that's what we did, using the #:auto-in
 
 
 |#
+
+;|#
\ No newline at end of file
diff --git a/graph-lib/graph/map3.rkt b/graph-lib/graph/map3.rkt
new file mode 100644
index 00000000..b145432f
--- /dev/null
+++ b/graph-lib/graph/map3.rkt
@@ -0,0 +1,150 @@
+#lang typed/racket
+
+(require (for-syntax racket/syntax
+                     syntax/stx
+                     syntax/parse
+                     syntax/parse/experimental/template
+                     "../lib/low-untyped.rkt")
+         "../lib/low.rkt"
+         "graph4.lp2.rkt"
+         "../type-expander/type-expander.lp2.rkt")
+
+;; TODO: DEBUG
+(define-syntax (dbg stx)
+  (syntax-parse stx
+    [(_ (~optional (~and norun #:norun)) code)
+     (if (attribute norun)
+         #'(ann 'code Any)
+         #'code)]))
+
+(begin-for-syntax
+  (define-template-metafunction (apply-compose stx)
+    (syntax-parse stx
+      [(_ [] [a])
+       #'a]
+      [(_ [] [a …])
+       #'(values a …)]
+      [(_ [f … (~and loc (f-last x … (~literal _) y …))] [a …])
+       (quasitemplate
+        (apply-compose [f …] [#,(syntax/loc #'loc (f-last x … a … y …))]))]
+      [(_ [f … f-last] [a …])
+       (quasitemplate
+        (apply-compose [f …] [#,(syntax/loc #'f-last (f-last a …))]))])))
+
+(begin-for-syntax
+  (define-syntax-class fun-descriptor
+    (pattern [in:expr f-auto:expr out:expr]
+             #:with code (generate-temporary #'f-auto)
+             #:with (f-arg …) #'(f-auto)
+             #:with (f-param …) #'(code)
+             #:with (f-type …) #'[(→ in out)])
+    (pattern [in:expr
+              {[f-arg:expr f-param:id f-type:expr] …}
+              code:expr
+              out:expr])))
+
+(define-syntax (map0 stx)
+  (syntax-parse stx
+    [(_ (~optional (~and norun #:norun))
+        #:∀ {∀-T:id …} global-out:expr
+        :fun-descriptor …)
+     (define/with-syntax local-map (generate-temporary 'map))
+     (define/with-syntax lst (generate-temporary 'lst))
+     (define/with-syntax (_ … inner-in) #'(in …))
+     (define/with-syntax icons #'(inst cons global-out (Listof global-out)))
+     (quasitemplate
+      (dbg (?? norun)
+           (let ()
+             (: local-map (∀ (∀-T …) (→ f-type … …
+                                        (Listof inner-in)
+                                        (Listof global-out))))
+             (define (local-map f-param … … lst)
+               (if (null? lst)
+                   '()
+                   (icons (apply-compose [code …] [(car lst)])
+                          (local-map f-param … … (cdr lst)))))
+             local-map)))]))
+
+(define-syntax (call-map0 stx)
+  (syntax-parse stx
+    [(_ (~optional (~and norun #:norun))
+        l:expr #:∀ {∀-T:id …} global-out:expr d:fun-descriptor …)
+     (quasitemplate
+      (dbg (?? norun)
+           #,(syntax/loc stx
+               ((map0 #:∀ {∀-T …} global-out d …) d.f-arg … … l))))]))
+
+(call-map0 #:norun '((a 1) (b 2) (c 3))
+           #:∀ {O}
+           O
+           [(Pairof O Any) car O]
+           [(Pairof Any (Pairof O Any)) cdr (Pairof O Any)])
+
+(call-map0 #:norun '(1 2 3)
+           #:∀ {A B}
+           B
+           [A add1 B]
+           [A identity A])
+
+(call-map0 #:norun '(1 2 3)
+           #:∀ {A B}
+           B
+           [A add1 B]
+           [A identity A])
+
+(call-map0 '((1 2) (3)) #:∀ {A B}
+           (Listof B)
+           [(Listof A) {[add1 add1*1 (→ A B)]}
+                       (call-map0 _ #:∀ {A B} B [A add1*1 B])
+                       (Listof B)])
+
+(call-map0 '((1 2) (3)) #:∀ {A B C}
+           (Listof C)
+           [(Listof B) {[add1 add1*2 (→ B C)]}
+                       (call-map0 _ #:∀ {B C} C [B add1*2 C])
+                       (Listof C)]
+           [(Listof A) {[add1 add1*1 (→ A B)]}
+                       (call-map0 _ #:∀ {A B} B [A add1*1 B])
+                       (Listof B)])
+
+(call-map0 '((1 2) (3)) #:∀ {A Y B X C}
+           (Listof C)
+           [(Listof B) {[add1 add1*2 (→ B X)]
+                        [add1 add1*2b (→ X C)]}
+                       (call-map0 _ #:∀ {B X C} C
+                                  [X add1*2b C]
+                                  [B add1*2 X])
+                       (Listof C)]
+           [(Listof A) {[add1 add1*1 (→ A Y)]
+                        [add1 add1*1b (→ Y B)]}
+                       (call-map0 _ #:∀ {A Y B} B
+                                  [Y add1*1b B]
+                                  [A add1*1 Y])
+                       (Listof B)])
+
+(call-map0 '(([1 b] [2 c]) ([3 d])) #:∀ {A X C}
+           (Listof C)
+           [(Listof A) {[add1 add1*2 (→ A X)]
+                        [add1 add1*2b (→ X C)]}
+                       (call-map0 _ #:∀ {A X C} C
+                                  [X add1*2b C]
+                                  [A add1*2 X])
+                       (Listof C)]
+           [(Listof (Pairof A Any)) {}
+                                    (call-map0 _ #:∀ {A} A
+                                               [(Pairof A Any) car A])
+                                    (Listof A)])
+
+#;(call-map0 '(([1 b] [2 c]) ([3 d])) #:∀ {A X C}
+           (Listof C)
+           [(Listof (Pairof A Any))
+            {[add1 add1*2b (→ A C)]}
+            (call-map0 _ #:∀ {A C} C
+                       [A add1*2b C]
+                       [(Pairof A Any) car A])
+            (Listof C)]
+           [(Listof (Pairof (Pairof A) Any))
+            {}
+            (call-map0 _ #:∀ {A} A
+                       [(Pairof (Pairof A Any) Any) car A])
+            (Listof (Pairof A Any))])
\ No newline at end of file
diff --git a/graph-lib/graph/map4.rkt b/graph-lib/graph/map4.rkt
new file mode 100644
index 00000000..a271b9d6
--- /dev/null
+++ b/graph-lib/graph/map4.rkt
@@ -0,0 +1,72 @@
+#lang typed/racket
+
+(require (for-syntax racket/syntax
+                     syntax/stx
+                     syntax/parse
+                     syntax/parse/experimental/template
+                     "../lib/low-untyped.rkt")
+         "../lib/low.rkt"
+         "graph4.lp2.rkt"
+         "../type-expander/type-expander.lp2.rkt")
+
+(begin-for-syntax
+  (define-syntax-class >0
+    (pattern v #:when (exact-positive-integer? (syntax-e #'v)))))
+
+(begin-for-syntax
+  (define-syntax-class ≥0
+    (pattern v #:when (exact-integer? (syntax-e #'v)))))
+
+(define-type-expander (Deep-Listof stx)
+  (syntax-parse stx
+    [(_ 0 T)
+     #'T]
+    [(_ d:>0 T)
+     #`(Listof (Deep-Listof #,(sub1 (syntax-e #'d)) T))]))
+
+(define-syntax (λdeep-map stx)
+  (syntax-parse stx
+    [(_ {∀-type:id …} A:expr B:expr 0)
+     #'(ann (λ (f x) (f x))
+            (∀ (∀-type …) (→ (→ A B) A B)))]
+    [(_ {∀-type:id …} A:expr B:expr d:exact-integer)
+     (define/with-syntax local-map (generate-temporary #'map))
+     #`(let ()
+         (: local-map (∀ (∀-type …) (→ (→ A B)
+                                       (Deep-Listof d A)
+                                       (Deep-Listof d B))))
+         (define (local-map f l)
+           (if (null? l)
+               '()
+               (cons ((λdeep-map {∀-type …} A B #,(sub1 (syntax-e #'d)))
+                      f (car l))
+                     (local-map f (cdr l)))))
+         local-map)]))
+
+(module+ test
+  (check-equal?: ((λdeep-map {A B} A B 3) add1 '([{1} {2 3}] [{4}]))
+                 : (Listof (Listof (Listof Number)))
+                 '([{2} {3 4}] [{5}])))
+
+#|
+(define-syntax (deep-map stx)
+  (syntax-parse stx
+    [(_ d:≥0 f:expr l:expr)
+     (syntax/loc #'f ((λdeep-map d) f l))]))
+
+(deep-map 3 add1 '([{1} {2 3}] [{4}]))
+
+;; Now we turn all map: calls into the form
+;; (compose-maps [(d f) …] [l …])
+
+(define-syntax (compose-maps stx)
+  (syntax-parse stx
+    [(_ [] [l])
+     #'l]
+    [(_ [] [l:expr …])
+     #'(values l …)]
+    [(_ [(d:≥0 f:expr) (d-rest:≥0 f-rest:expr) …] [l:expr …])
+     #'(deep-map d f (compose-maps [(d-rest f-rest) …] [l …]))]))
+
+(compose-maps [(3 add1) (3 add1)] ['([{1} {2 3}] [{4}])])
+|#
\ No newline at end of file
diff --git a/graph-lib/type-expander/type-expander.lp2.rkt b/graph-lib/type-expander/type-expander.lp2.rkt
index a4af93e9..b9fe1b31 100644
--- a/graph-lib/type-expander/type-expander.lp2.rkt
+++ b/graph-lib/type-expander/type-expander.lp2.rkt
@@ -91,7 +91,8 @@ else.
          (let ([def-ctx (syntax-local-make-definition-context)]
                [err-expr #'(λ _ (raise-syntax-error
                                  "Type name used out of context"))])
-           (for ([var (syntax->list type-vars)])
+           (for ([var (syntax-parse type-vars
+                        [(v:id …) (syntax->list #'(v …))])])
              (syntax-local-bind-syntaxes (list var) err-expr def-ctx))
            (internal-definition-context-seal def-ctx)
            (internal-definition-context-introduce def-ctx stx)))]
@@ -121,9 +122,9 @@ else.
            [(((~literal curry) T Arg1 …) . Args2)
             (expand-type #'(T Arg1 … . Args2))]
            ;; TODO: handle the pattern (∀ (TVar ... ooo) T)
-           [(∀:fa (TVar ...) T)
+           [(∀:fa (TVar:id ...) T:expr)
             #`(∀ (TVar ...) #,(expand-type (bind-type-vars #'(TVar ...) #'T)))]
-           [((~literal Rec) R T)
+           [((~literal Rec) R:id T:expr)
             #`(Rec R #,(expand-type (bind-type-vars #'(R) #'T)))]
            [((~literal quote) T) (expand-quasiquote 'quote 1 #'T)]
            [((~literal quasiquote) T) (expand-quasiquote 'quasiquote 1 #'T)]
@@ -309,7 +310,7 @@ variables in the result, we define two template metafunctions:
        (define-template-metafunction (tmpl-expand-type stx)
          (syntax-parse stx
            [(_ () t) (expand-type #'t)]
-           [(_ tvars t) (expand-type (bind-type-vars #'tvars #'t))]))]
+           [(_ (tvar …) t) (expand-type (bind-type-vars #'(tvar …) #'t))]))]
 
 @subsection{@racket[:]}