Make TR compile with contracts enabled again.

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

@@ -27,11 +27,12 @@
 (define (seen-before s t)
   (cons (Type-seq s) (Type-seq t)))
 (define/cond-contract (remember s t A)
- (Type/c Type/c (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> .
+ (Values/c Values/c
-                (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)))
+  (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> .
+  (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)))
  (cons (seen-before s t) A))
 (define/cond-contract (seen? s t)
- (Type/c Type/c . -> . any/c)
+ (Values/c Values/c . -> . any/c)
  (member (seen-before s t) (current-seen)))
 
 
@@ -167,7 +168,7 @@
     [(_ _) (fail! s t)]))
 
 (define/cond-contract (cgen/arr V X Y s-arr t-arr)
-  ((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . cset?)
   (define (cg S T) (cgen V X Y S T))
   (match* (s-arr t-arr)
     ;; the simplest case - no rests, drests, keywords
@@ -310,7 +311,8 @@
 ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
 ;; the index variables from the TOPLAS paper
 (define/cond-contract (cgen V X Y S T)
-  ((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?)
+   (or/c Values/c ValuesDots?) (or/c Values/c ValuesDots?). -> . cset?)
   ;; useful quick loop
   (define/cond-contract (cg S T)
    (Type/c Type/c . -> . cset?)
@@ -584,7 +586,7 @@
 ;; Y : (listof symbol?) - index variables that must have entries
 ;; R : Type/c - result type into which we will be substituting
 (define/cond-contract (subst-gen C Y R)
-  (cset? (listof symbol?) Type/c . -> . (or/c #f substitution/c))
+  (cset? (listof symbol?) (or/c Values/c ValuesDots?) . -> . (or/c #f substitution/c))
   (define var-hash (free-vars-hash (free-vars* R)))
   (define idx-hash (free-vars-hash (free-idxs* R)))
   ;; v : Symbol - variable for which to check variance
@@ -691,7 +693,7 @@
 ;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
 (define/cond-contract (cgen/list V X Y S T
                                  #:expected-cset [expected-cset (empty-cset '() '())])
-  (((listof symbol?) (listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c))
+  (((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c))
    (#:expected-cset cset?) . ->* . cset?)
   (unless (= (length S) (length T))
     (fail! S T))
@@ -716,7 +718,10 @@
 (define infer
  (let ()
   (define/cond-contract (infer X Y S T R [expected #f])
-    (((listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c) Type/c) ((or/c #f Type/c)) . ->* . (or/c boolean? substitution/c))
+    (((listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c)
+      (or/c #f Values/c ValuesDots?))
+     ((or/c #f Values/c ValuesDots?))
+     . ->* . (or/c boolean? substitution/c))
     (with-handlers ([exn:infer? (lambda _ #f)])
       (let* ([expected-cset (if expected
                                 (cgen null X Y R expected)

collects/typed-racket/infer/signatures.rkt

@@ -39,9 +39,9 @@
                             ;; domain
                             (listof Type/c)
                             ;; range
-                            (or/c #f Values? ValuesDots? Result? Type/c))
+                            (or/c #f Values/c ValuesDots?))
                            ;; optional expected type
-                           ((or/c #f Values? ValuesDots? Result? Type/c))
+                           ((or/c #f Values/c ValuesDots?))
                            . ->* . any)]
    [cond-contracted infer/vararg ((;; variables from the forall
                                    (listof symbol?)
@@ -54,10 +54,14 @@
                                    ;; rest
                                    (or/c #f Type/c)
                                    ;; range
-                                   (or/c #f Values? ValuesDots? Result? Type/c))
+                                   (or/c #f Values/c ValuesDots?))
                                   ;; [optional] expected type
-                                  ((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)]
+                                  ((or/c #f Values/c ValuesDots?)) . ->* . any)]
    [cond-contracted infer/dots (((listof symbol?)
                                  symbol?
-                                 (listof Type/c) (listof Type/c) Type/c Type/c (listof symbol?))
+                                 (listof Values/c)
-                                (#:expected (or/c #f Type/c)) . ->* . any)]))
+                                 (listof Values/c)
+                                 Values/c
+                                 (or/c Values/c ValuesDots?)
+                                 (listof symbol?))
+                                (#:expected (or/c #f Values/c ValuesDots?)) . ->* . any)]))

collects/typed-racket/rep/filter-rep.rkt

@@ -19,12 +19,14 @@
 (def-filter Bot () [#:fold-rhs #:base])
 (def-filter Top () [#:fold-rhs #:base])
 
-(def-filter TypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
+;; TODO: t should only be a Type/c, but that leads to circular dependencies
+(def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
   [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
   [#:frees (λ (f) (combine-frees (map f (cons t p))))]
   [#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
 
-(def-filter NotTypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
+;; TODO: t should only be a Type/c, but that leads to circular dependencies
+(def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
   [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
   [#:frees (λ (f) (combine-frees (map f (cons t p))))]
   [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])

collects/typed-racket/rep/object-rep.rkt

@@ -13,7 +13,7 @@
 (def-pathelem SyntaxPE () [#:fold-rhs #:base])
 (def-pathelem ForcePE () [#:fold-rhs #:base])
 ;; t is always a Name (can't put that into the contract b/c of circularity)
-(def-pathelem StructPE ([t Type/c] [idx natural-number/c])
+(def-pathelem StructPE ([t Type?] [idx natural-number/c])
   [#:frees (λ (f) (f t))]
   [#:fold-rhs (*StructPE (type-rec-id t) idx)])
 

collects/typed-racket/rep/type-rep.rkt

@@ -25,7 +25,17 @@
           (not (ValuesDots? e))
           (not (Result? e)))))
 
+;; (or/c Type/c Values? Results?)
+(define Values/c?
+   (λ (e)
+     (and (Type? e)
+          (not (Scope? e))
+          (not (arr? e))
+          (not (fld? e))
+          (not (ValuesDots? e)))))
+
 (define Type/c (flat-named-contract 'Type Type/c?))
+(define Values/c (flat-named-contract 'Values Values/c?))
 
 ;; Name = Symbol
 
@@ -417,7 +427,7 @@
 ;; handler: the type of the prompt handler
 ;;   prompts with this tag will return a union of `body` 
 ;;   and the codomains of `handler`
-(def-type Prompt-Tagof ([body Type/c] [handler Function?])
+(def-type Prompt-Tagof ([body Type/c] [handler Type/c])
   [#:frees (λ (f) (combine-frees (list (make-invariant (f body))
                                        (make-invariant (f handler)))))]
   [#:key 'prompt-tag])
@@ -760,6 +770,7 @@
  Mu? Poly? PolyDots?
  Filter? Object?
  Type/c Type/c?
+ Values/c
  Poly-n
  PolyDots-n
  free-vars*

collects/typed-racket/typecheck/tc-structs.rkt

@@ -13,6 +13,7 @@
          racket/function
          racket/match
          racket/list
+         racket/struct-info
          (only-in racket/contract
                   listof any/c or/c
                   [->* c->*]
@@ -150,7 +151,7 @@
 
 ;; Register the approriate types to the struct bindings.
 (define/cond-contract (register-struct-bindings! sty names desc si)
-  (c-> Struct? struct-names? struct-desc? (or/c #f struct-info?) (listof def-binding?))
+  (c-> Struct? struct-names? struct-desc? (or/c #f struct-info?) (listof binding?))
 
 
   (define tvars (struct-desc-tvars desc))

collects/typed-racket/types/substitute.rkt

@@ -37,7 +37,7 @@
 
 ;; substitute-many : Hash[Name,Type] Type -> Type
 (define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
-  ((simple-substitution/c Type/c) (#:Un procedure?) . ->* . Type/c)
+  ((simple-substitution/c (or/c Values/c arr?)) (#:Un procedure?) . ->* . (or/c Values/c arr?))
   (define (sb t) (substitute-many subst t #:Un Un))
   (define names (hash-keys subst))
   (define fvs (free-vars* target))
@@ -86,7 +86,7 @@
 ;; implements angle bracket substitution from the formalism
 ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
 (define/cond-contract (substitute-dots images rimage name target)
-  ((listof Type/c) (or/c #f Type/c) symbol? Type/c . -> . Type/c)
+  ((listof Type/c) (or/c #f Type/c) symbol? (or/c arr? Values/c) . -> . (or/c arr? Values/c))
   (define (sb t) (substitute-dots images rimage name t))
   (if (or (set-member? (free-vars-names (free-idxs* target)) name)
           (set-member? (free-vars-names (free-vars* target)) name))
@@ -163,7 +163,7 @@
 ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
 ;; subst-all : substitution Type -> Type
 (define/cond-contract (subst-all s ty)
-  (substitution/c Type/c . -> . Type/c)
+  (substitution/c (or/c arr? Values/c) . -> . (or/c Values/c arr?))
 
   (define t-substs
     (for/fold ([acc (hash)]) ([(v r) (in-hash s)])