diff --git a/hackett-doc/scribblings/hackett/reference.scrbl b/hackett-doc/scribblings/hackett/reference.scrbl
index a724860..2d72909 100644
--- a/hackett-doc/scribblings/hackett/reference.scrbl
+++ b/hackett-doc/scribblings/hackett/reference.scrbl
@@ -107,7 +107,7 @@ following combination of @racket[def], @racket[lambda], and @racket[case*]:
 The @racket[defn] form is generally preferred when defining top-level functions.
 
 @(hackett-examples
-  (defn square : (t:-> t:Integer t:Integer)
+  (defn square : {t:Integer t:-> t:Integer}
     [[x] {x * x}])
   (eval:check (square 5) 25))}
 
@@ -308,6 +308,47 @@ specified controls the fixity used by the associated @racket[type-constructor-id
   {(Leaf 1) :&: (Leaf 2) :&: (Leaf 3)})}
 @(close-eval data-examples-eval)
 
+@subsection[#:tag "reference-type-alias"]{Defining type aliases}
+
+@(define alias-examples-eval (make-hackett-eval))
+@defform[#:literals [left right]
+         (type type-clause type-expr)
+         #:grammar
+         ([type-clause name-id
+                       (code:line (name-id param-id ...+))]
+          [maybe-fixity-ann (code:line #:fixity fixity)
+                            (code:line)]
+          [fixity left right])]{
+
+Defines a @deftech{type alias} named @racket[name-id]. Uses of @racket[name-id] are equivalent to
+uses of the type specified in @racket[type-expr]. If @racket[type-clause] is a bare @racket[name-id],
+then @racket[name-id] is bound directly to the type alias.
+
+@(hackett-examples
+  #:eval alias-examples-eval
+  (type Num Double)
+  (def n : Num 1.5)
+  (#:type n))
+
+If @racket[param-id]s are specified, then uses of the type alias must supply as many arguments as
+there are @racket[param-id]s. The arguments are supplied like those to a type constructor—i.e. 
+@racket[(name-id type-argument ...)]—and the resulting type is @racket[type-expr] with each
+@racket[param-id] substituted with the corresponding @racket[type-argument].
+
+Though the application of a type alias is syntactically similar to the application of a type
+constructor, type aliases are effectively type-level macros, and they may not be partially applied.
+All uses of a type alias must be fully saturated.
+
+@(hackett-examples
+  #:eval alias-examples-eval
+  (type (Predicate a) {a t:-> t:Bool})
+  (def zero? : (Predicate t:Integer) (== 0))
+  (#:type zero?)
+  (eval:check (zero? 0) True)
+  (eval:check ((: zero? (Predicate t:Integer)) 0) True)
+  (eval:error (: zero? Predicate)))
+@(close-eval alias-examples-eval)}
+
 @subsection[#:tag "reference-numbers"]{Numbers}
 
 @deftype[t:Integer]{
diff --git a/hackett-lib/hackett/base.rkt b/hackett-lib/hackett/base.rkt
index c10d46c..58c5d53 100644
--- a/hackett-lib/hackett/base.rkt
+++ b/hackett-lib/hackett/base.rkt
@@ -1,11 +1,13 @@
 #lang racket/base
 
 (require (only-in hackett/private/adt case* case λ λ* lambda lambda* defn _)
+         (only-in hackett/private/type-alias type)
          (only-in hackett/private/class instance derive-instance)
          (except-in hackett/private/kernel λ lambda)
          hackett/private/provide
          (only-in hackett/private/toplevel @%top-interaction))
 (provide (all-from-out hackett/private/adt)
+         (all-from-out hackett/private/type-alias)
          (all-from-out hackett/private/class)
          (all-from-out hackett/private/kernel)
          (all-from-out hackett/private/provide)
diff --git a/hackett-lib/hackett/private/base.rkt b/hackett-lib/hackett/private/base.rkt
index 393c0ab..39ea00b 100644
--- a/hackett-lib/hackett/private/base.rkt
+++ b/hackett-lib/hackett/private/base.rkt
@@ -187,18 +187,36 @@
                                              syntax-local-introduce)
                                        xs)])
         (for/lists [es- ts_es]
-                 ([k (in-list ks)]
-                  [e (in-list (map car es+ts))]
-                  [e/elab (in-list es/elab)]
-                  [scoped-intdef-ctx (in-list scoped-intdef-ctxs)])
-        (let* ([e- (local-expand e/elab 'expression stop-ids (if scoped-intdef-ctx
-                                                                 (list intdef-ctx scoped-intdef-ctx)
-                                                                 intdef-ctx))]
-               [t_e (get-type e-)])
-          (unless t_e (raise-syntax-error #f "no inferred type" e))
-          (k (syntax-property e- 'disappeared-binding
-                              (cons (syntax-property e 'disappeared-binding) disappeared-bindings))
-             t_e)))))
+                   ([k (in-list ks)]
+                    [e (in-list (map car es+ts))]
+                    [e/elab (in-list es/elab)]
+                    [scoped-intdef-ctx (in-list scoped-intdef-ctxs)])
+          (let* ([e- (let ([intdef-ctxs (if scoped-intdef-ctx
+                                            (list intdef-ctx scoped-intdef-ctx)
+                                            intdef-ctx)])
+                       (let loop ([e e/elab])
+                         (syntax-parse (local-expand e 'expression stop-ids intdef-ctxs)
+                           #:literals [#%expression]
+                           ; Expand through #%expression forms if we don’t find an inferred type
+                           ; immediately and hope that the nested expression will have a type.
+                           [(head:#%expression e*)
+                            #:when (not (get-type this-syntax))
+                            (syntax-track-origin (loop #'e*) this-syntax #'head)]
+                           ; If we find a bare identifier, it’s either a variable, an out-of-context
+                           ; identifier, or an unbound identifier that stopped expanding just before
+                           ; introducing racket/base’s #%top (since that #%top is implicitly added to
+                           ; the stop list). The former two cases are okay, but the latter is not, so
+                           ; keep going to trigger the unbound identifier error if the identifier is
+                           ; actually unbound.
+                           [_:id
+                            #:when (not (identifier-binding this-syntax))
+                            (local-expand this-syntax 'expression '() intdef-ctxs)]
+                           [_ this-syntax])))]
+                 [t_e (get-type e-)])
+            (unless t_e (raise-syntax-error #f "no inferred type" e-))
+            (k (syntax-property e- 'disappeared-binding
+                                (cons (syntax-property e 'disappeared-binding) disappeared-bindings))
+               t_e)))))
 
     ; With everything inferred and checked, all that’s left to do is return the results.
     (values xs-* es- ts_es))
diff --git a/hackett-lib/hackett/private/infix.rkt b/hackett-lib/hackett/private/infix.rkt
index 7467d8d..ef6388f 100644
--- a/hackett-lib/hackett/private/infix.rkt
+++ b/hackett-lib/hackett/private/infix.rkt
@@ -35,7 +35,9 @@
 (define (infix-operator? x)
   (and (has-prop:infix-operator? x)
        (operator-fixity? (infix-operator-fixity x))))
-  
+
+; Infix transformer bindings; use the make-infix-variable-like-transformer constructor instead of
+; creating instances of this struct directly.
 (struct infix-variable-like-transformer (procedure fixity)
   #:property prop:procedure (struct-field-index procedure)
   #:property prop:infix-operator
diff --git a/hackett-lib/hackett/private/kernel.rkt b/hackett-lib/hackett/private/kernel.rkt
index ba3a2f9..c81ee58 100644
--- a/hackett-lib/hackett/private/kernel.rkt
+++ b/hackett-lib/hackett/private/kernel.rkt
@@ -90,23 +90,18 @@
    (begin
      (define-syntax-parser @%app
        [(~parens _ . args)
-        (syntax/loc this-syntax
-          (@%app/prefix . args))]
+        (datum->syntax this-syntax (cons #'@%app/prefix #'args) this-syntax)]
        [{~braces _ . args}
-        (syntax/loc this-syntax
-          (@%app/infix . args))])
+        (datum->syntax this-syntax (cons #'@%app/infix #'args) this-syntax)])
 
      (define-syntax-parser @%app/prefix
        [(_ f:expr) #'f]
        [(_ f:expr x:expr)
-        (syntax/loc this-syntax
-          (@%app1 f x))]
+        (datum->syntax this-syntax (list #'@%app1 #'f #'x) this-syntax)]
        [(_ f:expr x:expr xs:expr ...)
-        (quasisyntax/loc this-syntax
-          (@%app/prefix #,(~> (syntax/loc this-syntax
-                                (@%app1 f x))
-                              (syntax-property 'omit-type-tooltip #t))
-                        xs ...))])
+        #:with inner-app (~> (datum->syntax this-syntax (list #'@%app1 #'f #'x) this-syntax)
+                             (syntax-property 'omit-type-tooltip #t))
+        (datum->syntax this-syntax (list* #'@%app/prefix #'inner-app #'(xs ...)) this-syntax)])
 
      (define-syntax-parser @%app/infix
        [(_ a:expr op:infix-operator b:expr {~seq ops:infix-operator bs:expr} ...+)
@@ -114,24 +109,26 @@
         #:and ~!
         #:fail-unless (andmap #{eq? % 'left} (attribute ops.fixity))
                       "cannot mix left- and right-associative operators in the same infix expression"
-        (quasitemplate/loc this-syntax
-          (@%app/infix #,(~> (syntax/loc this-syntax
-                               (@%app/infix a op b))
+        #:with inner-app (~> (datum->syntax this-syntax (list #'@%app/infix #'a #'op #'b) this-syntax)
                              (syntax-property 'omit-type-tooltip #t))
-                       {?@ ops bs} ...))]
+        (~> (list* #'@%app/infix #'inner-app (syntax->list #'({?@ ops bs} ...)))
+            (datum->syntax this-syntax _ this-syntax))]
        [(_ {~seq as:expr ops:infix-operator} ...+ a:expr op:infix-operator b:expr)
         #:when (eq? 'right (attribute op.fixity))
         #:and ~!
         #:fail-unless (andmap #{eq? % 'right} (attribute ops.fixity))
                       "cannot mix left- and right-associative operators in the same infix expression"
-        (quasitemplate/loc this-syntax
-          (@%app/infix {?@ as ops} ...
-                       #,(~> (syntax/loc this-syntax
-                               (@%app/infix a op b))
-                             (syntax-property 'omit-type-tooltip #t))))]
+        #:with inner-app (~> (datum->syntax this-syntax (list #'@%app/infix #'a #'op #'b) this-syntax)
+                             (syntax-property 'omit-type-tooltip #t))
+        (~> (append (list #'@%app/infix) (syntax->list #'({?@ as ops} ...)) (list #'inner-app))
+            (datum->syntax this-syntax _ this-syntax))]
        [(_ a:expr op:expr b:expr)
-        (syntax/loc this-syntax
-          (@%app/prefix op a b))]
+        (quasisyntax/loc this-syntax
+          (#%expression
+           #,(~> (datum->syntax this-syntax (list #'op #'a #'b) this-syntax)
+                 ; Explicitly make 'paren-shape #f on the new application form to avoid the #\{ value
+                 ; being copied onto the prefix application when #%expression is expanded.
+                 (syntax-property 'paren-shape #f))))]
        [(_ a:expr)
         #'a]))))
 
diff --git a/hackett-lib/hackett/private/type-alias.rkt b/hackett-lib/hackett/private/type-alias.rkt
new file mode 100644
index 0000000..fd736fc
--- /dev/null
+++ b/hackett-lib/hackett/private/type-alias.rkt
@@ -0,0 +1,68 @@
+#lang curly-fn racket/base
+
+(require (for-syntax racket/base
+                     racket/format
+                     syntax/intdef
+                     threading
+
+                     hackett/private/infix
+                     hackett/private/typecheck
+                     hackett/private/util/stx)
+         syntax/parse/define
+
+         (only-in hackett/private/adt type-constructor-spec))
+
+(provide type)
+
+(begin-for-syntax
+  ; Alias transformer bindings; use the make-alias-transformer constructor instead of creating
+  ; instances of this struct directly.
+  (struct alias-transformer (procedure fixity)
+    #:property prop:procedure (struct-field-index procedure)
+    #:property prop:infix-operator
+    (λ (self) (alias-transformer-fixity self)))
+
+  (define (make-alias-transformer args type-template fixity)
+    (let ([arity (length args)])
+      (alias-transformer
+       (cond
+         [(zero? arity)
+          (make-variable-like-transformer type-template)]
+         [else
+          (syntax-parser
+            [(head:id t:type ...)
+             #:fail-unless (= (length (attribute t)) arity)
+                           (~a "expected " arity " argument(s) to type alias, got "
+                               (length (attribute t)))
+             (for/fold ([result (insts type-template (map cons args (attribute t)))])
+                       ([residual (in-list (attribute t.residual))])
+               (syntax-track-origin result residual #'head))]
+            [:id
+             #:fail-when #t (~a "expected " arity " argument(s) to type alias")
+             (error "unreachable")])])
+       fixity))))
+
+
+(define-syntax-parser type
+  [(_ ctor-spec:type-constructor-spec {~type type-template:expr})
+   #:with [ctor-spec*:type-constructor-spec] (type-namespace-introduce #'ctor-spec)
+   #:with fixity (attribute ctor-spec.fixity)
+
+   ; Create a dummy internal definition context with args.
+   #:do [(define intdef-ctx (syntax-local-make-definition-context))
+         (syntax-local-bind-syntaxes (attribute ctor-spec*.arg) #f intdef-ctx)]
+   #:with [arg* ...] (map #{internal-definition-context-introduce intdef-ctx %}
+                          (attribute ctor-spec*.arg))
+
+   ; Expanding the type in `ctx` checks immediately that it is a valid type,
+   ; rather than deferring that check to when the type alias is applied.
+   #:with {~var type-template- (type intdef-ctx)} #'type-template
+   (~>> #'(begin
+            (define-values [] type-template-.residual)
+            (define-syntax ctor-spec*.tag
+              (make-alias-transformer
+               (list (quote-syntax arg*) ...)
+               (quote-syntax type-template-.expansion)
+               'fixity)))
+        (internal-definition-context-track intdef-ctx))])
+
diff --git a/hackett-test/tests/hackett/integration/type-alias.rkt b/hackett-test/tests/hackett/integration/type-alias.rkt
new file mode 100644
index 0000000..f94e8ef
--- /dev/null
+++ b/hackett-test/tests/hackett/integration/type-alias.rkt
@@ -0,0 +1,38 @@
+#lang hackett
+
+(require hackett/private/test
+         (only-in racket/base submod)
+         (submod tests/hackett/typecheck assertions))
+
+(type X Integer)
+(def x : X 5)
+(typecheck-fail (: "" X))
+
+(type (Arr a b) {a -> b})
+(type (Pred a) (Arr a Bool))
+(type (BiRel a) {a -> a -> Bool})
+
+(type Y (forall [a b] (Monoid b) => (Either a b)))
+
+(typecheck-fail
+ (λ ([x : (Arr Bool)]) ; not enough args to alias
+   x))
+
+(defn never : (forall [a] (Pred a))
+  [[x] False])
+
+(test {(never 5) ==! False})
+(test {(never "asdasaf") ==! False})
+
+(def int= : (BiRel Integer)
+  ==)
+
+(test {{4 int= 6} ==! False})
+(test {{4 int= 4} ==! True})
+
+(type {a ~> b} #:fixity right {a -> (Maybe b)})
+
+(def head* : (forall [a] {(List a) ~> a}) head)
+
+(test {(head* {1 :: Nil}) ==! (Just 1)})
+(test {(head* {Nil : (List Integer)}) ==! Nothing})