add fsub test; typecheck? needs to call current-promote

tapl/tests/fsub-tests.rkt

@@ -25,6 +25,10 @@
 (check-type (f2 ra) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
 (check-type (f2 rab) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
 
+;; define-primop (actually #%app) needs to call current-promote
+(define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
+(check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
+
 (define f2poly
   (Λ ([X <: (× [: "a" Nat])])
      (λ ([x : X])

tapl/typecheck.rkt

@@ -166,12 +166,20 @@
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with (e ...) es
        #:with
+       ; old expander pattern
        ((~literal #%plain-lambda) tvs+
         ((~literal #%expression)
          ((~literal #%plain-lambda) xs+
           ((~literal letrec-syntaxes+values) stxs1 ()
             ((~literal letrec-syntaxes+values) stxs2 ()
               ((~literal #%expression) e+) ...)))))
+       ; new expander pattern
+       #;((~literal #%plain-lambda) tvs+
+        ((~literal #%expression)
+         ((~literal #%plain-lambda) xs+
+          ((~literal let-values) ()
+            ((~literal let-values) ()
+              ((~literal #%expression) e+) ...)))))
        (expand/df
         #`(λ #,tvs
             (λ (x ...)
@@ -182,10 +190,13 @@
       [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
 
   (define current-typecheck-relation (make-parameter #f))
-  (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
+  (define (typecheck? t1 t2)
+    ((current-typecheck-relation)
+     ((current-promote) t1)
+     ((current-promote) t2)))
   (define (typechecks? τs1 τs2)
     (and (= (stx-length τs1) (stx-length τs2))
-         (stx-andmap (current-typecheck-relation) τs1 τs2)))
+         (stx-andmap typecheck? τs1 τs2)))
   
   (define current-type-eval (make-parameter #f))