diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,56 @@
+1.13.0
+
+* BUG FIX: Fix semantic integrity hashing support
+    * Both parsing and pretty-printing semantic hashes were broken since version
+      1.11.0
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/345
+* BUG FIX: Allow leading whitespace in interpolated expresssions
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/369
+* BUG FIX: Fix `deriving (Interpret)` for sum types
+    * The types of alternatives were not correctly included in the corresponding
+      Dhall type
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/348
+* BREAKING CHANGE TO LANGUAGE: Records cannot store both types and terms
+    * Records can also not store type-level functions (like `List`)
+        * Records might be allowed to store type-level functions again in the
+          future
+    * This fixes a potential soundness bug
+    * The primarily practical consequence of this change is that if you are
+      hosting a "package" then you will need to split terms and types from your
+      package into different records for your users to import
+    * This also implies removing the `./Monoid` type-level function from the
+      `./Prelude/package.dhall` record
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/335
+* BREAKING CHANGE TO THE API: Replace `trifecta` with `megaparsec`
+    * This change the API to use the `Parser` type from `megaparsec`
+    * This also slightly changes the type of `exprFromText`
+    * If you program using the type classes provided by the `parsers` library
+      then this is not a breaking change as that interface is preserved
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/268
+* BREAKING CHANGE TO THE API: New `⩓` operator for merging record types
+    * Example: `{ foo : Text } ⩓ { bar : Bool } = { foo : Text, bar : Bool }`
+    * This is breaking because it adds a new constructor to the `Expr` type
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/342
+* BREAKING CHANGE TO THE API: New support for projecting a subset of fields
+    * Example: `{ x = 1, y = 2, z = 3 }.{ x, y } = { x = 1, y = 2 }`
+    * This is breaking because it adds a new constructor to the `Expr` type
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/350
+* API+UX feature: New support for pretty-printing diffs of Dhall expressions
+    * Error messages also use this feature to simplify large type mismatches
+    * There is also a new `Dhall.Diff` module
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/336
+* Add `version`, `resolve`, `type`, and `normalize` sub-commands to interpreter
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/352
+* Support GHC 7.10.3
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/340
+* `:type` command in `dhall-repl` now only displays the type
+    * Before it would also display the original expression
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/344
+* Trim dependency tree
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/351
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/268
+    * See: https://github.com/dhall-lang/dhall-haskell/pull/355
+
 1.12.0
 
 * Additional changes to support GHC 8.4
diff --git a/dhall-format/Main.hs b/dhall-format/Main.hs
--- a/dhall-format/Main.hs
+++ b/dhall-format/Main.hs
@@ -1,10 +1,5 @@
-{-# LANGUAGE DataKinds          #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE ExplicitNamespaces #-}
-{-# LANGUAGE FlexibleInstances  #-}
-{-# LANGUAGE OverloadedStrings  #-}
-{-# LANGUAGE RecordWildCards    #-}
-{-# LANGUAGE TypeOperators      #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
 
 {-| Utility executable for pretty-printing Dhall code
 
@@ -27,16 +22,16 @@
 -}
 module Main where
 
+import Control.Applicative (optional)
 import Control.Exception (SomeException)
 import Control.Monad (when)
 import Data.Monoid ((<>))
 import Data.Version (showVersion)
 import Dhall.Parser (exprAndHeaderFromText)
 import Dhall.Pretty (annToAnsiStyle, prettyExpr)
-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))
+import Options.Applicative (Parser, ParserInfo)
 import System.IO (stderr)
 import System.Exit (exitFailure, exitSuccess)
-import Text.Trifecta.Delta (Delta(..))
 
 import qualified Paths_dhall as Meta
 
@@ -46,25 +41,48 @@
 import qualified Data.Text.Lazy.IO
 import qualified Data.Text.Prettyprint.Doc                 as Pretty
 import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
-import qualified Options.Generic
+import qualified Options.Applicative
 import qualified System.Console.ANSI
 import qualified System.IO
 
-data Options w = Options
-    { version :: w ::: Bool           <?> "Display version and exit"
-    , inplace :: w ::: Maybe FilePath <?> "Modify the specified file in-place"
-    } deriving (Generic)
+data Options = Options
+    { version :: Bool
+    , inplace :: Maybe FilePath
+    }
 
-instance ParseRecord (Options Wrapped)
+parseOptions :: Parser Options
+parseOptions = Options <$> parseVersion <*> optional parseInplace
+  where
+    parseVersion =
+        Options.Applicative.switch
+        (   Options.Applicative.long "version"
+        <>  Options.Applicative.help "Display version and exit"
+        )
 
+    parseInplace =
+        Options.Applicative.strOption
+        (   Options.Applicative.long "inplace"
+        <>  Options.Applicative.help "Modify the specified file in-place"
+        <>  Options.Applicative.metavar "FILE"
+        )
+
 opts :: Pretty.LayoutOptions
 opts =
     Pretty.defaultLayoutOptions
         { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }
 
+parserInfo :: ParserInfo Options
+parserInfo =
+    Options.Applicative.info
+        (Options.Applicative.helper <*> parseOptions)
+        (   Options.Applicative.progDesc "Formatter for the Dhall language"
+        <>  Options.Applicative.fullDesc
+        )
+
 main :: IO ()
 main = do
-    Options {..} <- Options.Generic.unwrapRecord "Formatter for the Dhall language"
+    Options {..} <- Options.Applicative.execParser parserInfo
+
     when version $ do
       putStrLn (showVersion Meta.version)
       exitSuccess
@@ -80,7 +98,7 @@
             Just file -> do
                 strictText <- Data.Text.IO.readFile file
                 let lazyText = Data.Text.Lazy.fromStrict strictText
-                (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) lazyText of
+                (header, expr) <- case exprAndHeaderFromText "(stdin)" lazyText of
                     Left  err -> Control.Exception.throwIO err
                     Right x   -> return x
 
@@ -92,7 +110,7 @@
                 System.IO.hSetEncoding System.IO.stdin System.IO.utf8
                 inText <- Data.Text.Lazy.IO.getContents
 
-                (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) inText of
+                (header, expr) <- case exprAndHeaderFromText "(stdin)" inText of
                     Left  err -> Control.Exception.throwIO err
                     Right x   -> return x
 
diff --git a/dhall-hash/Main.hs b/dhall-hash/Main.hs
--- a/dhall-hash/Main.hs
+++ b/dhall-hash/Main.hs
@@ -1,43 +1,60 @@
-{-# LANGUAGE DataKinds          #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE ExplicitNamespaces #-}
-{-# LANGUAGE FlexibleInstances  #-}
-{-# LANGUAGE OverloadedStrings  #-}
-{-# LANGUAGE RecordWildCards    #-}
-{-# LANGUAGE TypeOperators      #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
 
 module Main where
 
 import Control.Exception (SomeException)
 import Control.Monad (when)
+import Data.Monoid ((<>))
 import Data.Version (showVersion)
 import Dhall.Core (normalize)
 import Dhall.Import (Imported(..), hashExpressionToCode, load)
 import Dhall.Parser (Src, exprFromText)
 import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))
+import Options.Applicative (Parser, ParserInfo)
 import System.IO (stderr)
 import System.Exit (exitFailure, exitSuccess)
-import Text.Trifecta.Delta (Delta(..))
 
 import qualified Paths_dhall as Meta
 
 import qualified Control.Exception
 import qualified Data.Text.Lazy.IO
 import qualified Dhall.TypeCheck
-import qualified Options.Generic
+import qualified Options.Applicative
 import qualified System.IO
 
-data Options w = Options
-    { explain :: w ::: Bool <?> "Explain error messages in more detail"
-    , version :: w ::: Bool <?> "Display version and exit"
-    } deriving (Generic)
+data Options = Options
+    { explain :: Bool
+    , version :: Bool
+    }
 
-instance ParseRecord (Options Wrapped)
+parseOptions :: Parser Options
+parseOptions = Options <$> parseExplain <*> parseVersion
+  where
+    parseExplain =
+        Options.Applicative.switch
+            (   Options.Applicative.long "explain"
+            <>  Options.Applicative.help "Explain error messages in more detail"
+            )
 
+    parseVersion =
+        Options.Applicative.switch
+            (   Options.Applicative.long "version"
+            <>  Options.Applicative.help "Display version and exit"
+            )
+
+parserInfo :: ParserInfo Options
+parserInfo =
+    Options.Applicative.info
+        (Options.Applicative.helper <*> parseOptions)
+        (   Options.Applicative.progDesc "Compute semantic hashes for Dhall expressions"
+        <>  Options.Applicative.fullDesc
+        )
+
 main :: IO ()
 main = do
-    Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"
+    Options {..} <- Options.Applicative.execParser parserInfo
+
     when version $ do
       putStrLn (showVersion Meta.version)
       exitSuccess
@@ -74,7 +91,7 @@
         System.IO.hSetEncoding System.IO.stdin System.IO.utf8
         inText <- Data.Text.Lazy.IO.getContents
 
-        expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of
+        expr <- case exprFromText "(stdin)" inText of
             Left  err  -> Control.Exception.throwIO err
             Right expr -> return expr
 
diff --git a/dhall-repl/Main.hs b/dhall-repl/Main.hs
--- a/dhall-repl/Main.hs
+++ b/dhall-repl/Main.hs
@@ -24,7 +24,6 @@
 import qualified System.Console.Haskeline.MonadException as Haskeline
 import qualified System.Console.Repline as Repline
 import qualified System.IO
-import qualified Text.Trifecta.Delta as Trifecta
 
 
 main :: IO ()
@@ -75,7 +74,7 @@
   => String -> m ( Dhall.Expr Dhall.Src Dhall.X )
 parseAndLoad src = do
   parsed <-
-    case Dhall.exprFromText ( Trifecta.Columns 0 0 ) ( LazyText.pack src ) of
+    case Dhall.exprFromText "(stdin)" ( LazyText.pack src ) of
       Left e ->
         liftIO ( throwIO e )
 
@@ -117,7 +116,7 @@
   exprType' <-
     normalize exprType
 
-  output System.IO.stdout ( Expr.Annot loaded exprType' )
+  output System.IO.stdout exprType'
 
 
 
@@ -233,6 +232,8 @@
     :: (Pretty.Pretty a, MonadIO m)
     => System.IO.Handle -> Dhall.Expr s a -> m ()
 output handle expr = do
+  liftIO (System.IO.hPutStrLn handle "")  -- Visual spacing
+
   let opts =
           Pretty.defaultLayoutOptions
               { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }
@@ -245,5 +246,6 @@
           else Pretty.unAnnotateS stream
 
   liftIO (Pretty.renderIO handle ansiStream)
+  liftIO (System.IO.hPutStrLn handle "") -- Pretty printing doesn't end with a new line
 
-  liftIO (putStrLn "") -- Pretty printing doesn't end with a new line
+  liftIO (System.IO.hPutStrLn handle "")  -- Visual spacing
diff --git a/dhall.cabal b/dhall.cabal
--- a/dhall.cabal
+++ b/dhall.cabal
@@ -1,5 +1,5 @@
 Name: dhall
-Version: 1.12.0
+Version: 1.13.0
 Cabal-Version: >=1.8.0.2
 Build-Type: Simple
 Tested-With: GHC == 8.0.1
@@ -82,6 +82,8 @@
     Prelude/Text/concatMapSep
     Prelude/Text/concatSep
     tests/format/*.dhall
+    tests/normalization/tutorial/combineTypes/*.dhall
+    tests/normalization/tutorial/projection/*.dhall
     tests/normalization/*.dhall
     tests/normalization/examples/Bool/and/*.dhall
     tests/normalization/examples/Bool/build/*.dhall
@@ -153,9 +155,8 @@
 Library
     Hs-Source-Dirs: src
     Build-Depends:
-        base                        >= 4.9.0.0  && < 5   ,
-        ansi-wl-pprint                           < 0.7 ,
-        base16-bytestring                        < 0.2 ,
+        base                        >= 4.8.2.0  && < 5   ,
+        ansi-terminal               >= 0.6.3.1  && < 0.8 ,
         bytestring                               < 0.11,
         case-insensitive                         < 1.3 ,
         containers                  >= 0.5.0.0  && < 0.6 ,
@@ -169,6 +170,7 @@
         http-client-tls             >= 0.2.0    && < 0.4 ,
         insert-ordered-containers   >= 0.1.0.1  && < 0.3 ,
         lens-family-core            >= 1.0.0    && < 1.3 ,
+        megaparsec                  >= 6.1.1    && < 6.5 ,
         memory                      >= 0.14     && < 0.15,
         parsers                     >= 0.12.4   && < 0.13,
         prettyprinter               >= 1.2.0.1  && < 1.3 ,
@@ -176,13 +178,16 @@
         scientific                  >= 0.3.0.0  && < 0.4 ,
         text                        >= 0.11.1.0 && < 1.3 ,
         transformers                >= 0.2.0.0  && < 0.6 ,
-        trifecta                    >= 1.6      && < 1.8 ,
         unordered-containers        >= 0.1.3.0  && < 0.3 ,
         vector                      >= 0.11.0.0 && < 0.13
+    if !impl(ghc >= 8.0)
+      Build-Depends: semigroups == 0.18.*
+
     Exposed-Modules:
         Dhall,
         Dhall.Context,
         Dhall.Core,
+        Dhall.Diff
         Dhall.Import,
         Dhall.Parser,
         Dhall.Pretty,
@@ -190,7 +195,7 @@
         Dhall.TypeCheck
     Other-Modules:
         Dhall.Pretty.Internal
-    GHC-Options: -Wall -Wcompat
+    GHC-Options: -Wall
 
 Executable dhall
     Hs-Source-Dirs: dhall
@@ -199,12 +204,12 @@
         ansi-terminal               >= 0.6.3.1  && < 0.9 ,
         base                        >= 4        && < 5   ,
         dhall                                            ,
-        optparse-generic            >= 1.1.1    && < 1.4 ,
+        optparse-applicative                       < 0.15,
         prettyprinter                                    ,
         prettyprinter-ansi-terminal >= 1.1.1    && < 1.2 ,
-        trifecta                    >= 1.6      && < 1.8 ,
+        megaparsec                  >= 6.1.1    && < 6.5 ,
         text                        >= 0.11.1.0 && < 1.3
-    GHC-Options: -Wall -Wcompat
+    GHC-Options: -Wall
     Other-Modules:
         Paths_dhall
 
@@ -220,9 +225,10 @@
         repline          >= 0.1.6.0  && < 0.2 ,
         prettyprinter                         ,
         prettyprinter-ansi-terminal           ,
-        text                                  ,
-        trifecta
-    GHC-Options: -Wall -Wcompat
+        text
+    if !impl(ghc >= 8.0)
+      Build-Depends: transformers == 0.4.2.*
+    GHC-Options: -Wall
 
 Executable dhall-format
     Hs-Source-Dirs: dhall-format
@@ -230,13 +236,13 @@
     Build-Depends:
         base                        >= 4        && < 5   ,
         ansi-terminal               >= 0.6.3.1  && < 0.9 ,
-        dhall                                ,
-        optparse-generic            >= 1.1.1    && < 1.4 ,
+        dhall                                            ,
+        megaparsec                  >= 6.1.1    && < 6.5 ,
+        optparse-applicative                       < 0.15,
         prettyprinter               >= 1.2.0.1  && < 1.3 ,
         prettyprinter-ansi-terminal >= 1.1.1    && < 1.2 ,
-        trifecta                    >= 1.6      && < 1.8 ,
         text                        >= 0.11.1.0 && < 1.3
-    GHC-Options: -Wall -Wcompat
+    GHC-Options: -Wall
     Other-Modules:
         Paths_dhall
 
@@ -244,11 +250,11 @@
     Hs-Source-Dirs: dhall-hash
     Main-Is: Main.hs
     Build-Depends:
-        base             >= 4        && < 5  ,
-        dhall                                ,
-        optparse-generic >= 1.1.1    && < 1.4,
-        trifecta         >= 1.6      && < 1.8,
-        text             >= 0.11.1.0 && < 1.3
+        base                 >= 4        && < 5   ,
+        dhall                                     ,
+        optparse-applicative                < 0.15,
+        megaparsec           >= 6.1.1    && < 6.5 ,
+        text                 >= 0.11.1.0 && < 1.3
     Other-Modules:
         Paths_dhall
 
@@ -256,7 +262,7 @@
     Type: exitcode-stdio-1.0
     Hs-Source-Dirs: tests
     Main-Is: Tests.hs
-    GHC-Options: -Wall -Wcompat
+    GHC-Options: -Wall
     Other-Modules:
         Format
         Normalization
diff --git a/dhall/Main.hs b/dhall/Main.hs
--- a/dhall/Main.hs
+++ b/dhall/Main.hs
@@ -1,25 +1,24 @@
-{-# LANGUAGE DataKinds          #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE ExplicitNamespaces #-}
-{-# LANGUAGE FlexibleInstances  #-}
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE OverloadedStrings  #-}
 {-# LANGUAGE RecordWildCards    #-}
-{-# LANGUAGE TypeOperators      #-}
 
 module Main where
 
-import Control.Exception (SomeException)
-import Control.Monad (when)
-import Data.Monoid (mempty)
+import Control.Applicative ((<|>))
+import Control.Exception (Exception, SomeException)
+import Data.Monoid (mempty, (<>))
+import Data.Text.Prettyprint.Doc (Pretty)
+import Data.Typeable (Typeable)
 import Data.Version (showVersion)
-import Dhall.Core (normalize)
+import Dhall.Core (Expr, Path)
 import Dhall.Import (Imported(..), load)
 import Dhall.Parser (Src)
 import Dhall.Pretty (annToAnsiStyle, prettyExpr)
 import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))
-import System.Exit (exitFailure, exitSuccess)
-import Text.Trifecta.Delta (Delta(..))
+import Options.Applicative (Parser)
+import System.Exit (exitFailure)
+import System.IO (Handle)
 
 import qualified Paths_dhall as Meta
 
@@ -27,32 +26,97 @@
 import qualified Data.Text.Lazy.IO
 import qualified Data.Text.Prettyprint.Doc                 as Pretty
 import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
+import qualified Dhall.Core
 import qualified Dhall.Parser
 import qualified Dhall.TypeCheck
-import qualified Options.Generic
+import qualified Options.Applicative
 import qualified System.Console.ANSI
 import qualified System.IO
 
-data Options w = Options
-    { explain :: w ::: Bool <?> "Explain error messages in more detail"
-    , version :: w ::: Bool <?> "Display version and exit"
-    , plain   :: w ::: Bool <?> "Disable syntax highlighting"
-    } deriving (Generic)
+data Options = Options
+    { mode    :: Mode
+    , explain :: Bool
+    , plain   :: Bool
+    }
 
-instance ParseRecord (Options Wrapped)
+data Mode = Default | Version | Resolve | Type | Normalize
 
+parseOptions :: Parser Options
+parseOptions = Options <$> parseMode <*> parseExplain <*> parsePlain
+  where
+    parseExplain =
+        Options.Applicative.switch
+            (   Options.Applicative.long "explain"
+            <>  Options.Applicative.help "Explain error messages in more detail"
+            )
+
+    parsePlain =
+        Options.Applicative.switch
+            (   Options.Applicative.long "plain"
+            <>  Options.Applicative.help "Disable syntax highlighting"
+            )
+
+parseMode :: Parser Mode
+parseMode =
+        subcommand "version"   "Display version"                 Version
+    <|> subcommand "resolve"   "Resolve an expression's imports" Resolve
+    <|> subcommand "type"      "Infer an expression's type"      Type
+    <|> subcommand "normalize" "Normalize an expression"         Normalize
+    <|> pure Default
+  where
+    subcommand name description mode =
+        Options.Applicative.subparser
+            (   Options.Applicative.command name parserInfo
+            <>  Options.Applicative.metavar name
+            )
+      where
+        parserInfo =
+            Options.Applicative.info parser
+                (   Options.Applicative.fullDesc
+                <>  Options.Applicative.progDesc description
+                )
+
+        parser =
+            Options.Applicative.helper <*> pure mode
+
 opts :: Pretty.LayoutOptions
 opts =
     Pretty.defaultLayoutOptions
         { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }
 
+data ImportResolutionDisabled =
+    ImportResolutionDisabled deriving (Exception, Typeable)
+
+instance Show ImportResolutionDisabled where
+    show _ = "\nImport resolution is disabled"
+
+throws :: Exception e => Either e a -> IO a
+throws (Left  e) = Control.Exception.throwIO e
+throws (Right a) = return a
+
+getExpression :: IO (Expr Src Path)
+getExpression = do
+    inText <- Data.Text.Lazy.IO.getContents
+
+    throws (Dhall.Parser.exprFromText "(stdin)" inText)
+
+assertNoImports :: Expr Src Path -> IO (Expr Src X)
+assertNoImports expression =
+    throws (traverse (\_ -> Left ImportResolutionDisabled) expression)
+
 main :: IO ()
 main = do
-    Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"
-    when version $ do
-      putStrLn (showVersion Meta.version)
-      exitSuccess
+    let parserInfo =
+            Options.Applicative.info
+                (Options.Applicative.helper <*> parseOptions)
+                (   Options.Applicative.progDesc "Interpreter for the Dhall language"
+                <>  Options.Applicative.fullDesc
+                )
 
+    Options {..} <- Options.Applicative.execParser parserInfo
+
+    System.IO.hSetEncoding System.IO.stdin System.IO.utf8
+
     let handle =
                 Control.Exception.handle handler2
             .   Control.Exception.handle handler1
@@ -82,36 +146,61 @@
                 System.IO.hPrint System.IO.stderr e
                 System.Exit.exitFailure
 
-    handle (do
-        System.IO.hSetEncoding System.IO.stdin System.IO.utf8
-        inText <- Data.Text.Lazy.IO.getContents
+    let render :: Pretty a => Handle -> Expr s a -> IO ()
+        render h e = do
+            let doc = prettyExpr e
 
-        expr <- case Dhall.Parser.exprFromText (Directed "(stdin)" 0 0 0 0) inText of
-            Left  err -> Control.Exception.throwIO err
-            Right x   -> return x
+            let layoutOptions = opts
 
-        let render h e = do
-                let doc = prettyExpr e
+            let stream = Pretty.layoutSmart layoutOptions doc
 
-                let layoutOptions = opts
-                let stream = Pretty.layoutSmart layoutOptions doc
+            supportsANSI <- System.Console.ANSI.hSupportsANSI h
+            let ansiStream =
+                    if supportsANSI && not plain
+                    then fmap annToAnsiStyle stream
+                    else Pretty.unAnnotateS stream
 
-                supportsANSI <- System.Console.ANSI.hSupportsANSI h
-                let ansiStream =
-                        if supportsANSI && not plain
-                        then fmap annToAnsiStyle stream
-                        else Pretty.unAnnotateS stream
+            Pretty.renderIO h ansiStream
+            Data.Text.Lazy.IO.hPutStrLn h ""
 
-                Pretty.renderIO h ansiStream
-                Data.Text.Lazy.IO.hPutStrLn h ""
+    handle $ case mode of
+        Version -> do
+            putStrLn (showVersion Meta.version)
 
+        Default -> do
+            expression <- getExpression
 
-        expr' <- load expr
+            resolvedExpression <- load expression
 
-        typeExpr <- case Dhall.TypeCheck.typeOf expr' of
-            Left  err      -> Control.Exception.throwIO err
-            Right typeExpr -> return typeExpr
+            inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression)
 
-        render System.IO.stderr (normalize typeExpr)
-        Data.Text.Lazy.IO.hPutStrLn System.IO.stderr mempty
-        render System.IO.stdout (normalize expr') )
+            render System.IO.stderr (Dhall.Core.normalize inferredType)
+
+            Data.Text.Lazy.IO.hPutStrLn System.IO.stderr mempty
+
+            render System.IO.stdout (Dhall.Core.normalize resolvedExpression)
+
+        Resolve -> do
+            expression <- getExpression
+
+            resolvedExpression <- load expression
+
+            render System.IO.stdout resolvedExpression
+
+        Normalize -> do
+            expression <- getExpression
+
+            resolvedExpression <- assertNoImports expression
+
+            _ <- throws (Dhall.TypeCheck.typeOf resolvedExpression)
+
+            render System.IO.stdout (Dhall.Core.normalize resolvedExpression)
+
+        Type -> do
+            expression <- getExpression
+
+            resolvedExpression <- assertNoImports expression
+
+            inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression)
+
+            render System.IO.stdout (Dhall.Core.normalize inferredType)
diff --git a/src/Dhall.hs b/src/Dhall.hs
--- a/src/Dhall.hs
+++ b/src/Dhall.hs
@@ -1,16 +1,15 @@
-{-# LANGUAGE DefaultSignatures   #-}
-{-# LANGUAGE DeriveAnyClass      #-}
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE DeriveGeneric       #-}
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE OverloadedStrings   #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE RecordWildCards     #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving  #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RecordWildCards            #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE TypeOperators              #-}
 
 {-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining
     how to use the language, the compiler, and this library
@@ -25,6 +24,7 @@
 
     -- * Types
     , Type(..)
+    , RecordType(..)
     , InputType(..)
     , Interpret(..)
     , InvalidType(..)
@@ -46,6 +46,8 @@
     , unit
     , string
     , pair
+    , record
+    , field
     , GenericInterpret(..)
     , GenericInject(..)
 
@@ -82,11 +84,12 @@
 import GHC.Generics
 import Numeric.Natural (Natural)
 import Prelude hiding (maybe, sequence)
-import Text.Trifecta.Delta (Delta(..))
 
+import qualified Control.Applicative
 import qualified Control.Exception
-import qualified Data.ByteString.Lazy
 import qualified Data.Foldable
+import qualified Data.Functor.Compose
+import qualified Data.Functor.Product
 import qualified Data.HashMap.Strict.InsOrd
 import qualified Data.Scientific
 import qualified Data.Sequence
@@ -94,7 +97,6 @@
 import qualified Data.Text
 import qualified Data.Text.Lazy
 import qualified Data.Text.Lazy.Builder
-import qualified Data.Text.Lazy.Encoding
 import qualified Data.Vector
 import qualified Dhall.Context
 import qualified Dhall.Core
@@ -166,13 +168,10 @@
     -> IO a
     -- ^ The decoded value in Haskell
 inputWith (Type {..}) ctx n txt = do
-    let delta = Directed "(input)" 0 0 0 0
-    expr  <- throws (Dhall.Parser.exprFromText delta txt)
+    expr  <- throws (Dhall.Parser.exprFromText "(input)" txt)
     expr' <- Dhall.Import.loadWithContext ctx expr
     let suffix =
-            ( Data.ByteString.Lazy.toStrict
-            . Data.Text.Lazy.Encoding.encodeUtf8
-            . Data.Text.Lazy.Builder.toLazyText
+            ( Data.Text.Lazy.Builder.toLazyText
             . build
             ) expected
     let annot = case expr' of
@@ -580,7 +579,7 @@
 
         Type extractIn expectedIn = autoWith opts
 
-deriving instance (Interpret a, Interpret b) => Interpret (a, b)
+instance (Interpret a, Interpret b) => Interpret (a, b)
 
 {-| Use the default options for interpreting a configuration file
 
@@ -884,7 +883,7 @@
 
 instance Inject Double where
     injectWith =
-        fmap (contramap (Data.Scientific.fromFloatDigits @Double)) injectWith
+        fmap (contramap (Data.Scientific.fromFloatDigits :: Double -> Scientific)) injectWith
 
 instance Inject () where
     injectWith _ = InputType {..}
@@ -923,7 +922,7 @@
 instance Inject a => Inject (Data.Set.Set a) where
     injectWith = fmap (contramap Data.Set.toList) injectWith
 
-deriving instance (Inject a, Inject b) => Inject (a, b)
+instance (Inject a, Inject b) => Inject (a, b)
 
 {-| This is the underlying class that powers the `Interpret` class's support
     for automatically deriving a generic implementation
@@ -945,10 +944,10 @@
     genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})
       where
         embed (L1 (M1 l)) =
-            UnionLit keyL (embedL l) Data.HashMap.Strict.InsOrd.empty
+            UnionLit keyL (embedL l) (Data.HashMap.Strict.InsOrd.singleton keyR declaredR)
 
         embed (R1 (M1 r)) =
-            UnionLit keyR (embedR r) Data.HashMap.Strict.InsOrd.empty
+            UnionLit keyR (embedR r) (Data.HashMap.Strict.InsOrd.singleton keyL declaredL)
 
         declared =
             Union (Data.HashMap.Strict.InsOrd.fromList [(keyL, declaredL), (keyR, declaredR)])
@@ -1058,3 +1057,91 @@
         n = undefined
 
         InputType embedIn declaredIn = injectWith opts
+
+{-| The 'RecordType' applicative functor allows you to build a 'Type' parser
+    from a Dhall record.
+
+    For example, let's take the following Haskell data type:
+
+> data Project = Project
+>   { projectName :: Text
+>   , projectDescription :: Text
+>   , projectStars :: Natural
+>   }
+
+    And assume that we have the following Dhall record that we would like to
+    parse as a @Project@:
+
+> { name =
+>     "dhall-haskell"
+> , description =
+>     "A configuration language guaranteed to terminate"
+> , stars =
+>     +289
+> }
+
+    Our parser has type 'Type' @Project@, but we can't build that out of any
+    smaller parsers, as 'Type's cannot be combined (they are only 'Functor's).
+    However, we can use a 'RecordType' to build a 'Type' for @Project@:
+
+> project :: Type Project
+> project =
+>   record
+>     ( Project <$> field "name" string
+>               <*> field "description" string
+>               <*> field "stars" natural
+>     )
+
+-}
+
+newtype RecordType a =
+  RecordType
+    ( Data.Functor.Product.Product
+        ( Control.Applicative.Const
+            ( Data.HashMap.Strict.InsOrd.InsOrdHashMap
+                Data.Text.Lazy.Text
+                ( Expr Src X )
+            )
+        )
+        ( Data.Functor.Compose.Compose
+            ( (->) ( Expr Src X ) )
+            Maybe
+        )
+        a
+    )
+  deriving (Functor, Applicative)
+
+
+-- | Run a 'RecordType' parser to build a 'Type' parser.
+record :: RecordType a -> Dhall.Type a
+record ( RecordType ( Data.Functor.Product.Pair ( Control.Applicative.Const fields ) ( Data.Functor.Compose.Compose extractF ) ) ) =
+  Type
+    { extract =
+        extractF
+    , expected =
+        Record fields
+    }
+
+
+-- | Parse a single field of a record.
+field :: Data.Text.Lazy.Text -> Type a -> RecordType a
+field key valueType =
+  let
+    extractBody expr = do
+      RecordLit fields <-
+        return expr
+
+      Data.HashMap.Strict.InsOrd.lookup key fields
+        >>= extract valueType
+
+  in
+    RecordType
+      ( Data.Functor.Product.Pair
+          ( Control.Applicative.Const
+              ( Data.HashMap.Strict.InsOrd.singleton
+                  key
+                  ( Dhall.expected valueType )
+              )
+          )
+          ( Data.Functor.Compose.Compose extractBody )
+      )
diff --git a/src/Dhall/Context.hs b/src/Dhall/Context.hs
--- a/src/Dhall/Context.hs
+++ b/src/Dhall/Context.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE BangPatterns               #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveFunctor #-}
 
 -- | This is a utility module that consolidates all `Context`-related operations
 
@@ -50,7 +48,6 @@
 match :: Context a -> Maybe (Text, a, Context a)
 match (Context ((k, v) : kvs)) = Just (k, v, Context kvs)
 match (Context           []  ) = Nothing
-
 {-# INLINABLE match #-}
 
 {-| Look up a key by name and index
@@ -61,9 +58,9 @@
 > lookup k n (insert j v c) = lookup k  n      c  -- k /= j
 -}
 lookup :: Text -> Integer -> Context a -> Maybe a
-lookup _ !_ (Context         []  ) =
+lookup _ _ (Context         []  ) =
     Nothing
-lookup x !n (Context ((k, v):kvs)) =
+lookup x n (Context ((k, v):kvs)) =
     if x == k
     then if n == 0
          then Just v
diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs
--- a/src/Dhall/Core.hs
+++ b/src/Dhall/Core.hs
@@ -60,8 +60,9 @@
 import Data.HashSet (HashSet)
 import Data.String (IsString(..))
 import Data.Scientific (Scientific)
-import Data.Sequence (Seq, ViewL(..), ViewR(..))
 import Data.Semigroup (Semigroup(..))
+import Data.Sequence (Seq, ViewL(..), ViewR(..))
+import Data.Set (Set)
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy.Builder (Builder)
 import Data.Text.Prettyprint.Doc (Pretty)
@@ -76,6 +77,7 @@
 import qualified Data.HashMap.Strict.InsOrd
 import qualified Data.HashSet
 import qualified Data.Sequence
+import qualified Data.Set
 import qualified Data.Text
 import qualified Data.Text.Lazy                        as Text
 import qualified Data.Text.Lazy.Builder                as Builder
@@ -111,7 +113,7 @@
     = File HasHome FilePath
     -- ^ Local path
     | URL  Text (Maybe PathHashed)
-    -- ^ URL of emote resource and optional headers stored in a path
+    -- ^ URL of remote resource and optional headers stored in a path
     | Env  Text
     -- ^ Environment variable
     deriving (Eq, Ord, Show)
@@ -305,16 +307,18 @@
     | OptionalFold
     -- | > OptionalBuild                            ~  Optional/build
     | OptionalBuild
-    -- | > Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }
+    -- | > Record       [(k1, t1), (k2, t2)]        ~  { k1 : t1, k2 : t1 }
     | Record    (InsOrdHashMap Text (Expr s a))
-    -- | > RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }
+    -- | > RecordLit    [(k1, v1), (k2, v2)]        ~  { k1 = v1, k2 = v2 }
     | RecordLit (InsOrdHashMap Text (Expr s a))
-    -- | > Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1 | k2 : t2 >
+    -- | > Union        [(k1, t1), (k2, t2)]        ~  < k1 : t1 | k2 : t2 >
     | Union     (InsOrdHashMap Text (Expr s a))
-    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1 | k2 : t2 | k3 : t3 >
+    -- | > UnionLit k v [(k1, t1), (k2, t2)]        ~  < k = v | k1 : t1 | k2 : t2 >
     | UnionLit Text (Expr s a) (InsOrdHashMap Text (Expr s a))
     -- | > Combine x y                              ~  x ∧ y
     | Combine (Expr s a) (Expr s a)
+    -- | > CombineTypes x y                         ~  x ⩓ y
+    | CombineTypes (Expr s a) (Expr s a)
     -- | > CombineRight x y                         ~  x ⫽ y
     | Prefer (Expr s a) (Expr s a)
     -- | > Merge x y (Just t )                      ~  merge x y : t
@@ -324,6 +328,8 @@
     | Constructors (Expr s a)
     -- | > Field e x                                ~  e.x
     | Field (Expr s a) Text
+    -- | > Project e xs                             ~  e.{ xs }
+    | Project (Expr s a) (Set Text)
     -- | > Note s x                                 ~  e
     | Note s (Expr s a)
     -- | > Embed path                               ~  path
@@ -391,10 +397,12 @@
     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)
+    CombineTypes a b     >>= k = CombineTypes (a >>= k) (b >>= k)
     Prefer a b           >>= k = Prefer (a >>= k) (b >>= k)
     Merge a b c          >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)
     Constructors a       >>= k = Constructors (a >>= k)
     Field a b            >>= k = Field (a >>= k) b
+    Project a b          >>= k = Project (a >>= k) b
     Note a b             >>= k = Note a (b >>= k)
     Embed a              >>= k = k a
 
@@ -452,10 +460,12 @@
     first k (Union a             ) = Union (fmap (first k) a)
     first k (UnionLit a b c      ) = UnionLit a (first k b) (fmap (first k) c)
     first k (Combine a b         ) = Combine (first k a) (first k b)
+    first k (CombineTypes a b    ) = CombineTypes (first k a) (first k b)
     first k (Prefer a b          ) = Prefer (first k a) (first k b)
     first k (Merge a b c         ) = Merge (first k a) (first k b) (fmap (first k) c)
     first k (Constructors a      ) = Constructors (first k a)
     first k (Field a b           ) = Field (first k a) b
+    first k (Project a b         ) = Project (first k a) b
     first k (Note a b            ) = Note (k a) (first k b)
     first _ (Embed a             ) = Embed a
 
@@ -690,6 +700,10 @@
   where
     a' = shift d v a
     b' = shift d v b
+shift d v (CombineTypes a b) = CombineTypes a' b'
+  where
+    a' = shift d v a
+    b' = shift d v b
 shift d v (Prefer a b) = Prefer a' b'
   where
     a' = shift d v a
@@ -705,6 +719,9 @@
 shift d v (Field a b) = Field a' b
   where
     a' = shift d v a
+shift d v (Project a b) = Project a' b
+  where
+    a' = shift d v a
 shift d v (Note a b) = Note a b'
   where
     b' = shift d v b
@@ -830,6 +847,10 @@
   where
     a' = subst x e a
     b' = subst x e b
+subst x e (CombineTypes a b) = CombineTypes a' b'
+  where
+    a' = subst x e a
+    b' = subst x e b
 subst x e (Prefer a b) = Prefer a' b'
   where
     a' = subst x e a
@@ -845,6 +866,9 @@
 subst x e (Field a b) = Field a' b
   where
     a' = subst x e a
+subst x e (Project a b) = Project a' b
+  where
+    a' = subst x e a
 subst x e (Note a b) = Note a b'
   where
     b' = subst x e b
@@ -1075,6 +1099,12 @@
     l₁ = alphaNormalize l₀
 
     r₁ = alphaNormalize r₀
+alphaNormalize (CombineTypes l₀ r₀) =
+    CombineTypes l₁ r₁
+  where
+    l₁ = alphaNormalize l₀
+
+    r₁ = alphaNormalize r₀
 alphaNormalize (Prefer l₀ r₀) =
     Prefer l₁ r₁
   where
@@ -1097,6 +1127,10 @@
     Field e₁ a
   where
     e₁ = alphaNormalize e₀
+alphaNormalize (Project e₀ a) =
+    Project e₁ a
+  where
+    e₁ = alphaNormalize e₀
 alphaNormalize (Note s e₀) =
     Note s e₁
   where
@@ -1194,10 +1228,12 @@
 denote (Union a             ) = Union (fmap denote a)
 denote (UnionLit a b c      ) = UnionLit a (denote b) (fmap denote c)
 denote (Combine a b         ) = Combine (denote a) (denote b)
+denote (CombineTypes a b    ) = CombineTypes (denote a) (denote b)
 denote (Prefer a b          ) = Prefer (denote a) (denote b)
 denote (Merge a b c         ) = Merge (denote a) (denote b) (fmap denote c)
 denote (Constructors a      ) = Constructors (denote a)
 denote (Field a b           ) = Field (denote a) b
+denote (Project a b         ) = Project (denote a) b
 denote (Embed a             ) = Embed a
 
 {-| Reduce an expression to its normal form, performing beta reduction and applying
@@ -1493,6 +1529,17 @@
             RecordLit (Data.HashMap.Strict.InsOrd.unionWith decide m n)
         decide l r =
             Combine l r
+    CombineTypes x y -> decide (loop x) (loop y)
+      where
+        decide (Record m) r | Data.HashMap.Strict.InsOrd.null m =
+            r
+        decide l (Record n) | Data.HashMap.Strict.InsOrd.null n =
+            l
+        decide (Record m) (Record n) =
+            Record (Data.HashMap.Strict.InsOrd.unionWith decide m n)
+        decide l r =
+            CombineTypes l r
+
     Prefer x y -> decide (loop x) (loop y)
       where
         decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m =
@@ -1536,6 +1583,21 @@
                     Just v  -> loop v
                     Nothing -> Field (RecordLit (fmap loop kvs)) x
             r' -> Field r' x
+    Project r xs     ->
+        case loop r of
+            RecordLit kvs ->
+                case traverse adapt (Data.Set.toList xs) of
+                    Just s  ->
+                        loop (RecordLit kvs')
+                      where
+                        kvs' = Data.HashMap.Strict.InsOrd.fromList s
+                    Nothing ->
+                        Project (RecordLit (fmap loop kvs)) xs
+              where
+                adapt x = do
+                    v <- Data.HashMap.Strict.InsOrd.lookup x kvs
+                    return (x, v)
+            r' -> Project r' xs
     Note _ e' -> loop e'
     Embed a -> Embed a
 
@@ -1704,6 +1766,13 @@
                 RecordLit _ -> False
                 _ -> True
             _ -> True
+    CombineTypes x y -> isNormalized x && isNormalized y && combine
+      where
+        combine = case x of
+            Record _ -> case y of
+                Record _ -> False
+                _ -> True
+            _ -> True
     Prefer x y -> isNormalized x && isNormalized y && combine
       where
         combine = case x of
@@ -1725,12 +1794,20 @@
         case t of
             Union _ -> False
             _       -> True
+
     Field r x -> isNormalized r &&
         case r of
             RecordLit kvs ->
                 case Data.HashMap.Strict.InsOrd.lookup x kvs of
                     Just _  -> False
                     Nothing -> True
+            _ -> True
+    Project r xs -> isNormalized r &&
+        case r of
+            RecordLit kvs ->
+                if all (flip Data.HashMap.Strict.InsOrd.member kvs) xs
+                    then False
+                    else True
             _ -> True
     Note _ e' -> isNormalized e'
     Embed _ -> True
diff --git a/src/Dhall/Diff.hs b/src/Dhall/Diff.hs
new file mode 100644
--- /dev/null
+++ b/src/Dhall/Diff.hs
@@ -0,0 +1,1120 @@
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
+
+{-| This module provides functionality for concisely displaying the difference
+    between two expressions
+
+    For example, this is used in type errors to explain why the actual type does
+    not match the expected type
+-}
+
+module Dhall.Diff (
+    -- * Diff
+      diffNormalized
+    , Dhall.Diff.diff
+    ) where
+
+import Data.Foldable (fold)
+import Data.HashMap.Strict.InsOrd (InsOrdHashMap)
+import Data.Monoid (Any(..))
+import Data.Scientific (Scientific)
+import Data.Semigroup
+import Data.Set (Set)
+import Data.String (IsString(..))
+import Data.Text.Lazy (Text)
+import Data.Text.Prettyprint.Doc (Doc, Pretty)
+import Data.List.NonEmpty (NonEmpty(..))
+import Dhall.Core (Const(..), Expr(..), Var(..))
+import Dhall.Pretty.Internal (Ann)
+import Numeric.Natural (Natural)
+
+import qualified Data.HashMap.Strict.InsOrd as HashMap
+import qualified Data.List.NonEmpty
+import qualified Data.Set
+import qualified Data.Text.Prettyprint.Doc  as Pretty
+import qualified Dhall.Core
+import qualified Dhall.Pretty.Internal      as Internal
+
+data Diff =
+    Diff
+        { same :: Bool
+        , doc  :: Doc Ann
+        }
+
+instance Data.Semigroup.Semigroup Diff where
+    Diff sameL docL <> Diff sameR docR = Diff (sameL && sameR) (docL <> docR)
+
+instance Monoid (Diff) where
+    mempty = Diff {..}
+      where
+        same = True
+
+        doc = mempty
+
+#if !(MIN_VERSION_base(4,11,0))
+    mappend = (<>)
+#endif
+
+instance IsString (Diff) where
+    fromString string = Diff {..}
+      where
+        same = True
+
+        doc = fromString string
+
+ignore :: Diff
+ignore = "…"
+
+align :: Diff -> Diff
+align (Diff {doc = docOld, ..}) = Diff {doc = Pretty.align docOld, .. }
+
+hardline :: Diff
+hardline = token Pretty.hardline
+
+minus :: Diff -> Diff
+minus l = ("- " <> l) { same = False }
+
+plus :: Diff -> Diff
+plus r = ("+ " <> r) { same = False }
+
+difference :: Diff -> Diff -> Diff
+difference l r = align (minus l <> hardline <> plus r)
+
+token :: Doc Ann -> Diff
+token doc = Diff {..}
+  where
+    same = True
+
+format :: Diff -> Diff -> Diff
+format suffix doc = doc <> (if same doc then suffix else hardline)
+
+builtin :: Doc Ann -> Diff
+builtin doc = token (Internal.builtin doc)
+
+keyword :: Doc Ann -> Diff
+keyword doc = token (Internal.keyword doc)
+
+operator :: Doc Ann -> Diff
+operator doc = token (Internal.operator doc)
+
+colon :: Diff
+colon = token Internal.colon
+
+comma :: Diff
+comma = token Internal.comma
+
+dot :: Diff
+dot = token Internal.dot
+
+equals :: Diff
+equals = token Internal.equals
+
+forall :: Diff
+forall = token Internal.forall
+
+lambda :: Diff
+lambda = token Internal.lambda
+
+langle :: Diff
+langle = token Internal.langle
+
+lbrace :: Diff
+lbrace = token Internal.lbrace
+
+lbracket :: Diff
+lbracket = token Internal.lbracket
+
+lparen :: Diff
+lparen = token Internal.lparen
+
+pipe :: Diff
+pipe = token Internal.pipe
+
+rangle :: Diff
+rangle = token Internal.rangle
+
+rarrow :: Diff
+rarrow = token Internal.rarrow
+
+rbrace :: Diff
+rbrace = token Internal.rbrace
+
+rbracket :: Diff
+rbracket = token Internal.rbracket
+
+rparen :: Diff
+rparen = token Internal.rparen
+
+-- | Render the difference between the normal form of two expressions
+diffNormalized :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann
+diffNormalized l0 r0 = Dhall.Diff.diff l1 r1
+  where
+    l1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize l0)
+    r1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize r0)
+
+-- | Render the difference between two expressions
+diff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann
+diff l0 r0 = doc
+  where
+    Diff {..} = diffExprA l0 r0
+
+diffPrimitive :: Eq a => (a -> Diff) -> a -> a -> Diff
+diffPrimitive f l r
+    | l == r    = ignore
+    | otherwise = difference (f l) (f r)
+
+diffLabel :: Text -> Text -> Diff
+diffLabel = diffPrimitive (token . Internal.prettyLabel)
+
+diffLabels :: Set Text -> Set Text -> Diff
+diffLabels ksL ksR =
+    braced (diffFieldNames <> (if anyEqual then [ ignore ] else []))
+  where
+    extraL = Data.Set.difference ksL ksR
+    extraR = Data.Set.difference ksR ksL
+
+    diffFieldNames = foldMap (adapt minus) extraL <> foldMap (adapt plus) extraR
+      where
+        adapt sign key = [ sign (token (Internal.prettyLabel key)) ]
+
+    anyEqual = not (Data.Set.null (Data.Set.intersection ksL ksR))
+
+diffNatural :: Natural -> Natural -> Diff
+diffNatural = diffPrimitive (token . Internal.prettyNatural)
+
+diffScientific :: Scientific -> Scientific -> Diff
+diffScientific = diffPrimitive (token . Internal.prettyScientific)
+
+diffConst :: Const -> Const -> Diff
+diffConst = diffPrimitive (token . Internal.prettyConst)
+
+diffBool :: Bool -> Bool -> Diff
+diffBool = diffPrimitive bool
+  where
+    bool True  = builtin "True"
+    bool False = builtin "False"
+
+diffInteger :: Integer -> Integer -> Diff
+diffInteger = diffPrimitive (token . Internal.prettyNumber)
+
+diffVar :: Var -> Var -> Diff
+diffVar (V xL nL) (V xR nR) = format mempty label <> "@" <> natural
+  where
+    label = diffLabel xL xR
+
+    natural = diffInteger nL nR
+
+diffMaybe :: Diff -> (a -> a -> Diff) -> (Maybe a -> Maybe a -> Diff)
+diffMaybe _ _ Nothing Nothing =
+    mempty
+diffMaybe prefix _ Nothing (Just _) =
+    difference mempty (prefix <> ignore)
+diffMaybe prefix _ (Just _) Nothing =
+    difference (prefix <> ignore) mempty
+diffMaybe prefix f (Just l) (Just r) =
+    prefix <> f l r
+
+enclosed
+    :: Diff
+    -> Diff
+    -> Diff
+    -> [Diff]
+    -> Diff
+enclosed l _ r []   = l <> r
+enclosed l m r docs = align (fold (zipWith (<>) prefixes docs) <> suffix)
+  where
+    prefixes = l : repeat (hardline <> m)
+
+    suffix = hardline <> r
+
+enclosed'
+    :: Diff
+    -> Diff
+    -> NonEmpty (Diff)
+    -> Diff
+enclosed' l m docs =
+    align (fold (Data.List.NonEmpty.zipWith (<>) prefixes docs))
+  where
+    prefixes = l :| repeat (hardline <> m)
+
+diffKeyVals
+    :: Pretty a
+    => Diff
+    -> InsOrdHashMap Text (Expr s a)
+    -> InsOrdHashMap Text (Expr s a)
+    -> [Diff]
+diffKeyVals assign kvsL kvsR =
+    diffFieldNames <> diffFieldValues <> (if anyEqual then [ ignore ] else [])
+  where
+    ksL = Data.Set.fromList (HashMap.keys kvsL)
+    ksR = Data.Set.fromList (HashMap.keys kvsR)
+
+    extraL = Data.Set.difference ksL ksR
+    extraR = Data.Set.difference ksR ksL
+
+    diffFieldNames = foldMap (adapt minus) extraL <> foldMap (adapt plus) extraR
+      where
+        adapt sign key =
+            [   sign (token (Internal.prettyLabel key))
+            <>  " "
+            <>  assign
+            <>  " "
+            <>  ignore
+            ]
+
+    shared = HashMap.intersectionWith diffExprA kvsL kvsR
+
+    diffFieldValues =
+        filter (not . same) (HashMap.foldMapWithKey adapt shared)
+      where
+        adapt key doc =
+            [   (if ksL == ksR then mempty else "  ")
+            <>  token (Internal.prettyLabel key)
+            <>  " "
+            <>  assign
+            <>  " "
+            <>  doc
+            ]
+
+    anyEqual = getAny (foldMap (Any . same) shared)
+
+braced :: [Diff] -> Diff
+braced = enclosed (lbrace <> " ") (comma <> " ") rbrace
+
+angled :: [Diff] -> Diff
+angled = enclosed (langle <> " ") (pipe <> " ") rangle
+
+diffRecord
+    :: Pretty a
+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff
+diffRecord kvsL kvsR = braced (diffKeyVals colon kvsL kvsR)
+
+diffRecordLit
+    :: Pretty a
+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff
+diffRecordLit kvsL kvsR = braced (diffKeyVals equals kvsL kvsR)
+
+diffUnion
+    :: Pretty a
+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff
+diffUnion kvsL kvsR = angled (diffKeyVals colon kvsL kvsR)
+
+diffUnionLit
+    :: Pretty a
+    => Text
+    -> Text
+    -> Expr s a
+    -> Expr s a
+    -> InsOrdHashMap Text (Expr s a)
+    -> InsOrdHashMap Text (Expr s a)
+    -> Diff
+diffUnionLit kL kR vL vR kvsL kvsR =
+        langle
+    <>  " "
+    <>  format " " (diffLabel kL kR)
+    <>  equals
+    <>  " "
+    <>  format " " (diffExprA vL vR)
+    <>  halfAngled (diffKeyVals equals kvsL kvsR)
+  where
+    halfAngled = enclosed (pipe <> " ") (pipe <> " ") rangle
+
+skeleton :: Pretty a => Expr s a -> Diff
+skeleton (Lam {}) =
+        lambda
+    <>  lparen
+    <>  ignore
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  ignore
+    <>  rparen
+    <>  " "
+    <>  rarrow
+    <>  " "
+    <>  ignore
+skeleton (Pi {}) =
+        forall
+    <>  lparen
+    <>  ignore
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  ignore
+    <>  rparen
+    <>  " "
+    <>  rarrow
+    <>  " "
+    <>  ignore
+skeleton (App {}) =
+        ignore
+    <>  " "
+    <>  ignore
+skeleton (Let {}) =
+        keyword "let"
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  equals
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  keyword "in"
+    <>  " "
+    <>  ignore
+skeleton (Annot {}) =
+        ignore
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  ignore
+skeleton (BoolAnd {}) =
+        ignore
+    <>  " "
+    <>  operator "&&"
+    <>  " "
+    <>  ignore
+skeleton (BoolOr {}) =
+        ignore
+    <>  " "
+    <>  operator "||"
+    <>  " "
+    <>  ignore
+skeleton (BoolEQ {}) =
+        ignore
+    <>  " "
+    <>  operator "=="
+    <>  " "
+    <>  ignore
+skeleton (BoolNE {}) =
+        ignore
+    <>  " "
+    <>  operator "!="
+    <>  " "
+    <>  ignore
+skeleton (BoolIf {}) =
+        keyword "if"
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  keyword "then"
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  keyword "else"
+    <>  " "
+    <>  ignore
+skeleton (NaturalPlus {}) =
+        ignore
+    <>  " "
+    <>  operator "+"
+    <>  " "
+    <>  ignore
+skeleton (NaturalTimes {}) =
+        ignore
+    <>  " "
+    <>  operator "*"
+    <>  " "
+    <>  ignore
+skeleton (TextLit {}) =
+        "\""
+    <>  ignore
+    <>  "\""
+skeleton (TextAppend {}) =
+        ignore
+    <>  " "
+    <>  operator "++"
+    <>  " "
+    <>  ignore
+skeleton (ListLit {}) =
+        lbracket
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rbracket
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  builtin "List"
+    <>  " "
+    <>  ignore
+skeleton (ListAppend {}) =
+        ignore
+    <>  " "
+    <>  operator "#"
+    <>  " "
+    <>  ignore
+skeleton (OptionalLit {}) =
+        lbracket
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rbracket
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  builtin "Optional"
+    <>  " "
+    <>  ignore
+skeleton (Record {}) =
+        lbrace
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rbrace
+skeleton (RecordLit {}) =
+        lbrace
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  equals
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rbrace
+skeleton (Union {}) =
+        langle
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  colon
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rangle
+skeleton (UnionLit {}) =
+        langle
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  equals
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rangle
+skeleton (Combine {}) =
+        ignore
+    <>  " "
+    <>  operator "∧"
+    <>  " "
+    <>  ignore
+skeleton (CombineTypes {}) =
+        ignore
+    <>  " "
+    <>  operator "⩓"
+    <>  " "
+    <>  ignore
+skeleton (Prefer {}) =
+        ignore
+    <>  " "
+    <>  operator "⫽"
+    <>  " "
+    <>  ignore
+skeleton (Merge {}) =
+        keyword "merge"
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  ignore
+skeleton (Constructors {}) =
+        keyword "constructors"
+    <>  " "
+    <>  ignore
+skeleton (Field {}) =
+        ignore
+    <>  dot
+    <>  ignore
+skeleton (Project {}) =
+        ignore
+    <>  dot
+    <>  lbrace
+    <>  " "
+    <>  ignore
+    <>  " "
+    <>  rbrace
+skeleton x = token (Pretty.pretty x)
+
+mismatch :: Pretty a => Expr s a -> Expr s a -> Diff
+mismatch l r = difference (skeleton l) (skeleton r)
+
+diffExprA :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprA l@(Annot {}) r@(Annot {}) =
+    enclosed' "  " (colon <> " ") (docs l r)
+  where
+    docs (Annot aL bL) (Annot aR bR) =
+        Data.List.NonEmpty.cons (align doc) (docs bL bR)
+      where
+        doc = diffExprB aL aR
+    docs aL aR =
+        diffExprB aL aR :| []
+diffExprA l@(Annot {}) r =
+    mismatch l r
+diffExprA l r@(Annot {}) =
+    mismatch l r
+diffExprA l r =
+    diffExprB l r
+
+diffExprB :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprB l@(Lam {}) r@(Lam {}) =
+    enclosed' "  " (rarrow <> " ") (docs l r)
+  where
+    docs (Lam aL bL cL) (Lam aR bR cR) =
+        Data.List.NonEmpty.cons (align doc) (docs cL cR)
+      where
+        doc =   lambda
+            <>  lparen
+            <>  format " " (diffLabel aL aR)
+            <>  colon
+            <>  " "
+            <>  format mempty (diffExprA bL bR)
+            <>  rparen
+
+    docs aL aR =
+        pure (diffExprC aL aR)
+diffExprB l@(Lam {}) r =
+    mismatch l r
+diffExprB l r@(Lam {}) =
+    mismatch l r
+diffExprB l@(BoolIf {}) r@(BoolIf {}) =
+    enclosed' "      " (keyword "else" <> "  ") (docs l r)
+  where
+    docs (BoolIf aL bL cL) (BoolIf aR bR cR) =
+        Data.List.NonEmpty.cons (align doc) (docs cL cR)
+      where
+        doc =   keyword "if"
+            <>  " "
+            <>  format " " (diffExprA aL aR)
+            <>  keyword "then"
+            <>  " "
+            <>  diffExprA bL bR
+    docs aL aR =
+        pure (diffExprB aL aR)
+diffExprB l@(BoolIf {}) r =
+    mismatch l r
+diffExprB l r@(BoolIf {}) =
+    mismatch l r
+diffExprB l@(Pi {}) r@(Pi {}) =
+    enclosed' "  " (rarrow <> " ") (docs l r)
+  where
+    docs (Pi aL bL cL) (Pi aR bR cR) =
+        Data.List.NonEmpty.cons (align doc) (docs cL cR)
+      where
+        doc =   forall
+            <>  lparen
+            <>  format " " (diffLabel aL aR)
+            <>  colon
+            <>  " "
+            <>  format mempty (diffExprA bL bR)
+            <>  rparen
+    docs aL aR = pure (diffExprB aL aR)
+diffExprB l@(Pi {}) r =
+    mismatch l r
+diffExprB l r@(Pi {}) =
+    mismatch l r
+diffExprB l@(Let {}) r@(Let {}) =
+    enclosed' "    " (keyword "in" <> "  ") (docs l r)
+  where
+    docs (Let aL bL cL dL) (Let aR bR cR dR) =
+        Data.List.NonEmpty.cons (align doc) (docs dL dR)
+      where
+        doc =   keyword "let"
+            <>  " "
+            <>  format " " (diffLabel aL aR)
+            <>  format " " (diffMaybe (colon <> " ") diffExprA bL bR)
+            <>  equals
+            <>  " "
+            <>  diffExprA cL cR
+    docs aL aR = pure (diffExprB aL aR)
+diffExprB l@(Let {}) r =
+    mismatch l r
+diffExprB l r@(Let {}) =
+    mismatch l r
+-- TODO: Implement proper list diff
+diffExprB l@(ListLit {}) r@(ListLit {}) =
+    mismatch l r
+diffExprB l@(ListLit {}) r =
+    mismatch l r
+diffExprB l r@(ListLit {}) =
+    mismatch l r
+diffExprB (OptionalLit aL bL) (OptionalLit aR bR) = align doc
+  where
+    doc =   lbracket
+        <>  " "
+        <>  format " " (diffMaybe mempty diffExprA bL bR)
+        <>  rbracket
+        <>  " "
+        <>  colon
+        <>  " "
+        <>  diffExprD (App Optional aL) (App Optional aR)
+diffExprB l@(OptionalLit {}) r =
+    mismatch l r
+diffExprB l r@(OptionalLit {}) =
+    mismatch l r
+diffExprB (Merge aL bL cL) (Merge aR bR cR) = align doc
+  where
+    doc =   keyword "merge"
+        <>  " "
+        <>  format " " (diffExprE aL aR)
+        <>  format " " (diffExprE bL bR)
+        <>  diffMaybe (colon <> " ") diffExprE cL cR
+diffExprB l@(Merge {}) r =
+    mismatch l r
+diffExprB l r@(Merge {}) =
+    mismatch l r
+diffExprB l r =
+    diffExprC l r
+
+diffExprC :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprC = diffBoolOr
+
+diffBoolOr :: Pretty a => Expr s a -> Expr s a -> Diff
+diffBoolOr l@(BoolOr {}) r@(BoolOr {}) =
+    enclosed' "    " (operator "||" <> "  ") (docs l r)
+  where
+    docs (BoolOr aL bL) (BoolOr aR bR) =
+        Data.List.NonEmpty.cons (diffTextAppend aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffTextAppend aL aR)
+diffBoolOr l@(BoolOr {}) r =
+    mismatch l r
+diffBoolOr l r@(BoolOr {}) =
+    mismatch l r
+diffBoolOr l r =
+    diffTextAppend l r
+
+diffTextAppend :: Pretty a => Expr s a -> Expr s a -> Diff
+diffTextAppend l@(TextAppend {}) r@(TextAppend {}) =
+    enclosed' "    " (operator "++" <> "  ") (docs l r)
+  where
+    docs (TextAppend aL bL) (TextAppend aR bR) =
+        Data.List.NonEmpty.cons (diffNaturalPlus aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffNaturalPlus aL aR)
+diffTextAppend l@(TextAppend {}) r =
+    mismatch l r
+diffTextAppend l r@(TextAppend {}) =
+    mismatch l r
+diffTextAppend l r =
+    diffNaturalPlus l r
+
+diffNaturalPlus :: Pretty a => Expr s a -> Expr s a -> Diff
+diffNaturalPlus l@(NaturalPlus {}) r@(NaturalPlus {}) =
+    enclosed' "  " (operator "+" <> " ") (docs l r)
+  where
+    docs (NaturalPlus aL bL) (NaturalPlus aR bR) =
+        Data.List.NonEmpty.cons (diffListAppend aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffListAppend aL aR)
+diffNaturalPlus l@(NaturalPlus {}) r =
+    mismatch l r
+diffNaturalPlus l r@(NaturalPlus {}) =
+    mismatch l r
+diffNaturalPlus l r =
+    diffListAppend l r
+
+diffListAppend :: Pretty a => Expr s a -> Expr s a -> Diff
+diffListAppend l@(ListAppend {}) r@(ListAppend {}) =
+    enclosed' "  " (operator "#" <> " ") (docs l r)
+  where
+    docs (ListAppend aL bL) (ListAppend aR bR) =
+        Data.List.NonEmpty.cons (diffBoolAnd aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffBoolAnd aL aR)
+diffListAppend l@(ListAppend {}) r =
+    mismatch l r
+diffListAppend l r@(ListAppend {}) =
+    mismatch l r
+diffListAppend l r =
+    diffBoolAnd l r
+
+diffBoolAnd :: Pretty a => Expr s a -> Expr s a -> Diff
+diffBoolAnd l@(BoolAnd {}) r@(BoolAnd {}) =
+    enclosed' "    " (operator "&&" <> "  ") (docs l r)
+  where
+    docs (BoolAnd aL bL) (BoolAnd aR bR) =
+        Data.List.NonEmpty.cons (diffCombine aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffCombine aL aR)
+diffBoolAnd l@(BoolAnd {}) r =
+    mismatch l r
+diffBoolAnd l r@(BoolAnd {}) =
+    mismatch l r
+diffBoolAnd l r =
+    diffCombine l r
+
+diffCombine :: Pretty a => Expr s a -> Expr s a -> Diff
+diffCombine l@(Combine {}) r@(Combine {}) =
+    enclosed' "  " (operator "∧" <> " ") (docs l r)
+  where
+    docs (Combine aL bL) (Combine aR bR) =
+        Data.List.NonEmpty.cons (diffPrefer aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffPrefer aL aR)
+diffCombine l@(Combine {}) r =
+    mismatch l r
+diffCombine l r@(Combine {}) =
+    mismatch l r
+diffCombine l r =
+    diffPrefer l r
+
+diffPrefer :: Pretty a => Expr s a -> Expr s a -> Diff
+diffPrefer l@(Prefer {}) r@(Prefer {}) =
+    enclosed' "  " (operator "⫽" <> " ") (docs l r)
+  where
+    docs (Prefer aL bL) (Prefer aR bR) =
+        Data.List.NonEmpty.cons (diffCombineTypes aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffCombineTypes aL aR)
+diffPrefer l@(Prefer {}) r =
+    mismatch l r
+diffPrefer l r@(Prefer {}) =
+    mismatch l r
+diffPrefer l r =
+    diffCombineTypes l r
+
+diffCombineTypes :: Pretty a => Expr s a -> Expr s a -> Diff
+diffCombineTypes l@(CombineTypes {}) r@(CombineTypes {}) =
+    enclosed' "  " (operator "*" <> " ") (docs l r)
+  where
+    docs (CombineTypes aL bL) (CombineTypes aR bR) =
+        Data.List.NonEmpty.cons (diffNaturalTimes aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffNaturalTimes aL aR)
+diffCombineTypes l@(CombineTypes {}) r =
+    mismatch l r
+diffCombineTypes l r@(CombineTypes {}) =
+    mismatch l r
+diffCombineTypes l r =
+    diffNaturalTimes l r
+
+diffNaturalTimes :: Pretty a => Expr s a -> Expr s a -> Diff
+diffNaturalTimes l@(NaturalTimes {}) r@(NaturalTimes {}) =
+    enclosed' "  " (operator "*" <> " ") (docs l r)
+  where
+    docs (NaturalTimes aL bL) (NaturalTimes aR bR) =
+        Data.List.NonEmpty.cons (diffBoolEQ aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffBoolEQ aL aR)
+diffNaturalTimes l@(NaturalTimes {}) r =
+    mismatch l r
+diffNaturalTimes l r@(NaturalTimes {}) =
+    mismatch l r
+diffNaturalTimes l r =
+    diffBoolEQ l r
+
+diffBoolEQ :: Pretty a => Expr s a -> Expr s a -> Diff
+diffBoolEQ l@(BoolEQ {}) r@(BoolEQ {}) =
+    enclosed' "    " (operator "==" <> "  ") (docs l r)
+  where
+    docs (BoolEQ aL bL) (BoolEQ aR bR) =
+        Data.List.NonEmpty.cons (diffBoolNE aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffBoolNE aL aR)
+diffBoolEQ l@(BoolEQ {}) r =
+    mismatch l r
+diffBoolEQ l r@(BoolEQ {}) =
+    mismatch l r
+diffBoolEQ l r =
+    diffBoolNE l r
+
+diffBoolNE :: Pretty a => Expr s a -> Expr s a -> Diff
+diffBoolNE l@(BoolNE {}) r@(BoolNE {}) =
+    enclosed' "    " (operator "!=" <> "  ") (docs l r)
+  where
+    docs (BoolNE aL bL) (BoolNE aR bR) =
+        Data.List.NonEmpty.cons (diffExprD aL aR) (docs bL bR)
+    docs aL aR =
+        pure (diffExprD aL aR)
+diffBoolNE l@(BoolNE {}) r =
+    mismatch l r
+diffBoolNE l r@(BoolNE {}) =
+    mismatch l r
+diffBoolNE l r =
+    diffExprD l r
+
+diffExprD :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprD l@(App {}) r@(App {}) =
+    enclosed' mempty mempty (Data.List.NonEmpty.reverse (docs l r))
+  where
+    docs (App aL bL) (App aR bR) =
+        Data.List.NonEmpty.cons (diffExprE bL bR) (docs aL aR)
+    docs (Constructors aL) (Constructors aR) =
+        diffExprE aL aR :| [ keyword "constructors" ]
+    docs aL@(App {}) aR@(Constructors {}) =
+        pure (mismatch aL aR)
+    docs aL@(Constructors {}) aR@(App {}) =
+        pure (mismatch aL aR)
+    docs aL aR =
+        pure (diffExprE aL aR)
+diffExprD l@(App {}) r =
+    mismatch l r
+diffExprD l r@(App {}) =
+    mismatch l r
+diffExprD l@(Constructors {}) r@(Constructors {}) =
+    enclosed' mempty mempty (keyword "constructors" :| [ diffExprE l r ])
+diffExprD l@(Constructors {}) r =
+    mismatch l r
+diffExprD l r@(Constructors {}) =
+    mismatch l r
+diffExprD l r =
+    diffExprE l r
+
+diffExprE :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprE l@(Field {}) r@(Field {}) =
+    enclosed' "  " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r))
+  where
+    docs (Field aL bL) (Field aR bR) =
+        Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR)
+    docs (Project aL bL) (Project aR bR) =
+        Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)
+    docs aL aR =
+        pure (diffExprF aL aR)
+diffExprE l@(Field {}) r =
+    mismatch l r
+diffExprE l r@(Field {}) =
+    mismatch l r
+diffExprE l@(Project {}) r@(Project {}) =
+    enclosed' "  " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r))
+  where
+    docs (Field aL bL) (Field aR bR) =
+        Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR)
+    docs (Project aL bL) (Project aR bR) =
+        Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)
+    docs aL aR =
+        pure (diffExprF aL aR)
+diffExprE l@(Project {}) r =
+    mismatch l r
+diffExprE l r@(Project {}) =
+    mismatch l r
+diffExprE l r =
+    diffExprF l r
+
+diffExprF :: Pretty a => Expr s a -> Expr s a -> Diff
+diffExprF (Var aL) (Var aR) =
+    diffVar aL aR
+diffExprF l@(Var {}) r =
+    mismatch l r
+diffExprF l r@(Var {}) =
+    mismatch l r
+diffExprF (Const aL) (Const aR) =
+    diffConst aL aR
+diffExprF l@(Const {}) r =
+    mismatch l r
+diffExprF l r@(Const {}) =
+    mismatch l r
+diffExprF Bool Bool =
+    "…"
+diffExprF l@Bool r =
+    mismatch l r
+diffExprF l r@Bool =
+    mismatch l r
+diffExprF Natural Natural =
+    "…"
+diffExprF l@Natural r =
+    mismatch l r
+diffExprF l r@Natural =
+    mismatch l r
+diffExprF NaturalFold NaturalFold =
+    "…"
+diffExprF l@NaturalFold r =
+    mismatch l r
+diffExprF l r@NaturalFold =
+    mismatch l r
+diffExprF NaturalBuild NaturalBuild =
+    "…"
+diffExprF l@NaturalBuild r =
+    mismatch l r
+diffExprF l r@NaturalBuild =
+    mismatch l r
+diffExprF NaturalIsZero NaturalIsZero =
+    "…"
+diffExprF l@NaturalIsZero r =
+    mismatch l r
+diffExprF l r@NaturalIsZero =
+    mismatch l r
+diffExprF NaturalEven NaturalEven =
+    "…"
+diffExprF l@NaturalEven r =
+    mismatch l r
+diffExprF l r@NaturalEven =
+    mismatch l r
+diffExprF NaturalOdd NaturalOdd =
+    "…"
+diffExprF l@NaturalOdd r =
+    mismatch l r
+diffExprF l r@NaturalOdd =
+    mismatch l r
+diffExprF NaturalToInteger NaturalToInteger =
+    "…"
+diffExprF l@NaturalToInteger r =
+    mismatch l r
+diffExprF l r@NaturalToInteger =
+    mismatch l r
+diffExprF NaturalShow NaturalShow =
+    "…"
+diffExprF l@NaturalShow r =
+    mismatch l r
+diffExprF l r@NaturalShow =
+    mismatch l r
+diffExprF Integer Integer =
+    "…"
+diffExprF l@Integer r =
+    mismatch l r
+diffExprF l r@Integer =
+    mismatch l r
+diffExprF IntegerShow IntegerShow =
+    "…"
+diffExprF l@IntegerShow r =
+    mismatch l r
+diffExprF l r@IntegerShow =
+    mismatch l r
+diffExprF Double Double =
+    "…"
+diffExprF l@Double r =
+    mismatch l r
+diffExprF l r@Double =
+    mismatch l r
+diffExprF DoubleShow DoubleShow =
+    "…"
+diffExprF l@DoubleShow r =
+    mismatch l r
+diffExprF l r@DoubleShow =
+    mismatch l r
+diffExprF Text Text =
+    "…"
+diffExprF l@Text r =
+    mismatch l r
+diffExprF l r@Text =
+    mismatch l r
+diffExprF List List =
+    "…"
+diffExprF l@List r =
+    mismatch l r
+diffExprF l r@List =
+    mismatch l r
+diffExprF ListBuild ListBuild =
+    "…"
+diffExprF l@ListBuild r =
+    mismatch l r
+diffExprF l r@ListBuild =
+    mismatch l r
+diffExprF ListFold ListFold =
+    "…"
+diffExprF l@ListFold r =
+    mismatch l r
+diffExprF l r@ListFold =
+    mismatch l r
+diffExprF ListLength ListLength =
+    "…"
+diffExprF l@ListLength r =
+    mismatch l r
+diffExprF l r@ListLength =
+    mismatch l r
+diffExprF ListHead ListHead =
+    "…"
+diffExprF l@ListHead r =
+    mismatch l r
+diffExprF l r@ListHead =
+    mismatch l r
+diffExprF ListLast ListLast =
+    "…"
+diffExprF l@ListLast r =
+    mismatch l r
+diffExprF l r@ListLast =
+    mismatch l r
+diffExprF ListIndexed ListIndexed =
+    "…"
+diffExprF l@ListIndexed r =
+    mismatch l r
+diffExprF l r@ListIndexed =
+    mismatch l r
+diffExprF ListReverse ListReverse =
+    "…"
+diffExprF l@ListReverse r =
+    mismatch l r
+diffExprF l r@ListReverse =
+    mismatch l r
+diffExprF Optional Optional =
+    "…"
+diffExprF l@Optional r =
+    mismatch l r
+diffExprF l r@Optional =
+    mismatch l r
+diffExprF OptionalFold OptionalFold =
+    "…"
+diffExprF l@OptionalFold r =
+    mismatch l r
+diffExprF l r@OptionalFold =
+    mismatch l r
+diffExprF OptionalBuild OptionalBuild =
+    "…"
+diffExprF l@OptionalBuild r =
+    mismatch l r
+diffExprF l r@OptionalBuild =
+    mismatch l r
+diffExprF (BoolLit aL) (BoolLit aR) =
+    diffBool aL aR
+diffExprF l@(BoolLit {}) r =
+    mismatch l r
+diffExprF l r@(BoolLit {}) =
+    mismatch l r
+diffExprF (IntegerLit aL) (IntegerLit aR) =
+    diffInteger aL aR
+diffExprF l@(IntegerLit {}) r =
+    mismatch l r
+diffExprF l r@(IntegerLit {}) =
+    mismatch l r
+diffExprF (NaturalLit aL) (NaturalLit aR) =
+    token (Internal.literal "+") <> diffNatural aL aR
+diffExprF l@(NaturalLit {}) r =
+    mismatch l r
+diffExprF l r@(NaturalLit {}) =
+    mismatch l r
+diffExprF (DoubleLit aL) (DoubleLit aR) =
+    diffScientific aL aR
+diffExprF l@(DoubleLit {}) r =
+    mismatch l r
+diffExprF l r@(DoubleLit {}) =
+    mismatch l r
+-- TODO: Implement proper textual diff
+diffExprF l@(TextLit {}) r@(TextLit {}) =
+    mismatch l r
+diffExprF l@(TextLit {}) r =
+    mismatch l r
+diffExprF l r@(TextLit {}) =
+    mismatch l r
+diffExprF (Record aL) (Record aR) =
+    diffRecord aL aR
+diffExprF l@(Record {}) r =
+    mismatch l r
+diffExprF l r@(Record {}) =
+    mismatch l r
+diffExprF (RecordLit aL) (RecordLit aR) =
+    diffRecordLit aL aR
+diffExprF l@(RecordLit {}) r =
+    mismatch l r
+diffExprF l r@(RecordLit {}) =
+    mismatch l r
+diffExprF (Union aL) (Union aR) =
+    diffUnion aL aR
+diffExprF l@(Union {}) r =
+    mismatch l r
+diffExprF l r@(Union {}) =
+    mismatch l r
+diffExprF (UnionLit aL bL cL) (UnionLit aR bR cR) =
+    diffUnionLit aL aR bL bR cL cR
+diffExprF l@(UnionLit {}) r =
+    mismatch l r
+diffExprF l r@(UnionLit {}) =
+    mismatch l r
+diffExprF aL aR =
+    if same doc
+    then ignore
+    else align ("( " <> doc <> hardline <> ")")
+  where
+    doc = diffExprA aL aR
diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs
--- a/src/Dhall/Import.hs
+++ b/src/Dhall/Import.hs
@@ -157,15 +157,10 @@
 #else
 import Network.HTTP.Client (HttpException(..), Manager)
 #endif
-import Text.Trifecta (Result(..))
-import Text.Trifecta.Delta (Delta(..))
 
 import qualified Control.Monad.Trans.State.Strict as State
 import qualified Crypto.Hash
-import qualified Data.ByteArray
 import qualified Data.ByteString
-import qualified Data.ByteString.Char8
-import qualified Data.ByteString.Lazy
 import qualified Data.CaseInsensitive
 import qualified Data.Foldable
 import qualified Data.List                        as List
@@ -186,9 +181,9 @@
 import qualified System.Environment
 import qualified System.Directory
 import qualified System.FilePath                  as FilePath
+import qualified Text.Megaparsec
 import qualified Text.Parser.Combinators
 import qualified Text.Parser.Token
-import qualified Text.Trifecta
 
 builderToString :: Builder -> String
 builderToString = Text.unpack . Builder.toLazyText
@@ -554,23 +549,6 @@
         <>  "\n"
         <>  "↳ " <> show actualHash <> "\n"
 
-parseFromFileEx
-    :: Text.Trifecta.Parser a
-    -> FilePath
-    -> IO (Text.Trifecta.Result a)
-parseFromFileEx parser path = do
-    text <- Data.Text.Lazy.IO.readFile path
-
-    let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 text
-
-    let strictBytes = Data.ByteString.Lazy.toStrict lazyBytes
-
-    let delta = Directed bytesPath 0 0 0 0
-
-    return (Text.Trifecta.parseByteString parser delta strictBytes)
-  where
-    bytesPath = Data.ByteString.Char8.pack path
-
 -- | Parse an expression from a `Path` containing a Dhall program
 exprFromPath :: Path -> StateT Status IO (Expr Src Path)
 exprFromPath (Path {..}) = case pathType of
@@ -592,18 +570,18 @@
                 -- 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`
-                let handler :: IOException -> IO (Result (Expr Src Path))
+                let handler :: IOException -> IO Text
                     handler e = do
                         -- If the fallback fails, reuse the original exception
                         -- to avoid user confusion
-                        parseFromFileEx parser (path </> "@")
+                        Data.Text.Lazy.IO.readFile (path </> "@")
                             `onException` throwIO e
 
-                x <- parseFromFileEx parser path `catch` handler
-                case x of
-                    Failure errInfo -> do
-                        throwIO (ParseError (Text.Trifecta._errDoc errInfo))
-                    Success expr -> do
+                text <- Data.Text.Lazy.IO.readFile path `catch` handler
+                case Text.Megaparsec.parse parser path text of
+                    Left errInfo -> do
+                        throwIO (ParseError errInfo text)
+                    Right expr -> do
                         return expr
             RawText -> do
                 text <- Data.Text.IO.readFile path
@@ -637,9 +615,7 @@
                                 )
                             )
                 let suffix =
-                        ( Data.ByteString.Lazy.toStrict
-                        . Data.Text.Lazy.Encoding.encodeUtf8
-                        . Builder.toLazyText
+                        ( Builder.toLazyText
                         . build
                         ) expected
                 let annot = case expr of
@@ -671,16 +647,13 @@
             Right text -> return text
 
         case pathMode of
-            Code -> do
-                let urlBytes = Data.Text.Lazy.Encoding.encodeUtf8 url
-                let delta =
-                        Directed (Data.ByteString.Lazy.toStrict urlBytes) 0 0 0 0
-                case Text.Trifecta.parseString parser delta (Text.unpack text) of
-                    Failure err -> do
+            Code ->
+                case Text.Megaparsec.parse parser (Text.unpack url) text of
+                    Left err -> do
                         -- Also try the fallback in case of a parse error, since
                         -- the parse error might signify that this URL points to
                         -- a directory list
-                        let err' = ParseError (Text.Trifecta._errDoc err)
+                        let err' = ParseError err text
 
                         request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url))
 
@@ -695,25 +668,23 @@
                             Left  _     -> liftIO (throwIO err')
                             Right text' -> return text'
 
-                        case Text.Trifecta.parseString parser delta (Text.unpack text') of
-                            Failure _    -> liftIO (throwIO err')
-                            Success expr -> return expr
-                    Success expr -> return expr
+                        case Text.Megaparsec.parse parser (Text.unpack url) text' of
+                            Left _     -> liftIO (throwIO err')
+                            Right expr -> return expr
+                    Right expr -> return expr
             RawText -> do
                 return (TextLit (Chunks [] (build text)))
     Env env -> liftIO (do
         x <- System.Environment.lookupEnv (Text.unpack env)
         case x of
             Just str -> do
+                let text = Text.pack str
                 case pathMode of
-                    Code -> do
-                        let envBytes = Data.Text.Lazy.Encoding.encodeUtf8 env
-                        let delta =
-                                Directed (Data.ByteString.Lazy.toStrict envBytes) 0 0 0 0
-                        case Text.Trifecta.parseString parser delta str of
-                            Failure errInfo -> do
-                                throwIO (ParseError (Text.Trifecta._errDoc errInfo))
-                            Success expr    -> do
+                    Code ->
+                        case Text.Megaparsec.parse parser (Text.unpack env) text of
+                            Left errInfo -> do
+                                throwIO (ParseError errInfo text)
+                            Right expr   -> do
                                 return expr
                     RawText -> return (TextLit (Chunks [] (build str)))
             Nothing  -> throwIO (MissingEnvironmentVariable env) )
@@ -860,14 +831,4 @@
     source code to add an integrity check to an import
 -}
 hashExpressionToCode :: Expr s X -> Text
-hashExpressionToCode expr = "sha256:" <> lazyText
-  where
-    bytes = hashExpression expr
-
-    bytes16 = Data.ByteArray.convert bytes
-
-    -- Notes that `decodeUtf8` is partial, but the base16-encoded bytestring
-    -- should always successfully decode
-    text = Data.Text.Encoding.decodeUtf8 bytes16
-
-    lazyText = Text.fromStrict text
+hashExpressionToCode expr = "sha256:" <> Text.pack (show (hashExpression expr))
diff --git a/src/Dhall/Parser.hs b/src/Dhall/Parser.hs
--- a/src/Dhall/Parser.hs
+++ b/src/Dhall/Parser.hs
@@ -23,76 +23,69 @@
 import Control.Applicative (Alternative(..), liftA2, optional)
 import Control.Exception (Exception)
 import Control.Monad (MonadPlus)
-import Data.ByteString (ByteString)
+import Data.ByteArray.Encoding (Base(..))
 import Data.Functor (void)
 import Data.HashMap.Strict.InsOrd (InsOrdHashMap)
-import Data.Sequence (ViewL(..))
-import Data.Semigroup (Semigroup(..))
 import Data.Scientific (Scientific)
+import Data.Semigroup (Semigroup(..))
+import Data.Sequence (ViewL(..))
+import Data.Set (Set)
 import Data.String (IsString(..))
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy.Builder (Builder)
-import Data.Typeable (Typeable)
+import Data.Void (Void)
 import Dhall.Core
 import Formatting.Buildable (Buildable(..))
 import Numeric.Natural (Natural)
 import Prelude hiding (const, pi)
-import Text.PrettyPrint.ANSI.Leijen (Doc)
 import Text.Parser.Combinators (choice, try, (<?>))
 import Text.Parser.Token (TokenParsing(..))
-import Text.Trifecta
-    (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..))
-import Text.Trifecta.Delta (Delta)
 
 import qualified Control.Monad
 import qualified Crypto.Hash
+import qualified Data.ByteArray.Encoding
+import qualified Data.ByteString
 import qualified Data.ByteString.Lazy
 import qualified Data.Char
 import qualified Data.HashMap.Strict.InsOrd
 import qualified Data.HashSet
 import qualified Data.List
 import qualified Data.Sequence
+import qualified Data.Set
 import qualified Data.Text
-import qualified Data.Text.Encoding
 import qualified Data.Text.Lazy
 import qualified Data.Text.Lazy.Builder
 import qualified Data.Text.Lazy.Encoding
+import qualified Text.Megaparsec
+import qualified Text.Megaparsec.Char
 import qualified Text.Parser.Char
 import qualified Text.Parser.Combinators
 import qualified Text.Parser.Token
 import qualified Text.Parser.Token.Style
-import qualified Text.PrettyPrint.ANSI.Leijen
-import qualified Text.Trifecta
 
 -- | Source code extract
-data Src = Src Delta Delta ByteString deriving (Eq, Show)
+data Src = Src Text.Megaparsec.SourcePos Text.Megaparsec.SourcePos Text
+  deriving (Eq, Show)
 
 instance Buildable Src where
-    build (Src begin _ bytes) =
+    build (Src begin _ text) =
             build text <> "\n"
         <>  "\n"
-        <>  build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin))
+        <>  build (Text.Megaparsec.sourcePosPretty begin)
         <>  "\n"
-      where
-        bytes' = Data.ByteString.Lazy.fromStrict bytes
 
-        text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes')
-
 {-| A `Parser` that is almost identical to
-    @"Text.Trifecta".`Text.Trifecta.Parser`@ except treating Haskell-style
+    @"Text.Megaparsec".`Text.Megaparsec.Parsec`@ except treating Haskell-style
     comments as whitespace
 -}
-newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a }
+newtype Parser a = Parser { unParser :: Text.Megaparsec.Parsec Void Text a }
     deriving
     (   Functor
     ,   Applicative
     ,   Monad
     ,   Alternative
     ,   MonadPlus
-    ,   Parsing
-    ,   CharParsing
-    ,   DeltaParsing
-    ,   MarkParsing Delta
+    ,   Text.Megaparsec.MonadParsec Void Text
     )
 
 instance Data.Semigroup.Semigroup a => Data.Semigroup.Semigroup (Parser a) where
@@ -106,26 +99,52 @@
 #endif
 
 instance IsString a => IsString (Parser a) where
-    fromString x = fmap fromString (Text.Parser.Char.string x)
+    fromString x = fromString x <$ Text.Megaparsec.Char.string (fromString x)
 
+instance Text.Parser.Combinators.Parsing Parser where
+  try = Text.Megaparsec.try
+
+  (<?>) = (Text.Megaparsec.<?>)
+
+  skipMany = Text.Megaparsec.skipMany
+
+  skipSome = Text.Megaparsec.skipSome
+
+  unexpected = fail
+
+  eof = Parser Text.Megaparsec.eof
+
+  notFollowedBy = Text.Megaparsec.notFollowedBy
+
+instance Text.Parser.Char.CharParsing Parser where
+  satisfy = Parser . Text.Megaparsec.Char.satisfy
+
+  char = Text.Megaparsec.Char.char
+
+  notChar = Text.Megaparsec.Char.char
+
+  anyChar = Text.Megaparsec.Char.anyChar
+
+  string = fmap Data.Text.Lazy.unpack . Text.Megaparsec.Char.string . fromString
+
+  text = fmap Data.Text.Lazy.toStrict . Text.Megaparsec.Char.string . Data.Text.Lazy.fromStrict
+
 instance TokenParsing Parser where
     someSpace =
         Text.Parser.Token.Style.buildSomeSpaceParser
-            (Parser someSpace)
+            (Parser (Text.Megaparsec.skipSome (Text.Megaparsec.Char.satisfy Data.Char.isSpace)))
             Text.Parser.Token.Style.haskellCommentStyle
 
-    nesting (Parser m) = Parser (nesting m)
-
-    semi = Parser semi
+    highlight _ = id
 
-    highlight h (Parser m) = Parser (highlight h m)
+    semi = token (Text.Megaparsec.Char.char ';' <?> ";")
 
 noted :: Parser (Expr Src a) -> Parser (Expr Src a)
 noted parser = do
-    before     <- Text.Trifecta.position
-    (e, bytes) <- Text.Trifecta.slicedWith (,) parser
-    after      <- Text.Trifecta.position
-    return (Note (Src before after bytes) e)
+    before      <- Text.Megaparsec.getPosition
+    (tokens, e) <- Text.Megaparsec.match parser
+    after       <- Text.Megaparsec.getPosition
+    return (Note (Src before after tokens) e)
 
 count :: (Semigroup a, Monoid a) => Int -> Parser a -> Parser a
 count n parser = mconcat (replicate n parser)
@@ -269,6 +288,29 @@
     whitespace
     return t ) <?> "label"
 
+noDuplicates :: Ord a => [a] -> Parser (Set a)
+noDuplicates = go Data.Set.empty
+  where
+    go found    []  = return found
+    go found (x:xs) =
+        if Data.Set.member x found
+        then fail "Duplicate key"
+        else go (Data.Set.insert x found) xs
+
+labels :: Parser (Set Text)
+labels = do
+    _openBrace
+    xs <- nonEmptyLabels <|> emptyLabels
+    _closeBrace
+    return xs
+  where
+    emptyLabels = pure Data.Set.empty
+
+    nonEmptyLabels = do
+        x  <- label
+        xs <- many (do _ <- _comma; label)
+        noDuplicates (x : xs)
+
 doubleQuotedChunk :: Parser a -> Parser (Chunks Src a)
 doubleQuotedChunk embedded =
     choice
@@ -279,7 +321,7 @@
   where
     interpolation = do
         _ <- Text.Parser.Char.text "${"
-        e <- expression embedded
+        e <- completeExpression embedded
         _ <- Text.Parser.Char.char '}'
         return (Chunks [(mempty, e)] mempty)
 
@@ -427,7 +469,7 @@
 
         interpolation = do
             _ <- Text.Parser.Char.text "${"
-            a <- expression embedded
+            a <- completeExpression embedded
             _ <- Text.Parser.Char.char '}'
             b <- singleQuoteContinue embedded
             return (Chunks [(mempty, a)] mempty <> b)
@@ -669,6 +711,11 @@
     void (Text.Parser.Char.char '∧' <?> "\"∧\"") <|> void (Text.Parser.Char.text "/\\")
     whitespace
 
+_combineTypes :: Parser ()
+_combineTypes = do
+    void (Text.Parser.Char.char '⩓' <?> "\"⩓\"") <|> void (Text.Parser.Char.text "//\\\\")
+    whitespace
+
 _prefer :: Parser ()
 _prefer = do
     void (Text.Parser.Char.char '⫽' <?> "\"⫽\"") <|> void (Text.Parser.Char.text "//")
@@ -1135,8 +1182,12 @@
 
 preferExpression :: Parser a -> Parser (Expr Src a)
 preferExpression =
-    makeOperatorExpression timesExpression _prefer Prefer
+    makeOperatorExpression combineTypesExpression _prefer Prefer
 
+combineTypesExpression :: Parser a -> Parser (Expr Src a)
+combineTypesExpression =
+    makeOperatorExpression timesExpression _combineTypes CombineTypes
+
 timesExpression :: Parser a -> Parser (Expr Src a)
 timesExpression =
     makeOperatorExpression equalExpression _times NaturalTimes
@@ -1164,9 +1215,12 @@
 selectorExpression :: Parser a -> Parser (Expr Src a)
 selectorExpression embedded = noted (do
     a <- primitiveExpression embedded
-    b <- many (try (do _dot; label))
-    return (foldl Field a b) )
 
+    let left  x  e = Field   e x
+    let right xs e = Project e xs
+    b <- many (try (do _dot; fmap left label <|> fmap right labels))
+    return (foldl (\e k -> k e) a b) )
+
 primitiveExpression :: Parser a -> Parser (Expr Src a)
 primitiveExpression embedded =
     noted
@@ -1513,9 +1567,13 @@
         _ <- Text.Parser.Char.text "sha256:"
         builder <- count 64 (satisfy hexdig <?> "hex digit")
         whitespace
-        let lazyText = Data.Text.Lazy.Builder.toLazyText builder
-        let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 lazyText
-        case Crypto.Hash.digestFromByteString (Data.ByteString.Lazy.toStrict lazyBytes) of
+        let lazyText    = Data.Text.Lazy.Builder.toLazyText builder
+        let lazyBytes16 = Data.Text.Lazy.Encoding.encodeUtf8 lazyText
+        let strictBytes16 = Data.ByteString.Lazy.toStrict lazyBytes16
+        strictBytes <- case Data.ByteArray.Encoding.convertFromBase Base16 strictBytes16 of
+            Left  string      -> fail string
+            Right strictBytes -> return (strictBytes :: Data.ByteString.ByteString)
+        case Crypto.Hash.digestFromByteString strictBytes of
           Nothing -> fail "Invalid sha256 hash"
           Just h -> pure h
 
@@ -1531,16 +1589,19 @@
         return RawText
 
 -- | A parsing error
-newtype ParseError = ParseError Doc deriving (Typeable)
+data ParseError = ParseError
+    { unwrap :: Text.Megaparsec.ParseError Char Void
+    , input  :: Text
+    }
 
 instance Show ParseError where
-    show (ParseError doc) =
-      "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> show doc
+    show (ParseError {..}) =
+      "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> Text.Megaparsec.parseErrorPretty' input unwrap
 
 instance Exception ParseError
 
 -- | Parse an expression from `Text` containing a Dhall program
-exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path)
+exprFromText :: String -> Text -> Either ParseError (Expr Src Path)
 exprFromText delta text = fmap snd (exprAndHeaderFromText delta text)
 
 {-| Like `exprFromText` but also returns the leading comments and whitespace
@@ -1556,24 +1617,17 @@
     This is used by @dhall-format@ to preserve leading comments and whitespace
 -}
 exprAndHeaderFromText
-    :: Delta
+    :: String
     -> Text
     -> Either ParseError (Text, Expr Src Path)
 exprAndHeaderFromText delta text = case result of
-    Failure errInfo    -> Left (ParseError (Text.Trifecta._errDoc errInfo))
-    Success (bytes, r) -> case Data.Text.Encoding.decodeUtf8' bytes of
-        Left  errInfo -> Left (ParseError (fromString (show errInfo)))
-        Right txt     -> do
-            let stripped = Data.Text.dropWhileEnd (/= '\n') txt
-            let lazyText = Data.Text.Lazy.fromStrict stripped
-            Right (lazyText, r)
+    Left errInfo   -> Left (ParseError { unwrap = errInfo, input = text })
+    Right (txt, r) -> Right (Data.Text.Lazy.dropWhileEnd (/= '\n') txt, r)
   where
-    string = Data.Text.Lazy.unpack text
-
-    parser = unParser (do
-        bytes <- Text.Trifecta.slicedWith (\_ x -> x) whitespace
+    parser = do
+        (bytes, _) <- Text.Megaparsec.match whitespace
         r <- expr
-        Text.Parser.Combinators.eof
-        return (bytes, r) )
+        Text.Megaparsec.eof
+        return (bytes, r)
 
-    result = Text.Trifecta.parseString parser delta string
+    result = Text.Megaparsec.parse (unParser parser) delta text
diff --git a/src/Dhall/Pretty/Internal.hs b/src/Dhall/Pretty/Internal.hs
--- a/src/Dhall/Pretty/Internal.hs
+++ b/src/Dhall/Pretty/Internal.hs
@@ -18,6 +18,36 @@
     , buildScientific
     , pretty
     , escapeText
+
+    , prettyConst
+    , prettyLabel
+    , prettyLabels
+    , prettyNatural
+    , prettyNumber
+    , prettyScientific
+
+    , builtin
+    , keyword
+    , literal
+    , operator
+
+    , colon
+    , comma
+    , dot
+    , equals
+    , forall
+    , label
+    , lambda
+    , langle
+    , lbrace
+    , lbracket
+    , lparen
+    , pipe
+    , rangle
+    , rarrow
+    , rbrace
+    , rbracket
+    , rparen
     ) where
 
 import {-# SOURCE #-} Dhall.Core
@@ -30,6 +60,7 @@
 import Data.HashMap.Strict.InsOrd (InsOrdHashMap)
 import Data.Monoid ((<>))
 import Data.Scientific (Scientific)
+import Data.Set (Set)
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy.Builder (Builder)
 import Data.Text.Prettyprint.Doc (Doc, Pretty, space)
@@ -42,6 +73,7 @@
 import qualified Data.HashMap.Strict.InsOrd
 import qualified Data.HashSet
 import qualified Data.List
+import qualified Data.Set
 import qualified Data.Text.Lazy                        as Text
 import qualified Data.Text.Lazy.Builder                as Builder
 import qualified Data.Text.Prettyprint.Doc             as Pretty
@@ -248,6 +280,13 @@
                         -> Pretty.pretty a
                 _       -> backtick <> Pretty.pretty a <> backtick
 
+prettyLabels :: Set Text -> Doc Ann
+prettyLabels a
+    | Data.Set.null a =
+        lbrace <> rbrace
+    | otherwise =
+        braces (map (duplicate . prettyLabel) (Data.Set.toList a))
+
 prettyNumber :: Integer -> Doc Ann
 prettyNumber = literal . Pretty.pretty
 
@@ -571,10 +610,10 @@
     prettyExprC7 a0
 
 prettyExprC7 :: Pretty a => Expr s a -> Doc Ann
-prettyExprC7 a0@(NaturalTimes _ _) =
-    enclose' "" "  " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))
+prettyExprC7 a0@(CombineTypes _ _) =
+    enclose' "" "  " (" " <> operator "⩓" <> " ") (operator "⩓" <> " ") (fmap duplicate (docs a0))
   where
-    docs (NaturalTimes a b) = prettyExprC8 a : docs b
+    docs (CombineTypes a b) = prettyExprC8 a : docs b
     docs (Note         _ b) = docs b
     docs                 b  = [ prettyExprC8 b ]
 prettyExprC7 (Note _ a) =
@@ -583,27 +622,39 @@
     prettyExprC8 a0
 
 prettyExprC8 :: Pretty a => Expr s a -> Doc Ann
-prettyExprC8 a0@(BoolEQ _ _) =
-    enclose' "" "    " (" " <> operator "==" <> " ") (operator "==" <> "  ") (fmap duplicate (docs a0))
+prettyExprC8 a0@(NaturalTimes _ _) =
+    enclose' "" "  " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))
   where
-    docs (BoolEQ a b) = prettyExprC9 a : docs b
-    docs (Note   _ b) = docs b
-    docs           b  = [ prettyExprC9 b ]
+    docs (NaturalTimes a b) = prettyExprC9 a : docs b
+    docs (Note         _ b) = docs b
+    docs                 b  = [ prettyExprC9 b ]
 prettyExprC8 (Note _ a) =
     prettyExprC8 a
 prettyExprC8 a0 =
     prettyExprC9 a0
 
 prettyExprC9 :: Pretty a => Expr s a -> Doc Ann
-prettyExprC9 a0@(BoolNE _ _) =
-    enclose' "" "    " (" " <> operator "!=" <> " ") (operator "!=" <> "  ") (fmap duplicate (docs a0))
+prettyExprC9 a0@(BoolEQ _ _) =
+    enclose' "" "    " (" " <> operator "==" <> " ") (operator "==" <> "  ") (fmap duplicate (docs a0))
   where
-    docs (BoolNE a b) = prettyExprD a : docs b
+    docs (BoolEQ a b) = prettyExprC10 a : docs b
     docs (Note   _ b) = docs b
-    docs           b  = [ prettyExprD b ]
+    docs           b  = [ prettyExprC10 b ]
 prettyExprC9 (Note _ a) =
     prettyExprC9 a
 prettyExprC9 a0 =
+    prettyExprC10 a0
+
+prettyExprC10 :: Pretty a => Expr s a -> Doc Ann
+prettyExprC10 a0@(BoolNE _ _) =
+    enclose' "" "    " (" " <> operator "!=" <> " ") (operator "!=" <> "  ") (fmap duplicate (docs a0))
+  where
+    docs (BoolNE a b) = prettyExprD a : docs b
+    docs (Note   _ b) = docs b
+    docs           b  = [ prettyExprD b ]
+prettyExprC10 (Note _ a) =
+    prettyExprC10 a
+prettyExprC10 a0 =
     prettyExprD a0
 
 prettyExprD :: Pretty a => Expr s a -> Doc Ann
@@ -621,9 +672,10 @@
     docs               b  = [ prettyExprE b ]
 
 prettyExprE :: Pretty a => Expr s a -> Doc Ann
-prettyExprE (Field a b) = prettyExprE a <> dot <> prettyLabel b
-prettyExprE (Note  _ b) = prettyExprE b
-prettyExprE  a          = prettyExprF a
+prettyExprE (Field   a b) = prettyExprE a <> dot <> prettyLabel b
+prettyExprE (Project a b) = prettyExprE a <> dot <> prettyLabels b
+prettyExprE (Note    _ b) = prettyExprE b
+prettyExprE  a            = prettyExprF a
 
 prettyExprF :: Pretty a => Expr s a -> Doc Ann
 prettyExprF (Var a) =
@@ -947,21 +999,27 @@
 
 -- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser"
 buildExprC7 :: Buildable a => Expr s a -> Builder
-buildExprC7 (NaturalTimes a b) = buildExprC8 a <> " * " <> buildExprC7 b
+buildExprC7 (CombineTypes a b) = buildExprC8 a <> " ⩓ " <> buildExprC7 b
 buildExprC7 (Note         _ b) = buildExprC7 b
 buildExprC7  a                 = buildExprC8 a
 
 -- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser"
 buildExprC8 :: Buildable a => Expr s a -> Builder
-buildExprC8 (BoolEQ a b) = buildExprC9 a <> " == " <> buildExprC8 b
-buildExprC8 (Note   _ b) = buildExprC8 b
-buildExprC8  a           = buildExprC9 a
+buildExprC8 (NaturalTimes a b) = buildExprC9 a <> " * " <> buildExprC8 b
+buildExprC8 (Note         _ b) = buildExprC8 b
+buildExprC8  a                 = buildExprC9 a
 
 -- | Builder corresponding to the @exprC9@ parser in "Dhall.Parser"
 buildExprC9 :: Buildable a => Expr s a -> Builder
-buildExprC9 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC9 b
+buildExprC9 (BoolEQ a b) = buildExprC10 a <> " == " <> buildExprC9 b
 buildExprC9 (Note   _ b) = buildExprC9 b
-buildExprC9  a           = buildExprD  a
+buildExprC9  a           = buildExprC10 a
+
+-- | Builder corresponding to the @exprC10@ parser in "Dhall.Parser"
+buildExprC10 :: Buildable a => Expr s a -> Builder
+buildExprC10 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC10 b
+buildExprC10 (Note   _ b) = buildExprC10 b
+buildExprC10  a           = buildExprD  a
 
 -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser"
 buildExprD :: Buildable a => Expr s a -> Builder
diff --git a/src/Dhall/Tutorial.hs b/src/Dhall/Tutorial.hs
--- a/src/Dhall/Tutorial.hs
+++ b/src/Dhall/Tutorial.hs
@@ -602,6 +602,20 @@
 -- > >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double
 -- > 4.2
 --
+-- ... and you can project out multiple fields into a new record using this
+-- syntax:
+--
+-- > someRecord.{ field₀, field₁, … }
+--
+-- For example:
+--
+-- > $ dhall
+-- > { x = 1, y = True, z = "ABC" }.{ x, y }
+-- > <Ctrl-D>
+-- > { x : Integer, y : Bool }
+-- > 
+-- > { x = 1, y = True }
+--
 -- __Exercise__: What is the type of this record:
 --
 -- > { foo = 1
@@ -900,6 +914,21 @@
 --
 -- __Exercise__: Combine any record with the empty record.  What do you expect
 -- to happen?
+--
+-- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53):
+--
+-- > $ dhall
+-- > { foo : Natural } ⩓ { bar : Text }
+-- > <Ctrl-D>
+-- > { foo : Natural, bar : Text }
+--
+-- ... which behaves the exact same, except at the type level, meaning that the
+-- operator descends recursively into record types:
+--
+-- > $ dhall
+-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }
+-- > <Ctrl-D>
+-- > { foo : { bar : Text, baz : Bool }, qux : Integer }
 
 -- $let
 --
@@ -1123,7 +1152,7 @@
 -- The @constructors@ keyword takes a union type argument and returns a record
 -- with one field per union type constructor:
 --
--- > $ dhall --pretty
+-- > $ dhall
 -- > constructors < Empty : {} | Person : { name : Text, age : Natural } >
 -- > <Ctrl-D>
 -- >
@@ -1615,55 +1644,8 @@
 -- >     (List (List Integer))
 -- >     (replicate +5 (List Integer) (replicate +5 Integer 1))
 --
--- If you want to evaluate and format an expression then you can use the
--- @--pretty@ flag of the @dhall@ executable:
---
--- > $ dhall --pretty
--- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate 
--- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
--- > <Ctrl-D>
--- > List (List (List Integer))
--- > 
--- >   [   [ [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       ]
--- >     : List (List Integer)
--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       ]
--- >     : List (List Integer)
--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       ]
--- >     : List (List Integer)
--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       ]
--- >     : List (List Integer)
--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       , [ 1, 1, 1, 1, 1 ] : List Integer
--- >       ]
--- >     : List (List Integer)
--- >   ]
--- > : List (List (List Integer))
---
 -- You can also use the formatter to modify files in place using the
--- @--inplace@ flag:
+-- @--inplace@ flag (i.e. for formatting source code):
 --
 -- > $ dhall-format --inplace ./unformatted
 -- > $ cat ./unformatted
@@ -1712,6 +1694,54 @@
 -- > {- This comment will be preserved by the formatter -}
 -- > -- ... and this comment will be preserved, too
 -- > 1
+--
+-- Note that you do not need to use @dhall-format@ to format the output of the
+-- @dhall@ interpreter.  The interpreter already automatically formats
+-- multi-line expressions, too:
+--
+-- > $ dhall
+-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate 
+-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
+-- > <Ctrl-D>
+-- > List (List (List Integer))
+-- > 
+-- >   [   [ [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       ]
+-- >     : List (List Integer)
+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       ]
+-- >     : List (List Integer)
+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       ]
+-- >     : List (List Integer)
+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       ]
+-- >     : List (List Integer)
+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer
+-- >       ]
+-- >     : List (List Integer)
+-- >   ]
+-- > : List (List (List Integer))
 
 -- $builtins
 --
@@ -2682,7 +2712,7 @@
 --
 -- __Exercise__: Browse the Prelude by running:
 --
--- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'
+-- > $ dhall <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'
 
 -- $conclusion
 --
diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs
--- a/src/Dhall/TypeCheck.hs
+++ b/src/Dhall/TypeCheck.hs
@@ -28,7 +28,7 @@
 import Data.Set (Set)
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy.Builder (Builder)
-import Data.Text.Prettyprint.Doc (Pretty(..))
+import Data.Text.Prettyprint.Doc (Doc, Pretty(..))
 import Data.Traversable (forM)
 import Data.Typeable (Typeable)
 import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..))
@@ -39,15 +39,25 @@
 import qualified Data.HashMap.Strict.InsOrd
 import qualified Data.Sequence
 import qualified Data.Set
-import qualified Data.Text.Lazy                   as Text
-import qualified Data.Text.Lazy.Builder           as Builder
+import qualified Data.Text.Lazy                        as Text
+import qualified Data.Text.Lazy.Builder                as Builder
+import qualified Data.Text.Prettyprint.Doc             as Pretty
+import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty
 import qualified Dhall.Context
 import qualified Dhall.Core
+import qualified Dhall.Diff
+import qualified Dhall.Pretty
+import qualified Dhall.Pretty.Internal
 
 traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f ()
 traverseWithIndex_ k xs =
     Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs)
 
+docToLazyText :: Doc a -> Text
+docToLazyText = Pretty.renderLazy . Pretty.layoutPretty opts
+  where
+    opts = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }
+
 axiom :: Const -> Either (TypeError s a) Const
 axiom Type = return Kind
 axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped)
@@ -424,25 +434,69 @@
                       (Pi "just" (Pi "_" "a" "optional")
                           (Pi "nothing" "optional" "optional") )
     loop ctx e@(Record    kts   ) = do
-        let process (k, t) = do
-                s <- fmap Dhall.Core.normalize (loop ctx t)
-                case s of
-                    Const Type -> return ()
-                    Const Kind -> return ()
-                    _          -> Left (TypeError ctx e (InvalidFieldType k t))
-        mapM_ process (Data.HashMap.Strict.InsOrd.toList kts)
-        return (Const Type)
+        case Data.HashMap.Strict.InsOrd.toList kts of
+            []            -> return (Const Type)
+            (k0, t0):rest -> do
+                s0 <- fmap Dhall.Core.normalize (loop ctx t0)
+                c <- case s0 of
+                    Const Type ->
+                        return Type
+                    Const Kind
+                        | Dhall.Core.judgmentallyEqual t0 (Const Type) ->
+                            return Kind
+                    _ -> Left (TypeError ctx e (InvalidFieldType k0 t0))
+                let process (k, t) = do
+                        s <- fmap Dhall.Core.normalize (loop ctx t)
+                        case s of
+                            Const Type ->
+                                if c == Type
+                                then return ()
+                                else Left (TypeError ctx e (FieldAnnotationMismatch k t k0 t0 Type))
+                            Const Kind ->
+                                if c == Kind
+                                then
+                                    if Dhall.Core.judgmentallyEqual t (Const Type)
+                                    then return ()
+                                    else Left (TypeError ctx e (InvalidFieldType k t))
+                                else Left (TypeError ctx e (FieldAnnotationMismatch k t k0 t0 Kind))
+                            _ ->
+                                Left (TypeError ctx e (InvalidFieldType k t))
+                mapM_ process rest
+                return (Const c)
     loop ctx e@(RecordLit kvs   ) = do
-        let process k v = do
-                t <- loop ctx v
-                s <- fmap Dhall.Core.normalize (loop ctx t)
-                case s of
-                    Const Type -> return ()
-                    Const Kind -> return ()
-                    _          -> Left (TypeError ctx e (InvalidField k v))
-                return t
-        kts <- Data.HashMap.Strict.InsOrd.traverseWithKey process kvs
-        return (Record kts)
+        case Data.HashMap.Strict.InsOrd.toList kvs of
+            []         -> return (Record Data.HashMap.Strict.InsOrd.empty)
+            (k0, v0):_ -> do
+                t0 <- loop ctx v0
+                s0 <- fmap Dhall.Core.normalize (loop ctx t0)
+                c <- case s0 of
+                    Const Type ->
+                        return Type
+                    Const Kind
+                        | Dhall.Core.judgmentallyEqual t0 (Const Type) ->
+                            return Kind
+                    _       -> Left (TypeError ctx e (InvalidField k0 v0))
+                let process k v = do
+                        t <- loop ctx v
+                        s <- fmap Dhall.Core.normalize (loop ctx t)
+                        case s of
+                            Const Type ->
+                                if c == Type
+                                then return ()
+                                else Left (TypeError ctx e (FieldMismatch k v k0 v0 Type))
+                            Const Kind ->
+                                if c == Kind
+                                then
+                                    if Dhall.Core.judgmentallyEqual t (Const Type)
+                                    then return ()
+                                    else Left (TypeError ctx e (InvalidFieldType k t))
+                                else Left (TypeError ctx e (FieldMismatch k v k0 v0 Kind))
+                            _ ->
+                                Left (TypeError ctx e (InvalidField k t))
+
+                        return t
+                kts <- Data.HashMap.Strict.InsOrd.traverseWithKey process kvs
+                return (Record kts)
     loop ctx e@(Union     kts   ) = do
         let process (k, t) = do
                 s <- fmap Dhall.Core.normalize (loop ctx t)
@@ -491,6 +545,52 @@
                 return (Record (Data.HashMap.Strict.InsOrd.fromList kts))
 
         combineTypes ktsX ktsY
+    loop ctx e@(CombineTypes l r) = do
+        tL <- loop ctx l
+        let l' = Dhall.Core.normalize l
+        cL <- case tL of
+            Const cL -> return cL
+            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
+        tR <- loop ctx r
+        let r' = Dhall.Core.normalize r
+        cR <- case tR of
+            Const cR -> return cR
+            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))
+        let decide Type Type =
+                return Type
+            decide Kind Kind =
+                return Kind
+            decide x y =
+                Left (TypeError ctx e (RecordTypeMismatch x y l r))
+        c <- decide cL cR
+
+        ktsL0 <- case l' of
+            Record kts -> return kts
+            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))
+        ktsR0 <- case r' of
+            Record kts -> return kts
+            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))
+
+        let combineTypes ktsL ktsR = do
+                let ksL =
+                        Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsL)
+                let ksR =
+                        Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsR)
+                let ks = Data.Set.union ksL ksR
+                forM_ (toList ks) (\k -> do
+                    case (Data.HashMap.Strict.InsOrd.lookup k ktsL, Data.HashMap.Strict.InsOrd.lookup k ktsR) of
+                        (Just (Record ktsL'), Just (Record ktsR')) -> do
+                            combineTypes ktsL' ktsR'
+                        (Nothing, Just _) -> do
+                            return ()
+                        (Just _, Nothing) -> do
+                            return ()
+                        _ -> do
+                            Left (TypeError ctx e (FieldCollision k)) )
+
+        combineTypes ktsL0 ktsR0
+
+        return (Const c)
     loop ctx e@(Prefer kvsX kvsY) = do
         tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)
         ktsX  <- case tKvsX of
@@ -597,7 +697,24 @@
                 case Data.HashMap.Strict.InsOrd.lookup x kts of
                     Just t' -> return t'
                     Nothing -> Left (TypeError ctx e (MissingField x t))
-            _          -> Left (TypeError ctx e (NotARecord x r t))
+            _ -> do
+                let text = docToLazyText (Dhall.Pretty.Internal.prettyLabel x)
+                Left (TypeError ctx e (NotARecord text r t))
+    loop ctx e@(Project r xs    ) = do
+        t <- fmap Dhall.Core.normalize (loop ctx r)
+        case t of
+            Record kts -> do
+                _ <- loop ctx t
+
+                let process k =
+                        case Data.HashMap.Strict.InsOrd.lookup k kts of
+                            Just t' -> return (k, t')
+                            Nothing -> Left (TypeError ctx e (MissingField k t))
+                let adapt = Record . Data.HashMap.Strict.InsOrd.fromList
+                fmap adapt (traverse process (Data.Set.toList xs))
+            _ -> do
+                let text = docToLazyText (Dhall.Pretty.Internal.prettyLabels xs)
+                Left (TypeError ctx e (NotARecord text r t))
     loop ctx   (Note s e'       ) = case loop ctx e' of
         Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m)
         Left (TypeError ctx'          e''  m) -> Left (TypeError ctx' (Note s  e'') m)
@@ -646,11 +763,15 @@
     | IfBranchMustBeTerm Bool (Expr s a) (Expr s a) (Expr s a)
     | InvalidField Text (Expr s a)
     | InvalidFieldType Text (Expr s a)
+    | FieldAnnotationMismatch Text (Expr s a) Text (Expr s a) Const
+    | FieldMismatch Text (Expr s a) Text (Expr s a) Const
     | InvalidAlternative Text (Expr s a)
     | InvalidAlternativeType Text (Expr s a)
     | ListAppendMismatch (Expr s a) (Expr s a)
     | DuplicateAlternative Text
     | MustCombineARecord Char (Expr s a) (Expr s a)
+    | CombineTypesRequiresRecordType (Expr s a) (Expr s a)
+    | RecordTypeMismatch Const Const (Expr s a) (Expr s a)
     | FieldCollision Text
     | MustMergeARecord (Expr s a) (Expr s a)
     | MustMergeUnion (Expr s a) (Expr s a)
@@ -676,13 +797,13 @@
     | NoDependentTypes (Expr s a) (Expr s a)
     deriving (Show)
 
-shortTypeMessage :: Buildable a => TypeMessage s a -> Builder
+shortTypeMessage :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> Builder
 shortTypeMessage msg =
     "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"
   where
     ErrorMessages {..} = prettyTypeMessage msg
 
-longTypeMessage :: Buildable a => TypeMessage s a -> Builder
+longTypeMessage :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> Builder
 longTypeMessage msg =
         "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"
     <>  "\n"
@@ -700,7 +821,22 @@
 _NOT :: Builder
 _NOT = "\ESC[1mnot\ESC[0m"
 
-prettyTypeMessage :: Buildable a => TypeMessage s a -> ErrorMessages
+prettyDiff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Builder
+prettyDiff exprL exprR = builder
+  where
+    doc =
+        fmap Dhall.Pretty.annToAnsiStyle (Dhall.Diff.diffNormalized exprL exprR)
+
+    opts = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }
+
+    stream = Pretty.layoutPretty opts doc
+
+    lazyText = Pretty.renderLazy stream
+
+    builder = Builder.fromLazyText lazyText
+
+prettyTypeMessage
+    :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> ErrorMessages
 prettyTypeMessage (UnboundVariable _) = ErrorMessages {..}
   -- We do not need to print variable name here. For the discussion see:
   -- https://github.com/dhall-lang/dhall-haskell/pull/116
@@ -1098,7 +1234,9 @@
 
 prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
   where
-    short = "Wrong type of function argument"
+    short = "Wrong type of function argument\n"
+        <>  "\n"
+        <>  prettyDiff expr1 expr3
 
     long =
         "Explanation: Every function declares what type or kind of argument to accept    \n\
@@ -1230,8 +1368,9 @@
 
 prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}
   where
-    short = "Expression doesn't match annotation"
-
+    short = "Expression doesn't match annotation\n"
+        <>  "\n"
+        <>  prettyDiff expr1 expr2
     long =
         "Explanation: You can annotate an expression with its type or kind using the     \n\
         \❰:❱ symbol, like this:                                                          \n\
@@ -1511,7 +1650,9 @@
 prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
     ErrorMessages {..}
   where
-    short = "❰if❱ branches must have matching types"
+    short = "❰if❱ branches must have matching types\n"
+        <>  "\n"
+        <>  prettyDiff expr1 expr3
 
     long =
         "Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\
@@ -1660,7 +1801,9 @@
 prettyTypeMessage (MismatchedListElements i expr0 _expr1 expr2) =
     ErrorMessages {..}
   where
-    short = "List elements should all have the same type"
+    short = "List elements should all have the same type\n"
+        <>  "\n"
+        <>  prettyDiff expr0 expr2
 
     long =
         "Explanation: Every element in a list must have the same type                    \n\
@@ -1696,7 +1839,9 @@
 prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =
     ErrorMessages {..}
   where
-    short = "List element has the wrong type"
+    short = "List element has the wrong type\n"
+        <>  "\n"
+        <>  prettyDiff expr0 expr2
 
     long =
         "Explanation: Every element in the list must have a type matching the type       \n\
@@ -1783,7 +1928,9 @@
 
 prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..}
   where
-    short = "❰Optional❱ element has the wrong type"
+    short = "❰Optional❱ element has the wrong type\n"
+        <>  "\n"
+        <>  prettyDiff expr0 expr2
 
     long =
         "Explanation: An ❰Optional❱ element must have a type matching the type annotation\n\
@@ -1825,32 +1972,75 @@
     short = "Invalid field type"
 
     long =
-        "Explanation: Every record type documents the type of each field, like this:     \n\
+        "Explanation: Every record type annotates each field with a ❰Type❱ or a ❰Kind❱,  \n\
+        \like this:                                                                      \n\
         \                                                                                \n\
+        \                                                                                \n\
         \    ┌──────────────────────────────────────────────┐                            \n\
-        \    │ { foo : Integer, bar : Integer, baz : Text } │                            \n\
-        \    └──────────────────────────────────────────────┘                            \n\
+        \    │ { foo : Integer, bar : Integer, baz : Text } │  Every field is annotated  \n\
+        \    └──────────────────────────────────────────────┘  with a ❰Type❱             \n\
         \                                                                                \n\
-        \However, fields cannot be annotated with expressions other than types           \n\
         \                                                                                \n\
-        \For example, these record types are " <> _NOT <> " valid:                       \n\
+        \    ┌────────────────────────────┐                                              \n\
+        \    │ { foo : Type, bar : Type } │  Every field is annotated                    \n\
+        \    └────────────────────────────┘  with a ❰Kind❱                               \n\
         \                                                                                \n\
         \                                                                                \n\
+        \However, the types of fields may " <> _NOT <> " be term-level values:           \n\
+        \                                                                                \n\
+        \                                                                                \n\
         \    ┌────────────────────────────┐                                              \n\
-        \    │ { foo : Integer, bar : 1 } │                                              \n\
+        \    │ { foo : Integer, bar : 1 } │  Invalid record type                         \n\
         \    └────────────────────────────┘                                              \n\
         \                             ⇧                                                  \n\
-        \                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱               \n\
+        \                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱ or ❰Kind❱     \n\
         \                                                                                \n\
         \                                                                                \n\
+        \You provided a record type with a field named:                                  \n\
+        \                                                                                \n\
+        \↳ " <> txt0 <> "                                                                \n\
+        \                                                                                \n\
+        \... annotated with the following expression:                                    \n\
+        \                                                                                \n\
+        \↳ " <> txt1 <> "                                                                \n\
+        \                                                                                \n\
+        \... which is neither a ❰Type❱ nor a ❰Kind❱                                      \n"
+      where
+        txt0 = build k
+        txt1 = build expr0
+
+prettyTypeMessage (FieldAnnotationMismatch k0 expr0 k1 expr1 c) = ErrorMessages {..}
+  where
+    short = "Field annotation mismatch"
+
+    long =
+        "Explanation: Every record type annotates each field with a ❰Type❱ or a ❰Kind❱,  \n\
+        \like this:                                                                      \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────────────────────┐                            \n\
+        \    │ { foo : Integer, bar : Integer, baz : Text } │  Every field is annotated  \n\
+        \    └──────────────────────────────────────────────┘  with a ❰Type❱             \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌────────────────────────────┐                                              \n\
+        \    │ { foo : Type, bar : Type } │  Every field is annotated                    \n\
+        \    └────────────────────────────┘  with a ❰Kind❱                               \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \However, you cannot have a record type with both a ❰Type❱ and ❰Kind❱ annotation:\n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \              This is a ❰Type❱ annotation                                       \n\
+        \              ⇩                                                                 \n\
         \    ┌───────────────────────────────┐                                           \n\
-        \    │ { foo : Integer, bar : Type } │                                           \n\
+        \    │ { foo : Integer, bar : Type } │  Invalid record type                      \n\
         \    └───────────────────────────────┘                                           \n\
         \                             ⇧                                                  \n\
-        \                             ❰Type❱ is a ❰Kind❱ and not a ❰Type❱                \n\
+        \                             ... but this is a ❰Kind❱ annotation                \n\
         \                                                                                \n\
         \                                                                                \n\
-        \You provided a record type with a key named:                                    \n\
+        \You provided a record type with a field named:                                  \n\
         \                                                                                \n\
         \↳ " <> txt0 <> "                                                                \n\
         \                                                                                \n\
@@ -1858,11 +2048,91 @@
         \                                                                                \n\
         \↳ " <> txt1 <> "                                                                \n\
         \                                                                                \n\
-        \... which is not a type                                                         \n"
+        \... which is a " <> here <> " whereas another field named:                      \n\
+        \                                                                                \n\
+        \↳ " <> txt2 <> "                                                                \n\
+        \                                                                                \n\
+        \... annotated with the following expression:                                    \n\
+        \                                                                                \n\
+        \↳ " <> txt3 <> "                                                                \n\
+        \                                                                                \n\
+        \... is a " <> there <> ", which does not match                                  \n"
       where
-        txt0 = build k
+        txt0 = build k0
         txt1 = build expr0
+        txt2 = build k1
+        txt3 = build expr1
 
+        here = case c of
+            Type -> "❰Type❱"
+            Kind -> "❰Kind❱"
+
+        there = case c of
+            Type -> "❰Kind❱"
+            Kind -> "❰Type❱"
+
+prettyTypeMessage (FieldMismatch k0 expr0 k1 expr1 c) = ErrorMessages {..}
+  where
+    short = "Field mismatch"
+
+    long =
+        "Explanation: Every record has fields that can be either terms or types, like    \n\
+        \this:                                                                           \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────────────┐                                    \n\
+        \    │ { foo = 1, bar = True, baz = \"ABC\" } │  Every field is a term           \n\
+        \    └──────────────────────────────────────┘                                    \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌───────────────────────────────┐                                           \n\
+        \    │ { foo = Integer, bar = Text } │  Every field is a type                    \n\
+        \    └───────────────────────────────┘                                           \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \However, you cannot have a record that stores both terms and types:             \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \              This is a term                                                    \n\
+        \              ⇩                                                                 \n\
+        \    ┌─────────────────────────┐                                                 \n\
+        \    │ { foo = 1, bar = Bool } │  Invalid record                                 \n\
+        \    └─────────────────────────┘                                                 \n\
+        \                       ⇧                                                        \n\
+        \                       ... but this is a type                                   \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \You provided a record with a field named:                                       \n\
+        \                                                                                \n\
+        \↳ " <> txt0 <> "                                                                \n\
+        \                                                                                \n\
+        \... whose value was:                                                            \n\
+        \                                                                                \n\
+        \↳ " <> txt1 <> "                                                                \n\
+        \                                                                                \n\
+        \... which is a " <> here <> " whereas another field named:                      \n\
+        \                                                                                \n\
+        \↳ " <> txt2 <> "                                                                \n\
+        \                                                                                \n\
+        \... whose value was:                                                            \n\
+        \                                                                                \n\
+        \↳ " <> txt3 <> "                                                                \n\
+        \                                                                                \n\
+        \... is a " <> there <> ", which does not match                                  \n"
+      where
+        txt0 = build k0
+        txt1 = build expr0
+        txt2 = build k1
+        txt3 = build expr1
+
+        here = case c of
+            Type -> "term"
+            Kind -> "type"
+
+        there = case c of
+            Type -> "type"
+            Kind -> "term"
+
 prettyTypeMessage (InvalidField k expr0) = ErrorMessages {..}
   where
     short = "Invalid field"
@@ -1875,26 +2145,19 @@
         \    │ { foo = 100, bar = True, baz = \"ABC\" } │                                \n\
         \    └────────────────────────────────────────┘                                  \n\
         \                                                                                \n\
-        \However, fields can only be terms and cannot be types or kinds                  \n\
-        \                                                                                \n\
-        \For example, these record literals are " <> _NOT <> " valid:                    \n\
-        \                                                                                \n\
+        \However, fields can only be terms and or ❰Type❱s and not ❰Kind❱s                \n\
         \                                                                                \n\
-        \    ┌───────────────────────────┐                                               \n\
-        \    │ { foo = 100, bar = Text } │                                               \n\
-        \    └───────────────────────────┘                                               \n\
-        \                         ⇧                                                      \n\
-        \                         ❰Text❱ is a type and not a term                        \n\
+        \For example, the following record literal is " <> _NOT <> " valid:              \n\
         \                                                                                \n\
         \                                                                                \n\
-        \    ┌───────────────────────────┐                                               \n\
-        \    │ { foo = 100, bar = Type } │                                               \n\
-        \    └───────────────────────────┘                                               \n\
-        \                         ⇧                                                      \n\
-        \                         ❰Type❱ is a kind and not a term                        \n\
+        \    ┌────────────────┐                                                          \n\
+        \    │ { foo = Type } │                                                          \n\
+        \    └────────────────┘                                                          \n\
+        \              ⇧                                                                 \n\
+        \              ❰Type❱ is a ❰Kind❱, which is not allowed                          \n\
         \                                                                                \n\
         \                                                                                \n\
-        \You provided a record literal with a key named:                                 \n\
+        \You provided a record literal with a field named:                               \n\
         \                                                                                \n\
         \↳ " <> txt0 <> "                                                                \n\
         \                                                                                \n\
@@ -1902,7 +2165,7 @@
         \                                                                                \n\
         \↳ " <> txt1 <> "                                                                \n\
         \                                                                                \n\
-        \... which is not a term                                                         \n"
+        \... which is not a term or ❰Type❱                                               \n"
       where
         txt0 = build k
         txt1 = build expr0
@@ -2031,7 +2294,9 @@
 
 prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}
   where
-    short = "You can only append ❰List❱s with matching element types"
+    short = "You can only append ❰List❱s with matching element types\n"
+        <>  "\n"
+        <>  prettyDiff expr0 expr1
 
     long =
         "Explanation: You can append two ❰List❱s using the ❰#❱ operator, like this:      \n\
@@ -2152,13 +2417,103 @@
         txt0 = build expr0
         txt1 = build expr1
 
+prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) =
+    ErrorMessages {..}
+  where
+    short = "❰⩓❱ requires arguments that are record types"
+
+    long =
+        "Explanation: You can only use the ❰⩓❱ operator on arguments that are record type\n\
+        \literals, like this:                                                            \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌─────────────────────────────────────┐                                     \n\
+        \    │ { age : Natural } ⩓ { name : Text } │                                     \n\
+        \    └─────────────────────────────────────┘                                     \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \... but you cannot use the ❰⩓❱ operator on any other type of arguments.  For    \n\
+        \example, you cannot use variable arguments:                                     \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌───────────────────────────────────┐                                       \n\
+        \    │ λ(t : Type) → t ⩓ { name : Text } │  Invalid: ❰t❱ might not be a record   \n\
+        \    └───────────────────────────────────┘  type                                 \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \────────────────────────────────────────────────────────────────────────────────\n\
+        \                                                                                \n\
+        \You tried to supply the following argument:                                     \n\
+        \                                                                                \n\
+        \↳ " <> txt0 <> "                                                                \n\
+        \                                                                                \n\
+        \... which normalized to:                                                        \n\
+        \                                                                                \n\
+        \↳ " <> txt1 <> "                                                                \n\
+        \                                                                                \n\
+        \... which is not a record type literal                                          \n"
+      where
+        txt0 = build expr0
+        txt1 = build expr1
+
+prettyTypeMessage (RecordTypeMismatch const0 const1 expr0 expr1) =
+    ErrorMessages {..}
+  where
+    short = "Record type mismatch"
+
+    long =
+        "Explanation: You can only use the ❰⩓❱ operator on record types if they are both \n\
+        \ ❰Type❱s or ❰Kind❱s:                                                            \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌─────────────────────────────────────┐                                     \n\
+        \    │ { age : Natural } ⩓ { name : Text } │  Valid: Both arguments are ❰Type❱s  \n\
+        \    └─────────────────────────────────────┘                                     \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────────────┐                                    \n\
+        \    │ { Input : Type } ⩓ { Output : Type } │  Valid: Both arguments are ❰Kind❱s \n\
+        \    └──────────────────────────────────────┘                                    \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \... but you cannot combine a ❰Type❱ and a ❰Kind❱:                               \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌────────────────────────────────────┐                                      \n\
+        \    │ { Input : Type } ⩓ { name : Text } │  Invalid: The arguments do not match \n\
+        \    └────────────────────────────────────┘                                      \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \────────────────────────────────────────────────────────────────────────────────\n\
+        \                                                                                \n\
+        \You tried to combine the following record type:                                 \n\
+        \                                                                                \n\
+        \↳ " <> txt0 <> "                                                                \n\
+        \                                                                                \n\
+        \... with this record types:                                                     \n\
+        \                                                                                \n\
+        \↳ " <> txt1 <> "                                                                \n\
+        \                                                                                \n\
+        \... but the former record type is a:                                            \n\
+        \                                                                                \n\
+        \↳ " <> txt2 <> "                                                                \n\
+        \                                                                                \n\
+        \... but the latter record type is a:                                            \n\
+        \                                                                                \n\
+        \↳ " <> txt3 <> "                                                                \n"
+      where
+        txt0 = build expr0
+        txt1 = build expr1
+        txt2 = build const0
+        txt3 = build const1
+
 prettyTypeMessage (FieldCollision k) = ErrorMessages {..}
   where
     short = "Field collision"
 
     long =
-        "Explanation: You can combine records if they don't share any fields in common,  \n\
-        \like this:                                                                      \n\
+        "Explanation: You can combine records or record types if they don't share any    \n\
+        \fields in common, like this:                                                    \n\
         \                                                                                \n\
         \                                                                                \n\
         \    ┌───────────────────────────────────────────┐                               \n\
@@ -2166,21 +2521,45 @@
         \    └───────────────────────────────────────────┘                               \n\
         \                                                                                \n\
         \                                                                                \n\
+        \    ┌─────────────────────────────────┐                                         \n\
+        \    │ { foo : Text } ⩓ { bar : Bool } │                                         \n\
+        \    └─────────────────────────────────┘                                         \n\
+        \                                                                                \n\
+        \                                                                                \n\
         \    ┌────────────────────────────────────────┐                                  \n\
         \    │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │                                  \n\
         \    └────────────────────────────────────────┘                                  \n\
         \                                                                                \n\
         \                                                                                \n\
-        \... but you cannot merge two records that share the same field                  \n\
+        \... but you cannot merge two records that share the same field unless the field \n\
+        \is a record on both sides.                                                      \n\
         \                                                                                \n\
-        \For example, the following expression is " <> _NOT <> " valid:                  \n\
+        \For example, the following expressions are " <> _NOT <> " valid:                \n\
         \                                                                                \n\
         \                                                                                \n\
         \    ┌───────────────────────────────────────────┐                               \n\
-        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱ fields\n\
-        \    └───────────────────────────────────────────┘                               \n\
+        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱   \n\
+        \    └───────────────────────────────────────────┘  fields                       \n\
         \                                                                                \n\
         \                                                                                \n\
+        \    ┌─────────────────────────────────┐                                         \n\
+        \    │ { foo : Bool } ∧ { foo : Text } │  Invalid: Colliding ❰foo❱ fields        \n\
+        \    └─────────────────────────────────┘                                         \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \... but the following expressions are valid:                                    \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────────────────────────┐                        \n\
+        \    │ { foo = { bar = True } } ∧ { foo = { baz = 1 } } │  Valid: Both ❰foo❱     \n\
+        \    └──────────────────────────────────────────────────┘  fields are records    \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌─────────────────────────────────────────────────────┐                     \n\
+        \    │ { foo : { bar : Bool } } ⩓ { foo : { baz : Text } } │  Valid: Both ❰foo❱  \n\
+        \    └─────────────────────────────────────────────────────┘  fields are records \n\
+        \                                                                                \n\
+        \                                                                                \n\
         \Some common reasons why you might get this error:                               \n\
         \                                                                                \n\
         \● You tried to use ❰∧❱ to update a field's value, like this:                    \n\
@@ -2413,7 +2792,9 @@
 prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
     ErrorMessages {..}
   where
-    short = "Wrong handler input type"
+    short = "Wrong handler input type\n"
+        <>  "\n"
+        <>  prettyDiff expr1 expr2
 
     long =
         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@@ -2473,7 +2854,9 @@
 prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
     ErrorMessages {..}
   where
-    short = "Wrong handler output type"
+    short = "Wrong handler output type\n"
+        <>  "\n"
+        <>  prettyDiff expr1 expr2
 
     long =
         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@@ -2535,7 +2918,9 @@
 prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =
     ErrorMessages {..}
   where
-    short = "Handlers should have the same output type"
+    short = "Handlers should have the same output type\n"
+        <>  "\n"
+        <>  prettyDiff expr0 expr1
 
     long =
         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
@@ -2680,7 +3065,7 @@
         txt0 = build expr0
         txt1 = build expr1
  
-prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..}
+prettyTypeMessage (NotARecord lazyText0 expr0 expr1) = ErrorMessages {..}
   where
     short = "Not a record"
 
@@ -2725,7 +3110,7 @@
         \                                                                                \n\
         \────────────────────────────────────────────────────────────────────────────────\n\
         \                                                                                \n\
-        \You tried to access a field named:                                              \n\
+        \You tried to access the field(s):                                               \n\
         \                                                                                \n\
         \↳ " <> txt0 <> "                                                                \n\
         \                                                                                \n\
@@ -2737,7 +3122,7 @@
         \                                                                                \n\
         \↳ " <> txt2 <> "                                                                \n"
       where
-        txt0 = build k
+        txt0 = build lazyText0
         txt1 = build expr0
         txt2 = build expr1
 
@@ -3073,12 +3458,12 @@
     , typeMessage :: TypeMessage s a
     } deriving (Typeable)
 
-instance (Buildable a, Buildable s) => Show (TypeError s a) where
+instance (Buildable a, Buildable s, Eq a, Pretty a) => Show (TypeError s a) where
     show = Text.unpack . Builder.toLazyText . build
 
-instance (Buildable a, Buildable s, Typeable a, Typeable s) => Exception (TypeError s a)
+instance (Buildable a, Buildable s, Eq a, Pretty a, Typeable a, Typeable s) => Exception (TypeError s a)
 
-instance (Buildable a, Buildable s) => Buildable (TypeError s a) where
+instance (Buildable a, Buildable s, Eq a, Pretty a) => Buildable (TypeError s a) where
     build (TypeError ctx expr msg)
         =   "\n"
         <>  (   if  Text.null (Builder.toLazyText (buildContext ctx))
@@ -3107,12 +3492,12 @@
 newtype DetailedTypeError s a = DetailedTypeError (TypeError s a)
     deriving (Typeable)
 
-instance (Buildable a, Buildable s) => Show (DetailedTypeError s a) where
+instance (Buildable a, Buildable s, Eq a, Pretty a) => Show (DetailedTypeError s a) where
     show = Text.unpack . Builder.toLazyText . build
 
-instance (Buildable a, Buildable s, Typeable a, Typeable s) => Exception (DetailedTypeError s a)
+instance (Buildable a, Buildable s, Eq a, Pretty a, Typeable a, Typeable s) => Exception (DetailedTypeError s a)
 
-instance (Buildable a, Buildable s) => Buildable (DetailedTypeError s a) where
+instance (Buildable a, Buildable s, Eq a, Pretty a) => Buildable (DetailedTypeError s a) where
     build (DetailedTypeError (TypeError ctx expr msg))
         =   "\n"
         <>  (   if  Text.null (Builder.toLazyText (buildContext ctx))
diff --git a/tests/Normalization.hs b/tests/Normalization.hs
--- a/tests/Normalization.hs
+++ b/tests/Normalization.hs
@@ -24,7 +24,8 @@
 normalizationTests :: TestTree
 normalizationTests =
     testGroup "normalization"
-        [ examples
+        [ tutorialExamples
+        , preludeExamples
         , simplifications
         , constantFolding
         , conversions
@@ -33,8 +34,15 @@
         , shouldNormalize "a remote-systems.conf builder" "remoteSystems"
         ]
 
-examples :: TestTree
-examples =
+tutorialExamples :: TestTree
+tutorialExamples =
+    testGroup "Tutorial examples"
+        [ shouldNormalize "⩓" "./tutorial/combineTypes/0"
+        , shouldNormalize "projection" "./tutorial/projection/0"
+        ]
+
+preludeExamples :: TestTree
+preludeExamples =
     testGroup "Prelude examples"
         [ shouldNormalize "Bool/and" "./examples/Bool/and/0"
         , shouldNormalize "Bool/and" "./examples/Bool/and/1"
diff --git a/tests/Parser.hs b/tests/Parser.hs
--- a/tests/Parser.hs
+++ b/tests/Parser.hs
@@ -130,6 +130,9 @@
             , shouldParse
                 "names that begin with reserved identifiers"
                 "./tests/parser/reservedPrefix.dhall"
+            , shouldParse
+                "interpolated expressions with leading whitespace"
+                "./tests/parser/template.dhall"
             ]
         ]
 
diff --git a/tests/normalization/tutorial/combineTypes/0A.dhall b/tests/normalization/tutorial/combineTypes/0A.dhall
new file mode 100644
--- /dev/null
+++ b/tests/normalization/tutorial/combineTypes/0A.dhall
@@ -0,0 +1,1 @@
+{ foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }
diff --git a/tests/normalization/tutorial/combineTypes/0B.dhall b/tests/normalization/tutorial/combineTypes/0B.dhall
new file mode 100644
--- /dev/null
+++ b/tests/normalization/tutorial/combineTypes/0B.dhall
@@ -0,0 +1,1 @@
+{ foo : { bar : Text, baz : Bool }, qux : Integer }
diff --git a/tests/normalization/tutorial/projection/0A.dhall b/tests/normalization/tutorial/projection/0A.dhall
new file mode 100644
--- /dev/null
+++ b/tests/normalization/tutorial/projection/0A.dhall
@@ -0,0 +1,1 @@
+{ x = 1, y = True, z = "ABC" }.{ x, y }
diff --git a/tests/normalization/tutorial/projection/0B.dhall b/tests/normalization/tutorial/projection/0B.dhall
new file mode 100644
--- /dev/null
+++ b/tests/normalization/tutorial/projection/0B.dhall
@@ -0,0 +1,1 @@
+{ x = 1, y = True }
diff --git a/tests/parser/template.dhall b/tests/parser/template.dhall
new file mode 100644
--- /dev/null
+++ b/tests/parser/template.dhall
@@ -0,0 +1,13 @@
+    \(record : { name        : Text
+               , value       : Double
+               , taxed_value : Double
+               , in_ca       : Bool
+               }
+     ) ->  ''
+Hello ${record.name}
+You have just won ${Double/show record.value} dollars!
+${ if record.in_ca
+   then "Well, ${Double/show record.taxed_value} dollars, after taxes"
+   else ""
+ }
+''
diff --git a/tests/typecheck/fieldsAreTypesA.dhall b/tests/typecheck/fieldsAreTypesA.dhall
--- a/tests/typecheck/fieldsAreTypesA.dhall
+++ b/tests/typecheck/fieldsAreTypesA.dhall
@@ -1,1 +1,1 @@
-{ x = Bool, y = List }
+{ x = Bool, y = Text }
diff --git a/tests/typecheck/fieldsAreTypesB.dhall b/tests/typecheck/fieldsAreTypesB.dhall
--- a/tests/typecheck/fieldsAreTypesB.dhall
+++ b/tests/typecheck/fieldsAreTypesB.dhall
@@ -1,1 +1,1 @@
-{ x : Type, y : Type → Type }
+{ x : Type, y : Type }