Change inference to take into account index vs regular vars.

original commit: 99e499a503b8b319bc0e512b698e5543634e3654

collects/typed-scheme/infer/infer-unit.rkt

@@ -3,12 +3,11 @@
 (require scheme/require
          (except-in 
           (path-up
-           "utils/utils.rkt" "utils/tc-utils.rkt"
+           "utils/utils.rkt" "utils/tc-utils.rkt" "types/utils.rkt"
            "rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-utils.rkt"
            "types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt"
            "env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt")
           make-env)
-         (path-up "types/utils.rkt")
          "constraint-structs.rkt"
 	 "signatures.rkt"                  
          scheme/match
@@ -499,26 +498,28 @@
   (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
 
 ;; X : variables to infer
+;; Y : indices to infer
 ;; S : actual argument types
 ;; T : formal argument types
 ;; R : result type
 ;; must-vars : variables that must be in the substitution
+;; must-idxs : index variables that must be in the substitution
 ;; expected : boolean
 ;; returns a substitution
 ;; if R is #f, we don't care about the substituion
 ;; just return a boolean result
-(define (infer X S T R must-vars [expected #f])
+(define (infer X Y S T R must-vars must-idxs [expected #f])
   (with-handlers ([exn:infer? (lambda _ #f)])  
-    (let ([cs (cgen/list null X S T)])
+    (let ([cs (cgen/list null X Y S T)])
       (if (not expected)
-          (subst-gen cs R must-vars)
-          (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
+          (subst-gen cs R (append must-vars must-idxs))
+          (subst-gen (cset-meet cs (cgen null X Y R expected)) R must-vars)))))
 
 ;; like infer, but T-var is the vararg type:
-(define (infer/vararg X S T T-var R must-vars [expected #f])
+(define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f])
   (define new-T (if T-var (extend S T T-var) T))
   (and ((length S) . >= . (length T))
-       (infer X S new-T R must-vars expected)))
+       (infer X Y S new-T R must-vars must-idxs expected)))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
@@ -538,10 +539,4 @@
           (subst-gen cs R must-vars)
           (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
 
-(define (infer/simple S T R)
-  (infer (fv/list T) S T R))
-
-(define (i s t r)
-  (infer/simple (list s) (list t) r))
-
 ;(trace cgen)

collects/typed-scheme/infer/signatures.rkt

@@ -1,6 +1,7 @@
-#lang scheme/base
-(require scheme/unit scheme/contract "constraint-structs.rkt" "../utils/utils.rkt")
-(require (rep type-rep) (utils unit-utils))
+#lang racket/base
+(require racket/unit racket/contract racket/require
+         "constraint-structs.rkt" 
+         (path-up "utils/utils.rkt" "utils/unit-utils.rkt" "rep/type-rep.rkt"))
 (provide (all-defined-out))
 
 (define-signature dmap^
@@ -29,13 +30,40 @@
   ([cnt restrict (Type? Type? . -> . Type?)]))
 
 (define-signature infer^
-  ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)]
-   [cnt infer/vararg (((listof symbol?) 
+  ([cnt infer ((;; variables from the forall
+                (listof symbol?) 
+                ;; indexes from the forall
+                (listof symbol?) 
+                ;; actual argument types from call site
+                (listof Type?)
+                ;; domain
+                (listof Type?)
+                ;; range
+                Type?
+                ;; free variables                
+                (listof symbol?)
+                ;; free indexes
+                (listof symbol?))
+               ;; optional expected type
+               ((or/c #f Type?)) 
+               . ->* . any)]
+   [cnt infer/vararg ((;; variables from the forall
+                       (listof symbol?) 
+                       ;; indexes from the forall
+                       (listof symbol?) 
+                       ;; actual argument types from call site
                        (listof Type?)
+                       ;; domain
                        (listof Type?)
+                       ;; rest
                        (or/c #f Type?)
+                       ;; range
                        Type?
+                       ;; free variables
+                       (listof symbol?)
+                       ;; free indexes
                        (listof symbol?))
+                      ;; [optional] expected type
                       ((or/c #f Type?)) . ->* . any)]
    [cnt infer/dots (((listof symbol?) 
                      symbol?

collects/typed-scheme/typecheck/tc-app.rkt

@@ -824,11 +824,11 @@
                              [else (= (length dom) (length argtys))]))
                      ;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
                      ;; note that we have to use argtys-t here, since argtys is a list of tc-results
-                     (lambda (dom rng rest drest a) 
+                     (lambda (dom rng rest drest a)
                        (if drest
                            (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) 
                                        #:expected (and expected (tc-results->values expected)))
-                           (infer/vararg vars argtys-t dom rest rng (fv rng) 
+                           (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng (fv rng) (fi rng)
                                          (and expected (tc-results->values expected)))))
                      t argtys expected)]
     ;; regular polymorphic functions without dotted rest, and without mandatory keyword args

collects/typed-scheme/types/utils.rkt

@@ -12,7 +12,7 @@
          scheme/contract
          (for-syntax scheme/base syntax/parse))
 
-(provide fv fv/list
+(provide fv fv/list fi
          substitute
          substitute-dots
          substitute-dotted
@@ -68,7 +68,7 @@
 ;; implements angle bracket substitution from the formalism
 ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
 (d/c (substitute-dots images rimage name target)
-  ((listof Type/c) (or/c #f (cons/c Type/c symbol?)) symbol? Type? . -> . Type?)
+  ((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
   (define (sb t) (substitute-dots images rimage name t))
   (if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
       (type-case (#:Type sb #:Filter (sub-f sb)) target
@@ -293,6 +293,7 @@
 
 ;; fv : Type -> Listof[Name]
 (define (fv t) (hash-map (free-vars* t) (lambda (k v) k)))
+(define (fi t) (for/list ([(k v) (in-hash (free-idxs* t))]) k))
 
 ;; fv/list : Listof[Type] -> Listof[Name]
 (define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))