diff --git a/collects/tests/typed-racket/succeed/type-alias-rec-struct.rkt b/collects/tests/typed-racket/succeed/type-alias-rec-struct.rkt
new file mode 100644
index 00000000..f25d920f
--- /dev/null
+++ b/collects/tests/typed-racket/succeed/type-alias-rec-struct.rkt
@@ -0,0 +1,6 @@
+#lang typed/racket/base
+;; Iteratee
+(define-type (Alias A D) (U #f (Main A D)))
+
+(struct: (A D) Main
+  ([resume : (Alias A D)])) ;
diff --git a/collects/typed-racket/private/parse-type.rkt b/collects/typed-racket/private/parse-type.rkt
index 7afd00da..c5aa22d3 100644
--- a/collects/typed-racket/private/parse-type.rkt
+++ b/collects/typed-racket/private/parse-type.rkt
@@ -366,33 +366,13 @@
        (let loop
          ([rator (parse-type #'id)]
           [args (map parse-type (syntax->list #'(arg args ...)))])
+         (resolve-app-check-error rator args stx)
          (match rator
-           [(Name: n)
-            (when (and (current-poly-struct)
-                       (free-identifier=? n (poly-name (current-poly-struct)))
-                       (not (or (ormap Error? args)
-                                (andmap type-equal? args (poly-vars (current-poly-struct))))))
-              (tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator args))
-            (make-App rator args stx)]
-           [(Poly: ns _)
-            (unless (= (length args) (length ns))
-              (tc-error "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)))
-            (instantiate-poly rator args)]
+           [(Name: _) (make-App rator args stx)]
+           [(Poly: _ _) (instantiate-poly rator args)]
            [(Mu: _ _) (loop (unfold rator) args)]
            [(Error:) Err]
-           [_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator args)
-              Err]))
-       #;
-       (let ([ty (parse-type #'id)])
-         #;(printf "ty is ~a" ty)
-         (unless (Poly? ty)
-           (tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
-         (unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
-           (tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
-                     (syntax-e #'id)
-                     (Poly-n ty)
-                     (length (syntax->list #'(arg args ...)))))
-         (instantiate-poly ty (map parse-type (syntax->list #'(arg args ...)))))]
+           [_ Err]))]
       [t:atom
        (-val (syntax-e #'t))]
       [_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
@@ -463,4 +443,3 @@
 (define parse-tc-results/id (parse/id parse-tc-results))
 
 (define parse-type/id (parse/id parse-type))
-
diff --git a/collects/typed-racket/types/resolve.rkt b/collects/typed-racket/types/resolve.rkt
index 24340294..a5c64a22 100644
--- a/collects/typed-racket/types/resolve.rkt
+++ b/collects/typed-racket/types/resolve.rkt
@@ -8,7 +8,8 @@
          racket/match
          racket/contract)
 
-(provide resolve-name resolve-app needs-resolving? resolve)
+(provide resolve-name resolve-app needs-resolving?
+         resolve resolve-app-check-error)
 (provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))])
 
 (define-struct poly (name vars) #:prefab)
@@ -21,24 +22,35 @@
 
 (define already-resolving? (make-parameter #f))
 
-(define (resolve-app rator rands stx)
-  (parameterize ([current-orig-stx stx]
 
-                 [already-resolving? #t])
+(define (resolve-app-check-error rator rands stx)
+  (parameterize ([current-orig-stx stx])
     (match rator
       [(Poly-unsafe: n _)
        (unless (= n (length rands))
          (tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a"
-                   n (length rands)))
-       (instantiate-poly rator rands)]
+                   n (length rands)))]
       [(Name: n)
        (when (and (current-poly-struct)
                   (free-identifier=? n (poly-name (current-poly-struct)))
                   (not (or (ormap Error? rands)
                            (andmap type-equal? rands (poly-vars (current-poly-struct))))))
-         (tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator rands))
+         (tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator rands))]
+      [(Mu: _ _) (void)]
+      [(App: _ _ _) (void)]
+      [(Error:) (void)]
+      [_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator rands)])))
+
+
+(define (resolve-app rator rands stx)
+  (parameterize ([current-orig-stx stx]
+                 [already-resolving? #t])
+    (resolve-app-check-error rator rands stx)
+    (match rator
+      [(Name: _)
        (let ([r (resolve-name rator)])
-         (and r  (resolve-app r rands stx)))]
+         (and r (resolve-app r rands stx)))]
+      [(Poly: _ _) (instantiate-poly rator rands)]
       [(Mu: _ _) (resolve-app (unfold rator) rands stx)]
       [(App: r r* s) (resolve-app (resolve-app r r* s) rands stx)]
       [_ (tc-error "cannot apply a non-polymorphic type: ~a" rator)])))
diff --git a/collects/typed-racket/types/substitute.rkt b/collects/typed-racket/types/substitute.rkt
index 05a3e7b8..3d3f4b7b 100644
--- a/collects/typed-racket/types/substitute.rkt
+++ b/collects/typed-racket/types/substitute.rkt
@@ -21,6 +21,7 @@
 (define-struct/cond-contract (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]) #:transparent)
 
 (define substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
+(define simple-substitution/c (hash/c symbol? Type/c #:immutable #t))
 
 (define (subst v t e) (substitute t v e))
 
@@ -32,38 +33,48 @@
     (values v (t-subst t))))
 
 
-;; substitute : Type Name Type -> Type
-(define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
-  ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
-  (define (sb t) (substitute image name t #:Un Un))
-  (if (hash-ref (free-vars* target) name #f)
+
+;; substitute-many : Hash[Name,Type] Type -> Type
+(define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
+  ((simple-substitution/c Type?) (#:Un procedure?) . ->* . Type?)
+  (define (sb t) (substitute-many subst t #:Un Un))
+  (define names (hash-keys subst))
+  (if (ormap (lambda (name) (hash-has-key? (free-vars* target) name)) names)
       (type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
                  target
                  [#:Union tys (Un (map sb tys))]
-                 [#:F name* (if (eq? name* name) image target)]
+                 [#:F name (hash-ref subst name target)]
                  [#:arr dom rng rest drest kws
-                        (begin
-                          (when (and (pair? drest)
-                                     (eq? name (cdr drest))
-                                     (not (bound-tvar? name)))
-                            (int-err "substitute used on ... variable ~a in type ~a" name target))
-                          (make-arr (map sb dom)
-                                    (sb rng)
-                                    (and rest (sb rest))
-                                    (and drest (cons (sb (car drest)) (cdr drest)))
-                                    (map sb kws)))]
+                        (cond
+                          ((and (pair? drest) (ormap (and/c (cdr drest) (not/c bound-tvar?)) names)) =>
+                           (lambda (name)
+                             (int-err "substitute used on ... variable ~a in type ~a" name target)))
+                          (else
+                           (make-arr (map sb dom)
+                                     (sb rng)
+                                     (and rest (sb rest))
+                                     (and drest (cons (sb (car drest)) (cdr drest)))
+                                     (map sb kws))))]
                  [#:ValuesDots types dty dbound
-                               (begin
-                                 (when (and (eq? name dbound) (not (bound-tvar? name)))
-                                   (int-err "substitute used on ... variable ~a in type ~a" name target))
+                               (cond
+                                 ((ormap (and/c dbound (not/c bound-tvar?)) names) =>
+                                  (lambda (name)
+                                    (int-err "substitute used on ... variable ~a in type ~a" name target)))
                                  (make-ValuesDots (map sb types) (sb dty) dbound))]
                  [#:ListDots dty dbound
-                             (begin
-                               (when (and (eq? name dbound) (not (bound-tvar? name)))
-                                 (int-err "substitute used on ... variable ~a in type ~a" name target))
+                             (cond
+                               ((ormap (and/c dbound (not/c bound-tvar?)) names) =>
+                                (lambda (name)
+                                  (int-err "substitute used on ... variable ~a in type ~a" name target)))
                                (make-ListDots (sb dty) dbound))])
       target))
 
+
+;; substitute : Type Name Type -> Type
+(define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
+  ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
+  (substitute-many (hash name image) target #:Un Un))
+
 ;; implements angle bracket substitution from the formalism
 ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
 (define/cond-contract (substitute-dots images rimage name target)
@@ -142,12 +153,21 @@
 ;; substitute many variables
 ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
 ;; subst-all : substitution Type -> Type
-(define/cond-contract (subst-all s t)
+(define/cond-contract (subst-all s ty)
   (substitution/c Type? . -> . Type?)
-  (for/fold ([t t]) ([(v r) (in-hash s)])
+
+  (define t-substs
+    (for/fold ([acc (hash)]) ([(v r) (in-hash s)])
+      (match r
+        [(t-subst img)
+         (hash-set acc v img)]
+        [_ acc])))
+  (define t-substed-ty (substitute-many t-substs ty))
+
+
+  (for/fold ([t t-substed-ty]) ([(v r) (in-hash s)])
     (match r
-      [(t-subst img)
-       (substitute img v t)]
+      [(t-subst img) t]
       [(i-subst imgs)
        (substitute-dots imgs #f v t)]
       [(i-subst/starred imgs rest)