From 44a858ba4a1808448731d23c506cb89cb2408c0e Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 25 Mar 2009 17:22:09 +0000
Subject: [PATCH 01/13] add `remove-duplicates'

svn: r14278

original commit: f48dbda950dc70be1966a352ded70bd12a339a24
---
 collects/typed-scheme/private/base-env.ss | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index f314d272..d6f49abe 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -550,6 +550,11 @@
 [last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
                        . -> . 
                        (Un (-pair a a) (-pair a (-val '())))))]
+[remove-duplicates
+ (-poly (a)
+        (cl->*
+         ((-lst a) . -> . (-lst a))
+         ((-lst a) (a a . -> . Univ) . -> . (-lst a))))]
 
 ;; scheme/tcp
 [tcp-listener? (make-pred-ty -TCP-Listener)]

From f288f984163377006863d8634ded7e9866aa2434 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Fri, 27 Mar 2009 13:47:12 +0000
Subject: [PATCH 02/13] Sam and I did some work to allow automatic inferred
 linking in (define-values/)invoke-unit/infer.

svn: r14315

original commit: 99aac7d7455c3ce9189d038f781558b6bd696424
---
 collects/typed-scheme/infer/infer.ss           | 7 ++++---
 collects/typed-scheme/typecheck/typechecker.ss | 8 +++++---
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/collects/typed-scheme/infer/infer.ss b/collects/typed-scheme/infer/infer.ss
index b8c37883..c660783e 100644
--- a/collects/typed-scheme/infer/infer.ss
+++ b/collects/typed-scheme/infer/infer.ss
@@ -3,10 +3,11 @@
 (require (except-in "../utils/utils.ss" infer))
 (require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
          "restrict.ss" "promote-demote.ss"
-         (only-in scheme/unit provide-signature-elements)
+         (only-in scheme/unit provide-signature-elements
+                  define-values/invoke-unit/infer link)
          (utils unit-utils))
          
 (provide-signature-elements restrict^ infer^)
 
-(define-values/link-units/infer
-  infer@ constraints@ dmap@ restrict@ promote-demote@)
+(define-values/invoke-unit/infer
+  (link infer@ constraints@ dmap@ restrict@ promote-demote@))
diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss
index ed935ff9..f398b18c 100644
--- a/collects/typed-scheme/typecheck/typechecker.ss
+++ b/collects/typed-scheme/typecheck/typechecker.ss
@@ -3,7 +3,9 @@
 (require "../utils/utils.ss")
 (require (utils unit-utils)
          mzlib/trace
-         (only-in scheme/unit provide-signature-elements)
+         (only-in scheme/unit
+                  provide-signature-elements
+                  define-values/invoke-unit/infer link)
          "signatures.ss" "tc-toplevel.ss"         
          "tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss"
          "tc-let-unit.ss" "tc-dots-unit.ss"
@@ -11,5 +13,5 @@
 
 (provide-signature-elements typechecker^ tc-expr^)
 
-(define-values/link-units/infer
-  tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@)
+(define-values/invoke-unit/infer
+  (link tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@))

From 474ead72a964437ad4973e263c9f560516a11181 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 31 Mar 2009 03:33:04 +0000
Subject: [PATCH 03/13] Add refinement types. Add `parse-commmand-line'

svn: r14372

original commit: cd4305ca4f395a183450b762b2c7e5be0fe4d7db
---
 .../tests/typed-scheme/succeed/cmdline.ss     | 38 +++++++++++++++++++
 .../typed-scheme/succeed/refinement-even.ss   | 15 ++++++++
 collects/typed-scheme/env/init-envs.ss        |  3 ++
 collects/typed-scheme/private/base-env.ss     | 13 +++++++
 collects/typed-scheme/private/parse-type.ss   |  9 ++++-
 collects/typed-scheme/private/prims.ss        |  7 +++-
 collects/typed-scheme/private/subtype.ss      |  3 ++
 collects/typed-scheme/rep/type-rep.ss         | 11 ++++++
 .../typed-scheme/typecheck/internal-forms.ss  |  2 +
 .../typed-scheme/typecheck/tc-toplevel.ss     | 13 ++++++-
 10 files changed, 111 insertions(+), 3 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/cmdline.ss
 create mode 100644 collects/tests/typed-scheme/succeed/refinement-even.ss

diff --git a/collects/tests/typed-scheme/succeed/cmdline.ss b/collects/tests/typed-scheme/succeed/cmdline.ss
new file mode 100644
index 00000000..61faa7b4
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/cmdline.ss
@@ -0,0 +1,38 @@
+#lang typed-scheme
+
+(require scheme/cmdline)
+
+(: version-str String)
+(define version-str "0.1")
+
+(current-command-line-arguments (vector "counter.mch"))
+
+(: verbose-mode (Parameter Boolean))
+(define verbose-mode (make-parameter #f))
+
+(: optimize-level (Parameter Integer))
+(define optimize-level (make-parameter 0))
+
+(: model-checking-mode (Parameter Any))
+(define model-checking-mode (make-parameter 'sat))
+
+(: file-to-model-check String)
+(define file-to-model-check
+ (command-line
+  #:program "eboc" ;; Should be name of executable
+  #:once-each
+  [("-v" "--verbose") "Compile with verbose messages"
+                      (verbose-mode #t)]
+  [("-m" "--mode") #{mode : String} "Mode to run the model checker on (sat, satbin)"
+                   (model-checking-mode (string-append mode))]
+  #:once-any
+  [("-o" "--optimize-1") "Compile with optimization level 1"
+                         (optimize-level 1)]
+  ["--optimize-2"        (; show help on separate lines
+                          "Compile with optimization level 2,"
+                          "which includes all of level 1")
+                         (optimize-level 2)]
+
+  #:args (#{filename : String}) ; expect one command-line argument: <filename>
+  ; return the argument as a filename to compile
+  filename))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/refinement-even.ss b/collects/tests/typed-scheme/succeed/refinement-even.ss
new file mode 100644
index 00000000..8d6d9693
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/refinement-even.ss
@@ -0,0 +1,15 @@
+#lang typed-scheme
+
+(declare-refinement even?)
+(define-type-alias Even (Refinement even?))
+
+(: x Integer)
+(define x 4)
+
+(: y Even)
+(define y (if (even? x) x (error 'bad)))
+
+(: f (Even -> String))
+(define (f e) (format "~a" e))
+
+(f y)
\ No newline at end of file
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 0b645105..71a8707f 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -29,6 +29,9 @@
      `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
     [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
     [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
+    [(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
+                                                      (quote-syntax ,pred)
+                                                      (syntax-local-certifier))]
     [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
     [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
     [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index d6f49abe..399202cc 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -545,6 +545,19 @@
 [list->string ((-lst -Char) . -> . -String)]
 [string->list (-String . -> . (-lst -Char))]
 [sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
+[find-system-path (Sym . -> . -Path)]
+
+;; scheme/cmdline
+
+[parse-command-line
+ (let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
+   (-polydots (b a)
+              (cl->* (-Pathlike 
+                      (Un (-lst -String) (-vec -String))
+                      (-lst (-pair mode-sym (-lst (-lst Univ))))
+                      ((list Univ) [a a] . ->... . b)
+                      (-lst -String)
+                      . -> . b))))]
 
 ;; scheme/list
 [last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 8cc2d1ce..187db130 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -10,7 +10,7 @@
          "union.ss"
          syntax/stx
          stxclass stxclass/util
-         (env type-environments type-name-env type-alias-env)
+         (env type-environments type-name-env type-alias-env lexical-env)
 	 "type-utils.ss"
          (prefix-in t: "base-types-extra.ss")
          scheme/match 
@@ -300,6 +300,13 @@
         (map list
              (map syntax-e (syntax->list #'(mname ...)))
              (map parse-type (syntax->list #'(mty ...)))))]
+      [(Refinement p?)
+       (and (eq? (syntax-e #'Refinement) 'Refinement)
+            (identifier? #'p?))
+       (match (lookup-type/lexical #'p?)
+              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+               (make-Refinement dom #'p? (syntax-local-certifier))]
+              [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       [(Instance t)
        (eq? (syntax-e #'Instance) 'Instance)
        (let ([v (parse-type #'t)])
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 3988110b..6bc35521 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -407,4 +407,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ [i:id t] ...)
      (syntax/loc stx
        (begin (: i t) ...
-              (provide i ...)))]))
\ No newline at end of file
+              (provide i ...)))]))
+
+(define-syntax (declare-refinement stx)
+  (syntax-parse stx
+    [(_ p:id)
+     (quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 0c2ffdb7..68de4667 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -293,6 +293,9 @@
 	      ;; single values shouldn't actually happen, but they're just like the type
 	      [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
 	      [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
+              ;; A refinement is a subtype of its parent
+              [(list (Refinement: par _ _) t)
+               (subtype* A0 par t)]
 	      ;; subtyping on other stuff
 	      [(list (Syntax: t) (Syntax: t*))
 	       (subtype* A0 t t*)]
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index ea2d2017..1a6aae41 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -209,6 +209,17 @@
 ;; value : Type
 (dt Hashtable (key value) [#:key 'hash])
 
+;; parent : Type
+;; pred : Identifier
+;; cert : Certifier
+(dt Refinement (parent pred cert)
+    [#:key (Type-key parent)]
+    [#:intern (list parent (hash-id pred))]
+    [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
+    [#:frees (free-vars* parent)
+             (free-idxs* parent)])
+    
+
 ;; t : Type
 (dt Syntax (t) [#:key 'syntax])
 
diff --git a/collects/typed-scheme/typecheck/internal-forms.ss b/collects/typed-scheme/typecheck/internal-forms.ss
index b85dd96c..a0ce6e9c 100644
--- a/collects/typed-scheme/typecheck/internal-forms.ss
+++ b/collects/typed-scheme/typecheck/internal-forms.ss
@@ -11,4 +11,6 @@
                 define-typed-struct-internal
                 define-typed-struct/exec-internal
                 assert-predicate-internal
+                declare-refinement-internal
                 :-internal)
+
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss
index f0553c1e..c415f38b 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.ss
+++ b/collects/typed-scheme/typecheck/tc-toplevel.ss
@@ -9,7 +9,7 @@
          "tc-structs.ss"
          (rep type-rep)
          (private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract)
-	 (env type-env init-envs type-name-env type-alias-env)
+	 (env type-env init-envs type-name-env type-alias-env lexical-env)
 	 (utils tc-utils)
 	 "provide-handling.ss"
          "def-binding.ss"
@@ -38,6 +38,17 @@
       ;; type aliases have already been handled by an earlier pass
       [(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
        (list)]
+
+      ;; declare-refinement
+      [(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
+       (match (lookup-type/lexical #'pred)
+              [(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
+               (register-type #'pred 
+                              (make-pred-ty (list dom)
+                                            rng
+                                            (make-Refinement dom #'pred (syntax-local-certifier))))
+               (list)]
+              [t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
       
       ;; require/typed
       [(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))

From 8c928ca0bf771cc3a99007b8ecf1bcac30708a2a Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 2 Apr 2009 03:03:44 +0000
Subject: [PATCH 04/13] Fix subtyping, printing, inference for refinement
 types.

svn: r14403

original commit: 6d07cf912830c478b22ef005bbf267cda3d06f2a
---
 collects/typed-scheme/infer/infer-unit.ss            | 3 +++
 collects/typed-scheme/private/subtype.ss             | 8 ++++----
 collects/typed-scheme/private/type-effect-printer.ss | 2 ++
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index bcfc0e85..dfc1c980 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -255,6 +255,9 @@
           [(a a) empty]
           [(_ (Univ:)) empty]
           
+          [((Refinement: S _ _) T)
+           (cg S T)]
+          
           [((F: (? (lambda (e) (memq e X)) v)) S)
            (when (match S
                    [(F: v*)
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 68de4667..ccfc78c8 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -220,6 +220,9 @@
 		       (unmatch))
 					;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
 	       (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
+              ;; A refinement is a subtype of its parent
+              [(list (Refinement: par _ _) t)
+               (subtype* A0 par t)]
 	      ;; use unification to see if we can use the polytype here
 	      [(list (Poly: vs b) s)
 	       (=> unmatch)
@@ -292,10 +295,7 @@
 	      [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
 	      ;; single values shouldn't actually happen, but they're just like the type
 	      [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
-	      [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
-              ;; A refinement is a subtype of its parent
-              [(list (Refinement: par _ _) t)
-               (subtype* A0 par t)]
+	      [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]              
 	      ;; subtyping on other stuff
 	      [(list (Syntax: t) (Syntax: t*))
 	       (subtype* A0 t t*)]
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index b5852df8..5ee756b0 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -123,6 +123,8 @@
     [(F: nm) (fp "~a" nm)]      
     [(Values: (list v ...)) (fp "~a" (cons 'values v))]
     [(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))]
+    [(Refinement: parent p? _)
+     (fp "(Refinement ~a ~a)" parent (syntax-e p?))]
     [(Param: in out) 
      (if (equal? in out)
          (fp "(Parameter ~a)" in)           

From 35a67354cae8830671d129f0f4b99c175bc51e16 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 3 Apr 2009 18:42:38 +0000
Subject: [PATCH 05/13] Require that `require/typed' uses the contracted
 version of typed identifiers.

svn: r14415

original commit: 6d302a93046299af4ccd58f8e8ea3938c258f7ac
---
 .../typed-scheme/fail/require-typed-wrong.ss  | 15 +++++++
 .../typed-scheme/private/require-contract.ss  | 31 ++++++++++---
 .../typecheck/provide-handling.ss             | 43 +++++++++++--------
 3 files changed, 66 insertions(+), 23 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/require-typed-wrong.ss

diff --git a/collects/tests/typed-scheme/fail/require-typed-wrong.ss b/collects/tests/typed-scheme/fail/require-typed-wrong.ss
new file mode 100644
index 00000000..d35a4f94
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/require-typed-wrong.ss
@@ -0,0 +1,15 @@
+#;
+(exn-pred ".*contract.*")
+#lang scheme/load
+
+(module m typed-scheme
+  (: x (Number -> Number))
+  (define (x n) (add1 n))
+  (provide x))
+
+(module n typed-scheme
+  (require (only-in 'm))
+  (require/typed 'm [x (String -> Number)])
+  (x "foo"))
+
+(require 'n)
diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss
index 73570ff2..fe767085 100644
--- a/collects/typed-scheme/private/require-contract.ss
+++ b/collects/typed-scheme/private/require-contract.ss
@@ -1,6 +1,9 @@
 #lang scheme/base
 
-(require scheme/contract (for-syntax scheme/base syntax/kerncase))
+(require scheme/contract (for-syntax scheme/base syntax/kerncase 
+                                     "../utils/tc-utils.ss"
+                                     (prefix-in tr: "typed-renaming.ss")))
+
 (provide require/contract define-ignored)
 
 (define-syntax (define-ignored stx)
@@ -20,12 +23,30 @@
                                           'inferred-name
                                           (syntax-e #'name)))])]))
 
+
+(define-syntax (get-alternate stx)
+  (syntax-case stx ()
+    [(_ id)
+     (tr:get-alternate #'id)]))
+
 (define-syntax (require/contract stx)
   (syntax-case stx ()
     [(require/contract nm cnt lib)
      (identifier? #'nm)
-     #`(begin (require (only-in lib [nm tmp]))     
-              (define-ignored nm (contract cnt tmp '(interface for #,(syntax->datum #'nm)) 'never-happen (quote-syntax nm))))]
+     (begin       
+       #`(begin (require (only-in lib [nm tmp]))     
+                (define-ignored nm 
+                  (contract cnt 
+                            (get-alternate tmp)
+                            '(interface for #,(syntax->datum #'nm))
+                            'never-happen
+                            (quote-syntax nm)))))]
     [(require/contract (orig-nm nm) cnt lib)     
-     #`(begin (require (only-in lib [orig-nm tmp]))
-              (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))
+     (begin 
+       #`(begin (require (only-in lib [orig-nm tmp]))
+                (define-ignored nm 
+                  (contract cnt 
+                            (get-alternate tmp) 
+                            '#,(syntax->datum #'nm)
+                            'never-happen
+                            (quote-syntax nm)))))]))
diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss
index 66b3576a..c2149375 100644
--- a/collects/typed-scheme/typecheck/provide-handling.ss
+++ b/collects/typed-scheme/typecheck/provide-handling.ss
@@ -5,7 +5,7 @@
          syntax/kerncase syntax/boundmap
          (env type-name-env type-alias-env)
          mzlib/trace
-         (private type-contract)
+         (private type-contract typed-renaming)
          (rep type-rep)
 	 (utils tc-utils)
          "def-binding.ss")
@@ -13,7 +13,8 @@
 (require (for-template scheme/base
                        scheme/contract))
 
-(provide remove-provides provide? generate-prov)
+(provide remove-provides provide? generate-prov
+         get-alternate)
 
 (define (provide? form)    
   (kernel-syntax-case form #f
@@ -24,6 +25,12 @@
 (define (remove-provides forms)
   (filter (lambda (e) (not (provide? e))) (syntax->list forms)))
 
+
+(define (renamer id #:alt [alt #f])
+  (if alt
+      (make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
+      (make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))
+
 (define (generate-prov stx-defs val-defs)
   (define mapping (make-free-identifier-mapping))
   (lambda (form)
@@ -54,35 +61,35 @@
                             (define/contract cnt-id #,cnt id)
                             (define-syntax export-id
                               (if (unbox typed-context?)
-                                  (make-rename-transformer (syntax-property #'id 
-                                                                            'not-free-identifier=? #t))
-                                  (make-rename-transformer (syntax-property #'cnt-id
-                                                                            'not-free-identifier=? #t))))
+                                  (renamer #'id #:alt #'cnt-id)
+                                  (renamer #'cnt-id)))
                             (#%provide (rename export-id out-id)))))]
                    [else 
-                    (with-syntax ([(export-id) (generate-temporaries #'(id))])
-                      #`(begin                             
+                    (with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
+                      #`(begin        
+                          (define-syntax error-id
+                            (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))
                           (define-syntax export-id
                             (if (unbox typed-context?)
-                                (make-rename-transformer (syntax-property #'id 
-                                                                          'not-free-identifier=? #t))
-                                (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
+                                (renamer #'id #:alt #'error-id)
+                                (renamer #'error-id)))
                           (provide (rename-out [export-id out-id]))))])))]
         [(mem? internal-id stx-defs) 
          =>
          (lambda (b)
            (with-syntax ([id internal-id]
                          [out-id external-id])
-             (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
-               #`(begin                    
+             (with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
+               #`(begin  
+                   (define-syntax error-id
+                     (lambda (stx)
+                       (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))
                    (define-syntax export-id
                      (if (unbox typed-context?)
-                         (begin
+                         (begin                           
                            (add-alias #'export-id #'id)
-                           (make-rename-transformer (syntax-property #'id 
-                                                                     'not-free-identifier=? #t)))
-                         (lambda (stx)
-                           (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
+                           (renamer #'id #:alt #'error-id))
+                         (renamer #'error-id)))
                    (provide (rename-out [export-id out-id]))))))]
         [(eq? (syntax-e internal-id) (syntax-e external-id))
          #`(provide #,internal-id)]

From 7b70ced1317e91fe23378fbb02071e49ace40ef2 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 3 Apr 2009 22:42:29 +0000
Subject: [PATCH 06/13] Report more information for untyped imported
 identifiers

svn: r14418

original commit: 2aab5762370806fb648694cbbd6cb1c44ba2fc83
---
 .../tests/typed-scheme/fail/untyped-srfi1.ss    |  7 +++++++
 collects/typed-scheme/env/lexical-env.ss        |  2 +-
 collects/typed-scheme/env/type-env.ss           |  2 +-
 collects/typed-scheme/env/type-name-env.ss      |  2 +-
 collects/typed-scheme/private/type-utils.ss     | 17 +++++++++++++++--
 5 files changed, 25 insertions(+), 5 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/untyped-srfi1.ss

diff --git a/collects/tests/typed-scheme/fail/untyped-srfi1.ss b/collects/tests/typed-scheme/fail/untyped-srfi1.ss
new file mode 100644
index 00000000..3a4ec74c
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/untyped-srfi1.ss
@@ -0,0 +1,7 @@
+#;
+(exn-pred ".*untyped identifier map.*" ".*srfi.*")
+#lang typed-scheme
+
+(require srfi/1)
+
+map
diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss
index 63a1295b..9ade4f0a 100644
--- a/collects/typed-scheme/env/lexical-env.ss
+++ b/collects/typed-scheme/env/lexical-env.ss
@@ -33,7 +33,7 @@
                                   =>
                                   (lambda (a)
                                     (-lst (substitute Univ (cdr a) (car a))))]
-                                 [else (lookup-fail (syntax-e i))]))))))
+                                 [else (lookup-fail i)]))))))
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment
diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss
index 59eb3cad..fd2b65db 100644
--- a/collects/typed-scheme/env/type-env.ss
+++ b/collects/typed-scheme/env/type-env.ss
@@ -39,7 +39,7 @@
 ;; given an identifier, return the type associated with it
 ;; if none found, calls lookup-fail
 ;; identifier -> type 
-(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))])
+(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
   (let ([v (module-identifier-mapping-get the-mapping id fail-handler)])
     (if (box? v) (unbox v) v)))
 
diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss
index 2fc2c900..f5656c13 100644
--- a/collects/typed-scheme/env/type-name-env.ss
+++ b/collects/typed-scheme/env/type-name-env.ss
@@ -35,7 +35,7 @@
 ;; given an identifier, return the type associated with it
 ;; optional argument is failure continuation - default calls lookup-fail
 ;; identifier (-> error) -> type 
-(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))])
+(define (lookup-type-name id [k (lambda () (lookup-type-fail id))])
   (begin0
     (module-identifier-mapping-get the-mapping id k)
     (add-type-name-reference id)))
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 0617aa0f..510273a2 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -29,7 +29,8 @@
          (struct-out DottedBoth)
          just-Dotted?
          tc-error/expr
-         lookup-fail)
+         lookup-fail
+         lookup-type-fail)
 
 
 ;; substitute : Type Name Type -> Type
@@ -218,4 +219,16 @@
   return)
 
 ;; error for unbound variables
-(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))
+(define (lookup-fail e) 
+  (match (identifier-binding e)
+    ['lexical (int-err "untyped lexical variable ~a" (syntax-e e))]
+    [#f (int-err "untyped top-level variable ~a" (syntax-e e))]
+    [(list _ _ nominal-source-mod nominal-source-id _ _ _)
+     (let-values ([(x y) (module-path-index-split nominal-source-mod)])
+       (cond [(and (not x) (not y))
+              (tc-error/expr "untyped identifier ~a" (syntax-e e))]
+             [else 
+              (tc-error/expr "untyped identifier ~a imported from module <~a>" (syntax-e e) x)]))]))
+
+(define (lookup-type-fail i)
+  (tc-error/expr "~a is not bound as a type" (syntax-e i)))

From b155c5e8f01f499629b764b3d97e57c825d5e8a5 Mon Sep 17 00:00:00 2001
From: Eli Barzilay <eli@racket-lang.org>
Date: Sun, 5 Apr 2009 17:46:20 +0000
Subject: [PATCH 07/13] Changed @itemize{...} to @itemize[...]  (done after
 comparing the doc tree and verifying that there are no changes). (Also fixed
 a few bugs that were in the code)

svn: r14427

original commit: c0a8a0122200209e38dff1959d79b58f847814db
---
 collects/typed-scheme/ts-guide.scrbl | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/ts-guide.scrbl b/collects/typed-scheme/ts-guide.scrbl
index 079a86fb..d3af990c 100644
--- a/collects/typed-scheme/ts-guide.scrbl
+++ b/collects/typed-scheme/ts-guide.scrbl
@@ -62,11 +62,11 @@ typed-scheme
 
 There are two differences between these programs:
 
-@itemize{
+@itemize[
   @item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
 
   @item*[@elem{The Type Annotation}]{We have added a type annotation
-for the @scheme[fib] function, using the @scheme[:] form.}  }
+for the @scheme[fib] function, using the @scheme[:] form.}  ]
 
 In general, these are most of the changes that have to be made to a
 PLT Scheme program to transform it into a Typed Scheme program.

From ac03c567169bbbaad2a924ba57115a122fd51978 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 6 Apr 2009 06:18:06 +0000
Subject: [PATCH 08/13] Fix static struct info

svn: r14433

original commit: d57f1a68a4303e0c52ca9f3e383719c3f9e4591f
---
 collects/typed-scheme/private/prims.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 6bc35521..b3a36458 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -343,7 +343,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
                                             (list #'struct-info
                                                   #'maker
                                                   #'pred
-                                                  (list #'sel ...)
+                                                  (reverse (list #'sel ...))
                                                   (list mut ...)
                                                   #f))))
                        #,(internal #'(define-typed-struct-internal nm ([fld : ty] ...) #:type-only))

From d946fc3b79bb02e505221ee33af231379bc85ed8 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 8 Apr 2009 15:04:03 +0000
Subject: [PATCH 09/13] Document typed-scheme/no-check

svn: r14465

original commit: 95988f86a2c60eed0edfd4710b9064ea035efb62
---
 collects/typed-scheme/ts-reference.scrbl | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index c2982e25..9a3bde3a 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -294,3 +294,18 @@ Other libraries can be used with Typed Scheme via
                [check-version (-> (U Symbol (Listof Any)))])
 (check-version)
 ]
+
+@section{Typed Scheme Syntax Without Type Checking}
+
+@defmodulelang[typed-scheme/no-check]
+
+On occasions where the Typed Scheme syntax is useful, but actual
+typechecking is not desired, the @schememodname[typed-scheme/no-check]
+language is useful.  It provides the same bindings and syntax as Typed
+Scheme, but does no type checking.
+
+Examples:
+
+@schememod[typed-scheme/no-check
+(: x Number)
+(define x "not-a-number")]
\ No newline at end of file

From b111dc6b989f6f49ad299b7cb279ba2de7e12ce6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 8 Apr 2009 20:24:05 +0000
Subject: [PATCH 10/13] Fix bug with match dots. Fix handling of keywords. Add
 keywords in call-with-input/output-port.

svn: r14469

original commit: ac7e87936043f80e97057c252b855159349001d6
---
 collects/tests/typed-scheme/succeed/match-dots.ss  | 8 ++++++++
 collects/tests/typed-scheme/xfail/apply-map-bug.ss | 8 ++++++++
 collects/typed-scheme/private/base-env.ss          | 9 +++++----
 collects/typed-scheme/rep/type-rep.ss              | 6 ++----
 collects/typed-scheme/typecheck/tc-app-unit.ss     | 6 +++---
 5 files changed, 26 insertions(+), 11 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/match-dots.ss
 create mode 100644 collects/tests/typed-scheme/xfail/apply-map-bug.ss

diff --git a/collects/tests/typed-scheme/succeed/match-dots.ss b/collects/tests/typed-scheme/succeed/match-dots.ss
new file mode 100644
index 00000000..c8a526c5
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/match-dots.ss
@@ -0,0 +1,8 @@
+#lang typed-scheme
+
+(require scheme/match)
+
+(: parse-sexpr : Any -> Number)
+(define (parse-sexpr sexpr)
+  (match sexpr
+    [(list #{(? symbol? a) : (Listof Symbol)} ...) 1]))
diff --git a/collects/tests/typed-scheme/xfail/apply-map-bug.ss b/collects/tests/typed-scheme/xfail/apply-map-bug.ss
new file mode 100644
index 00000000..d08a5c2f
--- /dev/null
+++ b/collects/tests/typed-scheme/xfail/apply-map-bug.ss
@@ -0,0 +1,8 @@
+
+#lang typed-scheme
+
+(: add-lists ((Listof Number) (Listof Number) * -> (Listof Number)))
+(define (add-lists lst . lsts)
+ (apply map #{+ :: (Number Number * -> Number)} lst lsts))
+
+(add-lists '(1 2 3) '(4 5 6) '(7 8 9))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 399202cc..4fbde9fb 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -419,11 +419,12 @@
 [symbol->string (Sym . -> . -String)]
 [vector-length (-poly (a) ((-vec a) . -> . -Integer))]
 
-[call-with-input-file (-poly (a) (cl-> [(-String (-Port . -> . a))  a]
-                                       [(-String (-Port . -> . a) Sym)  a]))]
+[call-with-input-file (-poly (a) (-String (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key .  a))]
+[call-with-output-file (-poly (a) (-String (-Output-Port . -> . a)
+                                   #:exists (one-of/c error 'append 'update 'replace 'truncate 'truncate/replace) #f
+                                   #:mode (Un (-val 'binary) (-val 'text)) #f 
+                                   . ->key .  a))]
 
-[call-with-output-file (-poly (a) (cl-> [(-String (-Port . -> . a))  a]
-                                        [(-String (-Port . -> . a) Sym)  a]))]
 [current-output-port (-Param -Output-Port -Output-Port)]
 [current-error-port (-Param -Output-Port -Output-Port)]
 [current-input-port (-Param -Input-Port -Input-Port)]
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index 1a6aae41..579d1cf8 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -364,8 +364,7 @@
                         (cons (sb (car drest))
                               (if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
                         #f)
-                    (for/list ([kw kws])
-                      (cons (car kw) (sb (cdr kw))))
+                    (map sb kws)
                     (map (lambda (e) (sub-eff sb e)) thn-eff)
                     (map (lambda (e) (sub-eff sb e)) els-eff))]
        [#:ValuesDots tys dty dbound
@@ -410,8 +409,7 @@
                         (cons (sb (car drest))
                               (if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
                         #f)
-                    (for/list ([kw kws])
-                      (cons (car kw) (sb (cdr kw))))
+                    (map sb kws)
                     (map (lambda (e) (sub-eff sb e)) thn-eff)
                     (map (lambda (e) (sub-eff sb e)) els-eff))]
        [#:ValuesDots tys dty dbound
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index 61b4f54b..63db7660 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -576,7 +576,7 @@
       [c:lv-clause
        #:with (#%plain-app reverse n:id) #'c.e
        #:with (v) #'(c.v ...) 
-       #:when (free-identifier=? name #'v)
+       #:when (free-identifier=? name #'n)
        (type-annotation #'v)]
       [_ #f]))
   (syntax-parse stx
@@ -757,8 +757,8 @@
      (match (tc-expr #'fn)
        [(tc-result: (Function: arities)) 
         (tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
-       [t (tc-error/expr #:return (ret (Un))
-                         "Cannot apply expression of type ~a, since it is not a function type" t)])]
+       [(tc-result: t) (tc-error/expr #:return (ret (Un))
+                                      "Cannot apply expression of type ~a, since it is not a function type" t)])]
     ;; even more special case for match
     [(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
      (and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))

From e5d7c897d40536487af2d4640f42cd822c446b70 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 9 Apr 2009 22:27:25 +0000
Subject: [PATCH 11/13] document quote for more types

svn: r14480

original commit: 2332f2f50ab0da2d6455742ce07e3d1aa3f26b86
---
 collects/typed-scheme/ts-reference.scrbl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl
index 9a3bde3a..d2911b68 100644
--- a/collects/typed-scheme/ts-reference.scrbl
+++ b/collects/typed-scheme/ts-reference.scrbl
@@ -87,7 +87,7 @@ The following base types are parameteric in their type arguments.
 types @scheme[t ...].  This can only appear as the return type of a
 function.}
 @defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
-@defform/none['sym]{where @scheme[sym] is a symbol, is the singleton type containing only that symbol}
+@defform/none['val]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
 @defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
 name or a type variable}
 @defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the

From 88b15b72198f6357206862b333b5979b0d20b7f1 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 9 Apr 2009 23:52:13 +0000
Subject: [PATCH 12/13] Fix bug with structure keys and polymorphic structs.
 Use `match*' Add test

svn: r14482

original commit: 69a3b7a70f56e01d732491d0fa001fe3c7667868
---
 .../typed-scheme/succeed/list-struct-sum.ss      | 16 ++++++++++++++++
 collects/typed-scheme/rep/type-rep.ss            |  2 +-
 collects/typed-scheme/typecheck/tc-expr-unit.ss  |  8 ++++----
 3 files changed, 21 insertions(+), 5 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/list-struct-sum.ss

diff --git a/collects/tests/typed-scheme/succeed/list-struct-sum.ss b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
new file mode 100644
index 00000000..08e7d49f
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
@@ -0,0 +1,16 @@
+
+#lang typed-scheme
+(require scheme/list)
+
+(define-type-alias (ListOf X) (U Empty (Cons X)))
+(define-struct: Empty ())
+(define-struct: (X) Cons ((first : X) (rest : (ListOf X))))
+
+(: sum ((ListOf Number) -> Number))
+(define (sum alon)
+ (cond
+   [(Empty? alon) 0]
+   [else (+ (Cons-first alon)
+            (sum (Cons-rest alon)))]))
+
+(sum (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
\ No newline at end of file
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index 579d1cf8..bd0338c5 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -106,7 +106,7 @@
                          poly?
                          pred-id
                          cert)]
-    [#:key (gensym)])
+    [#:key #f #;(gensym)])
 
 ;; kw : keyword?
 ;; ty : Type
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 133e87c6..8eb69eba 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -114,14 +114,14 @@
 ;; check-below : (/\ (Result Type -> Result)
 ;;                   (Type Type -> Type))
 (define (check-below tr1 expected)
-  (match (list tr1 expected)      
-    [(list (tc-result: t1 te1 ee1) t2)
+  (match* (tr1 expected)
+    [((tc-result: t1 te1 ee1) t2)
      (unless (subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      (ret expected)]
-    [(list t1 t2)
+    [(t1 t2)
      (unless (subtype t1 t2)
-       (tc-error/expr"Expected ~a, but got ~a" t2 t1))
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      expected]))
 
 (define (tc-expr/check form expected)

From 297a5745a65acbeb2d6b590844bd2cde5e21af35 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 10 Apr 2009 00:07:11 +0000
Subject: [PATCH 13/13] Fix polymorphic structure predicates.

svn: r14483

original commit: 929dc1d5b245e03d59eba55989c42c1a3e91954a
---
 .../tests/typed-scheme/succeed/list-struct-sum.ss     | 11 ++++++++++-
 collects/typed-scheme/typecheck/tc-structs.ss         |  6 +++++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/list-struct-sum.ss b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
index 08e7d49f..d448eac8 100644
--- a/collects/tests/typed-scheme/succeed/list-struct-sum.ss
+++ b/collects/tests/typed-scheme/succeed/list-struct-sum.ss
@@ -13,4 +13,13 @@
    [else (+ (Cons-first alon)
             (sum (Cons-rest alon)))]))
 
-(sum (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
\ No newline at end of file
+
+(: sum2 ((ListOf Number) -> Number))
+(define (sum2 alon)
+ (cond
+   [(Empty? alon) 0]
+   [(Cons? alon) (+ (Cons-first alon)
+                    (sum2 (Cons-rest alon)))]))
+
+(sum (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
+(sum2 (make-Cons 5 (make-Cons 3 (make-Cons 1 (make-Empty)))))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss
index 207e34d7..e48ff90b 100644
--- a/collects/typed-scheme/typecheck/tc-structs.ss
+++ b/collects/typed-scheme/typecheck/tc-structs.ss
@@ -87,6 +87,7 @@
 (define (mk/register-sty nm flds parent parent-field-types types 
                          #:wrapper [wrapper values] 
                          #:type-wrapper [type-wrapper values]
+                         #:pred-wrapper [pred-wrapper values]
                          #:mutable [setters? #f]
                          #:proc-ty [proc-ty #f]
                          #:maker [maker* #f]
@@ -105,6 +106,7 @@
         (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? 
                                #:wrapper wrapper
                                #:type-wrapper type-wrapper
+                               #:pred-wrapper pred-wrapper
                                #:maker (or maker* maker)
                                #:constructor-return cret))))
 
@@ -114,6 +116,7 @@
 (define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
                                #:wrapper [wrapper values]
                                #:type-wrapper [type-wrapper values]
+                               #:pred-wrapper [pred-wrapper values]
                                #:maker [maker* #f]
                                #:constructor-return [cret #f])
   ;; create the approriate names that define-struct will bind
@@ -126,7 +129,7 @@
      (list (cons (or maker* maker) 
                  (wrapper (->* external-fld-types (if cret cret name))))
            (cons pred
-                 (make-pred-ty (wrapper name))))
+                 (make-pred-ty (pred-wrapper name))))
      (map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
      (if setters?
          (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
@@ -168,6 +171,7 @@
                    ;; wrap everything in the approriate forall
                    #:wrapper (lambda (t) (make-Poly tvars t))
                    #:type-wrapper (lambda (t) (make-App t new-tvars #f))
+                   #:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t))
                    #:poly? #t))