diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,24 @@
+1.1.0
+
+* BREAKING CHANGE: Non-empty lists no longer require a type annotation
+    * This is a breaking change to the Haskell library, not the Dhall language
+    * This change does not break existing Dhall programs
+    * The `Expr` type was modified in a non-backwards-compatible way
+* Add new `exprA` parser
+* Add new `InvalidType` exception if `input` fails on an invalid `Type`
+* Improve documentation and tutorial
+
+1.0.2
+
+* Add support for Nix-style "double single-quote" multi-line string literals
+* Add `isNormalized`
+* Improve documentation and tutorial
+* Build against wider range of `http-client` versions
+
+1.0.1
+
+* Initial release
+
+1.0.0
+
+* Accidental premature upload to Hackage.  This release was blacklisted
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2016 Gabriel Gonzalez
+Copyright (c) 2017 Gabriel Gonzalez
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification,
diff --git a/dhall.cabal b/dhall.cabal
--- a/dhall.cabal
+++ b/dhall.cabal
@@ -1,11 +1,11 @@
 Name: dhall
-Version: 1.0.2
+Version: 1.1.0
 Cabal-Version: >=1.8.0.2
 Build-Type: Simple
 Tested-With: GHC == 7.10.2, GHC == 8.0.1
 License: BSD3
 License-File: LICENSE
-Copyright: 2016 Gabriel Gonzalez
+Copyright: 2017 Gabriel Gonzalez
 Author: Gabriel Gonzalez
 Maintainer: Gabriel439@gmail.com
 Bug-Reports: https://github.com/Gabriel439/Haskell-Dhall-Library/issues
@@ -22,6 +22,7 @@
     .
     Read "Dhall.Tutorial" to learn how to use this library
 Category: Compiler
+Extra-Source-Files: CHANGELOG.md
 Source-Repository head
     Type: git
     Location: https://github.com/Gabriel439/Haskell-Dhall-Library
@@ -35,8 +36,7 @@
         containers           >= 0.5.0.0  && < 0.6 ,
         http-client          >= 0.4.30   && < 0.6 ,
         http-client-tls      >= 0.2.0    && < 0.4 ,
-        microlens            >= 0.2.0.0  && < 0.5 ,
-        microlens-mtl        >= 0.1.3.1  && < 0.2 ,
+        lens                 >= 2.4      && < 4.16,
         neat-interpolation   >= 0.3.2.1  && < 0.4 ,
         parsers              >= 0.12.4   && < 0.13,
         system-filepath      >= 0.3.1    && < 0.5 ,
@@ -55,6 +55,7 @@
         Dhall.Parser,
         Dhall.Tutorial,
         Dhall.TypeCheck
+    GHC-Options: -Wall
 
 Executable dhall
     Hs-Source-Dirs: exec
@@ -65,3 +66,4 @@
         optparse-generic >= 1.1.1    && < 1.2,
         trifecta         >= 1.6      && < 1.7,
         text             >= 0.11.1.0 && < 1.3
+    GHC-Options: -Wall
diff --git a/exec/Main.hs b/exec/Main.hs
--- a/exec/Main.hs
+++ b/exec/Main.hs
@@ -8,7 +8,6 @@
 
 import Control.Exception (SomeException)
 import Data.Monoid (mempty)
-import Data.Traversable
 import Dhall.Core (pretty, normalize)
 import Dhall.Import (Imported(..), load)
 import Dhall.Parser (Src, exprFromText)
@@ -22,7 +21,6 @@
 import qualified Data.Text.Lazy.IO
 import qualified Dhall.TypeCheck
 import qualified Options.Generic
-import qualified System.Exit
 import qualified System.IO
 
 data Mode = Default | Resolve | TypeCheck | Normalize
diff --git a/src/Dhall.hs b/src/Dhall.hs
--- a/src/Dhall.hs
+++ b/src/Dhall.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleInstances   #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE QuasiQuotes         #-}
 {-# LANGUAGE RecordWildCards     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
@@ -20,6 +21,7 @@
     -- * Types
     , Type
     , Interpret(..)
+    , InvalidType(..)
     , bool
     , natural
     , integer
@@ -54,6 +56,7 @@
 import qualified Control.Exception
 import qualified Data.ByteString.Lazy
 import qualified Data.Map
+import qualified Data.Text
 import qualified Data.Text.Lazy
 import qualified Data.Text.Lazy.Builder
 import qualified Data.Text.Lazy.Encoding
@@ -62,19 +65,41 @@
 import qualified Dhall.Import
 import qualified Dhall.Parser
 import qualified Dhall.TypeCheck
-import qualified GHC.Generics
+import qualified NeatInterpolation
 
 throws :: Exception e => Either e a -> IO a
 throws (Left  e) = Control.Exception.throwIO e
 throws (Right r) = return r
 
+{-| Every `Type` must obey the contract that if an expression's type matches the
+    the `expected` type then the `extract` function must succeed.  If not, then
+    this exception is thrown
+
+    This exception indicates that an invalid `Type` was provided to the `input`
+    function
+-}
+data InvalidType = InvalidType deriving (Typeable)
+
+_ERROR :: Data.Text.Text
+_ERROR = "\ESC[1;31mError\ESC[0m"
+
+instance Show InvalidType where
+    show InvalidType = Data.Text.unpack [NeatInterpolation.text|
+$_ERROR: Invalid Dhall.Type
+
+Every Type must provide an extract function that succeeds if an expression
+matches the expected type.  You provided a Type that disobeys this contract
+|]
+
+instance Exception InvalidType
+
 {-| Type-check and evaluate a Dhall program, decoding the result into Haskell
 
     The first argument determines the type of value that you decode:
 
 >>> input integer "2"
 2
->>> input (vector double) "[ 1.0, 2.0 ] : List Bool"
+>>> input (vector double) "[1.0, 2.0]"
 [1.0,2.0]
 
     Use `auto` to automatically select which type to decode based on the
@@ -90,10 +115,10 @@
     -- ^ The Dhall program
     -> IO a
     -- ^ The decoded value in Haskell
-input (Type {..}) text = do
+input (Type {..}) txt = do
     let delta = Directed "(input)" 0 0 0 0
-    expr     <- throws (Dhall.Parser.exprFromText delta text)
-    expr'    <- Dhall.Import.load expr
+    expr  <- throws (Dhall.Parser.exprFromText delta txt)
+    expr' <- Dhall.Import.load expr
     let suffix =
             ( Data.ByteString.Lazy.toStrict
             . Data.Text.Lazy.Encoding.encodeUtf8
@@ -107,10 +132,10 @@
                 bytes' = bytes <> " : " <> suffix
             _ ->
                 Annot expr' expected
-    typeExpr <- throws (Dhall.TypeCheck.typeOf annot)
+    _ <- throws (Dhall.TypeCheck.typeOf annot)
     case extract (Dhall.Core.normalize expr') of
         Just x  -> return x
-        Nothing -> fail "input: malformed `Type`"
+        Nothing -> Control.Exception.throwIO InvalidType
 
 {-| Use this to provide more detailed error messages
 
@@ -326,30 +351,32 @@
     extractOut (OptionalLit _ es) = traverse extractIn es'
       where
         es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)
+    extractOut _ = Nothing
 
     expectedOut = App Optional expectedIn
 
 {-| Decode a `Vector`
 
->>> input (vector integer) "[ 1, 2, 3 ] : List Integer"
+>>> input (vector integer) "[1, 2, 3]"
 [1,2,3]
 -}
 vector :: Type a -> Type (Vector a)
 vector (Type extractIn expectedIn) = Type extractOut expectedOut
   where
     extractOut (ListLit _ es) = traverse extractIn es
+    extractOut  _             = Nothing
 
     expectedOut = App List expectedIn
 
 {-| Any value that implements `Interpret` can be automatically decoded based on
     the inferred return type of `input`
 
->>> input auto "[1, 2, 3 ] : List Integer" :: IO (Vector Integer)
+>>> input auto "[1, 2, 3]" :: IO (Vector Integer)
 [1,2,3]
 
     This class auto-generates a default implementation for records that
-    implement `Generic`.  This does not auto-generate an instance for sum types
-    nor recursive types.
+    implement `Generic`.  This does not auto-generate an instance for recursive
+    types.
 -}
 class Interpret a where
     auto :: Type a
@@ -406,6 +433,7 @@
             | name == nameL = fmap (L1 . M1) (extractL e)
             | name == nameR = fmap (R1 . M1) (extractR e)
             | otherwise     = Nothing
+        extract _ = Nothing
 
         expected =
             Union (Data.Map.fromList [(nameL, expectedL), (nameR, expectedR)])
@@ -424,6 +452,7 @@
         extract u@(UnionLit name' e _)
             | name == name' = fmap (R1 . M1) (extractR e)
             | otherwise     = fmap  L1       (extractL u)
+        extract _ = Nothing
 
         expected = Union (Data.Map.insert name expectedR expectedL)
 
@@ -441,6 +470,7 @@
         extract u@(UnionLit name' e _)
             | name == name' = fmap (L1 . M1) (extractL e)
             | otherwise     = fmap  R1       (extractR u)
+        extract _ = Nothing
 
         expected = Union (Data.Map.insert name expectedL expectedR)
 
diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs
--- a/src/Dhall/Context.hs
+++ b/src/Dhall/Context.hs
@@ -16,7 +16,8 @@
 import Data.Text.Lazy (Text)
 import Prelude hiding (lookup)
 
-{-| A @(Context a)@ associates `Text` labels with values of type @a@
+{-| A @(Context a)@ associates `Text` labels with values of type @a@.  Each
+    `Text` label can correspond to multiple values of type @a@
 
     The `Context` is used for type-checking when @(a = Expr X)@
 
@@ -24,9 +25,9 @@
     * You transform a `Context` using `fmap`
     * You consume a `Context` using `lookup` and `toList`
 
-    The difference between a `Context` and a `Map` is that a `Context` lets you
-    have multiple ordered occurrences of the same key and you can query for the
-    @n@th occurrence of a given key.
+    The difference between a `Context` and a `Data.Map.Map` is that a `Context`
+    lets you have multiple ordered occurrences of the same key and you can
+    query for the @n@th occurrence of a given key.
 -}
 newtype Context a = Context { getContext :: [(Text, a)] }
     deriving (Functor)
@@ -44,7 +45,7 @@
 
 > lookup _ _         empty  = Nothing
 > lookup k 0 (insert k v c) = Just v
-> lookup k n (insert k v c) = lookup k (n - 1) c  -- 1 <= n
+> lookup k n (insert k v c) = lookup k (n - 1) c
 > lookup k n (insert j v c) = lookup k  n      c  -- k /= j
 -}
 lookup :: Text -> Integer -> Context a -> Maybe a
diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs
--- a/src/Dhall/Core.hs
+++ b/src/Dhall/Core.hs
@@ -112,25 +112,25 @@
     nearest bound variable and the index increases by one for each bound
     variable of the same name going outward.  The following diagram may help:
 
->                                 +---refers to--+
->                                 |              |
->                                 v              |
-> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0
+>                               ┌──refers to──┐
+>                               │             │
+>                               v             │
+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@0
 >
->   +------------------refers to-----------------+
->   |                                            |
->   v                                            |
-> \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1
+> ┌─────────────────refers to─────────────────┐
+> │                                           │
+> v                                           │
+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x@1
 
     This `Int` behaves like a De Bruijn index in the special case where all
     variables have the same name.
 
     You can optionally omit the index if it is @0@:
 
->                           +refers to+
->                           |         |
->                           v         |
-> \(x : *) -> \(y : *) -> \(x : *) -> x
+>                               ┌─refers to─┐
+>                               │           │
+>                               v           │
+> λ(x : Type) → λ(y : Type) → λ(x : Type) → x
 
     Zero indices are omitted when pretty-printing `Var`s and non-zero indices
     appear as a numeric suffix.
@@ -158,8 +158,8 @@
     | Pi  Text (Expr s a) (Expr s a)
     -- | > App f a                                  ~  f a
     | App (Expr s a) (Expr s a)
-    -- | > Let x Nothing  r e  ~  let x     = r in e
-    --   > Let x (Just t) r e  ~  let x : t = r in e
+    -- | > Let x Nothing  r e                       ~  let x     = r in e
+    --   > Let x (Just t) r e                       ~  let x : t = r in e
     | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)
     -- | > Annot x t                                ~  x : t
     | Annot (Expr s a) (Expr s a)
@@ -211,8 +211,9 @@
     | TextAppend (Expr s a) (Expr s a)
     -- | > List                                     ~  List
     | List
-    -- | > ListLit t [x, y, z]                      ~  [x, y, z] : List t
-    | ListLit (Expr s a) (Vector (Expr s a))
+    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t
+    --   > ListLit  Nothing  [x, y, z]              ~  [x, y, z]
+    | ListLit (Maybe (Expr s a)) (Vector (Expr s a))
     -- | > ListBuild                                ~  List/build
     | ListBuild
     -- | > ListFold                                 ~  List/fold
@@ -238,9 +239,9 @@
     | Record    (Map Text (Expr s a))
     -- | > RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }
     | RecordLit (Map Text (Expr s a))
-    -- | > Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >
+    -- | > Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1 | k2 : t2 >
     | Union     (Map Text (Expr s a))
-    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 > 
+    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1 | k2 : t2 | k3 : t3 > 
     | UnionLit Text (Expr s a) (Map Text (Expr s a))
     -- | > Combine x y                              ~  x ∧ y
     | Combine (Expr s a) (Expr s a)
@@ -262,57 +263,57 @@
 instance Monad (Expr s) where
     return = pure
 
-    Const c           >>= _ = Const c
-    Var v             >>= _ = Var v
-    Lam x _A  b       >>= k = Lam x (_A >>= k) ( b >>= k)
-    Pi  x _A _B       >>= k = Pi  x (_A >>= k) (_B >>= k)
-    App f a           >>= k = App (f >>= k) (a >>= k)
-    Let f mt r e      >>= k = Let f (fmap (>>= k) mt) (r >>= k) (e >>= k)
-    Annot x t         >>= k = Annot (x >>= k) (t >>= k)
-    Bool              >>= _ = Bool
-    BoolLit b         >>= _ = BoolLit b
-    BoolAnd l r       >>= k = BoolAnd (l >>= k) (r >>= k)
-    BoolOr  l r       >>= k = BoolOr  (l >>= k) (r >>= k)
-    BoolEQ  l r       >>= k = BoolEQ  (l >>= k) (r >>= k)
-    BoolNE  l r       >>= k = BoolNE  (l >>= k) (r >>= k)
-    BoolIf x y z      >>= k = BoolIf (x >>= k) (y >>= k) (z >>= k)
-    Natural           >>= _ = Natural
-    NaturalLit n      >>= _ = NaturalLit n
-    NaturalFold       >>= _ = NaturalFold
-    NaturalBuild      >>= _ = NaturalBuild
-    NaturalIsZero     >>= _ = NaturalIsZero
-    NaturalEven       >>= _ = NaturalEven
-    NaturalOdd        >>= _ = NaturalOdd
-    NaturalPlus  l r  >>= k = NaturalPlus  (l >>= k) (r >>= k)
-    NaturalTimes l r  >>= k = NaturalTimes (l >>= k) (r >>= k)
-    Integer           >>= _ = Integer
-    IntegerLit n      >>= _ = IntegerLit n
-    Double            >>= _ = Double
-    DoubleLit n       >>= _ = DoubleLit n
-    Text              >>= _ = Text
-    TextLit t         >>= _ = TextLit t
-    TextAppend l r    >>= k = TextAppend (l >>= k) (r >>= k)
-    List              >>= _ = List
-    ListLit t es      >>= k = ListLit (t >>= k) (fmap (>>= k) es)
-    ListBuild         >>= _ = ListBuild
-    ListFold          >>= _ = ListFold
-    ListLength        >>= _ = ListLength
-    ListHead          >>= _ = ListHead
-    ListLast          >>= _ = ListLast
-    ListIndexed       >>= _ = ListIndexed
-    ListReverse       >>= _ = ListReverse
-    Optional          >>= _ = Optional
-    OptionalLit t es  >>= k = OptionalLit (t >>= k) (fmap (>>= k) es)
-    OptionalFold      >>= _ = OptionalFold
-    Record    kts     >>= k = Record    (fmap (>>= k) kts)
-    RecordLit kvs     >>= k = RecordLit (fmap (>>= k) kvs)
-    Union     kts     >>= k = Union     (fmap (>>= k) kts)
-    UnionLit k' v kts >>= k = UnionLit k' (v >>= k) (fmap (>>= k) kts)
-    Combine x y       >>= k = Combine (x >>= k) (y >>= k)
-    Merge x y t       >>= k = Merge (x >>= k) (y >>= k) (t >>= k)
-    Field r x         >>= k = Field (r >>= k) x
-    Note a b          >>= k = Note a (b >>= k)
-    Embed r           >>= k = k r
+    Const a          >>= _ = Const a
+    Var a            >>= _ = Var a
+    Lam a b c        >>= k = Lam a (b >>= k) (c >>= k)
+    Pi  a b c        >>= k = Pi a (b >>= k) (c >>= k)
+    App a b          >>= k = App (a >>= k) (b >>= k)
+    Let a b c d      >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)
+    Annot a b        >>= k = Annot (a >>= k) (b >>= k)
+    Bool             >>= _ = Bool
+    BoolLit a        >>= _ = BoolLit a
+    BoolAnd a b      >>= k = BoolAnd (a >>= k) (b >>= k)
+    BoolOr  a b      >>= k = BoolOr  (a >>= k) (b >>= k)
+    BoolEQ  a b      >>= k = BoolEQ  (a >>= k) (b >>= k)
+    BoolNE  a b      >>= k = BoolNE  (a >>= k) (b >>= k)
+    BoolIf a b c     >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)
+    Natural          >>= _ = Natural
+    NaturalLit a     >>= _ = NaturalLit a
+    NaturalFold      >>= _ = NaturalFold
+    NaturalBuild     >>= _ = NaturalBuild
+    NaturalIsZero    >>= _ = NaturalIsZero
+    NaturalEven      >>= _ = NaturalEven
+    NaturalOdd       >>= _ = NaturalOdd
+    NaturalPlus  a b >>= k = NaturalPlus  (a >>= k) (b >>= k)
+    NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)
+    Integer          >>= _ = Integer
+    IntegerLit a     >>= _ = IntegerLit a
+    Double           >>= _ = Double
+    DoubleLit a      >>= _ = DoubleLit a
+    Text             >>= _ = Text
+    TextLit a        >>= _ = TextLit a
+    TextAppend a b   >>= k = TextAppend (a >>= k) (b >>= k)
+    List             >>= _ = List
+    ListLit a b      >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)
+    ListBuild        >>= _ = ListBuild
+    ListFold         >>= _ = ListFold
+    ListLength       >>= _ = ListLength
+    ListHead         >>= _ = ListHead
+    ListLast         >>= _ = ListLast
+    ListIndexed      >>= _ = ListIndexed
+    ListReverse      >>= _ = ListReverse
+    Optional         >>= _ = Optional
+    OptionalLit a b  >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)
+    OptionalFold     >>= _ = OptionalFold
+    Record    a      >>= k = Record (fmap (>>= k) a)
+    RecordLit a      >>= k = RecordLit (fmap (>>= k) a)
+    Union     a      >>= k = Union (fmap (>>= k) a)
+    UnionLit a b c   >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)
+    Combine a b      >>= k = Combine (a >>= k) (b >>= k)
+    Merge a b c      >>= k = Merge (a >>= k) (b >>= k) (c >>= k)
+    Field a b        >>= k = Field (a >>= k) b
+    Note a b         >>= k = Note a (b >>= k)
+    Embed a          >>= k = k a
 
 instance Bifunctor Expr where
     first _ (Const a         ) = Const a
@@ -346,7 +347,7 @@
     first _ (TextLit a       ) = TextLit a
     first k (TextAppend a b  ) = TextAppend (first k a) (first k b)
     first _  List              = List
-    first k (ListLit a b     ) = ListLit (first k a) (fmap (first k) b)
+    first k (ListLit a b     ) = ListLit (fmap (first k) a) (fmap (first k) b)
     first _  ListBuild         = ListBuild
     first _  ListFold          = ListFold
     first _  ListLength        = ListLength
@@ -369,8 +370,7 @@
 
     second = fmap
 
-instance IsString (Expr s a)
-  where
+instance IsString (Expr s a) where
     fromString str = Var (fromString str)
 
 {-  There is a one-to-one correspondence between the builders in this section
@@ -461,7 +461,9 @@
     <>  buildExprA c
     <>  " in "
     <>  buildExprB d
-buildExprB (ListLit a b) =
+buildExprB (ListLit Nothing b) =
+    "[" <> buildElems (Data.Vector.toList b) <> "]"
+buildExprB (ListLit (Just a) b) =
     "[" <> buildElems (Data.Vector.toList b) <> "] : List "  <> buildExprE a
 buildExprB (OptionalLit a b) =
     "[" <> buildElems (Data.Vector.toList b) <> "] : Optional "  <> buildExprE a
@@ -680,7 +682,8 @@
 buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExprA b
 
 -- | Builder corresponding to the @unionLit@ parser in "Dhall.Parser"
-buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder
+buildUnionLit
+    :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder
 buildUnionLit a b c
     | Data.Map.null c =
             "< "
@@ -847,7 +850,7 @@
 shift _ _ List = List
 shift d v (ListLit a b) = ListLit a' b'
   where
-    a' =       shift d v  a
+    a' = fmap (shift d v) a
     b' = fmap (shift d v) b
 shift _ _ ListBuild = ListBuild
 shift _ _ ListFold = ListFold
@@ -978,7 +981,7 @@
 subst _ _ List = List
 subst x e (ListLit a b) = ListLit a' b'
   where
-    a' =       subst x e  a
+    a' = fmap (subst x e) a
     b' = fmap (subst x e) b
 subst _ _ ListBuild = ListBuild
 subst _ _ ListFold = ListFold
@@ -1078,7 +1081,7 @@
             App NaturalEven (NaturalLit n) -> BoolLit (even n)
             App NaturalOdd (NaturalLit n) -> BoolLit (odd n)
             App (App ListBuild t) k
-                | check     -> ListLit t (buildVector k')
+                | check     -> ListLit (Just t) (buildVector k')
                 | otherwise -> App f' a'
               where
                 labeled =
@@ -1100,16 +1103,16 @@
                 cons' y ys = App (App cons y) ys
             App (App ListLength _) (ListLit _ ys) ->
                 NaturalLit (fromIntegral (Data.Vector.length ys))
-            App (App ListHead _) (ListLit t ys) ->
+            App (App ListHead t) (ListLit _ ys) ->
                 normalize (OptionalLit t (Data.Vector.take 1 ys))
-            App (App ListLast _) (ListLit t ys) ->
+            App (App ListLast t) (ListLit _ ys) ->
                 normalize (OptionalLit t y)
               where
                 y = if Data.Vector.null ys
                     then Data.Vector.empty
                     else Data.Vector.singleton (Data.Vector.last ys)
-            App (App ListIndexed _) (ListLit t xs) ->
-                normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
+            App (App ListIndexed t) (ListLit _ xs) ->
+                normalize (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs)))
               where
                 t' = Record (Data.Map.fromList kts)
                   where
@@ -1121,8 +1124,8 @@
                     kvs = [ ("index", NaturalLit (fromIntegral n))
                           , ("value", x)
                           ]
-            App (App ListReverse _) (ListLit t xs) ->
-                normalize (ListLit t (Data.Vector.reverse xs))
+            App (App ListReverse t) (ListLit _ xs) ->
+                normalize (ListLit (Just t) (Data.Vector.reverse xs))
             App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
                 normalize (maybe nothing just' (toMaybe xs))
               where
@@ -1232,7 +1235,7 @@
     List -> List
     ListLit t es -> ListLit t' es'
       where
-        t'  =      normalize t
+        t'  = fmap normalize t
         es' = fmap normalize es
     ListBuild -> ListBuild
     ListFold -> ListFold
@@ -1421,7 +1424,7 @@
                     _ -> True
             _ -> True
     List -> True
-    ListLit t es -> isNormalized t && all isNormalized es
+    ListLit t es -> all isNormalized t && all isNormalized es
     ListBuild -> True
     ListFold -> True
     ListLength -> True
@@ -1463,12 +1466,15 @@
     Note _ e' -> isNormalized e'
     Embed _ -> True
 
+_ERROR :: Data.Text.Text
+_ERROR = "\ESC[1;31mError\ESC[0m"
+
 {-| Utility function used to throw internal errors that should never happen
     (in theory) but that are not enforced by the type system
 -}
 internalError :: Data.Text.Text -> forall b . b
 internalError text = error (Data.Text.unpack [NeatInterpolation.text|
-Error: Compiler bug
+$_ERROR: Compiler bug
 
 Explanation: This error message means that there is a bug in the Dhall compiler.
 You didn't do anything wrong, but if you would like to see this problem fixed
diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs
--- a/src/Dhall/Import.hs
+++ b/src/Dhall/Import.hs
@@ -75,6 +75,7 @@
 
 import Control.Exception
     (Exception, IOException, SomeException, catch, onException, throwIO)
+import Control.Lens (Lens', zoom)
 import Control.Monad (join)
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Trans.State.Strict (StateT)
@@ -90,13 +91,12 @@
 #endif
 import Data.Typeable (Typeable)
 import Filesystem.Path ((</>), FilePath)
-import Lens.Micro (Lens')
-import Lens.Micro.Mtl (zoom)
 import Dhall.Core (Expr, Path(..))
 import Dhall.Parser (Parser(..), ParseError(..), Src)
 import Dhall.TypeCheck (X(..))
 #if MIN_VERSION_http_client(0,5,0)
-import Network.HTTP.Client (HttpException(..), HttpExceptionContent(..), Manager)
+import Network.HTTP.Client
+    (HttpException(..), HttpExceptionContent(..), Manager)
 #else
 import Network.HTTP.Client (HttpException(..), Manager)
 #endif
@@ -142,7 +142,7 @@
 
     To be precise, a strong interpretaton of referential transparency means that
     if you compiled a URL you could replace the expression hosted at that URL
-    with the compiled result.  Let's term this \"static linking\".  Dhall (very
+    with the compiled result.  Let's call this \"static linking\".  Dhall (very
     intentionally) does not satisfy this stronger interpretation of referential
     transparency since \"statically linking\" an expression (i.e. permanently
     resolving all imports) means that the expression will no longer update if
@@ -183,9 +183,11 @@
 instance Show e => Show (Imported e) where
     show (Imported paths e) =
             (case paths of [] -> ""; _ -> "\n")
-        ++  unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths')
+        ++  unlines (map indent paths')
         ++  show e
       where
+        indent (n, path) =
+            take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)
         -- Canonicalize all paths
         paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths)))
 
@@ -295,7 +297,7 @@
       if you navigate to any downstream relative paths
     * Removing spurious @.@s and @..@s from the path
 
-    Also, there are way too many `reverse`s in the URL-handling cod  For now I
+    Also, there are way too many `reverse`s in the URL-handling code For now I
     don't mind, but if were to really do this correctly we'd store the URLs as
     `Text` for O(1) access to the end of the string.  The only reason we use
     `String` at all is for consistency with the @http-client@ library.
@@ -369,10 +371,9 @@
 exprFromFile path = do
     let string = Filesystem.Path.CurrentOS.encodeString path
 
-    -- Unfortunately, GHC throws an `InappropriateType`
-    -- exception when trying to read a directory, but does not
-    -- export the exception, so I must resort to a more
-    -- heavy-handed `catch`
+    -- Unfortunately, GHC throws an `InappropriateType` exception when trying to
+    -- to read a directory, but does not export the exception, so I must resort
+    -- to a more heavy-handed `catch`
     let handler :: IOException -> IO (Result (Expr Src Path))
         handler e = do
             let string' = Filesystem.Path.CurrentOS.encodeString (path </> "@")
diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs
--- a/src/Dhall/Parser.hs
+++ b/src/Dhall/Parser.hs
@@ -9,7 +9,7 @@
       exprFromText
 
     -- * Parsers
-    , expr
+    , expr, exprA
 
     -- * Types
     , Src(..)
@@ -34,10 +34,8 @@
 import Prelude hiding (FilePath, const, pi)
 import Text.PrettyPrint.ANSI.Leijen (Doc)
 import Text.Parser.Combinators (choice, try, (<?>))
-import Text.Parser.Expression (Assoc(..), Operator(..))
 import Text.Parser.Token (IdentifierStyle(..), TokenParsing(..))
 import Text.Parser.Token.Highlight (Highlight(..))
-import Text.Parser.Token.Style (CommentStyle(..))
 import Text.Trifecta
     (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..))
 import Text.Trifecta.Delta (Delta)
@@ -45,7 +43,6 @@
 import qualified Data.Char
 import qualified Data.HashSet
 import qualified Data.Map
-import qualified Data.ByteString
 import qualified Data.ByteString.Lazy
 import qualified Data.List
 import qualified Data.Sequence
@@ -58,13 +55,10 @@
 import qualified Filesystem.Path.CurrentOS
 import qualified Text.Parser.Char
 import qualified Text.Parser.Combinators
-import qualified Text.Parser.Expression
 import qualified Text.Parser.Token
 import qualified Text.Parser.Token.Style
 import qualified Text.PrettyPrint.ANSI.Leijen
 import qualified Text.Trifecta
-import qualified Text.Trifecta.Combinators
-import qualified Text.Trifecta.Delta
 
 -- | Source code extract
 data Src = Src Delta Delta ByteString deriving (Show)
@@ -160,10 +154,10 @@
 
 noted :: Parser (Expr Src a) -> Parser (Expr Src a)
 noted parser = do
-    before        <- Text.Trifecta.position
-    (expr, bytes) <- Text.Trifecta.slicedWith (,) parser
-    after         <- Text.Trifecta.position
-    return (Note (Src before after bytes) expr)
+    before     <- Text.Trifecta.position
+    (e, bytes) <- Text.Trifecta.slicedWith (,) parser
+    after      <- Text.Trifecta.position
+    return (Note (Src before after bytes) e)
 
 toMap :: [(Text, a)] -> Parser (Map Text a)
 toMap kvs = do
@@ -219,18 +213,18 @@
             _  -> minimum (map indentLength nonEmptyLines)
 
     p0 = do
-        Text.Parser.Char.string "''"
+        _ <- Text.Parser.Char.string "''"
         p1
 
     p1 = p2 <|> p3 <|> p4 <|> p5
 
     p2 = do
-        Text.Parser.Char.text "'''"
+        _  <- Text.Parser.Char.text "'''"
         s1 <- p1
         return ("''" <> s1)
 
     p3 = do
-        Text.Parser.Char.text "''"
+        _ <- Text.Parser.Char.text "''"
         return ""
 
     p4 = do
@@ -260,28 +254,30 @@
 
 -- | Parser for a top-level Dhall expression
 expr :: Parser (Expr Src Path)
-expr = exprA
+expr = exprA import_
 
-exprA :: Parser (Expr Src Path)
-exprA = do
-    a <- exprB
+-- | Parser for a top-level Dhall expression. The expression is parameterized
+-- over any parseable type, allowing the language to be extended as needed.
+exprA :: Show a => Parser a -> Parser (Expr Src a)
+exprA embedded = noted (do
+    a <- exprB embedded
 
     let exprA0 = do
             symbol ":"
-            b <- exprA
+            b <- exprA embedded
             return (Annot a b)
 
     let exprA1 = pure a
 
-    exprA0 <|> exprA1
+    exprA0 <|> exprA1 )
 
-exprB :: Parser (Expr Src Path)
-exprB = choice
+exprB :: Show a => Parser a -> Parser (Expr Src a)
+exprB embedded = choice
     [   noted      exprB0
     ,   noted      exprB1
     ,   noted      exprB3
     ,   noted      exprB5
-    ,   noted      exprB6
+    ,   noted (try exprB6)
     ,   noted      exprB7
     ,   noted (try exprB2)
     ,              exprB8
@@ -292,25 +288,25 @@
         symbol "("
         a <- label
         symbol ":"
-        b <- exprA
+        b <- exprA embedded
         symbol ")"
         arrow
-        c <- exprB
+        c <- exprB embedded
         return (Lam a b c)
 
     exprB1 = do
         reserve "if"
-        a <- exprA
+        a <- exprA embedded
         reserve "then"
-        b <- exprB
+        b <- exprB embedded
         reserve "else"
-        c <- exprC
+        c <- exprC embedded
         return (BoolIf a b c)
 
     exprB2 = do
-        a <- exprC
+        a <- exprC embedded
         arrow
-        b <- exprB
+        b <- exprB embedded
         return (Pi "_" a b)
 
     exprB3 = do
@@ -318,10 +314,10 @@
         symbol "("
         a <- label
         symbol ":"
-        b <- exprA
+        b <- exprA embedded
         symbol ")"
         arrow
-        c <- exprB
+        c <- exprB embedded
         return (Pi a b c)
 
     exprB5 = do
@@ -329,33 +325,33 @@
         a <- label
         b <- optional (do
             symbol ":"
-            exprA )
+            exprA embedded )
         symbol "="
-        c <- exprA
+        c <- exprA embedded
         reserve "in"
-        d <- exprB
+        d <- exprB embedded
         return (Let a b c d)
 
     exprB6 = do
         symbol "["
-        a <- elems
+        a <- elems embedded
         symbol "]"
         symbol ":"
         b <- listLike
-        c <- exprE
-        return (b c (Data.Vector.fromList a))
+        c <- exprE embedded
+        return (b c a)
 
     exprB7 = do
         reserve "merge"
-        a <- exprE
-        b <- exprE
+        a <- exprE embedded
+        b <- exprE embedded
         symbol ":"
-        c <- exprD
+        c <- exprD embedded
         return (Merge a b c)
 
-    exprB8 = exprC
+    exprB8 = exprC embedded
 
-listLike :: Parser (Expr Src Path -> Vector (Expr Src Path) -> Expr Src Path)
+listLike :: Parser (Expr Src a -> Vector (Expr Src a) -> Expr Src a)
 listLike =
     (   listLike0
     <|> listLike1
@@ -363,18 +359,18 @@
   where
     listLike0 = do
         reserve "List"
-        return ListLit
+        return (\a b -> ListLit (Just a) b)
 
     listLike1 = do
         reserve "Optional"
         return OptionalLit
 
-exprC :: Parser (Expr Src Path)
-exprC = exprC0
+exprC :: Show a => Parser a -> Parser (Expr Src a)
+exprC embedded = exprC0
   where
     chain pA pOp op pB = noted (do
         a <- pA
-        try (do pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a )
+        try (do _ <- pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a )
 
     exprC0 = chain exprC1 (symbol "||") BoolOr       exprC0
     exprC2 = chain exprC3 (symbol "++") TextAppend   exprC2
@@ -383,7 +379,7 @@
     exprC4 = chain exprC5  combine      Combine      exprC4
     exprC5 = chain exprC6 (symbol "*" ) NaturalTimes exprC5
     exprC6 = chain exprC7 (symbol "==") BoolEQ       exprC6
-    exprC7 = chain exprD  (symbol "!=") BoolNE       exprC7
+    exprC7 = chain (exprD embedded)  (symbol "!=") BoolNE       exprC7
 
 -- We can't use left-recursion to define `exprD` otherwise the parser will
 -- loop infinitely. However, I'd still like to use left-recursion in the
@@ -393,25 +389,25 @@
 -- * First, parse to count how many arguments the function is applied to
 -- * Second, restart the parse using left recursion bounded by the number of
 --   arguments
-exprD :: Parser (Expr Src Path)
-exprD = do
-    es <- some (noted (try exprE))
-    let app nL@(Note (Src before _ bytesL) eL) nR@(Note (Src _ after bytesR) eR) =
+exprD :: Show a => Parser a -> Parser (Expr Src a)
+exprD embedded = do
+    es <- some (noted (try (exprE embedded)))
+    let app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) =
             Note (Src before after (bytesL <> bytesR)) (App nL nR)
         app _ _ = Dhall.Core.internalError
             ("Dhall.Parser.exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")")
     return (Data.List.foldl1 app es)
 
-exprE :: Parser (Expr Src Path)
-exprE = noted (do
-    a <- exprF
+exprE :: Show a => Parser a -> Parser (Expr Src a)
+exprE embedded = noted (do
+    a <- exprF embedded
     b <- many (try (do
         symbol "."
         label ))
     return (Data.List.foldl Field a b) )
 
-exprF :: Parser (Expr Src Path)
-exprF = choice
+exprF :: Show a => Parser a -> Parser (Expr Src a)
+exprF embedded = choice
     [   noted (try exprF26)
     ,   noted (try exprF25)
     ,   noted      exprF24
@@ -421,6 +417,7 @@
     ,   noted (try exprF30)
     ,   noted      exprF31
     ,   noted      exprF32
+    ,   noted      exprF33
     ,   (choice
             [   noted      exprF03
             ,   noted      exprF04
@@ -448,7 +445,7 @@
             ]
         ) <?> "built-in value"
     ,   noted      exprF00
-    ,              exprF33
+    ,              exprF34
     ]
   where
     exprF00 = do
@@ -552,7 +549,7 @@
         return (IntegerLit a)
 
     exprF25 = (do
-        Text.Parser.Char.char '+'
+        _ <- Text.Parser.Char.char '+'
         a <- Text.Parser.Token.natural
         return (NaturalLit (fromIntegral a)) ) <?> "natural"
 
@@ -567,21 +564,23 @@
         a <- stringLiteral
         return (TextLit a)
 
-    exprF28 = record <?> "record type"
+    exprF28 = record embedded <?> "record type"
 
-    exprF29 = recordLit <?> "record literal"
+    exprF29 = recordLit embedded <?> "record literal"
 
-    exprF30 = union <?> "union type"
+    exprF30 = union embedded <?> "union type"
 
-    exprF31 = unionLit <?> "union literal"
+    exprF31 = unionLit embedded <?> "union literal"
 
-    exprF32 = do
-        a <- import_ <?> "import"
-        return (Embed a)
+    exprF32 = listLit embedded <?> "list literal"
 
     exprF33 = do
+        a <- embedded <?> "import"
+        return (Embed a)
+
+    exprF34 = do
         symbol "("
-        a <- exprA
+        a <- exprA embedded
         symbol ")"
         return a
 
@@ -604,15 +603,17 @@
         symbol "@"
         Text.Parser.Token.natural )
     let b = case m of
-            Just b  -> b
+            Just r  -> r
             Nothing -> 0
     return (V a b)
 
-elems :: Parser [Expr Src Path]
-elems = Text.Parser.Combinators.sepBy exprA (symbol ",")
+elems :: Show a => Parser a -> Parser (Vector (Expr Src a))
+elems embedded = do
+    a <- Text.Parser.Combinators.sepBy (exprA embedded) (symbol ",")
+    return (Data.Vector.fromList a)
 
-recordLit :: Parser (Expr Src Path)
-recordLit =
+recordLit :: Show a => Parser a -> Parser (Expr Src a)
+recordLit embedded =
         recordLit0
     <|> recordLit1
   where
@@ -622,62 +623,62 @@
 
     recordLit1 = do
         symbol "{"
-        a <- fieldValues
+        a <- fieldValues embedded
         b <- toMap a
         symbol "}"
         return (RecordLit b)
 
-fieldValues :: Parser [(Text, Expr Src Path)]
-fieldValues =
-    Text.Parser.Combinators.sepBy1 fieldValue (symbol ",")
+fieldValues :: Show a => Parser a -> Parser [(Text, Expr Src a)]
+fieldValues embedded =
+    Text.Parser.Combinators.sepBy1 (fieldValue embedded) (symbol ",")
 
-fieldValue :: Parser (Text, Expr Src Path)
-fieldValue = do
+fieldValue :: Show a => Parser a -> Parser (Text, Expr Src a)
+fieldValue embedded = do
     a <- label
     symbol "="
-    b <- exprA
+    b <- exprA embedded
     return (a, b)
 
-record :: Parser (Expr Src Path)
-record = do
+record :: Show a => Parser a -> Parser (Expr Src a)
+record embedded = do
     symbol "{"
-    a <- fieldTypes
+    a <- fieldTypes embedded
     b <- toMap a
     symbol "}"
     return (Record b)
 
-fieldTypes :: Parser [(Text, Expr Src Path)]
-fieldTypes =
-    Text.Parser.Combinators.sepBy fieldType (symbol ",")
+fieldTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)]
+fieldTypes embedded =
+    Text.Parser.Combinators.sepBy (fieldType embedded) (symbol ",")
 
-fieldType :: Parser (Text, Expr Src Path)
-fieldType = do
+fieldType :: Show a => Parser a -> Parser (Text, Expr Src a)
+fieldType embedded = do
     a <- label
     symbol ":"
-    b <- exprA
+    b <- exprA embedded
     return (a, b)
 
-union :: Parser (Expr Src Path)
-union = do
+union :: Show a => Parser a -> Parser (Expr Src a)
+union embedded = do
     symbol "<"
-    a <- alternativeTypes
+    a <- alternativeTypes embedded
     b <- toMap a
     symbol ">"
     return (Union b)
 
-alternativeTypes :: Parser [(Text, Expr Src Path)]
-alternativeTypes =
-    Text.Parser.Combinators.sepBy alternativeType (symbol "|")
+alternativeTypes :: Show a => Parser a -> Parser [(Text, Expr Src a)]
+alternativeTypes embedded =
+    Text.Parser.Combinators.sepBy (alternativeType embedded) (symbol "|")
 
-alternativeType :: Parser (Text, Expr Src Path)
-alternativeType = do
+alternativeType :: Show a => Parser a -> Parser (Text, Expr Src a)
+alternativeType embedded = do
     a <- label
     symbol ":"
-    b <- exprA
+    b <- exprA embedded
     return (a, b)
 
-unionLit :: Parser (Expr Src Path)
-unionLit =
+unionLit :: Show a => Parser a -> Parser (Expr Src a)
+unionLit embedded =
         try unionLit0
     <|>     unionLit1
   where
@@ -685,7 +686,7 @@
         symbol "<"
         a <- label
         symbol "="
-        b <- exprA
+        b <- exprA embedded
         symbol ">"
         return (UnionLit a b Data.Map.empty)
 
@@ -693,13 +694,20 @@
         symbol "<"
         a <- label
         symbol "="
-        b <- exprA
+        b <- exprA embedded
         symbol "|"
-        c <- alternativeTypes
+        c <- alternativeTypes embedded
         d <- toMap c
         symbol ">"
         return (UnionLit a b d)
 
+listLit :: Show a => Parser a -> Parser (Expr Src a)
+listLit embedded = do
+    symbol "["
+    a <- elems embedded
+    symbol "]"
+    return (ListLit Nothing a)
+
 import_ :: Parser Path
 import_ = do
     a <- import0 <|> import1
@@ -769,7 +777,7 @@
 
     parser = unParser (do
         Text.Parser.Token.whiteSpace
-        r <- exprA
+        r <- expr
         Text.Parser.Combinators.eof
         return r )
 
diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs
--- a/src/Dhall/Tutorial.hs
+++ b/src/Dhall/Tutorial.hs
@@ -18,7 +18,7 @@
     -- $lists
 
     -- * Optional values
-    -- $optional
+    -- $optional0
 
     -- * Records
     -- $records
@@ -132,7 +132,7 @@
     -- $listReverse
 
     -- ** @Optional@
-    -- $optional
+    -- $optional1
 
     -- *** @Optional/fold@
     -- $optionalFold
@@ -148,7 +148,7 @@
     ) where
 
 import Data.Vector (Vector)
-import Dhall (Interpret(..), Type, detailed, input)
+import Dhall
 
 -- $introduction
 --
@@ -158,7 +158,7 @@
 -- 
 -- > $ cat ./config
 -- > { foo = 1
--- > , bar = [3.0, 4.0, 5.0] : List Double
+-- > , bar = [3.0, 4.0, 5.0]
 -- > }
 -- 
 -- You can read the above configuration file into Haskell using the following
@@ -241,13 +241,13 @@
 -- Therefore, since we can decode a @Bool@, we must also be able to decode a
 -- @List@ of @Bool@s, like this:
 --
--- > >>> input auto "[True, False] : List Bool" :: IO (Vector Bool)
+-- > >>> input auto "[True, False]" :: IO (Vector Bool)
 -- > [True,False]
 --
 -- We could also specify what type to decode by providing an explicit `Type`
 -- instead of using `auto` with a type annotation:
 --
--- > >>> input (vector bool) "[True, False] : List Bool"
+-- > >>> input (vector bool) "[True, False]"
 -- > [True, False]
 --
 -- __Exercise:__ Create a @./config@ file that the following program can decode:
@@ -358,7 +358,7 @@
 --
 -- ... and read in all three files in a single expression:
 -- 
--- > >>> input auto "[ ./bool1 , ./bool2 , ./both ] : List Bool" :: IO (Vector Bool)
+-- > >>> input auto "[ ./bool1 , ./bool2 , ./both ]" :: IO (Vector Bool)
 -- > [True,False,False]
 --
 -- Each file path is replaced with the Dhall expression contained within that
@@ -375,7 +375,7 @@
 -- > }
 -- > EOF
 --
--- > $ echo "[ 3.0, 4.0, 5.0 ] : List Double" > ./bar
+-- > $ echo "[3.0, 4.0, 5.0]" > ./bar
 --
 -- > $ ./example
 -- > Example {foo = 1, bar = [3.0,4.0,5.0]}
@@ -419,7 +419,7 @@
 --
 -- You can import types, too.  For example, we can change our @./bar@ file to:
 --
--- > $ echo "[ 3.0, 4.0, 5.0 ] : List ./type" > ./bar
+-- > $ echo "[3.0, 4.0, 5.0] : List ./type" > ./bar
 --
 -- ... then specify the @./type@ in a separate file:
 --
@@ -464,35 +464,39 @@
 --
 -- You can store 0 or more values of the same type in a list, like this:
 --
--- > [1, 2, 3] : List Integer
+-- > [1, 2, 3]
 --
--- Every list must be followed by the type of the list.  The type annotation is
--- not optional and you will get an error if you omit the annotation:
+-- Every list can be followed by the type of the list.  The type annotation is
+-- required for empty lists but optional for non-empty lists.  You will get a
+-- type error if you provide an empty list without a type annotation:
 --
--- > >>> input auto "[1, 2, 3]" :: IO (Vector Integer)
--- > *** Exception: (input):1:10: error: unexpected
--- >     EOF, expected: ":"
--- > [1, 2, 3]<EOF> 
--- >          ^     
+-- > >>> input auto "[]" :: IO (Vector Integer)
+-- > *** Exception: 
+-- > Error: Empty lists need a type annotation
+-- > 
+-- > []
+-- > 
+-- > (input):1:1
+-- > >>> input auto "[] : List Integer" :: IO (Vector Integer)
+-- > []
 --
--- Also, list elements must all have the same type which must match the declared
--- type of the list.  You will get an error if you try to store any other type
--- of element:
+-- Also, list elements must all have the same type.  You will get an error if
+-- you try to store elements of different types in a list:
 --
--- > input auto "[1, True, 3] : List Integer" :: IO (Vector Integer)
+-- > >>> input auto "[1, True, 3]" :: IO (Vector Integer)
 -- > *** Exception: 
--- > Error: List element has the wrong type
+-- > Error: List elements should have the same type
 -- > 
--- > [1, True, 3] : List Integer
+-- > [1, True, 3]
 -- > 
 -- > (input):1:1
 --
--- __Exercise:__ Create a @./config@ file that decodes to the following result:
+-- __Exercise:__ What is the shortest @./config@ file that you can decode using
+-- this command:
 --
 -- > >>> input auto "./config" :: IO (Vector (Vector Integer))
--- > [[1,2,3],[4,5,6]]
 
--- $optional
+-- $optional0
 --
 -- @Optional@ values are exactly like lists except they can only hold 0 or 1
 -- elements.  They cannot hold 2 or more elements:
@@ -514,6 +518,9 @@
 -- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer)
 -- > Nothing
 --
+-- You cannot omit the type annotation for @Optional@ values.  The type
+-- annotation is mandatory
+--
 -- __Exercise:__ What is the shortest possible @./config@ file that you can decode
 -- like this:
 --
@@ -591,7 +598,7 @@
 --
 -- > $ cat > makeBools
 -- > \(n : Bool) ->
--- >     [ n && True, n && False, n || True, n || False ] : List Bool
+-- >     [ n && True, n && False, n || True, n || False ]
 -- > <Ctrl-D>
 --
 -- ... or we can use Dhall's support for Unicode characters to use @λ@ (U+03BB)
@@ -600,7 +607,7 @@
 --
 -- > $ cat > makeBools
 -- > λ(n : Bool) →
--- >     [ n && True, n && False, n || True, n || False ] : List Bool
+-- >     [ n && True, n && False, n || True, n || False ]
 -- > <Ctrl-D>
 --
 -- You can read this as a function of one argument named @n@ that has type
@@ -622,7 +629,7 @@
 -- > <Ctrl-D>
 -- > ∀(n : Bool) → List Bool
 -- > 
--- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool
+-- > λ(n : Bool) → [n && True, n && False, n || True, n || False]
 --
 -- The first line says that @makeBools@ is a function of one argument named @n@
 -- that has type @Bool@ and the function returns a @List@ of @Bool@s.  The @∀@
@@ -645,7 +652,7 @@
 --
 -- The second line of Dhall's output is our program's normal form:
 --
--- > λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool
+-- > λ(n : Bool) → [n && True, n && False, n || True, n || False]
 --
 -- ... which in this case happens to be identical to our original program.
 --
@@ -663,17 +670,17 @@
 -- > <Ctrl-D>
 -- > List Bool
 -- > 
--- > [True, False, True, True] : List Bool
+-- > [True, False, True, True]
 --
 -- Remember that file paths are synonymous with their contents, so the above
 -- code is exactly equivalent to:
 -- 
 -- > $ dhall
--- > (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) True
+-- > (λ(n : Bool) → [n && True, n && False, n || True, n || False]) True
 -- > <Ctrl-D>
 -- > List Bool
 -- > 
--- > [True, False, True, True] : List Bool
+-- > [True, False, True, True]
 --
 -- When you apply an anonymous function to an argument, you substitute the
 -- \"bound variable" with the function's argument:
@@ -688,13 +695,13 @@
 -- like this:
 --
 -- > -- If we replace all of these `n`s with `True` ...
--- > [n && True, n && False, n || True, n || False] : List Bool
+-- > [n && True, n && False, n || True, n || False]
 -- >
 -- > -- ... then we get this:
--- > [True && True, True && False, True || True, True || False] : List Bool
+-- > [True && True, True && False, True || True, True || False]
 -- >
 -- > -- ... which reduces to the following normal form:
--- > [True, False, True, True] : List Bool
+-- > [True, False, True, True]
 --
 -- Now that we've verified that our function type checks and works, we can use
 -- the same function within Haskell:
@@ -999,7 +1006,7 @@
 -- Notice that each handler has to return the same type of result (@Bool@ in
 -- this case) which must also match the declared result type of the @merge@.
 --
--- __Exercise__: Create a list of the following type with at least one element:
+-- __Exercise__: Create a list of the following type with at least one element
 -- per alternative:
 --
 -- > List < Left : Integer | Right : Double >
@@ -1112,7 +1119,7 @@
 -- ... and the second argument is the list to reverse:
 --
 -- > $ dhall
--- > List/reverse Bool ([True, False] : List Bool)
+-- > List/reverse Bool [True, False]
 -- > <Ctrl-D>
 -- > List Bool
 -- > 
@@ -1170,7 +1177,7 @@
 --
 -- > $ dhall
 -- >     let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map
--- > in  λ(f : Integer → Integer) → List/map Integer Integer f ([1, 2, 3] : List Integer)
+-- > in  λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3]
 -- > <Ctrl-D>
 -- > ∀(f : Integer → Integer) → List Integer
 -- > 
@@ -1734,7 +1741,7 @@
 -- Example:
 --
 -- > $ dhall
--- > List/fold Bool ([True, False, True] : List Bool) Bool (λ(x : Bool) → λ(y : Bool) → x && y) True
+-- > List/fold Bool [True, False, True] Bool (λ(x : Bool) → λ(y : Bool) → x && y) True
 -- > <Ctrl-D>
 -- > Bool
 -- > 
@@ -1783,7 +1790,7 @@
 -- Example:
 --
 -- > $ dhall
--- > List/length Integer ([1, 2, 3] : List Integer)
+-- > List/length Integer [1, 2, 3]
 -- > <Ctrl-D>
 -- > Natural
 -- > 
@@ -1803,7 +1810,7 @@
 -- Example:
 --
 -- > $ dhall
--- > List/head Integer ([1, 2, 3] : List Integer)
+-- > List/head Integer [1, 2, 3]
 -- > <Ctrl-D>
 -- > Optional Integer
 -- > 
@@ -1834,7 +1841,7 @@
 -- Example:
 --
 -- > $ dhall
--- > List/last Integer ([1, 2, 3] : List Integer)
+-- > List/last Integer [1, 2, 3]
 -- > <Ctrl-D>
 -- > Optional Integer
 -- > 
@@ -1865,7 +1872,7 @@
 -- Example
 --
 -- > $ dhall
--- > List/indexed Text (["ABC", "DEF", "GHI"] : List Text)
+-- > List/indexed Text ["ABC", "DEF", "GHI"]
 -- > <Ctrl-D>
 -- > List { index : Natural, value : Text }
 -- > 
@@ -1890,7 +1897,7 @@
 -- Example:
 --
 -- > $ dhall
--- > List/reverse Integer ([1, 2, 3] : List Integer)
+-- > List/reverse Integer [1, 2, 3]
 -- > <Ctrl-D>
 -- > List Integer
 -- > 
@@ -1917,9 +1924,9 @@
 -- >
 -- > List/reverse a ([x, y] : List a) = [y, x] : List a
 
--- $optional
+-- $optional1
 --
--- Dhall @Optional@ literals are a 0 or 1 values inside of brackets:
+-- Dhall @Optional@ literals are 0 or 1 values inside of brackets:
 --
 -- > Γ ⊢ t : Type   Γ ⊢ x : t
 -- > ────────────────────────
@@ -2132,13 +2139,7 @@
 
 -- $faq
 --
--- * Why do lists require a type annotation?
---
--- Dhall requires type annotations on lists in order to gracefully deal with
--- empty lists.  Without a type annotation the compiler would not be able to
--- infer the type of an empty list expression:
---
--- > []
+-- * Why do empty lists require a type annotation?
 --
 -- Unlike Haskell, Dhall cannot infer a polymorphic type for the empty list
 -- because Dhall represents polymorphic values as functions of types, like this:
@@ -2149,18 +2150,3 @@
 -- the above polymorphic function then you'd get the unexpected behavior where
 -- a list literal is a function if the list has 0 elements but not a function
 -- otherwise.
---
--- * Why do lists require a type annotation when using `input`, like this:
--- 
--- > >>> input (list bool) "[True, False] : List Bool"
---
--- The type annotation on a list is not a real type annotation.  Instead, the
--- annotation on a list is part of the mandatory syntax for lists.  This is why
--- you get a parse error instead of a type error if you omit the annotation:
---
--- > dhall
--- > [1, 2]
--- > (stdin):2:1: error: unexpected
--- >     EOF, expected: ":"
--- >     <EOF> 
--- >     ^    
diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs
--- a/src/Dhall/TypeCheck.hs
+++ b/src/Dhall/TypeCheck.hs
@@ -117,11 +117,11 @@
     go _ _ = return False
 
 {-| Type-check an expression and return the expression's type if type-checking
-    suceeds or an error if type-checking fails
+    succeeds or an error if type-checking fails
 
     `typeWith` does not necessarily normalize the type since full normalization
     is not necessary for just type-checking.  If you actually care about the
-    returned type then you may want to `normalize` it afterwards.
+    returned type then you may want to `Dhall.Core.normalize` it afterwards.
 -}
 typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X)
 typeWith _     (Const c         ) = do
@@ -355,7 +355,26 @@
     return Text
 typeWith _      List              = do
     return (Pi "_" (Const Type) (Const Type))
-typeWith ctx e@(ListLit t xs    ) = do
+typeWith ctx e@(ListLit  Nothing  xs) = do
+    if Data.Vector.null xs
+        then Left (TypeError ctx e MissingListType)
+        else do
+            t <- typeWith ctx (Data.Vector.head xs)
+            s <- fmap Dhall.Core.normalize (typeWith ctx t)
+            case s of
+                Const Type -> return ()
+                _ -> Left (TypeError ctx e (InvalidListType t))
+            flip Data.Vector.imapM_ xs (\i x -> do
+                t' <- typeWith ctx x
+                if propEqual t t'
+                    then return ()
+                    else do
+                        let nf_t  = Dhall.Core.normalize t
+                        let nf_t' = Dhall.Core.normalize t'
+                        let err   = MismatchedListElements i nf_t x nf_t'
+                        Left (TypeError ctx e err) )
+            return (App List t)
+typeWith ctx e@(ListLit (Just t ) xs) = do
     s <- fmap Dhall.Core.normalize (typeWith ctx t)
     case s of
         Const Type -> return ()
@@ -562,6 +581,8 @@
     | TypeMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)
     | AnnotMismatch (Expr s X) (Expr s X) (Expr s X)
     | Untyped
+    | MissingListType
+    | MismatchedListElements Int (Expr s X) (Expr s X) (Expr s X)
     | InvalidListElement Int (Expr s X) (Expr s X) (Expr s X)
     | InvalidListType (Expr s X)
     | InvalidOptionalElement (Expr s X) (Expr s X) (Expr s X)
@@ -1121,9 +1142,9 @@
 ● You omit a function argument by mistake:
 
 
-    ┌────────────────────────────────────────┐
-    │ List/head   ([1, 2, 3] : List Integer) │
-    └────────────────────────────────────────┘
+    ┌───────────────────────┐
+    │ List/head   [1, 2, 3] │
+    └───────────────────────┘
                 ⇧
                 ❰List/head❱ is missing the first argument,
                 which should be: ❰Integer❱
@@ -1510,8 +1531,8 @@
 
     long =
         Builder.fromText [NeatInterpolation.text|
-Explanation: Every ❰List❱ documents the type of its elements with a type
-annotation, like this:
+Explanation: ❰List❱s can optionally document the type of their elements with a
+type annotation, like this:
 
 
     ┌──────────────────────────┐
@@ -1525,7 +1546,7 @@
     │ [] : List Integer │  An empty ❰List❱
     └───────────────────┘
                 ⇧
-                You still specify the type even when the ❰List❱ is empty
+                You must specify the type when the ❰List❱ is empty
 
 
 The element type must be a type and not something else.  For example, the
@@ -1546,8 +1567,6 @@
                  This is a ❰Kind❱ and not a ❰Type❱
 
 
-Even if the ❰List❱ is empty you still must specify a valid type
-
 You declared that the ❰List❱'s elements should have type:
 
 ↳ $txt0
@@ -1557,6 +1576,76 @@
       where
         txt0 = Text.toStrict (Dhall.Core.pretty expr0)
 
+prettyTypeMessage MissingListType = do
+    ErrorMessages {..}
+  where
+    short = "Empty lists need a type annotation"
+
+    long =
+        Builder.fromText [NeatInterpolation.text|
+Explanation: Lists do not require a type annotation if they have at least one
+element:
+
+
+    ┌───────────┐
+    │ [1, 2, 3] │  The compiler can infer that this list has type ❰List Integer❱
+    └───────────┘
+
+
+However, empty lists still require a type annotation:
+
+
+    ┌───────────────────┐
+    │ [] : List Integer │  This type annotation is mandatory
+    └───────────────────┘
+
+
+You cannot supply an empty list without a type annotation
+|]
+
+prettyTypeMessage (MismatchedListElements i expr0 expr1 expr2) =
+    ErrorMessages {..}
+  where
+    short = "List elements should have the same type"
+
+    long =
+        Builder.fromText [NeatInterpolation.text|
+Explanation: Every element in a list must have the same type
+
+For example, this is a valid ❰List❱:
+
+
+    ┌───────────┐
+    │ [1, 2, 3] │  Every element in this ❰List❱ is an ❰Integer❱
+    └───────────┘
+
+
+.. but this is $_NOT a valid ❰List❱:
+
+
+    ┌───────────────┐
+    │ [1, "ABC", 3] │  The first and second element have different types
+    └───────────────┘
+
+
+Your first ❰List❱ elements has this type:
+
+↳ $txt0
+
+... but the following element at index $txt1:
+
+↳ $txt2
+
+... has this type instead:
+
+↳ $txt3
+|]
+      where
+        txt0 = Text.toStrict (Dhall.Core.pretty expr0)
+        txt1 = Text.toStrict (Dhall.Core.pretty i    )
+        txt2 = Text.toStrict (Dhall.Core.pretty expr1)
+        txt3 = Text.toStrict (Dhall.Core.pretty expr2)
+
 prettyTypeMessage (InvalidListElement i expr0 expr1 expr2) =
     ErrorMessages {..}
   where
@@ -2597,9 +2686,9 @@
 
 ● You might have thought that ❰++❱ was the operator to combine two lists:
 
-    ┌───────────────────────────────────────────────────────────┐
-    │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │  Not valid
-    └───────────────────────────────────────────────────────────┘
+    ┌────────────────────────┐
+    │ [1, 2, 3] ++ [4, 5, 6] │  Not valid
+    └────────────────────────┘
 
   The Dhall programming language does not provide a built-in operator for
   combining two lists