From e3f8fff0e84c05e8f9bd0c73af0bae05c7b3b7ef Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Sun, 27 Jun 2010 20:07:33 -0400
Subject: [PATCH] Generalize mutated variables when inferring types.

original commit: 90d8a3cc13dd76ba8d1eaefa98ee5e3248e43b04
---
 .../typed-scheme/private/type-annotation.rkt  | 40 ++++++++-----------
 .../typed-scheme/typecheck/tc-let-unit.rkt    | 10 ++---
 2 files changed, 21 insertions(+), 29 deletions(-)

diff --git a/collects/typed-scheme/private/type-annotation.rkt b/collects/typed-scheme/private/type-annotation.rkt
index 7bb90cb7..75c4db9a 100644
--- a/collects/typed-scheme/private/type-annotation.rkt
+++ b/collects/typed-scheme/private/type-annotation.rkt
@@ -112,49 +112,41 @@
   (map (lambda (e) (get-type e #:default default)) stxs))
 
 ;; list[identifier] stx (stx -> tc-results?) (stx tc-results? -> tc-results?) -> tc-results?
+;; stxs : the identifiers, possibly with type annotations on them
+;; expr : the RHS expression
+;; tc-expr : a function like `tc-expr' from tc-expr-unit
+;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
 (d/c (get-type/infer stxs expr tc-expr tc-expr/check)
   ((listof identifier?) syntax? (syntax? . -> . tc-results?) (syntax? tc-results? . -> . tc-results?) . -> . tc-results?)
   (match stxs
-    ['() 
-     (tc-expr/check expr (ret null))]
-    [(list stx)
-     (cond [(type-annotation stx #:infer #t)
-            => (lambda (ann)
-                 (tc-expr/check expr (ret ann)))]
-           [else (tc-expr expr)])]
     [(list stx ...)
      (let ([anns (for/list ([s stxs]) (type-annotation s #:infer #t))])
        (if (for/and ([a anns]) a)
-           (begin (tc-expr/check expr (ret anns)))
+           (tc-expr/check expr (ret anns))
            (let ([ty (tc-expr expr)])
              (match ty
-               [(tc-results: tys) 
+               [(tc-results: tys fs os) 
                 (if (not (= (length stxs) (length tys)))
                     (begin
                       (tc-error/delayed 
                                       "Expression should produce ~a values, but produces ~a values of types ~a"
                                       (length stxs) (length tys) (stringify tys))
                       (ret (map (lambda _ (Un)) stxs)))
-                    (ret 
-                     (for/list ([stx stxs] [ty tys] [a anns])
-                       (cond [a => (lambda (ann) (check-type stx ty ann) ann)]
-                             [else ty]))))]
-               [ty (tc-error/delayed 
-                    "Expression should produce ~a values, but produces one values of type ~a"
-                    (length stxs) ty)
-                   (ret (map (lambda _ (Un)) stxs))]))))]))
-
+                    (combine-results 
+                     (for/list ([stx stxs] [ty tys] [a anns] [f fs] [o os])
+                       (cond [a (check-type stx ty a) (ret a f o)]
+			     ;; mutated variables get generalized, so that we don't infer too small a type
+			     [(is-var-mutated? stx) (ret (generalize ty) f o)]
+                             [else (ret ty f o)]))))]))))]))
 
 ;; check that e-type is compatible with ty in context of stx
 ;; otherwise, error
 ;; syntax type type -> void
-
 (define (check-type stx e-type ty)
-  (let ([stx* (current-orig-stx)])
-    (parameterize ([current-orig-stx stx])
-      (unless (subtype e-type ty)
-        ;(printf "orig-stx: ~a" (syntax->datum stx*))
-        (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))
+  (parameterize ([current-orig-stx stx])
+    (unless (subtype e-type ty)
+      ;(printf "orig-stx: ~a" (syntax->datum stx*))
+      (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty))))
 
 (define (dotted? stx)
   (cond [(syntax-property stx type-dotted-symbol) => syntax-e]
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.rkt b/collects/typed-scheme/typecheck/tc-let-unit.rkt
index 32c6c355..2f64af3a 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-let-unit.rkt
@@ -1,4 +1,4 @@
-#lang scheme/unit
+#lang racket/unit
 
 (require (rename-in "../utils/utils.rkt" [infer r:infer]))
 (require "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
@@ -7,12 +7,12 @@
 	 (env lexical-env type-alias-env global-env type-env-structs)
          (rep type-rep)
          syntax/free-vars
-         mzlib/trace unstable/debug
-         scheme/match (prefix-in c: scheme/contract)
-         (except-in scheme/contract -> ->* one-of/c)
+         racket/trace unstable/debug
+         racket/match (prefix-in c: racket/contract)
+         (except-in racket/contract -> ->* one-of/c)
          syntax/kerncase syntax/parse
          (for-template 
-          scheme/base
+          racket/base
           "internal-forms.rkt"))
 
 (require (only-in srfi/1/list s:member))