diff --git a/stlc-tests.rkt b/stlc-tests.rkt
index 7e5f556..4c121a8 100644
--- a/stlc-tests.rkt
+++ b/stlc-tests.rkt
@@ -6,19 +6,19 @@
 (check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
 
 ; check fns with literal or id bodies
-(check-type (λ ([x : Int]) x) : (→ Int Int))
-(check-type (λ ([x : Unit] [y : Int]) x y) : (→ Unit Int Int))
+(check-type (λ ([x : Int]) x) : (Int → Int))
+(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
 
 ;; check fns with multi-expr body
-(check-type (λ ([x : Int]) (void) x) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) x) : (Int → Int))
 (check-type-error (λ ([x : Int]) 1 x))
-(check-type (λ ([x : Int]) (void) (void) x) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
 
 ; HO fn
-(check-type-and-result ((λ ([f : (→ Int Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
-(check-type (λ ([f : (→ Int Int)]) (f 10)) : (→ (→ Int Int) Int))
-(check-type (λ ([f : (→ Int Int)]) (λ ([x : Int]) (f (f x)))) : (→ (→ Int Int) (→ Int Int)))
-(check-type-error (λ (f : (→ Int Int)) (λ (x : String) (f (f x)))))
+(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
+(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
+(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
+(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
 
 ;; shadowed var
 (check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
@@ -55,10 +55,10 @@
 (check-type-and-result (begin (+ 1 2)) : Int => 3)
 (check-type-error (begin 1 2))
 
-(check-type (λ ([x : Int]) (void) (+ x 1)) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
 (check-type-error (λ ([x : Int]) 1 1))
-(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (→ Int Int Int))
-(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a b c)) 1 2 3)
+(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
+(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
                        : Int => 6)
 
 ; define
@@ -81,7 +81,7 @@
 ;;; recursive fn
 (define (add1 [x : Int]) : Int
   (+ x 1))
-(define (map [f : (→ Int Int)] [lst : (Listof Int)]) : (Listof Int)
+(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
   (if (null? {Int} lst)
       (null {Int})
       (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
@@ -119,7 +119,7 @@
 (check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
 (check-type-error (Cons "one" (Null)))
 (check-type-error (Cons 1 2))
-(define (map/IntList [f : (→ Int Int)] [lst : IntList]) : IntList
+(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
   (cases lst
     [Null () (Null)]
     [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
@@ -129,7 +129,7 @@
                        : IntList => (Cons 3 (Cons 2 (Null))))
 (check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
 (define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-(define (map/BoolList [f : (→ Bool Int)] [lst : BoolList]) : IntList
+(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
   (cases lst
     [BoolNull () (Null)]
     [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
@@ -143,7 +143,7 @@
               (cases lst
                 [Null () (None)]
                 [Cons (x xs) (Just x)]))
-            : (→ IntList MaybeInt))
+            : (IntList → MaybeInt))
 (check-type ((λ ([lst : IntList]) 
               (cases lst
                 [Null () (None)]
diff --git a/stlc.rkt b/stlc.rkt
index 3039487..c66785c 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -39,12 +39,12 @@
   (syntax-parse stx #:datum-literals (variant)
     [(_ τ:id (variant (Cons:id τ_fld ...) ...))
      #:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
-     #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)] ...)))
+     #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)] ...)))
      #'(begin
          (struct Cons (x ...) #:transparent) ...)]
     [(_ τ:id (Cons:id τ_fld ...))
      #:with (x ...) (generate-temporaries #'(τ_fld ...))
-     #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)])))
+     #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
      #'(begin 
          (struct Cons (x ...) #:transparent))]))
 (define-syntax (cases stx)
@@ -52,7 +52,7 @@
     [(_ e [Cons (x ...) body ... body_result] ...)
      #:with e+ (expand/df #'e)
      #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
-     #:with ((→ τ ... τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
+     #:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
      #:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
      #:with ((lam (x+ ...) body+ ... body_result+) ...) 
             (stx-map (λ (bods xs τs) 
@@ -91,9 +91,9 @@
   (syntax-parse stx
     [(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
 
-(define-syntax (define-prim stx)
-  (syntax-parse stx
-    [(_ op τ_arg τ_res)
+(define-syntax (define-primop stx)
+  (syntax-parse stx #:datum-literals (:) #:literals (→)
+    [(_ op:id : (τ_arg ... → τ_result))
      #:with op/tc (format-id #'op "~a/tc" #'op)
      #'(begin
          (provide (rename-out [op/tc op]))
@@ -101,17 +101,20 @@
            (syntax-parse stx
              [f:id #'op] ; HO case
              [(_ e (... ...))
-              #:with (e+ (... ...)) (stx-map expand/df #'(e (... ...)))
-              #:when (stx-andmap (λ (τ) (assert-type τ τ_arg)) #'(e+ (... ...)))
-              (⊢ (syntax/loc stx (op e+ (... ...))) τ_res)])))]))
-(define-prim + #'Int #'Int)
-(define-prim - #'Int #'Int)
-(define-prim = #'Int #'Bool)
-(define-prim < #'Int #'Bool)
-(define-prim not #'Bool #'Bool)
-(define-prim or #'Bool #'Bool)
-(define-prim and #'Bool #'Bool)
-(define-prim abs #'Int #'Int)
+              #:with es+ (stx-map expand/df #'(e (... ...))) 
+              #:with τs #'(τ_arg ...)
+              #:fail-unless (= (stx-length #'es+) (stx-length #'τs))
+                            "Wrong number of arguments"
+              #:when (stx-andmap assert-type #'es+ #'τs)
+              (⊢ (quasisyntax/loc stx (op . es+)) #'τ_result)])))]))
+(define-primop + : (Int Int → Int))
+(define-primop - : (Int Int → Int))
+(define-primop = : (Int Int → Bool))
+(define-primop < : (Int Int → Bool))
+(define-primop or : (Bool Bool → Bool))
+(define-primop and : (Bool Bool → Bool))
+(define-primop not : (Bool → Bool))
+(define-primop abs : (Int → Int))
 
 
 (define-syntax (λ/tc stx)
@@ -133,7 +136,7 @@
      ;; manually handle the implicit begin
      #:when (stx-map assert-Unit-type #'(e++ ...))
      #:with τ_body (typeof #'e_result++)
-     (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(→ τ ... τ_body))]))
+     (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(τ ... → τ_body))]))
 
 (define-syntax (let/tc stx)
   (syntax-parse stx #:datum-literals (:)
@@ -153,7 +156,7 @@
     [(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
     [(_ e_fn e_arg ...)
      #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
-     #:with (→ τ ... τ_res) (typeof #'e_fn+)
+     #:with (τ ... → τ_res) (typeof #'e_fn+)
      #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
      (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
 
@@ -210,7 +213,7 @@
 (define-syntax (define/tc stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ (f:id [x:id : τ] ...) : τ_result e ...)
-     #:when (Γ (type-env-extend #'([f (→ τ ... τ_result)])))
+     #:when (Γ (type-env-extend #'([f (τ ... → τ_result)])))
      #'(define f (λ/tc ([x : τ] ...) e ...))]
     [(_ x:id e) #'(define x e)]))
 
@@ -281,7 +284,7 @@
      #:with (v ...) #'(deffn+.rhs ...)
      #:with (e ...) (template ((?@ . mb-form.e) ...))
      ;; base type env
-     #:when (Γ (type-env-extend #'((+ (→ Int Int Int)))))
+     #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
 ;; NOTE: for struct def, define-values *must* come before define-syntaxes
 ;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
      (quasisyntax/loc stx 
diff --git a/stx-utils.rkt b/stx-utils.rkt
index 551555d..509b5da 100644
--- a/stx-utils.rkt
+++ b/stx-utils.rkt
@@ -11,4 +11,5 @@
   (define paren-prop (syntax-property stx 'paren-shape))
   (and paren-prop (char=? #\{ paren-prop)))
 (define (stx-member v stx)
-  (member v (syntax->list stx) free-identifier=?))
\ No newline at end of file
+  (member v (syntax->list stx) free-identifier=?))
+(define (stx-length stx) (length (syntax->list stx)))
\ No newline at end of file
diff --git a/sysf-tests.rkt b/sysf-tests.rkt
index 4a07600..ede0883 100644
--- a/sysf-tests.rkt
+++ b/sysf-tests.rkt
@@ -6,14 +6,14 @@
 (check-type (Just {Int} 1) : (Maybe Int))
 (check-type-error (Just {Int} #f))
 (check-not-type (Just {Int} 1) : (Maybe Bool))
-(check-type (λ {X} ([x : X]) x) : (∀ (X) (→ X X)))
+(check-type (λ {X} ([x : X]) x) : (∀ (X) (X → X)))
 (check-type-error ((λ ([x : X]) x) 1))
 
 ;; lists
 (define-type (MyList X) (variant (Null) (Cons X (MyList X))))
 (check-type (Null {Int}) : (MyList Int))
 (check-type (Cons {Int} 1 (Null {Int})) : (MyList Int))
-(define (map/List {A B} [f : (→ A B)] [lst : (MyList A)]) : (MyList B)
+(define (map/List {A B} [f : (A → B)] [lst : (MyList A)]) : (MyList B)
   (cases {A} lst
     [Null () (Null {B})]
     [Cons (x xs) (Cons {B} (f {A B} x) (map/List {A B} f xs))]))
@@ -36,7 +36,7 @@
 (check-type-error (list {Int} 1 2 #f))
 (check-type-error (list {Bool} 1 2 3))
 ;; map
-(define (map {A B} [f : (→ A B)] [lst : (Listof A)]) : (Listof B)
+(define (map {A B} [f : (A → B)] [lst : (Listof A)]) : (Listof B)
   (if (null? {A} lst)
       (null {B})
       (cons {B} (f {A B} (first {A} lst)) (map {A B} f (rest {A} lst)))))
@@ -50,7 +50,7 @@
 (define-type Queen (Q Int Int))
 
 ;; filter
-(define (filter {A} [p? : (→ A Bool)] [lst : (Listof A)]) : (Listof A)
+(define (filter {A} [p? : (A → Bool)] [lst : (Listof A)]) : (Listof A)
   (if (null? {A} lst)
       (null {A})
       (let ([x (first {A} lst)])
@@ -63,7 +63,7 @@
  : (Listof Int) => (list {Int} 1 2 3 4 6 7))
 
 ;; foldr
-(define (foldr {A B} [f : (→ A B B)] [base : B] [lst : (Listof A)]) : B
+(define (foldr {A B} [f : (A B → B)] [base : B] [lst : (Listof A)]) : B
   (if (null? {A} lst)
       base
       (f (first {A} lst) (foldr {A B} f base (rest {A} lst)))))
@@ -71,7 +71,7 @@
 (check-type-and-result (foldr {Int Int} + 0 (build-list {Int} add1 4)) : Int => 10)
 
 ;; foldl
-(define (foldl {A B} [f : (→ A B B)] [acc : B] [lst : (Listof A)]) : B
+(define (foldl {A B} [f : (A B → B)] [acc : B] [lst : (Listof A)]) : B
   (if (null? {A} lst)
       acc
       (foldl {A B} f (f (first {A} lst) acc) (rest {A} lst))))
@@ -90,7 +90,7 @@
 (check-type-error (tails {Int} (list {Bool} 1 2 3)))
 (check-not-type (tails {Int} (list {Int} 1 2 3)) : (Listof Int))
 
-(define (andmap {A} [f : (→ A Bool)] [lst : (Listof A)]) : Bool
+(define (andmap {A} [f : (A → Bool)] [lst : (Listof A)]) : Bool
   (if (null? {A} lst)
       #t
       (and (f (first {A} lst)) (andmap {A} f (rest {A} lst)))))
@@ -112,16 +112,16 @@
       (let ([q1 (first {Queen} lst)])
         (andmap {Queen} (λ ([q2 : Queen]) (safe? q1 q2)) (rest {Queen} lst)))))
 
-(check-type safe/list? : (→ (Listof Queen) Bool))
+(check-type safe/list? : ((Listof Queen) → Bool))
 
 (define (valid? [lst : (Listof Queen)]) : Bool
   (andmap {(Listof Queen)} safe/list? (tails {Queen} lst)))
 
-(define (build-list-help {A} [f : (→ Int A)] [n : Int] [m : Int]) : (Listof A)
+(define (build-list-help {A} [f : (Int → A)] [n : Int] [m : Int]) : (Listof A)
   (if (= n m)
       (null {A})
       (cons {A} (f {A} n) (build-list-help {A} f (add1 n) m))))
-(define (build-list {A} [f : (→ Int A)] [n : Int]) : (Listof A)
+(define (build-list {A} [f : (Int → A)] [n : Int]) : (Listof A)
   (build-list-help {A} f 0 n))
 
 (check-type-and-result (build-list {Int} add1 8)
@@ -163,9 +163,9 @@
 
 ;; testing for variable capture
 (define (polyf {X} [x : X]) : X x)
-(check-type polyf : (∀ (X) (→ X X)))
-(define (polyf2 {X} [x : X]) : (∀ (X) (→ X X)) polyf)
-(check-type polyf2 : (∀ (X) (→ X (∀ (X) (→ X X)))))
+(check-type polyf : (∀ (X) (X → X)))
+(define (polyf2 {X} [x : X]) : (∀ (X) (X → X)) polyf)
+(check-type polyf2 : (∀ (X) (X → (∀ (X) (X → X)))))
 
 ;; the following test fails bc X gets captured (2014-08-18)
 ;; - 2014-08-20: fixed
@@ -177,21 +177,21 @@
 ;;    capture is not ok when forall is applied to non-base types, ie →
 ;;    (see test below)
 ;; - 2014-08-20: fixed by implementing manual subst
-(check-type (inst polyf2 Int) : (→ Int (∀ (X) (→ X X))))
+(check-type (inst polyf2 Int) : (Int → (∀ (X) (X → X))))
 ;; the following test "fails" bc forall is nested
 ;; - Typed Racket has same behavior, so ok
 (check-type-error (inst (inst polyf2 Int) Bool))
 (check-type-error ((inst polyf2 Int) #f))
 ;; again, the following example has type (∀ (Int) (→ Int Int)), which is ok
 ;; - 2014-08-20: fixed by impl manual subst
-(check-type ((inst polyf2 Int) 1) : (∀ (X) (→ X X)))
-(check-type (inst ((inst polyf2 Int) 1) Bool) : (→ Bool Bool))
+(check-type ((inst polyf2 Int) 1) : (∀ (X) (X → X)))
+(check-type (inst ((inst polyf2 Int) 1) Bool) : (Bool → Bool))
 ;; test same example with type-instantiating apply instead of inst
-(check-type (polyf2 {Int} 1) : (∀ (Y) (→ Y Y)))
+(check-type (polyf2 {Int} 1) : (∀ (Y) (Y → Y)))
 (check-type-error (polyf2 {Int} #f))
 (check-type-and-result ((polyf2 {Int} 1) {Bool} #f) : Bool => #f)
 (check-type-error ((polyf2 {Int} 1) {Bool} 2))
 
-(check-type (inst polyf (→ Int Int)) : (→ (→ Int Int) (→ Int Int)))
+(check-type (inst polyf (Int → Int)) : ((Int → Int) → (Int → Int)))
 ;; the follow test fails because the binder is renamed to (→ Int Int)
-(check-type (inst polyf2 (→ Int Int)) : (→ (→ Int Int) (∀ (X) (→ X X))))
\ No newline at end of file
+(check-type (inst polyf2 (Int → Int)) : ((Int → Int) → (∀ (X) (X → X))))
\ No newline at end of file
diff --git a/sysf.rkt b/sysf.rkt
index 5a14503..c91fb3f 100644
--- a/sysf.rkt
+++ b/sysf.rkt
@@ -54,7 +54,7 @@
   (syntax-parse stx #:datum-literals (variant)
     [(_ (Tycon:id X:id ...) (variant (Cons:id τ_fld ...) ...))
      #:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
-     #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (→ τ_fld ... (Tycon X ...)))] ...)))
+     #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (τ_fld ... → (Tycon X ...)))] ...)))
      #'(begin ; should be racket begin
          (struct Cons (x ...) #:transparent) ...)]
     [(_ any ...) #'(stlc:define-type any ...)]))
@@ -76,12 +76,12 @@
 
 ;; cases ----------------------------------------------------------------------
 (define-syntax (cases stx)
-  (syntax-parse stx #:literals (∀)
+  (syntax-parse stx #:literals (∀ →)
     [(_ τs:inst-τs e [Cons (x ...) body ... body_result] ...)
      #:with e+ (expand/df #'e)
      #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
      #:with (τ_Cons:∀τ ...) (stx-map typeof #'(Cons+ ...))
-     #:with ((→ τ ... τ_res) ...) 
+     #:with ((τ ... → τ_res) ...) 
             (stx-map (λ (∀τ) (apply-forall ∀τ #'τs)) #'(τ_Cons ...))
      ;; check constructor type in every branch matches expr being matched
      #:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_res ...))
@@ -124,7 +124,7 @@
      ;; manually typecheck the implicit begin
      #:when (stx-map assert-Unit-type #'(e++ ...))
      #:with τ_body (typeof #'e_result++)
-     (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (→ τ ... τ_body)))]
+     (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (τ ... → τ_body)))]
     [(_ any ...) #'(stlc:λ any ...)]))
 
 ; define ----------------------------------------------------------------------
@@ -133,7 +133,7 @@
     ;; most of the code from this case, except for the curly? check,
     ;; is copied from stlc:define
     [(_ (f:id tvs:tyvars [x:id : τ] ...) : τ_result e ...)
-     #:when (Γ (type-env-extend #'([f (∀ tvs (→ τ ... τ_result))])))
+     #:when (Γ (type-env-extend #'([f (∀ tvs (τ ... → τ_result))])))
      #'(define f (λ/tc tvs ([x : τ] ...) e ...))]
     [(_ any ...) #'(stlc:define any ...)]))
 
@@ -146,7 +146,7 @@
     [(_ e_fn τs:inst-τs e_arg ...)
      #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
      #:with τ_fn:∀τ (typeof #'e_fn+)
-     #:with (→ τ_arg ... τ_res) (apply-forall #'τ_fn #'τs)
+     #:with (τ_arg ... → τ_res) (apply-forall #'τ_fn #'τs)
      #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
      (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
     ;; handle type apply of non-poly fn here; just pass through
diff --git a/typecheck.rkt b/typecheck.rkt
index 81c4b68..f5aab2a 100644
--- a/typecheck.rkt
+++ b/typecheck.rkt
@@ -26,7 +26,7 @@
 
 (define-for-syntax (type=? τ1 τ2)
 ;  (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
-  (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
+  (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀ →)
     [(x:id y:id) (free-identifier=? τ1 τ2)]
     [(∀τ1 ∀τ2)
      #:with (∀ τvars1 τ_body1) #'∀τ1 
@@ -40,6 +40,9 @@
      (and (= (length (syntax->list #'τvars1))
              (length (syntax->list #'τvars2)))
           (type=? (apply-forall #'∀τ1 #'fresh-τvars) (apply-forall #'∀τ2 #'fresh-τvars)))]
+    [((τ_arg1 ... → τ_result1) (τ_arg2 ... → τ_result2))
+     (and (= (length (syntax->list #'(τ_arg1 ...))) (length (syntax->list #'(τ_arg2 ...))))
+          (type=? #'τ_result1 #'τ_result2))]
     [((tycon1:id τ1 ...) (tycon2:id τ2 ...)) 
      (and (free-identifier=? #'tycon1 #'tycon2)
           (= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
@@ -91,7 +94,7 @@
 
 ;; apply-forall ---------------------------------------------------------------
 (define-for-syntax (subst x τ mainτ)
-  (syntax-parse mainτ #:datum-literals (∀)
+  (syntax-parse mainτ #:datum-literals (∀ →)
     [y:id
      #:when (free-identifier=? #'y x)
      τ]
@@ -104,6 +107,12 @@
      #:with (∀ tyvars τbody) #'∀τ
      #:when (not (stx-member x #'tyvars))
      #`(∀ tyvars #,(subst x τ #'τbody))]
+    ;; need the ~and because for the result, I need to use the → literal 
+    ;; from the context of the input, and not the context here
+    [(τ_arg ... (~and (~datum →) arrow) τ_result)
+     #:with (τ_arg/subst ... τ_result/subst) 
+            (stx-map (curry subst x τ) #'(τ_arg ... τ_result))
+      #'(τ_arg/subst ... arrow τ_result/subst)]
     [(tycon:id τarg ...)
      #:with (τarg/subst ...) (stx-map (curry subst x τ) #'(τarg ...))
      #'(tycon τarg/subst ...)]))