try (1+ succ-idx) types))
                (first? (not old-types)))
            (values (intmap-replace typev label entry) first?)))))

  (define (update-in-types label typev types saturate?)
    (let*-values (((typev entry) (ensure-entry typev label))
                  ((old-types) (vector-ref entry 0))
                  ;; TODO: If the label has only one predecessor, we can
                  ;; avoid the meet.
                  ((types) (if (not old-types)
                               types
                               (let ((meet (if saturate?
                                               type-entry-saturating-union
                                               type-entry-union)))
                                 (intmap-intersect old-types types meet)))))
      (if (eq? old-types types)
          (values typev #f)
          (let ((entry (vector-replace entry 0 types)))
            (values (intmap-replace typev label entry) #t)))))

  (define (propagate-types label typev succ-idx succ-label types)
    (let*-values
        (((typev first?) (update-out-types label typev types succ-idx))
         ((saturate?) (and (not first?) (<= succ-label label)))
         ((typev changed?) (update-in-types succ-label typev types saturate?)))
      (values (if changed? (list succ-label) '()) typev)))

  (define (visit-exp label typev k types exp)
    (define (propagate1 succ-label types)
      (propagate-types label typev 0 succ-label types))
    (define (propagate2 succ0-label types0 succ1-label types1)
      (let*-values (((changed0 typev)
                     (propagate-types label typev 0 succ0-label types0))
                    ((changed1 typev)
                     (propagate-types label typev 1 succ1-label types1)))
        (values (append changed0 changed1) typev)))
    ;; Each of these branches must propagate to its successors.
    (match exp
      (($ $branch kt ($ $values (arg)))
       ;; The "normal" continuation is the #f branch.
       (let ((kf-types (restrict-var types arg
                                     (make-type-entry (logior &false &nil)
                                                      0
                                                      0)))
             (kt-types (restrict-var types arg
                                     (make-type-entry
                                      (logand &all-types 
                                              (lognot (logior &false &nil)))
                                      -inf.0 +inf.0))))
         (propagate2 k kf-types kt kt-types)))
      (($ $branch kt ($ $primcall name args))
       ;; The "normal" continuation is the #f branch.
       (let ((kf-types (infer-primcall types 0 name args #f))
             (kt-types (infer-primcall types 1 name args #f)))
         (propagate2 k kf-types kt kt-types)))
      (($ $prompt escape? tag handler)
       ;; The "normal" continuation enters the prompt.
       (propagate2 k types handler types))
      (($ $primcall name args)
       (propagate1 k
                   (match (intmap-ref conts k)
                     (($ $kargs _ defs)
                      (infer-primcall types 0 name args
                                      (match defs ((var) var) (() #f))))
                     (_
                      ;; (pk 'warning-no-restrictions name)
                      types))))
      (($ $values args)
       (match (intmap-ref conts k)
         (($ $kargs _ defs)
          (let ((in types))
            (let lp ((defs defs) (args args) (out types))
              (match (cons defs args)
                ((() . ())
                 (propagate1 k out))
                (((def . defs) . (arg . args))
                 (lp defs args
                     (adjoin-var out def (var-type-entry in arg))))))))
         (_
          (propagate1 k types))))
      ((or ($ $call) ($ $callk))
       (propagate1 k types))
      (($ $rec names vars funs)
       (let ((proc-type (make-type-entry &procedure -inf.0 +inf.0)))
         (propagate1 k (adjoin-vars types vars proc-type))))
      (_
       (match (intmap-ref conts k)
         (($ $kargs (_) (var))
          (let ((entry (match exp
                         (($ $const val)
                          (constant-type val))
                         ((or ($ $prim) ($ $fun) ($ $closure))
                          ;; Could be more precise here.
                          (make-type-entry &procedure -inf.0 +inf.0)))))
            (propagate1 k (adjoin-var types var entry))))))))

  (define (visit-cont label typev)
    (let ((types (vector-ref (intmap-ref typev label) 0)))
      (define (propagate0)
        (values '() typev))
      (define (propagate1 succ-label types)
        (propagate-types label typev 0 succ-label types))
      (define (propagate2 succ0-label types0 succ1-label types1)
        (let*-values (((changed0 typev)
                       (propagate-types label typev 0 succ0-label types0))
                      ((changed1 typev)
                       (propagate-types label typev 1 succ1-label types1)))
          (values (append changed0 changed1) typev)))
      
      ;; Add types for new definitions, and restrict types of
      ;; existing variables due to side effects.
      (match (intmap-ref conts label)
        (($ $kargs names vars ($ $continue k src exp))
         (visit-exp label typev k types exp))
        (($ $kreceive arity k)
         (match (intmap-ref conts k)
           (($ $kargs names vars)
            (propagate1 k (adjoin-vars types vars all-types-entry)))))
        (($ $kfun src meta self tail clause)
         (if clause
             (propagate1 clause (adjoin-var types self all-types-entry))
             (propagate0)))
        (($ $kclause arity kbody kalt)
         (match (intmap-ref conts kbody)
           (($ $kargs _ defs)
            (let ((body-types (adjoin-vars types defs all-types-entry)))
              (if kalt
                  (propagate2 kbody body-types kalt types)
                  (propagate1 kbody body-types))))))
        (($ $ktail) (propagate0)))))

  (worklist-fold* visit-cont
                  (intset-add empty-intset kfun)
                  (compute-initial-state)))

(define (lookup-pre-type types label def)
  (let* ((entry (intmap-ref types label))
         (tentry (var-type-entry (vector-ref entry 0) def)))
    (values (type-entry-type tentry)
            (type-entry-min tentry)
            (type-entry-max tentry))))

(define (lookup-post-type types label def succ-idx)
  (let* ((entry (intmap-ref types label))
         (tentry (var-type-entry (vector-ref entry (1+ succ-idx)) def)))
    (values (type-entry-type tentry)
            (type-entry-min tentry)
            (type-entry-max tentry))))

(define (primcall-types-check? types label name args)
  (match (hashq-ref *type-checkers* name)
    (#f #f)
    (checker
     (let ((entry (intmap-ref types label)))
       (apply checker (vector-ref entry 0) args)))))