diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index ade8952..97c652d 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -239,6 +239,15 @@
     (stx->list tys)
     typecheck?)))
 
+;; (SyntaxListof Type) -> Type
+;; The input types are already expanded/normalized
+;; avoids namespace module mismatch issue in some cases
+(define-for-syntax (mk-U- tys)
+  (define tys- (prune+sort tys))
+  (if (= 1 (stx-length tys-))
+      (stx-car tys-)
+      (mk-U*- tys-)))
+
 (define-syntax (U stx)
   (syntax-parse stx
     [(_ . tys)
@@ -690,7 +699,7 @@
     [~Discard
      (type-eval #'★/t)]
     [(~U* τ ...)
-     (type-eval #`(U #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))]
+     (mk-U- (stx-map replace-bind-and-discard-with-★ #'(τ ...)))]
     [(~Any/bvs τ-cons () τ ...)
      #:when (reassemblable? t)
      (define subitems (for/list ([t (in-syntax #'(τ ...))])
@@ -992,12 +1001,20 @@
 
 (define-typed-syntax inst
   [(_ e τ:type ...) ≫
+   #:fail-unless (stx-andmap instantiable? #'(τ.norm ...))
+                 "types must be instantiable"
    [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
    #:fail-unless (pure? #'e-) "expression must be pure"
    --------
    [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
   [(_ e) ≫ --- [≻ e]])
 
+;; Type -> Bool
+;; determine if a type is suitable for instantiating a variable
+(define-for-syntax (instantiable? ty)
+  (and (flat-type? ty)
+       (finite? ty)))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Sequencing & Definitions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1188,6 +1205,11 @@
    #:with tyX_args #'(tyX_in ... tyX_out)
    ;; solve for type variables Xs
    #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
+   ;; make sure types are legal
+   #:with tyXs (inst-types/cs #'Xs* #'cs #'Xs)
+   #:fail-unless (for/and ([ty (in-syntax #'tyXs)])
+                   (instantiable? ty))
+                 "type variables must be flat and finite"
    ;; instantiate polymorphic function type
    #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
    #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
@@ -1240,19 +1262,21 @@
                #:when (stx-contains-id? ty X))
       X))
 
-  ;; Type -> Bool
-  ;; checks if the type contains any unions
-  (define (contains-union? ty)
+  ;; (SyntaxListOf ID) Type -> Bool
+  ;; checks if the type contains any variables under unions
+  (define (tyvar-under-union? Xs ty)
     (syntax-parse ty
       [(~U* _ ...)
-       #t]
+       (for/or ([X (in-syntax Xs)])
+         (stx-contains-id? ty X))]
       [(~Base _) #f]
       [X:id #f]
       [(~Any/bvs _ _ τ ...)
-       (stx-ormap contains-union? #'(τ ...))]
+       (for/or ([ty2 (in-syntax #'(τ ...))])
+         (tyvar-under-union? Xs ty2))]
       [_
        (type-error #:src (get-orig ty)
-                   #:msg "contains-union?: unrecognized-type: ~a"
+                   #:msg "tyvar-under-union?: unrecognized-type: ~a"
                    ty)]))
 
   ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
@@ -1283,7 +1307,7 @@
                         ([a (in-stx-list #'args)]
                          [tyXin (in-stx-list #'(τ_inX ...))])
                 (define ty_in (inst-type/cs/orig Xs cs tyXin datum=?))
-                (when (contains-union? ty_in)
+                (when (tyvar-under-union? Xs ty_in)
                   (type-error #:src a
                               #:msg (format "can't infer types with unions: ~a\nraw: ~a"
                                             (type->str ty_in) ty_in)))
@@ -1291,7 +1315,7 @@
                   (infer+erase (if (null? (find-free-Xs Xs ty_in))
                                    (add-expected-type a ty_in)
                                    a)))
-                (when (contains-union? #'ty_a)
+                (when (tyvar-under-union? Xs #'ty_a)
                   (type-error #:src a
                               #:msg (format "can't infer types with unions: ~a\nraw: ~a"
                                             (type->str #'ty_a) #'ty_a)))
diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt
index 3deb30d..a5626ab 100644
--- a/racket/typed/tests/expressions.rkt
+++ b/racket/typed/tests/expressions.rkt
@@ -67,3 +67,6 @@
      (lambda ([x : τ])
        (match x
          [(bind y τ) y]))))
+
+(typecheck-fail (inst id5 (→fn Int Int))
+                #:with-msg "types must be instantiable")
diff --git a/racket/typed/tests/inference.rkt b/racket/typed/tests/inference.rkt
index 3148edc..8719c50 100644
--- a/racket/typed/tests/inference.rkt
+++ b/racket/typed/tests/inference.rkt
@@ -24,6 +24,26 @@
 (define string-int-list : (List (U String Int))
   (list "hi" 42 "badgers"))
 
-;; shouldn't mess about with unions
+;; fails because unification is too strict, requiring equality as opposed to
+;; upper&lower bounds
+(check-type (poly-cons (ann "go" (U String Int)) string-int-list)
+            : (List (U String Int)))
 (typecheck-fail (poly-cons "go" string-int-list))
 
+(typecheck-fail (poly-cons (lambda () 0) (ann (list) (List (→fn Int))))
+                #:with-msg "type variables must be flat and finite")
+
+;; Failure because inference doesn't handle variables under unions
+(define (∀ (X) (unwrap! [x : (Maybe X)] -> X))
+  (match x
+    [(some (bind v X))
+     v]
+    [none
+     (error "none")]))
+
+(typecheck-fail (unwrap! (some 5))
+                #:with-msg "can't infer types with unions")
+
+(check-type ((inst unwrap! Int) (some 5))
+            : Int
+            -> 5)
diff --git a/racket/typed/tests/sequences.rkt b/racket/typed/tests/sequences.rkt
index 3782588..2d093a3 100644
--- a/racket/typed/tests/sequences.rkt
+++ b/racket/typed/tests/sequences.rkt
@@ -4,9 +4,7 @@
 
 (check-type empty-sequence : (Sequence (U)))
 
-(typecheck-fail (sequence-length empty-sequence))
-
-(check-type ((inst sequence-length (U)) empty-sequence)
+(check-type (sequence-length empty-sequence)
             : Int
             ⇒ 0)