more progress on bounded polymorphism

Author: capfredf

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)]
 

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

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))