Do substitution properly from dmap.

collects/typed-scheme/private/infer-unit.ss

@@ -319,23 +319,28 @@
                 [else (fail! S T)])]))))
 
 (define (subst-gen C R)
-  (for/list ([(k v) (car (car (cset-maps C)))])
+  (define (constraint->type v #:variable [variable #f])
     (match v
       [(struct c (S X T))
-       (let ([var (hash-ref (free-vars* R) X Constant)])
+       (let ([var (hash-ref (free-vars* R) (or variable X) Constant)])
-         ;(printf "variance was: ~a~nR was ~a~n" var R)
+         ;(printf "variance was: ~a~nR was ~a~nX was ~a~n" var R (or variable X))
-         (list
-          X
          (evcase var 
                  [Constant S]
                  [Covariant S]
                  [Contravariant T]
-                 [Invariant 
+                 [Invariant S]))]))
-                  #; ; don't fail, we just pretend in covariance
+  (match (car (cset-maps C))
-                  (unless (type-equal? S T)
+    [(cons cmap (struct dmap (dm)))
-                              ;(printf "invariant and not equal ~a ~a" S T)
+     (append 
-                              (fail! S T))
+      (for/list ([(k dc) dm])
-                  S])))])))
+        (match dc
+          [(struct dcon (fixed rest))
+           (list k
+                 (for/list ([f fixed])
+                   (constraint->type f #:variable k))
+                 (and rest (constraint->type rest)))]))
+      (for/list ([(k v) cmap])
+        (list k (constraint->type v))))]))
 
 (define (cgen/list X V S T)
   (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))

collects/typed-scheme/private/type-rep.ss

@@ -101,9 +101,9 @@
 (dt arr (dom rng rest drest thn-eff els-eff)
     [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom)))
                                     (match drest
-                                      [(cons t (? symbol? bnd))
+                                      #;[(cons t (? symbol? bnd))
                                        (let ([vs (free-vars* t)])
-                                         (list (flip-variances (fix-bound vs bnd))))]
+                                         (list (flip-variances vs)))]
                                       [(cons t bnd) (list (flip-variances (free-vars* t)))]
                                       [_ null])
                                     (list (free-vars* rng))
@@ -111,9 +111,9 @@
                                          (map free-vars* (append thn-eff els-eff)))))
              (combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom)))
                                     (match drest
-                                      [(cons t (? number? bnd))
+                                      #;[(cons t (? number? bnd))
                                        (let ([vs (free-idxs* t)])
-                                         (list (flip-variances (fix-bound vs bnd))))]
+                                         (list (flip-variances vs)))]
                                       [(cons t bnd) (list (flip-variances (free-idxs* t)))]
                                       [_ null])
                                     (list (free-idxs* rng))                                      

collects/typed-scheme/private/type-utils.ss

@@ -54,7 +54,6 @@
   (define (sb t) (substitute-dots images name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
-                 [#:F name* target]
                  [#:arr dom rng rest drest thn-eff els-eff
                         (if (and (pair? drest)
                                  (eq? name (cdr drest)))                            
@@ -101,7 +100,14 @@
 ;; substitution = Listof[List[Name,Type]]
 ;; subst-all : substition Type -> Type
 (define (subst-all s t)
-  (foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
+  (for/fold ([t t]) ([e s])
+    (match e
+      [(list v (list imgs ...) #f)
+       (substitute-dots imgs v t)]
+      [(list v (list ts) starred)
+       (int-err "subst-all: nyi")]
+      [(list v img)
+       (substitute img v t)])))
 
 
 ;; unfold : Type -> Type