From 683ebb1023bbe51a3453a32411d3f8c84728f983 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@indiana.edu>
Date: Mon, 22 Dec 2014 12:34:48 -0500
Subject: [PATCH 1/3] printer fix for paths

---
 typed-racket-lib/typed-racket/types/printer.rkt | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 4a5e2b07..3a356ee3 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -130,8 +130,9 @@
     [(CarPE:) 'car]
     [(CdrPE:) 'cdr]
     [(ForcePE:) 'force]
-    [(StructPE: t i) `(,(pathelem->sexp t) ,i)]
-    [else `(Unknown Path Element: ,(struct->vector pathelem))]))
+    [(StructPE: t i) `(,(type->sexp t)-,i)]
+    [(SyntaxPE:) 'syntax]
+    [else `(Invalid Path-Element: ,(struct->vector pathelem))]))
 
 ;; object->sexp : Object -> S-expression
 ;; Print an Object (see object-rep.rkt) to the given port

From 53d1d8a15df1be58d23951e492fd97f37d8c0da0 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@indiana.edu>
Date: Mon, 22 Dec 2014 12:35:15 -0500
Subject: [PATCH 2/3] restrict structural recursion

---
 .../typed-racket/infer/restrict.rkt           | 83 +++++++++++++------
 1 file changed, 57 insertions(+), 26 deletions(-)

diff --git a/typed-racket-lib/typed-racket/infer/restrict.rkt b/typed-racket-lib/typed-racket/infer/restrict.rkt
index 84008896..5318e8c8 100644
--- a/typed-racket-lib/typed-racket/infer/restrict.rkt
+++ b/typed-racket-lib/typed-racket/infer/restrict.rkt
@@ -2,36 +2,67 @@
 
 (require "../utils/utils.rkt")
 (require (rep type-rep)
-         (types union subtype remove-intersect resolve)
+         (types abbrev base-abbrev union subtype remove-intersect resolve)
          "signatures.rkt"
-         racket/match)
+         racket/match
+         racket/set)
 
 (import infer^)
 (export restrict^)
 
-;; we don't use union map directly, since that might produce too many elements
-  (define (union-map f l)
-    (match l
-      [(Union: es)
-       (let ([l (map f es)])
-         (apply Un l))]))
 
-;; NEW IMPL
 ;; restrict t1 to be a subtype of t2
-;; if `f' is 'new, use t2 when giving up, otherwise use t1
-(define (restrict* t1 t2 [f 'new])
-  (cond
-    [(subtype t1 t2) t1] ;; already a subtype
-    [(match t2 
-       [(Poly: vars t)
-        (and (infer vars null (list t1) (list t) #f) t1)]
-       [_ #f])]
-    [(Union? t1) (union-map (lambda (e) (restrict* e t2 f)) t1)]
-    [(Union? t2) (union-map (lambda (e) (restrict* t1 e f)) t2)]
-    [(needs-resolving? t1) (restrict* (resolve-once t1) t2 f)]
-    [(needs-resolving? t2) (restrict* t1 (resolve-once t2) f)]
-    [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
-    [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
-    [else (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt
-
-(define restrict restrict*)
+;; if `pref' is 'new, use t2 when giving up, otherwise use t1
+(define (restrict t1 t2 [pref 'new])
+  ;; build-type: build a type while propogating bottom
+  (define (build-type constructor . args)
+    (if (memf Bottom? args) -Bottom (apply constructor args)))
+  ;; resolved is a set tracking previously seen restrict cases
+  ;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
+  ;; subtyping performs a similar check for the same
+  ;; reason
+  (define (restrict* t1 t2 pref resolved)
+    (match* (t1 t2)
+      ;; already a subtype
+      [(_ _) #:when (subtype t1 t2) 
+             t1]
+      
+      ;; polymorphic restrict
+      [(_ (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f)
+                          t1]
+      
+      ;; structural recursion on types
+      [((Pair: a1 d1) (Pair: a2 d2)) 
+       (build-type -pair 
+                   (restrict* a1 a2 pref resolved) 
+                   (restrict* d1 d2 pref resolved))]
+      ;; FIXME: support structural updating for structs when structs are updated to
+      ;; contain not only *if* they are polymorphic, but *which* fields are too  
+      ;;[((Struct: _ _ _ _ _ _)
+      ;; (Struct: _ _ _ _ _ _))]
+      [((Syntax: t1*) (Syntax: t2*))
+       (build-type -Syntax (restrict* t1* t2* pref resolved))]
+      [((Promise: t1*) (Promise: t2*))
+       (build-type -Promise (restrict* t1* t2* pref resolved))]
+      
+      ;; unions
+      [((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))]
+      [(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))]
+      
+      ;; resolve resolvable types if we haven't already done so
+      [((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
+                                (restrict* (resolve-once t1) t2 pref (set-add resolved (cons t1 t2)))]
+      [(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
+                                (restrict* t1 (resolve-once t2) pref (set-add resolved (cons t1 t2)))]
+      
+      ;; we don't actually want this - want something that's a part of t1
+      [(_ _) #:when (subtype t2 t1)
+             t2]
+      
+      ;; there's no overlap, so the restriction is empty
+      [(_ _) #:when (not (overlap t1 t2)) 
+             (Un)]
+      
+      ;; t2 and t1 have a complex relationship, so we punt
+      [(_ _) (if (eq? pref 'new) t2 t1)]))
+  (restrict* t1 t2 pref (set)))

From e1b8eff1f976511e723de389ac8d7c6840c7ed43 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andmkent@indiana.edu>
Date: Mon, 22 Dec 2014 12:35:30 -0500
Subject: [PATCH 3/3] initial let-aliasing addition

---
 .../scribblings/guide/occurrence.scrbl        | 36 +++++++++
 .../typed-racket/env/lexical-env.rkt          | 76 +++++++++++++++++--
 .../typed-racket/env/type-env-structs.rkt     | 64 ++++++++++++----
 .../typecheck/check-class-unit.rkt            | 12 +--
 .../typed-racket/typecheck/tc-envops.rkt      | 38 ++++++----
 .../typed-racket/typecheck/tc-expr-unit.rkt   | 14 +++-
 .../typed-racket/typecheck/tc-lambda-unit.rkt |  7 +-
 .../typed-racket/typecheck/tc-let-unit.rkt    | 34 ++++++---
 typed-racket-test/succeed/aliasing-tests.rkt  | 41 ++++++++++
 typed-racket-test/succeed/slow-check.rkt      | 44 +++++------
 .../unit-tests/typecheck-tests.rkt            | 74 +++++++++++++++++-
 11 files changed, 354 insertions(+), 86 deletions(-)
 create mode 100644 typed-racket-test/succeed/aliasing-tests.rkt

diff --git a/typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl b/typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl
index 50222539..4fa76ce3 100644
--- a/typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl
@@ -157,3 +157,39 @@ interactions, which may include mutations. It is possible to work
 around this by moving the variable inside of a module or into a local
 binding form like @racket[let].
 
+@section{@racket[let]-aliasing}
+
+Typed Racket is able to reason about some cases when variables introduced 
+by let-expressions alias other values (e.g. when they alias non-mutated identifiers, 
+@racket[car]/@racket[cdr]/@racket[struct] accesses into immutable values, etc...). 
+This allows programs which explicitly rely on occurrence typing and aliasing to 
+typecheck:
+
+@racketblock+eval[#:eval the-eval
+(: f (Any -> Number))
+(define (f x) 
+  (let ([y x])
+    (cond
+      [(number? y) x]
+      [(and (pair? y) 
+            (number? (car y)))
+       (car x)]
+      [else 42])))
+]
+
+It also allows the typechecker to check programs which use macros 
+that heavily rely on let-bindings internally (such as @racket[match]):
+
+@racketblock+eval[#:eval the-eval
+(: g (Any -> Number))
+(define (g x) 
+  (match x
+    [(? number?) x]
+    [`(_ . (_ . ,(? number?))) (cddr x)]
+    [`(_ . (_ . ,(? pair? p))) 
+     (if (number? (caddr x))
+         (car p)
+         41)]
+    [_ 42]))    
+]
+
diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt
index 329c765f..1bf2e9d8 100644
--- a/typed-racket-lib/typed-racket/env/lexical-env.rkt
+++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt
@@ -7,19 +7,26 @@
 ;; but split here for performance
 
 (require "../utils/utils.rkt"
-         racket/keyword-transform racket/list
+         racket/keyword-transform racket/list racket/match racket/set
          (for-syntax syntax/parse racket/base)
          (contract-req)
          (env type-env-structs global-env mvar-env)
+         (rep object-rep type-rep rep-utils)
          (utils tc-utils)
          (only-in (rep type-rep) Type/c)
          (typecheck renamer)
+         (types subtype resolve union)
          (except-in (types utils abbrev kw-types) -> ->* one-of/c))
 
-(provide lexical-env with-lexical-env with-lexical-env/extend
+(provide lexical-env 
+         with-lexical-env 
+         with-lexical-env/extend-types
+         with-lexical-env/extend-types+aliases
          update-type/lexical)
 (provide/cond-contract
- [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))])
+ [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
+ [lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]
+ [path-type ((listof PathElem?) Type/c . -> . Type/c)])
 
 ;; the current lexical environment
 (define lexical-env (make-parameter empty-prop-env))
@@ -29,9 +36,12 @@
   (parameterize ([lexical-env e]) . b))
 
 ;; run code in an extended env
-(define-syntax-rule (with-lexical-env/extend is ts . b)
+(define-syntax-rule (with-lexical-env/extend-types is ts . b)
   (with-lexical-env (extend/values (lexical-env) is ts) . b))
 
+;; run code in an extended env + an alias extension
+(define-syntax-rule (with-lexical-env/extend-types+aliases is ts os . b)
+  (with-lexical-env (extend+alias/values (lexical-env) is ts os) . b))
 
 ;; find the type of identifier i, looking first in the lexical env, then in the top-level env
 ;; identifier -> Type
@@ -54,8 +64,8 @@
                                            => (λ (prop)
                                                 (define orig (car (flatten prop)))
                                                 (define pre-t
-                                                  (lookup-type/lexical orig env
-                                                    #:fail (lambda (i) (lookup-fail i) #f)))
+                                                  (lookup-type/lexical 
+                                                   orig env #:fail (lambda (i) (lookup-fail i) #f)))
                                                 (define t (if pre-t
                                                               (kw-convert pre-t #f)
                                                               Err))
@@ -63,6 +73,10 @@
                                                 t)]
                                           [else ((or fail lookup-fail) i)]))))))
 
+;; looks up the representative object for an id (i.e. itself or an alias if one exists)
+(define (lookup-alias/lexical i [env (lexical-env)])
+  (lookup-alias env i -id-path))
+
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment
@@ -86,3 +100,53 @@
                     [new-v (f i v)]
                     [new-env (extend env i new-v)])
                new-env)))]))
+
+;; returns the result of following a path into a type
+;; (Listof PathElem) Type -> Type
+;; Ex. '(CarPE) (Pair α β) -> α
+;; resolved is the set of resolved types so far at a particular
+;; path - it ensures we are making progress, that we do not
+;; continue unfolding types infinitely while not progressing.
+;; It is intentionally reset each time we decrease the
+;; paths size on a recursive call, and maintained/extended
+;; when the path does not decrease on a recursive call.
+(define (path-type path t [resolved (set)])
+  (match* (t path)
+    ;; empty path
+    [(t (list)) t]
+    
+    ;; pair ops
+    [((Pair: t s) (list rst ... (CarPE:)))
+     (path-type rst t)]
+    [((Pair: t s) (list rst ... (CdrPE:)))
+     (path-type rst s)]
+
+    ;; syntax ops
+    [((Syntax: t) (list rst ... (SyntaxPE:)))
+     (path-type rst t)]
+
+    ;; promise op
+    [((Promise: t) (list rst ... (ForcePE:)))
+     (path-type rst t)]
+
+    ;; struct ops
+    [((Struct: nm par flds proc poly pred)
+      (list rst ... (StructPE: (? (λ (s) (subtype t s)) s) idx)))
+     (match-let ([(fld: ft _ _) (list-ref flds idx)])
+       (path-type rst ft))]
+    
+    [((Union: ts) _)
+     (apply Un (map (λ (t) (path-type path t resolved)) ts))]
+    
+    ;; paths into polymorphic types
+    [((Poly: _ body-t) _) (path-type path body-t resolved)]
+    [((PolyDots: _ body-t) _) (path-type path body-t resolved)]
+    [((PolyRow: _ _ body-t) _) (path-type path body-t resolved)]
+    
+    ;; types which need resolving
+    [((? needs-resolving?) _) #:when (not (set-member? resolved t))
+     (path-type path (resolve-once t) (set-add resolved t))]
+    
+    ;; type/path mismatch =(
+    [(_ _)
+     (int-err "\n\tBad path/type lookup!\n\tPath:~a\n\tType: ~a\n" path t)]))
diff --git a/typed-racket-lib/typed-racket/env/type-env-structs.rkt b/typed-racket-lib/typed-racket/env/type-env-structs.rkt
index 8990cb28..34562975 100644
--- a/typed-racket-lib/typed-racket/env/type-env-structs.rkt
+++ b/typed-racket-lib/typed-racket/env/type-env-structs.rkt
@@ -3,13 +3,16 @@
 (require racket/match
          syntax/id-table
          (except-in "../utils/utils.rkt" env)
-         (contract-req))
+         (contract-req)
+         (rep object-rep))
 
 (require-for-cond-contract (rep type-rep filter-rep))
 
 ;; types is a free-id-table of identifiers to types
 ;; props is a list of known propositions
-(define-struct/cond-contract env ([types immutable-free-id-table?] [props (listof Filter/c)])
+(define-struct/cond-contract env ([types immutable-free-id-table?] 
+                                  [props (listof Filter/c)]
+                                  [aliases immutable-free-id-table?])
   #:transparent
   #:property prop:custom-write
   (lambda (e prt mode)
@@ -22,33 +25,62 @@
   [lookup (env? identifier? (identifier? . -> . any) . -> . any)]
   [env-props (env? . -> . (listof Filter/c))]
   [replace-props (env? (listof Filter/c) . -> . env?)]
-  [empty-prop-env env?])
+  [empty-prop-env env?]
+  [extend+alias/values (env? (listof identifier?) (listof Type/c) (listof Object?) . -> . env?)]
+  [lookup-alias (env? identifier? (identifier? . -> . (or/c #f Object?)) . -> . (or/c #f Object?))])
 
 (define empty-prop-env
   (env
     (make-immutable-free-id-table)
-    null))
+    null
+    (make-immutable-free-id-table)))
 
 
 (define (replace-props e props)
-  (match e
-    [(env tys _)
-     (env tys props)]))
+  (match-let ([(env tys _ als) e])
+    (env tys props als)))
 
 (define (lookup e key fail)
-  (match e
-    [(env tys _) (free-id-table-ref tys key (λ () (fail key)))]))
+  (match-let ([(env tys _ _) e])
+    (free-id-table-ref tys key (λ () (fail key)))))
 
 
 ;; extend that works on single arguments
 (define (extend e k v)
   (extend/values e (list k) (list v)))
 
-;; takes two lists of identifiers and types to be added
+;; extends an environment with types (no aliases)
 (define (extend/values e ks vs)
-  (match e
-    [(env tys p)
-     (env
-       (for/fold ([tys tys]) ([k (in-list ks)] [v (in-list vs)])
-         (free-id-table-set tys k v))
-       p)]))
+  (match-let* ([(env tys ps als) e]
+               [tys* (for/fold ([tys tys]) ([k (in-list ks)] [v (in-list vs)])
+                       (free-id-table-set tys k v))])
+    (env tys* ps als)))
+
+;; extends an environment with types and aliases
+(define (extend+alias/values e ids ts os)
+  (match-let*-values 
+   ([((env tys ps als)) e]
+    [(tys* als*) (for/fold ([tys tys]
+                            [als als]) 
+                           ([id (in-list ids)] 
+                            [t (in-list ts)]
+                            [o (in-list os)])
+                   (match o
+                     ;; no alias, so just record the type as usual
+                     [(Empty:)
+                      (values (free-id-table-set tys id t) als)]
+                     ;; id is aliased to an identifier
+                     [(Path: '() id*)
+                      ;; record the alias relation *and* type of that alias id
+                      (values (free-id-table-set tys id* t) 
+                              (free-id-table-set als id o))]
+                     ;; id is aliased to an object with a non-empty path
+                     [(Path: p x)
+                      ;; just record the alias
+                      (values tys (free-id-table-set als id o))]))])
+   (env tys* ps als*)))
+
+(define (lookup-alias e key fail)
+  (match-let ([(env _ _ als) e])
+    (free-id-table-ref als key (λ () (fail key)))))
+
diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
index c137d03b..b768dc58 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
@@ -450,32 +450,32 @@
                                local-private-table private-method-types
                                self-type))
   (do-timestamp "built local tables")
-  (with-lexical-env/extend lexical-names/top-level lexical-types/top-level
+  (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
     (check-super-new super-new super-inits super-init-rest))
   (do-timestamp "checked super-new")
-  (with-lexical-env/extend lexical-names/top-level lexical-types/top-level
+  (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
     (for ([stx other-top-level-exprs])
       (tc-expr stx)))
   (do-timestamp "checked other top-level exprs")
-  (with-lexical-env/extend lexical-names/top-level lexical-types/top-level
+  (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
     (check-field-set!s (hash-ref parse-info 'initializer-body)
                        local-field-table
                        inits))
   (do-timestamp "checked field initializers")
   (define checked-method-types
-    (with-lexical-env/extend lexical-names lexical-types
+    (with-lexical-env/extend-types lexical-names lexical-types
       (check-methods (append (hash-ref parse-info 'pubment-names)
                              (hash-ref parse-info 'overridable-names))
                      internal-external-mapping method-stxs
                      methods self-type)))
   (do-timestamp "checked methods")
   (define checked-augment-types
-    (with-lexical-env/extend lexical-names lexical-types
+    (with-lexical-env/extend-types lexical-names lexical-types
       (check-methods (hash-ref parse-info 'augment-names)
                      internal-external-mapping method-stxs
                      augments self-type)))
   (do-timestamp "checked augments")
-  (with-lexical-env/extend lexical-names lexical-types
+  (with-lexical-env/extend-types lexical-names lexical-types
     (check-private-methods method-stxs (hash-ref parse-info 'private-names)
                            private-method-types self-type))
   (do-timestamp "checked privates")
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index 67fdf3a8..3b9e95e4 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -16,48 +16,54 @@
                     [one-of/c -one-of/c])
          (typecheck tc-metafunctions))
 
-(provide
-  with-lexical-env/extend-props)
+(provide with-lexical-env/extend-props)
+
 
 (define/cond-contract (update t ft pos? lo)
   (Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
+  ;; build-type: build a type while propogating bottom
+  (define (build-type constructor . args)
+    (if (memf Bottom? args) -Bottom (apply constructor args)))
   (match* ((resolve t) lo)
     ;; pair ops
     [((Pair: t s) (list rst ... (CarPE:)))
-     (-pair (update t ft pos? rst) s)]
+     (build-type -pair (update t ft pos? rst) s)]
     [((Pair: t s) (list rst ... (CdrPE:)))
-     (-pair t (update s ft pos? rst))]
+     (build-type -pair t (update s ft pos? rst))]
 
     ;; syntax ops
     [((Syntax: t) (list rst ... (SyntaxPE:)))
-     (-Syntax (update t ft pos? rst))]
+     (build-type -Syntax (update t ft pos? rst))]
 
     ;; promise op
     [((Promise: t) (list rst ... (ForcePE:)))
-     (-Promise (update t ft pos? rst))]
+     (build-type -Promise (update t ft pos? rst))]
 
     ;; struct ops
     [((Struct: nm par flds proc poly pred)
       (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)))
-     (make-Struct nm par
-                  (list-update flds idx (match-lambda
-                                          [(fld: e acc-id #f)
-                                           (make-fld (update e ft pos? rst) acc-id #f)]
-                                          [_ (int-err "update on mutable struct field")]))
-                  proc poly pred)]
+     ;; note: this updates fields regardless of whether or not they are
+     ;; a polymorphic field. Because subtyping is nominal and accessor 
+     ;; functions do not reflect this, this behavior is unobservable
+     ;; except when an a variable aliases the field in a let binding
+     (build-type make-Struct nm par
+                 (list-update flds idx (match-lambda
+                                         [(fld: e acc-id #f)
+                                          (make-fld (update e ft pos? rst) acc-id #f)]
+                                         [_ (int-err "update on mutable struct field")]))
+                 proc poly pred)]
 
     ;; otherwise
-    [(t (list))
+    [(t '())
      (if pos?
          (restrict t ft)
          (remove t ft))]
     [((Union: ts) lo)
-     (apply Un (map (lambda (t) (update t ft pos? lo)) ts))]
+     (apply Un (map (λ (t) (update t ft pos? lo)) ts))]
     [(t* lo)
      ;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
      ;; dosen't happen
-     #;
-     (int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
+     ;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
      t]))
 
 ;; Returns #f if anything becomes (U)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 563f8065..44039eaf 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -7,7 +7,7 @@
          "check-below.rkt" "../types/kw-types.rkt"
          (types utils abbrev union subtype type-table filter-ops remove-intersect resolve generalize)
          (private-in syntax-properties)
-         (rep type-rep filter-rep)
+         (rep type-rep filter-rep object-rep)
          (only-in (infer infer) restrict)
          (utils tc-utils)
          (env lexical-env)
@@ -41,8 +41,16 @@
   (--> identifier? full-tc-results/c)
   (define rename-id (contract-rename-id-property id))
   (define id* (or rename-id id))
-  (define ty (lookup-type/lexical id*))
-  (define obj (-id-path id*))
+  ;; see if id* is an alias for an object
+  ;; if not (-id-path id*) is returned
+  (define obj (lookup-alias/lexical id*))
+  (define-values (alias-path alias-id)
+    (match obj
+      [(Path: p x) (values p x)]
+      [(Empty:) (values (list) id*)]))
+  ;; calculate the type, resolving aliasing and paths if necessary
+  (define ty (path-type alias-path (lookup-type/lexical alias-id)))
+  
   (ret ty
        (if (overlap ty (-val #f))
            (-FS (-not-filter (-val #f) obj) (-filter (-val #f) obj))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index 08627eaa..f6cde47a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -81,7 +81,7 @@
   (make-arr*
     arg-types
     (abstract-results
-      (with-lexical-env/extend
+      (with-lexical-env/extend-types
         (append rest-names arg-names)
         (append rest-types arg-types)
         (tc-body/check body expected))
@@ -507,8 +507,9 @@
 (define (tc/rec-lambda/check formals* body name args return)
   (define formals (syntax->list formals*))
   (define ft (t:->* args (tc-results->values return)))
-  (with-lexical-env/extend
-   (cons name formals) (cons ft args)
+  (with-lexical-env/extend-types
+   (cons name formals) 
+   (cons ft args)
    (values
      (replace-names (map (λ (f) (list f -empty-obj)) (cons name formals)) (ret ft))
      (replace-names (map (λ (f) (list f -empty-obj)) (cons name formals)) (tc-body/check body return)))))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index 0e86abd3..1807e64d 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -6,7 +6,7 @@
          (private type-annotation parse-type syntax-properties)
          (env lexical-env type-alias-helper mvar-env
               global-env scoped-tvar-env)
-         (rep filter-rep)
+         (rep filter-rep object-rep)
          syntax/free-vars
          (typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops)
          (utils tarjan)
@@ -43,33 +43,43 @@
    . -> .
    tc-results/c)
   (with-cond-contract t/p ([expected-types (listof (listof Type/c))]
+                           [objs           (listof (listof Object?))]
                            [props          (listof (listof Filter?))])
-    (define-values (expected-types props)
-      (for/lists (e p)
+    (define-values (expected-types objs props)
+      (for/lists (e o p)
         ([e-r   (in-list expected-results)]
          [names (in-list namess)])
         (match e-r
           [(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...)
            (values e-ts
+                   os
                    (apply append
                           (for/list ([n (in-list names)]
                                      [t (in-list e-ts)]
                                      [f+ (in-list fs+)]
-                                     [f- (in-list fs-)])
+                                     [f- (in-list fs-)]
+                                     [o (in-list os)])
                             (cond
                               [(not (overlap t (-val #f)))
                                (list f+)]
                               [(is-var-mutated? n)
                                (list)]
-                              [else
-                               (list (-imp (-not-filter (-val #f) n) f+)
-                                     (-imp (-filter (-val #f) n) f-))]))))]
+                              ;; n is being bound to an expression w/ object o
+                              ;; we don't need any new info, aliasing and the
+                              ;; lexical environment will have the needed info
+                              [(Path? o) (list)]
+                              ;; n is being bound to an expression w/o an object
+                              ;; so remember n in our propositions
+                              [else (list (-or (-and (-not-filter (-val #f) n) f+)
+                                               (-and (-filter (-val #f) n) f-)))]))))]
           [(list (tc-result: e-ts (NoFilter:) _) ...)
            (values e-ts null)]))))
   ;; extend the lexical environment for checking the body
-  (with-lexical-env/extend
+  ;; with types and potential aliases
+  (with-lexical-env/extend-types+aliases
     (append* namess)
     (append* expected-types)
+    (append* objs)
     (replace-names
       (get-names+objects namess expected-results)
       (with-lexical-env/extend-props
@@ -223,9 +233,11 @@
              (get-type/infer names expr
                              (lambda (e) (tc-expr/maybe-expected/t e names))
                              tc-expr/check))
-           (with-lexical-env/extend names ts
-             (replace-names (map list names os)
-               (loop (cdr clauses))))])))
+           (with-lexical-env/extend-types 
+            names 
+            ts
+            (replace-names (map list names os)
+                           (loop (cdr clauses))))])))
 
 ;; this is so match can provide us with a syntax property to
 ;; say that this binding is only called in tail position
diff --git a/typed-racket-test/succeed/aliasing-tests.rkt b/typed-racket-test/succeed/aliasing-tests.rkt
new file mode 100644
index 00000000..ea084e85
--- /dev/null
+++ b/typed-racket-test/succeed/aliasing-tests.rkt
@@ -0,0 +1,41 @@
+#lang typed/racket
+
+
+;; This checks that restrict can successfully update
+;; by unfolding recursive definitions and structurally updating
+;; down car/cdr paths
+(define: (number-of-macro-definitions [expr : Sexp]) : Number
+  (match expr
+    [`(define-syntaxes (,s . ,z ). ,_ ) ;`(define-syntaxes (,s ...) ,_ ...)
+     (if (and (list?  expr) (list? z))
+         (length (cons s z));;s -> cadr expr
+         (error "corrupted file"))]
+    [_ 0]))
+(define: (num-of-define-syntax [exprs : (Listof Sexp)]) : Number
+  (foldl (lambda: ([t : Sexp] [r : Number]) (+ (number-of-macro-definitions t) r)) 0 exprs))
+
+(struct snafu ([x : Number]))
+
+#;(define (foo [f : snafu]) : Integer ;; doesn't (i.e. shouldn't) typecheck
+  (if (exact-integer? (snafu-x f))
+      (snafu-x f)
+      42))
+
+#;(define (goo [f : snafu]) : Integer ;; doesn't (i.e. shouldn't) typecheck
+  (let ([n (snafu-x f)])
+    (if (exact-integer? n)
+        (snafu-x f)
+        42)))
+
+(define (bar [f : snafu]) : Integer
+  (let ([n (snafu-x f)])
+    (if (exact-integer? n)
+        n
+        42)))
+
+(define (baz [f : snafu]) : Integer
+  (let ([n (snafu-x f)])
+    (if (exact-integer? (snafu-x f))
+        n
+        42)))
+
diff --git a/typed-racket-test/succeed/slow-check.rkt b/typed-racket-test/succeed/slow-check.rkt
index 6ee118d8..48826cd8 100644
--- a/typed-racket-test/succeed/slow-check.rkt
+++ b/typed-racket-test/succeed/slow-check.rkt
@@ -19,29 +19,27 @@
                             (match x
                               [(list _ (list (list (? number? x) y (? number? xs) ys))) 1]
                               [_ 2])]))
-
-; typechecking this will be fast after implications are removed
-;
-;                       (: filters-more (-> Boolean Boolean Boolean Boolean Boolean 
-;                                           Boolean Boolean Boolean Boolean Natural))
-;                       (define (filters-more inc1? inc2? inc3? a-min? 
-;                                             a-max? b-min? b-max? c-min? c-max?)
-;                         (let-values ([(a-min? a-max?)  (if inc1? 
-;                                                            (values a-min? a-max?) 
-;                                                            (values a-max? a-min?))]
-;                                      [(b-min? b-max?)  (if inc2? 
-;                                                            (values b-min? b-max?) 
-;                                                            (values b-max? b-min?))]
-;                                      [(c-min? c-max?)  (if inc3? 
-;                                                            (values c-min? c-max?) 
-;                                                            (values c-max? c-min?))])
-;                           (cond [a-min?  0]
-;                                 [b-min?  1]
-;                                 [a-max?  2]
-;                                 [b-max?  3]
-;                                 [c-min?  4]
-;                                 [c-max?  5]
-;                                 [else    6])))
+                       
+                       (: filters-more (-> Boolean Boolean Boolean Boolean Boolean 
+                                           Boolean Boolean Boolean Boolean Natural))
+                       (define (filters-more inc1? inc2? inc3? a-min? 
+                                             a-max? b-min? b-max? c-min? c-max?)
+                         (let-values ([(a-min? a-max?)  (if inc1? 
+                                                            (values a-min? a-max?) 
+                                                            (values a-max? a-min?))]
+                                      [(b-min? b-max?)  (if inc2? 
+                                                            (values b-min? b-max?) 
+                                                            (values b-max? b-min?))]
+                                      [(c-min? c-max?)  (if inc3? 
+                                                            (values c-min? c-max?) 
+                                                            (values c-max? c-min?))])
+                           (cond [a-min?  0]
+                                 [b-min?  1]
+                                 [a-max?  2]
+                                 [b-max?  3]
+                                 [c-min?  4]
+                                 [c-max?  5]
+                                 [else    6])))
                        
                        (: bar : Any → Any)
                        (define (bar s)
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 7c8d94e6..07e2c067 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -273,6 +273,7 @@
   racket/future
   racket/list
   racket/math
+  racket/match
   racket/path
   racket/place
   racket/port
@@ -320,7 +321,6 @@
               (-filter (-val #f) var))
          (make-Path null var))))
 
-
 (define tests
   (test-suite
     "Typechecker tests"
@@ -3354,7 +3354,77 @@
        [tc-e ((letrec ((loop (lambda: ([x : (Listof Integer)]) (cond ((null? (cdr x)) #t) (else #f))))) loop)
               (list 1 2))
              -Boolean]
-        )
+       
+       ;; bottom propogation from cons
+       [tc-e (let ()
+               (: f ((U (Listof Number) (Listof String)) -> (Listof Number)))
+               (define f (λ (l) (cond
+                                  [(empty? l) '()]
+                                  [(number? (car l)) l]
+                                  [else (map string-length l)])))
+               (void))
+             -Void]
+       
+       ;; aliasing unit tests
+       [tc-e (let ()
+               (: foo (-> Any Number))
+               (define foo 
+                 (λ (x)
+                   (let ([y x])
+                     (if (number? y)
+                         x
+                         42))))
+               (void))
+             -Void]
+       
+       [tc-e (let ()
+               (: foo (-> Any Number))
+               (define foo
+                 (λ (x)
+                   (match x
+                     [(? number?) x]
+                     [`(_ . (_ . ,(? number?))) (cddr x)]
+                     [`(_ . (_ . ,(? pair? p))) 
+                      (if (number? (caddr x))
+                          (car p)
+                          41)]
+                     [_ 42])))
+               (void))
+             -Void]
+       
+       ;; tests looking up path-types into unions
+       [tc-e (let ()
+               (: foo ((U (Pairof Number Number) (Pairof Number String)) -> Number))
+               (define foo (λ (p)
+                             (let ([x (car p)])
+                               x)))
+               (void))
+             -Void]
+       
+       ;; tests looking up path-types into polymorphic functions
+       [tc-e (let ()
+               (: poly-foo (All (α β) (U (Pairof Number α) (Pairof Number β)) -> Number))
+               (define poly-foo (λ (p) (let ([x (car p)])
+                                         x)))
+               (void))
+             -Void]
+       
+       [tc-e (let ()
+               (: poly-foo (All (α β) ((U (Pairof Number α) (Pairof Number β)) -> (U α β))))
+               (define poly-foo (λ (p)
+                                  (let ([x (cdr p)])
+                                    x)))
+               (void))
+             -Void]
+       
+       [tc-e (let ()
+               (: poly-foo-dots (All (α ... β) (U (Pairof Number α) (Pairof Number β)) -> Number))
+               (define poly-foo-dots (λ (p)
+                                       (let ([x (car p)])
+                                         (car p))))
+               (void))
+             -Void]
+       )
 
   (test-suite
    "tc-literal tests"