Take the meet of constraints earlier in the inference process.

This avoids constraint explosions in some cases, notably when working
with polydots and plain variable arity functions at the same time.

However, this also weakens inference a bit (breaks it for
unholy-terror and related tests), but not in a way that affects any
practical use cases that I know of.

collects/tests/typed-scheme/fail/values-dots.rkt

@@ -1,5 +1,5 @@
 #;
-(exn-pred 7)
+(exn-pred 10)
 #lang typed-scheme
 
 (require typed-scheme/private/extra-procs)

collects/tests/typed-scheme/succeed/ann-map-funcs.rkt

@@ -1,11 +0,0 @@
-#lang typed/racket
-
-(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
-
-(define (map-with-funcs . fs)
- (lambda as
-   (map (lambda: ([f : (a ... a -> b)])
-          (apply f as))
-        fs)))
-
-(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number)))

collects/tests/typed-scheme/xfail/ann-map-funcs.rkt

@@ -0,0 +1,21 @@
+#lang typed/racket
+
+;; This test is similar to unholy-terror.
+;; Recent changes to the numeric tower makes this generate a ridiculous amount
+;; of inference contraints.
+;; Changes to the inference engine breaks inference on this test, but unlike
+;; unholy terror, this one fails quite fast, so it's not as bad.
+;; Reverting these changes would make inference work again, given enough time
+;; and memory (on the order of hours, and gigabytes of memory).
+;; For future reference, ~600k inference constraints were generated (due to a
+;; repeated cross product) before I killed it.
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+
+(define (map-with-funcs . fs)
+ (lambda as
+   (map (lambda: ([f : (a ... a -> b)])
+          (apply f as))
+        fs)))
+
+(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number)))

collects/tests/typed-scheme/xfail/unholy-terror.rkt

@@ -1,5 +1,8 @@
 #lang typed-scheme
 
+;; Changes to the numeric tower cause this test to generate a ridiculous
+;; number of inference constraints. Inference takes 5+ minutes.
+
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
             (map (lambda: ([y : (a ... a -> Number)])

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

@@ -640,12 +640,21 @@
 ;; Y : the set of index variables to be constrained
 ;; S : a list of types to be the subtypes of T
 ;; T : a list of types
+;; expected-cset : a cset representing the expected type, to meet early and
+;;  keep the number of constraints in check. (empty by default)
 ;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
-(d/c (cgen/list V X Y S T)
+(d/c (cgen/list V X Y S T
-  ((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?) . -> . cset?)
+                #:expected-cset [expected-cset (empty-cset '() '())])
+  (((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?))
+   (#:expected-cset cset?) . ->* . cset?)
   (unless (= (length S) (length T))
     (fail! S T))
-  (cset-meet* (for/list ([s S] [t T]) (cgen V X Y s t))))
+  (cset-meet*
+   (for/list ([s S] [t T])
+             ;; 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 V X Y s t) expected-cset))))
 
 ;; X : variables to infer
 ;; Y : indices to infer
@@ -658,10 +667,11 @@
 ;; just return a boolean result
 (define (infer X Y S T R [expected #f])
   (with-handlers ([exn:infer? (lambda _ #f)])  
-    (let* ([cs (cgen/list null X Y S T)]
+    (let* ([expected-cset (if expected
-           [cs* (if expected 
+                              (cgen null X Y R expected)
-                    (cset-meet cs (cgen null X Y R expected))
+                              (empty-cset '() '()))]
-                    cs)])
+           [cs  (cgen/list null X Y S T #:expected-cset expected-cset)]
+           [cs* (cset-meet cs expected-cset)])
           (if R (subst-gen cs* Y R) #t))))
 
 ;; like infer, but T-var is the vararg type:
@@ -676,16 +686,19 @@
   (with-handlers ([exn:infer? (lambda _ #f)])
     (let* ([short-S (take S (length T))]
            [rest-S (drop S (length T))]
-           [cs-short (cgen/list null X (list dotted-var) short-S T)]
+           [expected-cset (if expected
+                              (cgen null X (list dotted-var) R expected)
+                              (empty-cset '() '()))]
+           [cs-short (cgen/list null X (list dotted-var) short-S T
+                                #:expected-cset expected-cset)]
            [new-vars (var-store-take dotted-var T-dotted (length rest-S))]
            [new-Ts (for/list ([v new-vars])
                      (substitute (make-F v) dotted-var 
                                  (substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))]
-           [cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts)]
+           [cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
+                                 #:expected-cset expected-cset)]
            [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
            [cs (cset-meet cs-short cs-dotted*)])
-      (if (not expected)
+      (subst-gen (cset-meet cs expected-cset) (list dotted-var) R))))
-          (subst-gen cs (list dotted-var) R)
-          (subst-gen (cset-meet cs (cgen null X (list dotted-var) R expected)) (list dotted-var) R)))))
 
 ;(trace cgen)