From 0e1a8484653110af2ab14ac6982f1239b6cb9c90 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 20 Jul 2015 18:03:33 -0400
Subject: [PATCH] add fsub test; typecheck? needs to call current-promote

---
 tapl/tests/fsub-tests.rkt |  4 ++++
 tapl/typecheck.rkt        | 15 +++++++++++++--
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
index f2f15a7..046c5f9 100644
--- a/tapl/tests/fsub-tests.rkt
+++ b/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])
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index d919a5f..ebb44ac 100644
--- a/tapl/typecheck.rkt
+++ b/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))