From 830b72f602510a5ec4c9a7c09c1ec2c4dffc9284 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 17 Mar 2021 21:38:46 -0400
Subject: [PATCH 01/13] WIP bounded polymorphism

---
 .../typed-racket/infer/infer-unit.rkt         | 47 ++++++-----
 .../typed-racket/infer/signatures.rkt         |  6 +-
 .../typed-racket/private/parse-type.rkt       | 16 +++-
 .../typed-racket/rep/type-rep.rkt             | 77 +++++++++++++++----
 .../typed-racket/typecheck/tc-funapp.rkt      |  5 +-
 .../typed-racket/typecheck/tc-lambda-unit.rkt |  1 +
 .../typed-racket/types/subtype.rkt            | 17 +++-
 7 files changed, 129 insertions(+), 40 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index da1db939b..b2c0cdf9d 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -48,36 +48,37 @@
 (define-struct/cond-contract context
   ([bounds (listof symbol?)]
    [vars (listof symbol?)]
-   [indices (listof symbol?)]) #:transparent)
+   [indices (listof symbol?)]
+   [type-bounds (hash/c symbol? Type?)]) #:transparent)
 
 (define (context-add-vars ctx vars)
   (match ctx
-    [(context V X Y)
-     (context V (append vars X) Y)]))
+    [(context V X Y TB)
+     (context V (append vars X) Y TB)]))
 
 (define (context-add-var ctx var)
   (match ctx
-    [(context V X Y)
-     (context V (cons var X) Y)]))
+    [(context V X Y TB)
+     (context V (cons var X) Y TB)]))
 
 (define (context-add ctx #:bounds [bounds empty] #:vars [vars empty] #:indices [indices empty])
   (match ctx
-    [(context V X Y)
-     (context (append bounds V) (append vars X) (append indices Y))]))
+    [(context V X Y TB)
+     (context (append bounds V) (append vars X) (append indices Y) TB)]))
 
 (define (inferable-index? ctx bound)
   (match ctx
-    [(context _ _ Y)
+    [(context _ _ Y TB)
      (memq bound Y)]))
 
 (define ((inferable-var? ctx) var)
   (match ctx
-    [(context _ X _)
+    [(context _ X _ TB)
      (memq var X)]))
 
 (define (empty-cset/context ctx)
   (match ctx
-    [(context _ X Y)
+    [(context _ X Y TB)
      (empty-cset X Y)]))
 
 
@@ -474,7 +475,7 @@
 ;; produces a cset which determines a substitution that makes S a subtype of T
 ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
 ;; the index variables from the TOPLAS paper
-(define/cond-contract (cgen context S T [obj #f])
+(define/cond-contract (cgen context S T [obj #f] [bound #f])
   (->* (context? (or/c Values/c ValuesDots? AnyValues?)
                  (or/c Values/c ValuesDots? AnyValues?))
        ((or/c #f OptObject?))
@@ -483,7 +484,7 @@
   (define/cond-contract (cg S T [obj #f])
    (->* (Type? Type?) ((or/c #f OptObject?))
         (or/c #f cset?))
-   (cgen context S T obj))
+   (cgen context S T obj bound))
   (define/cond-contract (cg/inv S T)
    (Type? Type? . -> . (or/c #f cset?))
    (cgen/inv context S T))
@@ -576,7 +577,10 @@
            [_ #f])
          #f
          ;; constrain v to be below T (but don't mention bounds)
-         (singleton -Bottom v (var-demote T (context-bounds context)))]
+         (eprintf "hi...........~a ~n" v)
+         (if (subtype (hash-ref (context-type-bounds context) v) T obj)
+             (singleton -Bottom v (var-demote T (context-bounds context)))
+             #f)]
 
         [(S (F: (? (inferable-var? context) v)))
          #:return-when
@@ -584,8 +588,11 @@
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
+         (eprintf "bye...........~a ~a <: ~a ~n" v S (hash-ref (context-type-bounds context) v))
          ;; constrain v to be above S (but don't mention bounds)
-         (singleton (var-promote S (context-bounds context)) v Univ)]
+         (if (subtype S (hash-ref (context-type-bounds context) v) obj)
+             (singleton (var-promote S (context-bounds context)) v (hash-ref (context-type-bounds context) v))
+             #f)]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))
@@ -1003,17 +1010,19 @@
  (let ()
    (define/cond-contract (infer X Y S T R [expected #f]
                                 #:multiple? [multiple-substitutions? #f]
+                                #:bounds [bounds '#()]
                                 #:objs [objs '()])
      (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
        (or/c #f Values/c AnyValues? ValuesDots?))
       ((or/c #f Values/c AnyValues? ValuesDots?)
        #:multiple? boolean?
+       #:bounds (hash/c symbol? Type?)
        #:objs (listof OptObject?))
       . ->* . (or/c boolean?
                     substitution/c
                     (cons/c substitution/c
                             (listof substitution/c))))
-     (define ctx (context null X Y))
+     (define ctx (context null X Y bounds))
      (define expected-cset
        (if expected
            (cgen ctx R expected)
@@ -1030,7 +1039,8 @@
 
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X Y S T T-var R [expected #f]
-                      #:objs [objs '()])
+                      #:objs [objs '()]
+                      #:bounds [bounds '#hash()])
   (and ((length S) . >= . (length T))
        (let* ([fewer-ts (- (length S) (length T))]
               [new-T (match T-var
@@ -1040,7 +1050,8 @@
                         (append T (repeat-list rst-ts
                                                (quotient fewer-ts (length rst-ts))))]
                        [_ T])])
-         (infer X Y S new-T R expected #:objs objs))))
+         (infer X Y S new-T R expected #:objs objs
+                #:bounds bounds))))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
@@ -1055,7 +1066,7 @@
      (generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
    (define (subst t)
      (substitute-dots (map make-F new-vars) #f dotted-var t))
-   (define ctx (context null (append new-vars X) (list dotted-var)))
+   (define ctx (context null (append new-vars X) (list dotted-var) '#hash()))
 
    (define expected-cset (if expected
                              (cgen ctx (subst R) expected)
diff --git a/typed-racket-lib/typed-racket/infer/signatures.rkt b/typed-racket-lib/typed-racket/infer/signatures.rkt
index b0ab755e8..4d35e7580 100644
--- a/typed-racket-lib/typed-racket/infer/signatures.rkt
+++ b/typed-racket-lib/typed-racket/infer/signatures.rkt
@@ -39,7 +39,8 @@
                            ((or/c #f Values/c AnyValues? ValuesDots?)
                             ;; optional multiple substitutions?
                             #:multiple? boolean?
-                            #:objs (listof OptObject?))
+                            #:objs (listof OptObject?)
+                            #:bounds (hash/c symbol? Type?))
                            . ->* . any)]
    [cond-contracted infer/vararg ((;; variables from the forall
                                    (listof symbol?)
@@ -55,7 +56,8 @@
                                    (or/c #f Values/c AnyValues? ValuesDots?))
                                   ;; [optional] expected type
                                   ((or/c #f Values/c AnyValues? ValuesDots?)
-                                   #:objs (listof OptObject?))
+                                   #:objs (listof OptObject?)
+                                   #:bounds (hash/c symbol? Type?))
                                   . ->* . any)]
    [cond-contracted infer/dots (((listof symbol?)
                                  symbol?
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 64a7412da..1e922a167 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -193,6 +193,9 @@
            (parse-literal-alls #'t.type))]
     [_ null]))
 
+(define-syntax-class maybe-bounded
+  #:datum-literals (<:)
+  (pattern (name:id <: bound:id)))
 
 ;; Syntax -> Type
 ;; Parse a Forall type
@@ -215,7 +218,18 @@
                     "variable" (syntax-e maybe-dup)))
      (let* ([vars (stx-map syntax-e #'(vars ...))])
        (extend-tvars vars
-         (make-Poly vars (parse-type #'t.type))))]
+                     (make-Poly vars (parse-type #'t.type))))]
+    [(:All^ (vars:maybe-bounded ...) . t:omit-parens)
+     (define maybe-dup (check-duplicate-identifier (attribute vars.name)))
+     (when maybe-dup
+       (parse-error "duplicate type variable"
+                    "variable" (syntax-e maybe-dup)))
+     (define bounds (for/hash ([i (stx-map syntax-e (attribute vars.name))]
+                               [j (attribute vars.bound)])
+                      (values i (parse-type j))))
+     (let* ([vars (stx-map syntax-e (attribute vars.name))])
+       (extend-tvars vars
+                     (make-Poly vars (parse-type #'t.type) #:bounds bounds)))]
     ;; Next two are row polymorphic cases
     [(:All^ (var:id #:row) . t:omit-parens)
      (add-disappeared-use #'kw)
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 257eb1523..34cd81be2 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -46,6 +46,9 @@
          PolyDots-unsafe:
          Mu? Poly? PolyDots? PolyRow?
          Poly-n
+         F-n
+         F-bound
+         F?
          PolyDots-n
          Class? Row? Row:
          free-vars*
@@ -84,6 +87,8 @@
                      [PolyDots:* PolyDots:]
                      [PolyRow:* PolyRow:]
                      [Mu* make-Mu]
+                     [F* make-F]
+                     [F:* F:]
                      [make-Mu unsafe-make-Mu]
                      [Poly* make-Poly]
                      [PolyDots* make-PolyDots]
@@ -139,13 +144,32 @@
 
 ;; free type variables
 ;; n is a Name
-(def-type F ([n symbol?])
+(def-type F ([n symbol?]
+             [bound (or/c #f Type?)])
+  #:no-provide
   [#:frees
    [#:vars (_) (single-free-var n)]
    [#:idxs (_) empty-free-vars]]
   [#:fmap (_ #:self self) self]
   [#:for-each (_) (void)])
 
+(define (F* n [bound #f])
+  (make-F n bound))
+
+
+(define-match-expander F:*
+  (lambda (stx)
+    (syntax-case stx ()
+      [(_ n)
+       #'(? F? (app (lambda (t)
+                      (F-n t))
+                    n))]
+      [(_ n b)
+       #'(? F? (app (lambda (t)
+                      (list (F-n t) (F-bound t)))
+                    (list n b)))])))
+
+
 (define Name-table (make-free-id-table))
 
 ;; Name, an indirection of a type through the environment
@@ -519,10 +543,14 @@
 ;; n is how many variables are bound here
 ;; body is a type
 (def-type Poly ([n exact-nonnegative-integer?]
+                [bounds (hash/c exact-nonnegative-integer?
+                                Type?
+                                #:immutable #t
+                                #:flat #t)]
                 [body Type?])
   #:no-provide
   [#:frees (f) (f body)]
-  [#:fmap (f) (make-Poly n (f body))]
+  [#:fmap (f) (make-Poly n bounds (f body))]
   [#:for-each (f) (f body)]
   [#:mask (λ (t) (mask (Poly-body t)))])
 
@@ -1456,7 +1484,7 @@
       ;; De Bruijn indices
       [(B: idx) (transform idx lvl cur #f)]
       ;; Type variables
-      [(F: var) (transform var lvl cur #f)]
+      [(F: var _) (transform var lvl cur #f)]
       ;; forms w/ dotted type vars/indices
       [(RestDots: ty d)
        (make-RestDots (rec ty) (transform d lvl d #t))]
@@ -1477,7 +1505,7 @@
        (make-PolyRow constraints (rec/lvl body (add1 lvl)))]
       [(PolyDots: n body)
        (make-PolyDots n (rec/lvl body (+ n lvl)))]
-      [(Poly: n body)
+      [(Poly: n bound body)
        (make-Poly n (rec/lvl body (+ n lvl)))]
       [_ (Rep-fmap cur rec)])))
 
@@ -1618,7 +1646,7 @@
 (define (Mu-body* name t)
   (match t
     [(Mu: body)
-     (instantiate-type body (make-F name))]))
+     (instantiate-type body (F* name))]))
 
 ;; unfold : Mu -> Type
 (define/cond-contract (unfold t)
@@ -1638,19 +1666,33 @@
 ;;
 ;; list<symbol> type #:original-names list<symbol> -> type
 ;;
-(define (Poly* names body #:original-names [orig names])
+(define (Poly* names body #:bounds [bounds '#hash()] #:original-names [orig names])
   (if (null? names) body
-      (let ([v (make-Poly (length names) (abstract-type body names))])
+      (let* ([len (length names)]
+             [new-bounds (let ([max-idx (sub1 len)])
+                           (for/hash ([(n v) bounds])
+                             (values (- max-idx (index-of names n)) v)))]
+             [v (make-Poly len new-bounds (abstract-type body names))])
         (hash-set! type-var-name-table v orig)
         v)))
 
 ;; Poly 'smart' destructor
 (define (Poly-body* names t)
   (match t
-    [(Poly: n body)
+    [(Poly: n bounds body)
+     (define new-bounds (for/hash ([(idx v) bounds])
+                          (values (list-ref names idx) v)))
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (eprintf "new bounds is ~a ~n" new-bounds)
+     (instantiate-type body
+                       
+                       (map (lambda (n)
+                              (make-F n 
+                                      (hash-ref new-bounds n #f)
+                                      )) names)
+                       #;
+                       (map F* names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)
@@ -1665,7 +1707,7 @@
     [(PolyDots: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map F* names))]))
 
 
 ;; PolyRow 'smart' constructor
@@ -1683,7 +1725,7 @@
 (define (PolyRow-body* names t)
   (match t
     [(PolyRow: constraints body)
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map  names))]))
 
 
 ;;***************************************************************
@@ -1746,7 +1788,16 @@
                    (let* ([n (Poly-n t)]
                           [syms (build-list n (lambda _ (gensym)))])
                      (list syms (Poly-body* syms t))))
-                 (list nps bp)))])))
+                 (list nps bp)))]
+      [(_ nps bounds bp)
+       #'(? Poly?
+            (app (lambda (t)
+                   (let* ([n (Poly-n t)]
+                          [syms (build-list n (lambda _ (gensym)))]
+                          [bounds (for/hash ([(idx v) (Poly-bounds t)])
+                                    (values (list-ref syms idx) v))])
+                     (list syms bounds (Poly-body* syms t))))
+                 (list nps bounds bp)))])))
 
 ;; This match expander uses the names from the hashtable
 (define-match-expander Poly-names:
@@ -1939,7 +1990,7 @@
     [(Some: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map  names))]))
 
 
 (define-match-expander Some-names:
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 6170b6c3d..04e5ab741 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -192,7 +192,7 @@
          #:expected expected)]
       ;; regular polymorphic functions without dotted rest,
       ;; we do not choose any instantiations with mandatory keyword arguments
-      [(Poly: vars (Fun: arrows))
+      [(Poly: vars bounds (Fun: arrows))
        ;; check there are no RestDots
        #:when (not (for/or ([a (in-list arrows)])
                      (RestDots? (Arrow-rst a))))
@@ -214,7 +214,8 @@
                          (infer/vararg vars null argtys dom rst rng
                                        (and expected
                                             (tc-results->values expected))
-                                       #:objs argobjs)))
+                                       #:objs argobjs
+                                       #:bounds bounds)))
          #:function-type f-type
          #:args-results args-res
          #:expected expected)]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 63096f484..3d7b5ccbd 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -715,6 +715,7 @@
     [(tc-result1: (app resolve (and t (Poly-fresh: ns fresh-ns expected*))))
      ;; make sure the declared and annotated type variable arities match up
      ;; with the expected type variable arity
+     (eprintf "app resolve tc-result ~n")
      (for ([tvars (in-list tvarss)])
        (when (and (pair? tvars) (list? (car tvars)))
          (tc-error
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 3d580858e..c1de91710 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -802,11 +802,20 @@
    (match t2
      [(Evt: result2) (subtype* A result1 result2)]
      [_ (continue<: A t1 t2 obj)])]
-  [(case: F (F: var1))
-   (match t2
+  [(case: F (F: var1 bound))
+   (match* (t2 bound)
      ;; tvars are equal if they are the same variable
-     [(F: var2) (and (eq? var1 var2) A)]
-     [_ (continue<: A t1 t2 obj)])]
+     [((F: var2) _) (and (eq? var1 var2) A)]
+     [(_ (? Type?)) (subtype* A bound t2 obj)
+      #;
+      (eprintf "t2 is ~a bound is ~a ~n" t2 bound)
+      #;
+      (if bound
+          (let ([ret (subtype* A bound t2 obj)])
+            (eprintf "subtype ret is ~a ~n" ret)
+            ret)
+          (continue<: A t1 t2 obj))]
+     [(_ _ ) (continue<: A t1 t2 obj)])]
   [(case: Fun (Fun: arrows1))
    (match* (t2 arrows1)
      ;; special case when t1 can be collapsed into simpler arrow

From e20d4cd8cf0e148c003a132e03a274f0912b7d0c Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 17 Mar 2021 21:58:29 -0400
Subject: [PATCH 02/13] simplify code

---
 typed-racket-lib/typed-racket/rep/type-rep.rkt  | 10 ++--------
 typed-racket-lib/typed-racket/types/subtype.rkt | 12 ++----------
 2 files changed, 4 insertions(+), 18 deletions(-)

diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 34cd81be2..1b4c21eaf 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -160,14 +160,8 @@
 (define-match-expander F:*
   (lambda (stx)
     (syntax-case stx ()
-      [(_ n)
-       #'(? F? (app (lambda (t)
-                      (F-n t))
-                    n))]
-      [(_ n b)
-       #'(? F? (app (lambda (t)
-                      (list (F-n t) (F-bound t)))
-                    (list n b)))])))
+      [(_ n) #'(F: n _)]
+      [(_ n b) #'(F: n b)])))
 
 
 (define Name-table (make-free-id-table))
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index c1de91710..3673eb946 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -806,16 +806,8 @@
    (match* (t2 bound)
      ;; tvars are equal if they are the same variable
      [((F: var2) _) (and (eq? var1 var2) A)]
-     [(_ (? Type?)) (subtype* A bound t2 obj)
-      #;
-      (eprintf "t2 is ~a bound is ~a ~n" t2 bound)
-      #;
-      (if bound
-          (let ([ret (subtype* A bound t2 obj)])
-            (eprintf "subtype ret is ~a ~n" ret)
-            ret)
-          (continue<: A t1 t2 obj))]
-     [(_ _ ) (continue<: A t1 t2 obj)])]
+     [(_ (? Type?)) (subtype* A bound t2 obj)]
+     [(_ _) (continue<: A t1 t2 obj)])]
   [(case: Fun (Fun: arrows1))
    (match* (t2 arrows1)
      ;; special case when t1 can be collapsed into simpler arrow

From d8e3e4dc85dc3f096fc9e94a25ea935c527cbb16 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 18 Mar 2021 07:54:59 -0400
Subject: [PATCH 03/13] fix printing message for F:

---
 typed-racket-lib/typed-racket/infer/infer-unit.rkt | 12 +++++++-----
 typed-racket-lib/typed-racket/types/printer.rkt    |  3 ++-
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index b2c0cdf9d..90171cf36 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -578,8 +578,9 @@
          #f
          ;; constrain v to be below T (but don't mention bounds)
          (eprintf "hi...........~a ~n" v)
-         (if (subtype (hash-ref (context-type-bounds context) v) T obj)
-             (singleton -Bottom v (var-demote T (context-bounds context)))
+         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
+         (if (and maybe-type-bound (subtype maybe-type-bound T obj))
+             (singleton maybe-type-bound v (var-demote T (context-bounds context)))
              #f)]
 
         [(S (F: (? (inferable-var? context) v)))
@@ -588,10 +589,11 @@
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
-         (eprintf "bye...........~a ~a <: ~a ~n" v S (hash-ref (context-type-bounds context) v))
+         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
+         (eprintf "bye...........~a ~a <: ~a ~n" v S maybe-type-bound)
          ;; constrain v to be above S (but don't mention bounds)
-         (if (subtype S (hash-ref (context-type-bounds context) v) obj)
-             (singleton (var-promote S (context-bounds context)) v (hash-ref (context-type-bounds context) v))
+         (if (and maybe-type-bound (subtype S maybe-type-bound obj))
+             (singleton (var-promote S (context-bounds context)) v maybe-type-bound)
              #f)]
 
         ;; recursive names should get resolved as they're seen
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 7abb422d8..8a75d1dd5 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -714,10 +714,11 @@
     [(? Base?) (Base-name type)]
     [(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))]
     [(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]
-    [(F: nm)
+    [(F: nm bound)
      (cond
        [(eq? nm imp-var) "Imp"]
        [(eq? nm self-var) "Self"]
+       [(Type? bound) (format "~a <: ~a" nm (t->s bound))]
        [else nm])]
     [(Param: in out)
      (if (equal? in out)

From a068f4f99ccdb1ff266f2f4d4e364495aa26afa8 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 18 Mar 2021 09:57:25 -0400
Subject: [PATCH 04/13] remove print

---
 typed-racket-lib/typed-racket/infer/infer-unit.rkt         | 2 --
 typed-racket-lib/typed-racket/rep/type-rep.rkt             | 6 ++----
 typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt | 1 -
 3 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 90171cf36..df19a69b9 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -577,7 +577,6 @@
            [_ #f])
          #f
          ;; constrain v to be below T (but don't mention bounds)
-         (eprintf "hi...........~a ~n" v)
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          (if (and maybe-type-bound (subtype maybe-type-bound T obj))
              (singleton maybe-type-bound v (var-demote T (context-bounds context)))
@@ -590,7 +589,6 @@
            [_ #f])
          #f
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
-         (eprintf "bye...........~a ~a <: ~a ~n" v S maybe-type-bound)
          ;; constrain v to be above S (but don't mention bounds)
          (if (and maybe-type-bound (subtype S maybe-type-bound obj))
              (singleton (var-promote S (context-bounds context)) v maybe-type-bound)
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 1b4c21eaf..526434416 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1680,11 +1680,9 @@
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
      (eprintf "new bounds is ~a ~n" new-bounds)
      (instantiate-type body
-                       
                        (map (lambda (n)
-                              (make-F n 
-                                      (hash-ref new-bounds n #f)
-                                      )) names)
+                              (make-F n (hash-ref new-bounds n #f)))
+                            names)
                        #;
                        (map F* names))]))
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 3d7b5ccbd..63096f484 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -715,7 +715,6 @@
     [(tc-result1: (app resolve (and t (Poly-fresh: ns fresh-ns expected*))))
      ;; make sure the declared and annotated type variable arities match up
      ;; with the expected type variable arity
-     (eprintf "app resolve tc-result ~n")
      (for ([tvars (in-list tvarss)])
        (when (and (pair? tvars) (list? (car tvars)))
          (tc-error

From 571faffc9aad85380b4af5845773bbef1ed9a430 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 18 Mar 2021 12:06:53 -0400
Subject: [PATCH 05/13] bug fix

---
 .../typed-racket/infer/infer-unit.rkt         | 26 ++++++++++++++-----
 .../typed-racket/rep/type-rep.rkt             | 13 ++++------
 typed-racket-test/fail/bounded-poly.rkt       |  9 +++++++
 typed-racket-test/succeed/bounded-poly.rkt    |  9 +++++++
 4 files changed, 42 insertions(+), 15 deletions(-)
 create mode 100644 typed-racket-test/fail/bounded-poly.rkt
 create mode 100644 typed-racket-test/succeed/bounded-poly.rkt

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index df19a69b9..61ae4a647 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -578,9 +578,15 @@
          #f
          ;; constrain v to be below T (but don't mention bounds)
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
-         (if (and maybe-type-bound (subtype maybe-type-bound T obj))
-             (singleton maybe-type-bound v (var-demote T (context-bounds context)))
-             #f)]
+         (if maybe-type-bound
+             (if (subtype maybe-type-bound T obj)
+                 (singleton maybe-type-bound
+                            v
+                            (var-demote T (context-bounds context)))
+                 #f)
+             (singleton -Bottom
+                        v
+                        (var-demote T (context-bounds context))))]
 
         [(S (F: (? (inferable-var? context) v)))
          #:return-when
@@ -590,9 +596,15 @@
          #f
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          ;; constrain v to be above S (but don't mention bounds)
-         (if (and maybe-type-bound (subtype S maybe-type-bound obj))
-             (singleton (var-promote S (context-bounds context)) v maybe-type-bound)
-             #f)]
+         (if maybe-type-bound
+             (if (subtype S maybe-type-bound obj)
+                 (singleton (var-demote S (context-bounds context))
+                            v
+                            maybe-type-bound)
+                 #f)
+             (singleton (var-demote S (context-bounds context))
+                        v
+                        Univ))]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))
@@ -1010,7 +1022,7 @@
  (let ()
    (define/cond-contract (infer X Y S T R [expected #f]
                                 #:multiple? [multiple-substitutions? #f]
-                                #:bounds [bounds '#()]
+                                #:bounds [bounds '#hash()]
                                 #:objs [objs '()])
      (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
        (or/c #f Values/c AnyValues? ValuesDots?))
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 526434416..54e498c66 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1499,8 +1499,8 @@
        (make-PolyRow constraints (rec/lvl body (add1 lvl)))]
       [(PolyDots: n body)
        (make-PolyDots n (rec/lvl body (+ n lvl)))]
-      [(Poly: n bound body)
-       (make-Poly n (rec/lvl body (+ n lvl)))]
+      [(Poly: n bounds body)
+       (make-Poly n bounds (rec/lvl body (+ n lvl)))]
       [_ (Rep-fmap cur rec)])))
 
 
@@ -1678,13 +1678,10 @@
                           (values (list-ref names idx) v)))
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (eprintf "new bounds is ~a ~n" new-bounds)
      (instantiate-type body
                        (map (lambda (n)
                               (make-F n (hash-ref new-bounds n #f)))
-                            names)
-                       #;
-                       (map F* names))]))
+                            names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)
@@ -1717,7 +1714,7 @@
 (define (PolyRow-body* names t)
   (match t
     [(PolyRow: constraints body)
-     (instantiate-type body (map  names))]))
+     (instantiate-type body (map F* names))]))
 
 
 ;;***************************************************************
@@ -1982,7 +1979,7 @@
     [(Some: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map  names))]))
+     (instantiate-type body (map F* names))]))
 
 
 (define-match-expander Some-names:
diff --git a/typed-racket-test/fail/bounded-poly.rkt b/typed-racket-test/fail/bounded-poly.rkt
new file mode 100644
index 000000000..9f23e6b81
--- /dev/null
+++ b/typed-racket-test/fail/bounded-poly.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket/base
+
+(: a-func (All ([X <: Integer])
+               (-> X String)))
+(define (a-func a)
+  (number->string a))
+
+
+(a-func 19.999) ;; fail
diff --git a/typed-racket-test/succeed/bounded-poly.rkt b/typed-racket-test/succeed/bounded-poly.rkt
new file mode 100644
index 000000000..6f91bb2ee
--- /dev/null
+++ b/typed-racket-test/succeed/bounded-poly.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket/base
+
+(: a-func (All ([X <: Integer])
+               (-> X String)))
+(define (a-func a)
+  (number->string a))
+
+
+(a-func 10) ;; pass

From 3e48d28d0bb09b5973b1acb01b3cb64139495f63 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Fri, 19 Mar 2021 10:54:01 -0400
Subject: [PATCH 06/13] bug fix

---
 .../typed-racket/infer/infer-unit.rkt         | 20 +++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 61ae4a647..94175110d 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -22,6 +22,7 @@
          "signatures.rkt" "fail.rkt"
          "promote-demote.rkt"
          racket/match
+         (only-in racket/function curry curryr)
          ;racket/trace
          (contract-req)
          (for-syntax
@@ -576,7 +577,6 @@
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
-         ;; constrain v to be below T (but don't mention bounds)
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          (if maybe-type-bound
              (if (subtype maybe-type-bound T obj)
@@ -584,9 +584,8 @@
                             v
                             (var-demote T (context-bounds context)))
                  #f)
-             (singleton -Bottom
-                        v
-                        (var-demote T (context-bounds context))))]
+             ;; constrain v to be below T (but don't mention bounds)
+             (singleton -Bottom v (var-demote T (context-bounds context))))]
 
         [(S (F: (? (inferable-var? context) v)))
          #:return-when
@@ -594,17 +593,22 @@
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
-         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          ;; constrain v to be above S (but don't mention bounds)
+         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
+         (let ([sing (curry singleton (var-promote S (context-bounds context)) v)])
+           (cond
+             [(and maybe-type-bound (subtype S maybe-type-bound obj))
+              (sing maybe-type-bound)]
+             [(not maybe-type-bound) (sing Univ)]
+             [else #f]))
+         #;
          (if maybe-type-bound
              (if (subtype S maybe-type-bound obj)
                  (singleton (var-demote S (context-bounds context))
                             v
                             maybe-type-bound)
                  #f)
-             (singleton (var-demote S (context-bounds context))
-                        v
-                        Univ))]
+             (singleton (var-promote S (context-bounds context)) v Univ))]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))

From 1996b947bb79ad5a37f90656e21eac2315b0db85 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Fri, 19 Mar 2021 13:49:30 -0400
Subject: [PATCH 07/13] simplify code

---
 .../typed-racket/infer/infer-unit.rkt         | 25 ++++++-------------
 1 file changed, 8 insertions(+), 17 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 94175110d..bdc368577 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -577,15 +577,14 @@
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
+         ;; constrain v to be below T (but don't mention bounds)
          (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
-         (if maybe-type-bound
-             (if (subtype maybe-type-bound T obj)
-                 (singleton maybe-type-bound
-                            v
-                            (var-demote T (context-bounds context)))
-                 #f)
-             ;; constrain v to be below T (but don't mention bounds)
-             (singleton -Bottom v (var-demote T (context-bounds context))))]
+         (let ([sing (curryr singleton v (var-demote T (context-bounds context)))])
+           (cond
+             [(and maybe-type-bound (subtype maybe-type-bound T obj))
+              (sing maybe-type-bound)]
+             [(not maybe-type-bound) (sing -Bottom)]
+             [else #f]))]
 
         [(S (F: (? (inferable-var? context) v)))
          #:return-when
@@ -600,15 +599,7 @@
              [(and maybe-type-bound (subtype S maybe-type-bound obj))
               (sing maybe-type-bound)]
              [(not maybe-type-bound) (sing Univ)]
-             [else #f]))
-         #;
-         (if maybe-type-bound
-             (if (subtype S maybe-type-bound obj)
-                 (singleton (var-demote S (context-bounds context))
-                            v
-                            maybe-type-bound)
-                 #f)
-             (singleton (var-promote S (context-bounds context)) v Univ))]
+             [else #f]))]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))

From 2d92176b27da4a33dffd72cae7c64d499e51f08e Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Sun, 21 Mar 2021 10:16:39 -0400
Subject: [PATCH 08/13] small fix

---
 typed-racket-test/main.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/typed-racket-test/main.rkt b/typed-racket-test/main.rkt
index d40e4a308..a131c5639 100644
--- a/typed-racket-test/main.rkt
+++ b/typed-racket-test/main.rkt
@@ -192,7 +192,7 @@
   (define missed-opt? (make-parameter #f))
   (define bench? (make-parameter #f))
   (define math? (make-parameter #f))
-  (define excl (make-parameter (list)))
+  (define excl (make-parameter (set)))
   (define single (make-parameter #f))
   (current-namespace (make-base-namespace))
   (command-line

From 755a62cd9685c9f3606d41139966f4acb0704331 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Mon, 22 Mar 2021 15:41:22 -0400
Subject: [PATCH 09/13] simplify code

---
 .../typed-racket/infer/infer-unit.rkt         | 39 ++++++++-----------
 .../typed-racket/infer/signatures.rkt         |  6 +--
 .../typed-racket/rep/type-rep.rkt             | 11 +-----
 .../typed-racket/typecheck/tc-funapp.rkt      |  5 +--
 4 files changed, 21 insertions(+), 40 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index bdc368577..d2ad42e77 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -49,37 +49,36 @@
 (define-struct/cond-contract context
   ([bounds (listof symbol?)]
    [vars (listof symbol?)]
-   [indices (listof symbol?)]
-   [type-bounds (hash/c symbol? Type?)]) #:transparent)
+   [indices (listof symbol?)]) #:transparent)
 
 (define (context-add-vars ctx vars)
   (match ctx
-    [(context V X Y TB)
-     (context V (append vars X) Y TB)]))
+    [(context V X Y)
+     (context V (append vars X) Y)]))
 
 (define (context-add-var ctx var)
   (match ctx
-    [(context V X Y TB)
-     (context V (cons var X) Y TB)]))
+    [(context V X Y)
+     (context V (cons var X) Y)]))
 
 (define (context-add ctx #:bounds [bounds empty] #:vars [vars empty] #:indices [indices empty])
   (match ctx
-    [(context V X Y TB)
-     (context (append bounds V) (append vars X) (append indices Y) TB)]))
+    [(context V X Y)
+     (context (append bounds V) (append vars X) (append indices Y))]))
 
 (define (inferable-index? ctx bound)
   (match ctx
-    [(context _ _ Y TB)
+    [(context _ _ Y)
      (memq bound Y)]))
 
 (define ((inferable-var? ctx) var)
   (match ctx
-    [(context _ X _ TB)
+    [(context _ X _)
      (memq var X)]))
 
 (define (empty-cset/context ctx)
   (match ctx
-    [(context _ X Y TB)
+    [(context _ X Y)
      (empty-cset X Y)]))
 
 
@@ -570,7 +569,7 @@
 
         ;; variables that are in X and should be constrained
         ;; all other variables are compatible only with themselves
-        [((F: (? (inferable-var? context) v)) T)
+        [((F: (? (inferable-var? context) v) maybe-type-bound) T)
          #:return-when
          (match T
            ;; fail when v* is an index variable
@@ -578,7 +577,6 @@
            [_ #f])
          #f
          ;; constrain v to be below T (but don't mention bounds)
-         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          (let ([sing (curryr singleton v (var-demote T (context-bounds context)))])
            (cond
              [(and maybe-type-bound (subtype maybe-type-bound T obj))
@@ -586,14 +584,13 @@
              [(not maybe-type-bound) (sing -Bottom)]
              [else #f]))]
 
-        [(S (F: (? (inferable-var? context) v)))
+        [(S (F: (? (inferable-var? context) v) maybe-type-bound))
          #:return-when
          (match S
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
          ;; constrain v to be above S (but don't mention bounds)
-         (define maybe-type-bound (hash-ref (context-type-bounds context) v #f))
          (let ([sing (curry singleton (var-promote S (context-bounds context)) v)])
            (cond
              [(and maybe-type-bound (subtype S maybe-type-bound obj))
@@ -1017,19 +1014,17 @@
  (let ()
    (define/cond-contract (infer X Y S T R [expected #f]
                                 #:multiple? [multiple-substitutions? #f]
-                                #:bounds [bounds '#hash()]
                                 #:objs [objs '()])
      (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
        (or/c #f Values/c AnyValues? ValuesDots?))
       ((or/c #f Values/c AnyValues? ValuesDots?)
        #:multiple? boolean?
-       #:bounds (hash/c symbol? Type?)
        #:objs (listof OptObject?))
       . ->* . (or/c boolean?
                     substitution/c
                     (cons/c substitution/c
                             (listof substitution/c))))
-     (define ctx (context null X Y bounds))
+     (define ctx (context null X Y))
      (define expected-cset
        (if expected
            (cgen ctx R expected)
@@ -1046,8 +1041,7 @@
 
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X Y S T T-var R [expected #f]
-                      #:objs [objs '()]
-                      #:bounds [bounds '#hash()])
+                      #:objs [objs '()])
   (and ((length S) . >= . (length T))
        (let* ([fewer-ts (- (length S) (length T))]
               [new-T (match T-var
@@ -1057,8 +1051,7 @@
                         (append T (repeat-list rst-ts
                                                (quotient fewer-ts (length rst-ts))))]
                        [_ T])])
-         (infer X Y S new-T R expected #:objs objs
-                #:bounds bounds))))
+         (infer X Y S new-T R expected #:objs objs))))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
@@ -1073,7 +1066,7 @@
      (generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
    (define (subst t)
      (substitute-dots (map make-F new-vars) #f dotted-var t))
-   (define ctx (context null (append new-vars X) (list dotted-var) '#hash()))
+   (define ctx (context null (append new-vars X) (list dotted-var)))
 
    (define expected-cset (if expected
                              (cgen ctx (subst R) expected)
diff --git a/typed-racket-lib/typed-racket/infer/signatures.rkt b/typed-racket-lib/typed-racket/infer/signatures.rkt
index 4d35e7580..b0ab755e8 100644
--- a/typed-racket-lib/typed-racket/infer/signatures.rkt
+++ b/typed-racket-lib/typed-racket/infer/signatures.rkt
@@ -39,8 +39,7 @@
                            ((or/c #f Values/c AnyValues? ValuesDots?)
                             ;; optional multiple substitutions?
                             #:multiple? boolean?
-                            #:objs (listof OptObject?)
-                            #:bounds (hash/c symbol? Type?))
+                            #:objs (listof OptObject?))
                            . ->* . any)]
    [cond-contracted infer/vararg ((;; variables from the forall
                                    (listof symbol?)
@@ -56,8 +55,7 @@
                                    (or/c #f Values/c AnyValues? ValuesDots?))
                                   ;; [optional] expected type
                                   ((or/c #f Values/c AnyValues? ValuesDots?)
-                                   #:objs (listof OptObject?)
-                                   #:bounds (hash/c symbol? Type?))
+                                   #:objs (listof OptObject?))
                                   . ->* . any)]
    [cond-contracted infer/dots (((listof symbol?)
                                  symbol?
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 54e498c66..8f2e12e0f 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1777,16 +1777,7 @@
                    (let* ([n (Poly-n t)]
                           [syms (build-list n (lambda _ (gensym)))])
                      (list syms (Poly-body* syms t))))
-                 (list nps bp)))]
-      [(_ nps bounds bp)
-       #'(? Poly?
-            (app (lambda (t)
-                   (let* ([n (Poly-n t)]
-                          [syms (build-list n (lambda _ (gensym)))]
-                          [bounds (for/hash ([(idx v) (Poly-bounds t)])
-                                    (values (list-ref syms idx) v))])
-                     (list syms bounds (Poly-body* syms t))))
-                 (list nps bounds bp)))])))
+                 (list nps bp)))])))
 
 ;; This match expander uses the names from the hashtable
 (define-match-expander Poly-names:
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 04e5ab741..6170b6c3d 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -192,7 +192,7 @@
          #:expected expected)]
       ;; regular polymorphic functions without dotted rest,
       ;; we do not choose any instantiations with mandatory keyword arguments
-      [(Poly: vars bounds (Fun: arrows))
+      [(Poly: vars (Fun: arrows))
        ;; check there are no RestDots
        #:when (not (for/or ([a (in-list arrows)])
                      (RestDots? (Arrow-rst a))))
@@ -214,8 +214,7 @@
                          (infer/vararg vars null argtys dom rst rng
                                        (and expected
                                             (tc-results->values expected))
-                                       #:objs argobjs
-                                       #:bounds bounds)))
+                                       #:objs argobjs)))
          #:function-type f-type
          #:args-results args-res
          #:expected expected)]

From 668a0d59743c74ff29cd1cd6a8e4101d773afdc0 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Mon, 22 Mar 2021 19:53:20 -0400
Subject: [PATCH 10/13] simplify code x1

---
 .../typed-racket/infer/infer-unit.rkt         | 42 +++++++++++--------
 1 file changed, 24 insertions(+), 18 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index d2ad42e77..716eaf415 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -22,7 +22,7 @@
          "signatures.rkt" "fail.rkt"
          "promote-demote.rkt"
          racket/match
-         (only-in racket/function curry curryr)
+         (only-in racket/function curry curryr thunk)
          ;racket/trace
          (contract-req)
          (for-syntax
@@ -66,6 +66,7 @@
     [(context V X Y)
      (context (append bounds V) (append vars X) (append indices Y))]))
 
+
 (define (inferable-index? ctx bound)
   (match ctx
     [(context _ _ Y)
@@ -493,6 +494,21 @@
   ;; this constrains just x (which is a single var)
   (define (singleton S x T)
     (insert empty x S T))
+
+  (define (constrain tvar-a tvar-b #:above above)
+    (match-define (F: var maybe-type-bound) tvar-a)
+    (define-values (default sub sing) (if above
+                                          (values Univ
+                                                  (thunk (subtype tvar-b maybe-type-bound obj))
+                                                  (curry singleton (var-promote tvar-b (context-bounds context)) var))
+                                          (values -Bottom
+                                                  (thunk (subtype maybe-type-bound tvar-b obj))
+                                                  (curryr singleton var (var-demote tvar-b (context-bounds context))))))
+    (cond
+      [(not maybe-type-bound) (sing default)]
+      [(sub) (sing maybe-type-bound)]
+      [else #f]))
+
   ;; FIXME -- figure out how to use parameters less here
   ;;          subtyping doesn't need to use it quite as much
   (define cs (current-seen))
@@ -569,34 +585,24 @@
 
         ;; variables that are in X and should be constrained
         ;; all other variables are compatible only with themselves
-        [((F: (? (inferable-var? context) v) maybe-type-bound) T)
+        [((and (F: (? (inferable-var? context))) S) T)
          #:return-when
          (match T
            ;; fail when v* is an index variable
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
-         ;; constrain v to be below T (but don't mention bounds)
-         (let ([sing (curryr singleton v (var-demote T (context-bounds context)))])
-           (cond
-             [(and maybe-type-bound (subtype maybe-type-bound T obj))
-              (sing maybe-type-bound)]
-             [(not maybe-type-bound) (sing -Bottom)]
-             [else #f]))]
-
-        [(S (F: (? (inferable-var? context) v) maybe-type-bound))
+         ;; constrain S to be below T (but don't mention bounds)
+         (constrain S T #:above #f)]
+
+        [(S (and (F: (? (inferable-var? context))) T))
          #:return-when
          (match S
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
-         ;; constrain v to be above S (but don't mention bounds)
-         (let ([sing (curry singleton (var-promote S (context-bounds context)) v)])
-           (cond
-             [(and maybe-type-bound (subtype S maybe-type-bound obj))
-              (sing maybe-type-bound)]
-             [(not maybe-type-bound) (sing Univ)]
-             [else #f]))]
+         ;; constrain T to be above S (but don't mention bounds)
+         (constrain T S #:above #t)]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))

From c20853587829f1a0eade15ff796fb7e677df04d8 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 24 Mar 2021 22:17:44 -0400
Subject: [PATCH 11/13] WIP F-bounded Polymorphism

---
 .../typed-racket/infer/infer-unit.rkt         | 47 ++++++++++++-------
 .../typed-racket/private/parse-type.rkt       | 13 +++--
 .../typed-racket/rep/type-rep.rkt             | 21 +++++++--
 typed-racket-test/succeed/bounded-poly.rkt    | 10 ++++
 4 files changed, 65 insertions(+), 26 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 716eaf415..18b938d29 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -39,6 +39,7 @@
 (define (empty-set) '())
 
 (define current-seen (make-parameter (empty-set)))
+(define infered-tvar-map (make-parameter (hash)))
 
 ;; Type Type -> Pair<Seq, Seq>
 ;; construct a pair for the set of seen type pairs
@@ -476,7 +477,7 @@
 ;; produces a cset which determines a substitution that makes S a subtype of T
 ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
 ;; the index variables from the TOPLAS paper
-(define/cond-contract (cgen context S T [obj #f] [bound #f])
+(define/cond-contract (cgen context S T [obj #f])
   (->* (context? (or/c Values/c ValuesDots? AnyValues?)
                  (or/c Values/c ValuesDots? AnyValues?))
        ((or/c #f OptObject?))
@@ -485,7 +486,7 @@
   (define/cond-contract (cg S T [obj #f])
    (->* (Type? Type?) ((or/c #f OptObject?))
         (or/c #f cset?))
-   (cgen context S T obj bound))
+   (cgen context S T obj))
   (define/cond-contract (cg/inv S T)
    (Type? Type? . -> . (or/c #f cset?))
    (cgen/inv context S T))
@@ -496,7 +497,15 @@
     (insert empty x S T))
 
   (define (constrain tvar-a tvar-b #:above above)
-    (match-define (F: var maybe-type-bound) tvar-a)
+    (define (maybe-type-app t)
+      (match t
+        [(App: t1 (list (F: var))) #:when (hash-has-key? (infered-tvar-map) var)
+                                   (define v (hash-ref (infered-tvar-map) var))
+                                   (-App t1 (list v))]
+        [_ t]))
+
+    (match-define (F: var (app maybe-type-app maybe-type-bound)) tvar-a)
+
     (define-values (default sub sing) (if above
                                           (values Univ
                                                   (thunk (subtype tvar-b maybe-type-bound obj))
@@ -506,7 +515,9 @@
                                                   (curryr singleton var (var-demote tvar-b (context-bounds context))))))
     (cond
       [(not maybe-type-bound) (sing default)]
-      [(sub) (sing maybe-type-bound)]
+      [(sub)
+       (infered-tvar-map (hash-set (infered-tvar-map) var maybe-type-bound))
+       (sing maybe-type-bound)]
       [else #f]))
 
   ;; FIXME -- figure out how to use parameters less here
@@ -983,6 +994,7 @@
         (build-subst md))
       (build-subst (stream-first (cset-maps C)))))
 
+
 ;; context : the context of what to infer/not infer
 ;; S : a list of types to be the subtypes of T
 ;; T : a list of types
@@ -1000,9 +1012,9 @@
           (for/list/fail ([s (in-list S)]
                           [t (in-list T)]
                           [obj (in-list/rest objs #f)])
-                         ;; We meet early to prune the csets to a reasonable size.
-                         ;; This weakens the inference a bit, but sometimes avoids
-                         ;; constraint explosion.
+            ;; We meet early to prune the csets to a reasonable size.
+            ;; This weakens the inference a bit, but sometimes avoids
+            ;; constraint explosion.
             (% cset-meet (cgen context s t obj) expected-cset)))))
 
 
@@ -1048,16 +1060,17 @@
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X Y S T T-var R [expected #f]
                       #:objs [objs '()])
-  (and ((length S) . >= . (length T))
-       (let* ([fewer-ts (- (length S) (length T))]
-              [new-T (match T-var
-                       [(? Type? var-t) (list-extend S T var-t)]
-                       [(Rest: rst-ts)
-                        #:when (zero? (remainder fewer-ts (length rst-ts)))
-                        (append T (repeat-list rst-ts
-                                               (quotient fewer-ts (length rst-ts))))]
-                       [_ T])])
-         (infer X Y S new-T R expected #:objs objs))))
+  (parameterize ([infered-tvar-map (hash)])
+    (and ((length S) . >= . (length T))
+         (let* ([fewer-ts (- (length S) (length T))]
+                [new-T (match T-var
+                         [(? Type? var-t) (list-extend S T var-t)]
+                         [(Rest: rst-ts)
+                          #:when (zero? (remainder fewer-ts (length rst-ts)))
+                          (append T (repeat-list rst-ts
+                                                 (quotient fewer-ts (length rst-ts))))]
+                         [_ T])])
+           (infer X Y S new-T R expected #:objs objs)))))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index 1e922a167..ec55ceffd 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -195,7 +195,9 @@
 
 (define-syntax-class maybe-bounded
   #:datum-literals (<:)
-  (pattern (name:id <: bound:id)))
+  #:attributes (name bound)
+  (pattern (name:id <: bound:expr))
+  (pattern name:id #:attr bound #f))
 
 ;; Syntax -> Type
 ;; Parse a Forall type
@@ -224,9 +226,12 @@
      (when maybe-dup
        (parse-error "duplicate type variable"
                     "variable" (syntax-e maybe-dup)))
-     (define bounds (for/hash ([i (stx-map syntax-e (attribute vars.name))]
-                               [j (attribute vars.bound)])
-                      (values i (parse-type j))))
+     (define bounds (for/fold ([acc (hash)])
+                              ([i (stx-map syntax-e (attribute vars.name))]
+                               [j (attribute vars.bound)]
+                               #:when j)
+                      (hash-set acc i
+                                (extend-tvars (hash-keys acc) (parse-type j)))))
      (let* ([vars (stx-map syntax-e (attribute vars.name))])
        (extend-tvars vars
                      (make-Poly vars (parse-type #'t.type) #:bounds bounds)))]
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 8f2e12e0f..e91ba3f54 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -24,6 +24,7 @@
          syntax/id-set
          racket/contract
          racket/lazy-require
+         racket/syntax
          racket/unsafe/undefined
          (for-syntax racket/base
                      racket/syntax
@@ -110,6 +111,7 @@
       (App? x)))
 
 (lazy-require
+ ("../types/substitute.rkt" (subst))
  ("../types/overlap.rkt" (overlap?))
  ("../types/prop-ops.rkt" (-and))
  ("../types/resolve.rkt" (resolve-app))
@@ -1660,28 +1662,37 @@
 ;;
 ;; list<symbol> type #:original-names list<symbol> -> type
 ;;
+
 (define (Poly* names body #:bounds [bounds '#hash()] #:original-names [orig names])
   (if (null? names) body
       (let* ([len (length names)]
-             [new-bounds (let ([max-idx (sub1 len)])
-                           (for/hash ([(n v) bounds])
-                             (values (- max-idx (index-of names n)) v)))]
+             [new-bounds (for/hash ([(n v) bounds])
+                           (values (index-of names n) v))]
              [v (make-Poly len new-bounds (abstract-type body names))])
         (hash-set! type-var-name-table v orig)
         v)))
 
+(define (unsubst ty orig-names names)
+  (for/fold ([acc ty])
+            ([o orig-names]
+             [n names])
+    (subst o (make-F n #f) acc)
+    #;
+    (subst o (make-Name (format-id #f "~a" n) 0 #f) acc)))
+
 ;; Poly 'smart' destructor
 (define (Poly-body* names t)
+  (define orig-names (hash-ref type-var-name-table t))
   (match t
     [(Poly: n bounds body)
      (define new-bounds (for/hash ([(idx v) bounds])
-                          (values (list-ref names idx) v)))
+                          (values (list-ref names idx) (unsubst v orig-names names))))
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
      (instantiate-type body
                        (map (lambda (n)
                               (make-F n (hash-ref new-bounds n #f)))
-                            names))]))
+                        names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)
diff --git a/typed-racket-test/succeed/bounded-poly.rkt b/typed-racket-test/succeed/bounded-poly.rkt
index 6f91bb2ee..caf70c911 100644
--- a/typed-racket-test/succeed/bounded-poly.rkt
+++ b/typed-racket-test/succeed/bounded-poly.rkt
@@ -7,3 +7,13 @@
 
 
 (a-func 10) ;; pass
+
+
+(struct (A) foo ([a : A]) #:type-name Foo)
+
+(: c-func (All ([X <: Integer] [Y <: (Foo X)])
+               (-> X Y String)))
+(define (c-func a b)
+  (number->string a))
+
+(c-func 10 (foo 10))

From 2c0cf9bda5c365722e75cd183c21cb086c3e274d Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 25 Mar 2021 16:57:16 -0400
Subject: [PATCH 12/13] fix a bug; it took me 3 hours to realize why this
 caused TR to diverge

---
 typed-racket-lib/typed-racket/rep/type-rep.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index e91ba3f54..2474ceffd 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1682,7 +1682,7 @@
 
 ;; Poly 'smart' destructor
 (define (Poly-body* names t)
-  (define orig-names (hash-ref type-var-name-table t))
+  (define orig-names (hash-ref type-var-name-table t null))
   (match t
     [(Poly: n bounds body)
      (define new-bounds (for/hash ([(idx v) bounds])

From f199e4752b2963061ff3fc9e590e67de7b983c3f Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Sat, 27 Mar 2021 11:50:34 -0400
Subject: [PATCH 13/13] more progress on bounded polymorphism

---
 typed-racket-lib/typed-racket/infer/infer-unit.rkt | 8 ++++++--
 typed-racket-lib/typed-racket/rep/type-rep.rkt     | 7 ++++++-
 typed-racket-test/succeed/bounded-poly.rkt         | 7 +++++++
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 18b938d29..86d112655 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -596,7 +596,7 @@
 
         ;; variables that are in X and should be constrained
         ;; all other variables are compatible only with themselves
-        [((and (F: (? (inferable-var? context))) S) T)
+        [((F: (? (inferable-var? context))) T)
          #:return-when
          (match T
            ;; fail when v* is an index variable
@@ -606,7 +606,7 @@
          ;; constrain S to be below T (but don't mention bounds)
          (constrain S T #:above #f)]
 
-        [(S (and (F: (? (inferable-var? context))) T))
+        [(S (F: (? (inferable-var? context))))
          #:return-when
          (match S
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
@@ -623,6 +623,10 @@
          (let ([s (resolve-once s)])
            (and s (cg s t obj)))]
 
+        [((F: var (? Type? bound)) t)
+         (let ([s (resolve-once bound)])
+           (and s (cg s t obj)))]
+
         ;; constrain b1 to be below T, but don't mention the new vars
         [((Poly: v1 b1) T) (cgen (context-add context #:bounds v1) b1 T)]
 
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 2474ceffd..334aed47b 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -1691,7 +1691,12 @@
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
      (instantiate-type body
                        (map (lambda (n)
-                              (make-F n (hash-ref new-bounds n #f)))
+                              (define v (match (hash-ref new-bounds n #f)
+                                          [(App: rator (list (F: vb _)))
+                                           #:when (hash-has-key? new-bounds vb)
+                                           (make-App rator (list (hash-ref new-bounds vb)))]
+                                          [_else _else]))
+                              (make-F n v))
                         names))]))
 
 ;; PolyDots 'smart' constructor
diff --git a/typed-racket-test/succeed/bounded-poly.rkt b/typed-racket-test/succeed/bounded-poly.rkt
index caf70c911..445db0bd9 100644
--- a/typed-racket-test/succeed/bounded-poly.rkt
+++ b/typed-racket-test/succeed/bounded-poly.rkt
@@ -17,3 +17,10 @@
   (number->string a))
 
 (c-func 10 (foo 10))
+
+(: d-func (All ([X <: Integer] [Y <: (Foo X)])
+               (-> X Y String)))
+(define (d-func a b)
+  (number->string (foo-a b)))
+
+(d-func 42 (foo 10))