diff --git a/dhall/dhall.cabal b/dhall/dhall.cabal
index 952d31726..cc7337743 100644
--- a/dhall/dhall.cabal
+++ b/dhall/dhall.cabal
@@ -616,7 +616,10 @@ Library
         Dhall.Normalize
         Dhall.Parser.Combinators
         Dhall.Pretty.Internal
+        Dhall.Shift
         Dhall.Syntax
+        Dhall.Syntax.Import
+        Dhall.Syntax.Optics
         Dhall.URL
         Paths_dhall
     Autogen-Modules:
diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs
index 3a4711cec..7581fb751 100644
--- a/dhall/src/Dhall/Binary.hs
+++ b/dhall/src/Dhall/Binary.hs
@@ -32,21 +32,23 @@ import Dhall.Syntax
     , Chunks (..)
     , Const (..)
     , DhallDouble (..)
-    , Directory (..)
     , Expr (..)
+    , FunctionBinding (..)
+    , MultiLet (..)
+    , PreferAnnotation (..)
+    , RecordField (..)
+    , Var (..)
+    )
+import Dhall.Syntax.Import
+    ( Directory (..)
     , File (..)
     , FilePrefix (..)
-    , FunctionBinding (..)
     , Import (..)
     , ImportHashed (..)
     , ImportMode (..)
     , ImportType (..)
-    , MultiLet (..)
-    , PreferAnnotation (..)
-    , RecordField (..)
     , Scheme (..)
     , URL (..)
-    , Var (..)
     )
 
 import Data.Foldable (toList)
diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs
index 744cad134..6119516ac 100644
--- a/dhall/src/Dhall/Core.hs
+++ b/dhall/src/Dhall/Core.hs
@@ -1,5 +1,7 @@
-{-# LANGUAGE RankNTypes      #-}
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE OverloadedLists   #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE RecordWildCards   #-}
 
 {-| This module contains the core calculus for the Dhall language.
 
@@ -76,16 +78,19 @@ module Dhall.Core (
     , Eval.textShow
     , censorExpression
     , censorText
-    , Syntax.desugarWith
+    , desugarWith
     ) where
 
 import Control.Exception      (Exception)
 import Control.Monad.IO.Class (MonadIO (..))
+import Data.List.NonEmpty     (NonEmpty (..))
 import Data.Text              (Text)
 import Dhall.Normalize
 import Dhall.Pretty.Internal
 import Dhall.Src              (Src (..))
 import Dhall.Syntax
+import Dhall.Syntax.Import
+import Dhall.Syntax.Optics
 import Instances.TH.Lift      ()
 import Lens.Family            (over)
 import Prettyprinter          (Pretty)
@@ -93,7 +98,7 @@ import Prettyprinter          (Pretty)
 import qualified Control.Exception
 import qualified Data.Text
 import qualified Dhall.Eval        as Eval
-import qualified Dhall.Syntax      as Syntax
+import qualified Dhall.Optics      as Optics
 
 -- | Pretty-print a value
 pretty :: Pretty a => a -> Text
@@ -145,6 +150,30 @@ throws (Left  e) = liftIO (Control.Exception.throwIO e)
 throws (Right r) = return r
 {-# INLINABLE throws #-}
 
+-- | Desugar all @with@ expressions
+desugarWith :: Expr s a -> Expr s a
+desugarWith = Optics.rewriteOf subExpressions rewrite
+  where
+    rewrite e@(With record (key :| []) value) =
+        Just
+            (Prefer
+                mempty
+                (PreferFromWith e)
+                record
+                (RecordLit [ (key, makeRecordField value) ])
+            )
+    rewrite e@(With record (key0 :| key1 : keys) value) =
+        Just
+            (Let
+                (makeBinding "_" record)
+                (Prefer mempty (PreferFromWith e) "_"
+                    (RecordLit
+                        [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ]
+                    )
+                )
+            )
+    rewrite _ = Nothing
+
 {- $setup
 >>> import qualified Codec.Serialise
 >>> import qualified Dhall.Binary
diff --git a/dhall/src/Dhall/Freeze.hs b/dhall/src/Dhall/Freeze.hs
index b6546d029..176a7192e 100644
--- a/dhall/src/Dhall/Freeze.hs
+++ b/dhall/src/Dhall/Freeze.hs
@@ -24,13 +24,13 @@ module Dhall.Freeze
 import Data.Foldable       (for_)
 import Data.List.NonEmpty  (NonEmpty)
 import Data.Maybe          (fromMaybe)
-import Dhall.Pretty        (CharacterSet, detectCharacterSet)
-import Dhall.Syntax
+import Dhall.Core
     ( Expr (..)
     , Import (..)
     , ImportHashed (..)
     , ImportType (..)
     )
+import Dhall.Pretty        (CharacterSet, detectCharacterSet)
 import Dhall.Util
     ( Censor
     , CheckFailed (..)
diff --git a/dhall/src/Dhall/Import.hs b/dhall/src/Dhall/Import.hs
index 47c8d18df..38a869498 100644
--- a/dhall/src/Dhall/Import.hs
+++ b/dhall/src/Dhall/Import.hs
@@ -172,9 +172,8 @@ import Data.Maybe                 (fromMaybe)
 import Data.Text                  (Text)
 import Data.Typeable              (Typeable)
 import Data.Void                  (Void, absurd)
-import Dhall.TypeCheck            (TypeError)
 
-import Dhall.Syntax
+import Dhall.Core
     ( Chunks (..)
     , Directory (..)
     , Expr (..)
@@ -190,6 +189,7 @@ import Dhall.Syntax
     , recordFieldExprs
     )
 
+import Dhall.TypeCheck            (TypeError)
 import System.FilePath ((</>))
 import Text.Megaparsec (SourcePos (SourcePos), mkPos)
 
@@ -244,7 +244,7 @@ import qualified Text.Parser.Token
 
 {- $setup
 
-    >>> import Dhall.Syntax
+    >>> import Dhall.Syntax.Import
 -}
 
 -- | An import failed because of a cycle in the import graph
diff --git a/dhall/src/Dhall/Lint.hs b/dhall/src/Dhall/Lint.hs
index 52666b7d8..c1e2f09c1 100644
--- a/dhall/src/Dhall/Lint.hs
+++ b/dhall/src/Dhall/Lint.hs
@@ -21,7 +21,7 @@ module Dhall.Lint
 import Control.Applicative ((<|>))
 import Data.List.NonEmpty  (NonEmpty (..))
 
-import Dhall.Syntax
+import Dhall.Core
     ( Binding (..)
     , Chunks (..)
     , Directory (..)
diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs
index 0f0ce6179..3193d0940 100644
--- a/dhall/src/Dhall/Normalize.hs
+++ b/dhall/src/Dhall/Normalize.hs
@@ -14,7 +14,7 @@ module Dhall.Normalize (
     , ReifiedNormalizer (..)
     , judgmentallyEqual
     , subst
-    , Syntax.shift
+    , shift
     , isNormalized
     , isNormalizedWith
     , freeIn
@@ -26,6 +26,7 @@ import Data.Functor.Identity (Identity (..))
 import Data.List.NonEmpty    (NonEmpty (..))
 import Data.Sequence         (ViewL (..), ViewR (..))
 import Data.Traversable
+import Dhall.Shift           (shift)
 import Instances.TH.Lift     ()
 import Prelude               hiding (succ)
 
@@ -43,11 +44,12 @@ import Dhall.Syntax
 
 import qualified Data.Sequence
 import qualified Data.Set
-import qualified Data.Text     as Text
-import qualified Dhall.Eval    as Eval
+import qualified Data.Text           as Text
+import qualified Dhall.Eval          as Eval
 import qualified Dhall.Map
-import qualified Dhall.Syntax  as Syntax
-import qualified Lens.Family   as Lens
+import qualified Dhall.Syntax        as Syntax
+import qualified Dhall.Syntax.Optics as Syntax.Optics
+import qualified Lens.Family         as Lens
 
 {-| Returns `True` if two expressions are α-equivalent and β-equivalent and
     `False` otherwise
@@ -69,24 +71,24 @@ subst (V x n) e (Lam cs (FunctionBinding src0 y src1 src2 _A) b) =
     Lam cs (FunctionBinding src0 y src1 src2 _A') b'
   where
     _A' = subst (V x n )                         e  _A
-    b'  = subst (V x n') (Syntax.shift 1 (V y 0) e)  b
+    b'  = subst (V x n') (shift 1 (V y 0) e)  b
     n'  = if x == y then n + 1 else n
 subst (V x n) e (Pi cs y _A _B) = Pi cs y _A' _B'
   where
     _A' = subst (V x n )                         e  _A
-    _B' = subst (V x n') (Syntax.shift 1 (V y 0) e) _B
+    _B' = subst (V x n') (shift 1 (V y 0) e) _B
     n'  = if x == y then n + 1 else n
 subst v e (Var v') = if v == v' then e else Var v'
 subst (V x n) e (Let (Binding src0 f src1 mt src2 r) b) =
     Let (Binding src0 f src1 mt' src2 r') b'
   where
-    b' = subst (V x n') (Syntax.shift 1 (V f 0) e) b
+    b' = subst (V x n') (shift 1 (V f 0) e) b
       where
         n' = if x == f then n + 1 else n
 
     mt' = fmap (fmap (subst (V x n) e)) mt
     r'  =             subst (V x n) e  r
-subst x e expression = Lens.over Syntax.subExpressions (subst x e) expression
+subst x e expression = Lens.over Syntax.Optics.subExpressions (subst x e) expression
 
 {-| This function is used to determine whether folds like @Natural/fold@ or
     @List/fold@ should be lazy or strict in their accumulator based on the type
@@ -194,9 +196,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
               case f' of
                 Lam _ (FunctionBinding _ x _ _ _A) b₀ -> do
 
-                    let a₂ = Syntax.shift 1 (V x 0) a'
+                    let a₂ = shift 1 (V x 0) a'
                     let b₁ = subst (V x 0) a₂ b₀
-                    let b₂ = Syntax.shift (-1) (V x 0) b₁
+                    let b₂ = shift (-1) (V x 0) b₁
 
                     loop b₂
                 _ ->
@@ -256,7 +258,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                         pure (TextLit (Chunks [] (Text.pack (show n))))
                     App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)
                       where
-                        _A₁ = Syntax.shift 1 "a" _A₀
+                        _A₁ = shift 1 "a" _A₀
 
                         list = App List _A₀
 
@@ -383,9 +385,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                             Just app' -> loop app'
     Let (Binding _ f _ _ _ r) b -> loop b''
       where
-        r'  = Syntax.shift   1  (V f 0) r
+        r'  = shift   1  (V f 0) r
         b'  = subst (V f 0) r' b
-        b'' = Syntax.shift (-1) (V f 0) b'
+        b'' = shift (-1) (V f 0) b'
     Annot x _ -> loop x
     Bool -> pure Bool
     BoolLit b -> pure (BoolLit b)
@@ -631,7 +633,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
             RecordLit kvs ->
                 case Dhall.Map.lookup x kvs of
                     Just v  -> pure $ recordFieldValue v
-                    Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure k
+                    Nothing -> Field <$> (RecordLit <$> traverse (Syntax.Optics.recordFieldExprs loop) kvs) <*> pure k
             Project r_ _ -> loop (Field r_ k)
             Prefer cs _ (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
                 Just v -> pure (Field (Prefer cs PreferFromSource (singletonRecordLit v) r_) k)
diff --git a/dhall/src/Dhall/Parser.hs b/dhall/src/Dhall/Parser.hs
index cdff713d4..35e47d701 100644
--- a/dhall/src/Dhall/Parser.hs
+++ b/dhall/src/Dhall/Parser.hs
@@ -25,11 +25,10 @@ import Control.Exception (Exception)
 import Data.Text         (Text)
 import Data.Void         (Void)
 import Dhall.Src         (Src (..))
-import Dhall.Syntax
 import Text.Megaparsec   (ParseErrorBundle (..), PosState (..))
 
 import qualified Data.Text       as Text
-import qualified Dhall.Core      as Core
+import           Dhall.Core      as Core
 import qualified Text.Megaparsec
 
 import Dhall.Parser.Combinators
diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs
index e49d89143..818483a66 100644
--- a/dhall/src/Dhall/Parser/Expression.hs
+++ b/dhall/src/Dhall/Parser/Expression.hs
@@ -14,6 +14,7 @@ import Data.List.NonEmpty      (NonEmpty (..))
 import Data.Text               (Text)
 import Dhall.Src               (Src (..))
 import Dhall.Syntax
+import Dhall.Syntax.Import
 import Text.Parser.Combinators (choice, try, (<?>))
 
 import qualified Control.Monad
diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs
index a070faa6a..297af175f 100644
--- a/dhall/src/Dhall/Parser/Token.hs
+++ b/dhall/src/Dhall/Parser/Token.hs
@@ -132,6 +132,7 @@ import Data.Functor            (void, ($>))
 import Data.Ratio              ((%))
 import Data.Text               (Text)
 import Dhall.Syntax
+import Dhall.Syntax.Import
 import Text.Parser.Combinators (choice, try, (<?>))
 
 import qualified Control.Monad              as Monad
@@ -671,7 +672,7 @@ pathComponent componentType = do
     let pathData =
             case componentType of
                 FileComponent ->
-                    Text.Megaparsec.takeWhile1P Nothing Dhall.Syntax.pathCharacter
+                    Text.Megaparsec.takeWhile1P Nothing Dhall.Syntax.Import.pathCharacter
                 URLComponent ->
                     star pchar
 
diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs
index 6dd66aa22..45a0aa9b8 100644
--- a/dhall/src/Dhall/Pretty/Internal.hs
+++ b/dhall/src/Dhall/Pretty/Internal.hs
@@ -96,6 +96,7 @@ import qualified Data.Maybe
 import qualified Data.Text                     as Text
 import qualified Data.Time                     as Time
 import qualified Dhall.Map                     as Map
+import qualified Dhall.Syntax.Optics           as Syntax.Optics
 import qualified Prettyprinter                 as Pretty
 import qualified Prettyprinter.Render.String   as Pretty
 import qualified Prettyprinter.Render.Terminal as Terminal
@@ -148,7 +149,7 @@ instance FromJSON CharacterSet where
 -- If any parts of the expression uses the Unicode syntax, the whole expression
 -- is deemed to be using the Unicode syntax.
 detectCharacterSet :: Expr Src a -> CharacterSet
-detectCharacterSet = foldOf (cosmosOf subExpressions . to exprToCharacterSet)
+detectCharacterSet = foldOf (cosmosOf Syntax.Optics.subExpressions . to exprToCharacterSet)
   where
     exprToCharacterSet = \case
         Embed _ -> mempty -- Don't go down the embed route, otherwise: <<loop>>
diff --git a/dhall/src/Dhall/Schemas.hs b/dhall/src/Dhall/Schemas.hs
index 9ae8faca8..eff15dfd0 100644
--- a/dhall/src/Dhall/Schemas.hs
+++ b/dhall/src/Dhall/Schemas.hs
@@ -20,11 +20,11 @@ import Control.Exception   (Exception)
 import Data.Maybe          (fromMaybe)
 import Data.Text           (Text)
 import Data.Void           (Void)
+import Dhall.Core          (Expr (..), Import, Var (..))
 import Dhall.Crypto        (SHA256Digest)
 import Dhall.Map           (Map)
 import Dhall.Pretty        (CharacterSet (..), detectCharacterSet)
 import Dhall.Src           (Src)
-import Dhall.Syntax        (Expr (..), Import, Var (..))
 import Dhall.Util
     ( Censor (..)
     , Header (..)
@@ -46,7 +46,6 @@ import qualified Dhall.Optics                       as Optics
 import qualified Dhall.Parser                       as Parser
 import qualified Dhall.Pretty
 import qualified Dhall.Substitution                 as Substitution
-import qualified Dhall.Syntax                       as Syntax
 import qualified Dhall.TypeCheck                    as TypeCheck
 import qualified Dhall.Util                         as Util
 import qualified Prettyprinter                      as Pretty
@@ -136,7 +135,7 @@ decodeSchemas (RecordLit keyValues) = do
     let typeMetadata = Data.Map.fromList $ do
             (name, (_Type, _default)) <- Map.toList m
 
-            return (Import.hashExpression (Syntax.denote _Type), (name, _default))
+            return (Import.hashExpression (Core.denote _Type), (name, _default))
 
     return typeMetadata
 decodeSchemas  _ =
@@ -174,7 +173,7 @@ rewriteWithSchemas _schemas expression = do
                     Left _ ->
                         empty
                     Right subExpressionType ->
-                        return (Import.hashExpression (Syntax.denote subExpressionType))
+                        return (Import.hashExpression (Core.denote subExpressionType))
 
                 (name, _default) <- Data.Map.lookup hash typeMetadata
 
@@ -196,10 +195,10 @@ rewriteWithSchemas _schemas expression = do
 
     let rewrittenExpression :: Expr Src Import
         rewrittenExpression =
-            fmap Void.absurd (Optics.transformOf Syntax.subExpressions schemasRewrite normalizedExpression)
+            fmap Void.absurd (Optics.transformOf Core.subExpressions schemasRewrite normalizedExpression)
 
     if Normalize.freeIn (V "schemas" 0) rewrittenExpression
-        then return (Let (Syntax.makeBinding "schemas" _schemas) rewrittenExpression)
+        then return (Let (Core.makeBinding "schemas" _schemas) rewrittenExpression)
         else return expression
 
 -- | Errors that can be thrown by `rewriteWithSchemas`
diff --git a/dhall/src/Dhall/Shift.hs b/dhall/src/Dhall/Shift.hs
new file mode 100644
index 000000000..82b81dde5
--- /dev/null
+++ b/dhall/src/Dhall/Shift.hs
@@ -0,0 +1,104 @@
+{-| This module provides the 'shift' function used in normalization and
+    type-checking.
+-}
+
+module Dhall.Shift (shift) where
+
+import Dhall.Syntax
+    ( Binding (..)
+    , Expr (..)
+    , FunctionBinding (..)
+    , Var (..)
+    )
+import Dhall.Syntax.Optics (subExpressions)
+
+import qualified Lens.Family as Lens
+
+{-| `shift` is used by both normalization and type-checking to avoid variable
+    capture by shifting variable indices
+
+    For example, suppose that you were to normalize the following expression:
+
+> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
+
+    If you were to substitute @y@ with @x@ without shifting any variable
+    indices, then you would get the following incorrect result:
+
+> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
+
+    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
+    order to avoid being misinterpreted as the @x@ bound by the innermost
+    lambda.  If we perform that `shift` then we get the correct result:
+
+> λ(a : Type) → λ(x : a) → λ(x : a) → x@1
+
+    As a more worked example, suppose that you were to normalize the following
+    expression:
+
+>     λ(a : Type)
+> →   λ(f : a → a → a)
+> →   λ(x : a)
+> →   λ(x : a)
+> →   (λ(x : a) → f x x@1) x@1
+
+    The correct normalized result would be:
+
+>     λ(a : Type)
+> →   λ(f : a → a → a)
+> →   λ(x : a)
+> →   λ(x : a)
+> →   f x@1 x
+
+    The above example illustrates how we need to both increase and decrease
+    variable indices as part of substitution:
+
+    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
+      substitute it into the body of the innermost lambda expression in order
+      to avoid variable capture.  This substitution changes the body of the
+      lambda expression to @(f x\@2 x\@1)@
+
+    * We then remove the innermost lambda and therefore decrease the indices of
+      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
+      less @x@ variable is now bound within that scope
+
+    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
+    the indices of all variables named @x@ whose indices are greater than
+    @(n + m)@, where @m@ is the number of bound variables of the same name
+    within that scope
+
+    In practice, @d@ is always @1@ or @-1@ because we either:
+
+    * increment variables by @1@ to avoid variable capture during substitution
+    * decrement variables by @1@ when deleting lambdas after substitution
+
+    @n@ starts off at @0@ when substitution begins and increments every time we
+    descend into a lambda or let expression that binds a variable of the same
+    name in order to avoid shifting the bound variables by mistake.
+-}
+shift :: Int -> Var -> Expr s a -> Expr s a
+shift d (V x n) (Var (V x' n')) = Var (V x' n'')
+  where
+    n'' = if x == x' && n <= n' then n' + d else n'
+shift d (V x n) (Lam cs (FunctionBinding src0 x' src1 src2 _A) b) =
+    Lam cs (FunctionBinding src0 x' src1 src2 _A') b'
+  where
+    _A' = shift d (V x n ) _A
+    b'  = shift d (V x n') b
+      where
+        n' = if x == x' then n + 1 else n
+shift d (V x n) (Pi cs x' _A _B) = Pi cs x' _A' _B'
+  where
+    _A' = shift d (V x n ) _A
+    _B' = shift d (V x n') _B
+      where
+        n' = if x == x' then n + 1 else n
+shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
+    Let (Binding src0 f src1 mt' src2 r') e'
+  where
+    e' = shift d (V x n') e
+      where
+        n' = if x == f then n + 1 else n
+
+    mt' = fmap (fmap (shift d (V x n))) mt
+    r'  =             shift d (V x n)  r
+shift d v expression = Lens.over subExpressions (shift d v) expression
diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs
index 7c3646b4b..df580bead 100644
--- a/dhall/src/Dhall/Syntax.hs
+++ b/dhall/src/Dhall/Syntax.hs
@@ -17,6 +17,8 @@
 
 {-| This module contains the core syntax types and optics for them.
 
+The import types are excluded and can be found in "Dhall.Syntax.Import".
+
 'reservedIdentifiers', 'denote' and friends are included because they are
 involved in a dependency circle with "Dhall.Pretty.Internal".
 -}
@@ -45,49 +47,26 @@ module Dhall.Syntax (
     , wrapInLets
 
     -- ** Optics
-    , subExpressions
-    , subExpressionsWith
     , unsafeSubExpressions
     , chunkExprs
-    , bindingExprs
-    , recordFieldExprs
-    , functionBindingExprs
 
     -- ** Handling 'Note's
     , denote
     , renote
     , shallowDenote
 
-    -- * 'Import'
-    , Directory(..)
-    , File(..)
-    , FilePrefix(..)
-    , Import(..)
-    , ImportHashed(..)
-    , ImportMode(..)
-    , ImportType(..)
-    , URL(..)
-    , Scheme(..)
-    , pathCharacter
-
     -- * Reserved identifiers
     , reservedIdentifiers
     , reservedKeywords
 
-    -- * `Data.Text.Text` manipulation
+    -- * `Chunks` manipulation
     , toDoubleQuoted
     , longestSharedWhitespacePrefix
     , linesLiteral
     , unlinesLiteral
 
-    -- * Desugaring
-    , desugarWith
-
     -- * Utilities
     , internalError
-    -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a
-    -- module cycle
-    , shift
     ) where
 
 import                Control.DeepSeq            (NFData)
@@ -104,12 +83,17 @@ import                Data.Traversable           ()
 import                Data.Void                  (Void)
 import                Dhall.Map                  (Map)
 import {-# SOURCE #-} Dhall.Pretty.Internal
+    ( CharacterSet (..)
+    , prettyConst
+    , prettyExpr
+    , prettyVar
+    )
 import                Dhall.Src                  (Src (..))
 import                GHC.Generics               (Generic)
 import                Instances.TH.Lift          ()
 import                Language.Haskell.TH.Syntax (Lift)
 import                Numeric.Natural            (Natural)
-import                Prettyprinter              (Doc, Pretty)
+import                Prettyprinter              (Pretty)
 import                Unsafe.Coerce              (unsafeCoerce)
 
 import qualified Control.Monad
@@ -118,10 +102,7 @@ import qualified Data.HashSet
 import qualified Data.List.NonEmpty as NonEmpty
 import qualified Data.Text
 import qualified Data.Time          as Time
-import qualified Dhall.Crypto
-import qualified Dhall.Optics       as Optics
 import qualified Lens.Family        as Lens
-import qualified Network.URI        as URI
 import qualified Prettyprinter      as Pretty
 
 deriving instance Lift Time.Day
@@ -131,6 +112,7 @@ deriving instance Lift (Fixed.Fixed a)
 
 -- $setup
 -- >>> import Dhall.Binary () -- For the orphan instance for `Serialise (Expr Void Import)`
+-- >>> import Dhall.Syntax.Import (Import)
 
 {-| Constants for a pure type system
 
@@ -780,27 +762,6 @@ wrapInLets bs e = foldr Let e bs
 -}
 data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a)
 
--- | A traversal over the immediate sub-expressions of an expression.
-subExpressions
-    :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
-subExpressions = subExpressionsWith (pure . Embed)
-{-# INLINABLE subExpressions #-}
-
-{-| A traversal over the immediate sub-expressions of an expression which
-    allows mapping embedded values
--}
-subExpressionsWith
-    :: Applicative f => (a -> f (Expr s b)) -> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
-subExpressionsWith h _ (Embed a) = h a
-subExpressionsWith _ f (Note a b) = Note a <$> f b
-subExpressionsWith _ f (Let a b) = Let <$> bindingExprs f a <*> f b
-subExpressionsWith _ f (Record a) = Record <$> traverse (recordFieldExprs f) a
-subExpressionsWith _ f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a
-subExpressionsWith _ f (Lam cs fb e) = Lam cs <$> functionBindingExprs f fb <*> f e
-subExpressionsWith _ f (Field a b) = Field <$> f a <*> pure b
-subExpressionsWith _ f expression = unsafeSubExpressions f expression
-{-# INLINABLE subExpressionsWith #-}
-
 {-| An internal utility used to implement transformations that require changing
     one of the type variables of the `Expr` type
 
@@ -899,54 +860,9 @@ unhandledConstructor constructor =
     internalError
         (   "Dhall.Syntax.unsafeSubExpressions: Unhandled "
         <>  constructor
-        <>  " construtor"
+        <>  " constructor"
         )
 
-{-| Traverse over the immediate 'Expr' children in a 'Binding'.
--}
-bindingExprs
-  :: (Applicative f)
-  => (Expr s a -> f (Expr s b))
-  -> Binding s a -> f (Binding s b)
-bindingExprs f (Binding s0 n s1 t s2 v) =
-  Binding
-    <$> pure s0
-    <*> pure n
-    <*> pure s1
-    <*> traverse (traverse f) t
-    <*> pure s2
-    <*> f v
-{-# INLINABLE bindingExprs #-}
-
-{-| Traverse over the immediate 'Expr' children in a 'RecordField'.
--}
-recordFieldExprs
-    :: Applicative f
-    => (Expr s a -> f (Expr s b))
-    -> RecordField s a -> f (RecordField s b)
-recordFieldExprs f (RecordField s0 e s1 s2) =
-    RecordField
-        <$> pure s0
-        <*> f e
-        <*> pure s1
-        <*> pure s2
-{-# INLINABLE recordFieldExprs #-}
-
-{-| Traverse over the immediate 'Expr' children in a 'FunctionBinding'.
--}
-functionBindingExprs
-    :: Applicative f
-    => (Expr s a -> f (Expr s b))
-    -> FunctionBinding s a -> f (FunctionBinding s b)
-functionBindingExprs f (FunctionBinding s0 label s1 s2 type_) =
-    FunctionBinding
-        <$> pure s0
-        <*> pure label
-        <*> pure s1
-        <*> pure s2
-        <*> f type_
-{-# INLINABLE functionBindingExprs #-}
-
 -- | A traversal over the immediate sub-expressions in 'Chunks'.
 chunkExprs
   :: Applicative f
@@ -956,220 +872,6 @@ chunkExprs f (Chunks chunks final) =
   flip Chunks final <$> traverse (traverse f) chunks
 {-# INLINABLE chunkExprs #-}
 
-{-| Internal representation of a directory that stores the path components in
-    reverse order
-
-    In other words, the directory @\/foo\/bar\/baz@ is encoded as
-    @Directory { components = [ "baz", "bar", "foo" ] }@
--}
-newtype Directory = Directory { components :: [Text] }
-    deriving stock (Eq, Generic, Ord, Show)
-    deriving anyclass NFData
-
-instance Semigroup Directory where
-    Directory components₀ <> Directory components₁ =
-        Directory (components₁ <> components₀)
-
-instance Pretty Directory where
-    pretty (Directory {..}) = foldMap prettyPathComponent (reverse components)
-
-prettyPathComponent :: Text -> Doc ann
-prettyPathComponent text
-    | Data.Text.all pathCharacter text =
-        "/" <> Pretty.pretty text
-    | otherwise =
-        "/\"" <> Pretty.pretty text <> "\""
-
-{-| A `File` is a `directory` followed by one additional path component
-    representing the `file` name
--}
-data File = File
-    { directory :: Directory
-    , file      :: Text
-    } deriving (Eq, Generic, Ord, Show, NFData)
-
-instance Pretty File where
-    pretty (File {..}) =
-            Pretty.pretty directory
-        <>  prettyPathComponent file
-
-instance Semigroup File where
-    File directory₀ _ <> File directory₁ file =
-        File (directory₀ <> directory₁) file
-
--- | The beginning of a file path which anchors subsequent path components
-data FilePrefix
-    = Absolute
-    -- ^ Absolute path
-    | Here
-    -- ^ Path relative to @.@
-    | Parent
-    -- ^ Path relative to @..@
-    | Home
-    -- ^ Path relative to @~@
-    deriving (Eq, Generic, Ord, Show, NFData)
-
-instance Pretty FilePrefix where
-    pretty Absolute = ""
-    pretty Here     = "."
-    pretty Parent   = ".."
-    pretty Home     = "~"
-
--- | The URI scheme
-data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)
-
--- | This type stores all of the components of a remote import
-data URL = URL
-    { scheme    :: Scheme
-    , authority :: Text
-    , path      :: File
-    , query     :: Maybe Text
-    , headers   :: Maybe (Expr Src Import)
-    } deriving (Eq, Generic, Ord, Show, NFData)
-
-instance Pretty URL where
-    pretty (URL {..}) =
-            schemeDoc
-        <>  "://"
-        <>  Pretty.pretty authority
-        <>  pathDoc
-        <>  queryDoc
-        <>  foldMap prettyHeaders headers
-      where
-        prettyHeaders h =
-          " using (" <> Pretty.unAnnotate (Pretty.pretty h) <> ")"
-
-        File {..} = path
-
-        Directory {..} = directory
-
-        pathDoc =
-                foldMap prettyURIComponent (reverse components)
-            <>  prettyURIComponent file
-
-        schemeDoc = case scheme of
-            HTTP  -> "http"
-            HTTPS -> "https"
-
-        queryDoc = case query of
-            Nothing -> ""
-            Just q  -> "?" <> Pretty.pretty q
-
-prettyURIComponent :: Text -> Doc ann
-prettyURIComponent text =
-        Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text
-
--- | The type of import (i.e. local vs. remote vs. environment)
-data ImportType
-    = Local FilePrefix File
-    -- ^ Local path
-    | Remote URL
-    -- ^ URL of remote resource and optional headers stored in an import
-    | Env  Text
-    -- ^ Environment variable
-    | Missing
-    deriving (Eq, Generic, Ord, Show, NFData)
-
-parent :: File
-parent = File { directory = Directory { components = [ ".." ] }, file = "" }
-
-instance Semigroup ImportType where
-    Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁)
-
-    Remote (URL { path = path₀, ..}) <> Local Here path₁ =
-        Remote (URL { path = path₀ <> path₁, ..})
-
-    Local prefix file₀ <> Local Parent file₁ =
-        Local prefix (file₀ <> parent <> file₁)
-
-    Remote (URL { path = path₀, .. }) <> Local Parent path₁ =
-        Remote (URL { path = path₀ <> parent <> path₁, .. })
-
-    import₀ <> Remote (URL { headers = headers₀, .. }) =
-        Remote (URL { headers = headers₁, .. })
-      where
-        importHashed₀ = Import (ImportHashed Nothing import₀) Code
-
-        headers₁ = fmap (fmap (importHashed₀ <>)) headers₀
-
-    _ <> import₁ =
-        import₁
-
-instance Pretty ImportType where
-    pretty (Local prefix file) =
-        Pretty.pretty prefix <> Pretty.pretty file
-
-    pretty (Remote url) = Pretty.pretty url
-
-    pretty (Env env) = "env:" <> prettyEnvironmentVariable env
-
-    pretty Missing = "missing"
-
--- | How to interpret the import's contents (i.e. as Dhall code or raw text)
-data ImportMode = Code | RawText | Location
-  deriving (Eq, Generic, Ord, Show, NFData)
-
--- | A `ImportType` extended with an optional hash for semantic integrity checks
-data ImportHashed = ImportHashed
-    { hash       :: Maybe Dhall.Crypto.SHA256Digest
-    , importType :: ImportType
-    } deriving (Eq, Generic, Ord, Show, NFData)
-
-instance Semigroup ImportHashed where
-    ImportHashed _ importType₀ <> ImportHashed hash importType₁ =
-        ImportHashed hash (importType₀ <> importType₁)
-
-instance Pretty ImportHashed where
-    pretty (ImportHashed  Nothing p) =
-      Pretty.pretty p
-    pretty (ImportHashed (Just h) p) =
-      Pretty.group (Pretty.flatAlt long short)
-      where
-        long =
-            Pretty.align
-                (   Pretty.pretty p <> Pretty.hardline
-                <>  "  sha256:" <> Pretty.pretty (show h)
-                )
-
-        short = Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h)
-
--- | Reference to an external resource
-data Import = Import
-    { importHashed :: ImportHashed
-    , importMode   :: ImportMode
-    } deriving (Eq, Generic, Ord, Show, NFData)
-
-instance Semigroup Import where
-    Import importHashed₀ _ <> Import importHashed₁ code =
-        Import (importHashed₀ <> importHashed₁) code
-
-instance Pretty Import where
-    pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix
-      where
-        suffix :: Text
-        suffix = case importMode of
-            RawText  -> " as Text"
-            Location -> " as Location"
-            Code     -> ""
-
-{-| Returns `True` if the given `Char` is valid within an unquoted path
-    component
-
-    This is exported for reuse within the @"Dhall.Parser.Token"@ module
--}
-pathCharacter :: Char -> Bool
-pathCharacter c =
-         '\x21' == c
-    ||  ('\x24' <= c && c <= '\x27')
-    ||  ('\x2A' <= c && c <= '\x2B')
-    ||  ('\x2D' <= c && c <= '\x2E')
-    ||  ('\x30' <= c && c <= '\x3B')
-    ||  c == '\x3D'
-    ||  ('\x40' <= c && c <= '\x5A')
-    ||  ('\x5E' <= c && c <= '\x7A')
-    ||  c == '\x7C'
-    ||  c == '\x7E'
-
 -- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)
 --
 -- This also remove CharacterSet annotations.
@@ -1373,119 +1075,6 @@ toDoubleQuoted literal =
 
     indent = Data.Text.length longestSharedPrefix
 
-{-| `shift` is used by both normalization and type-checking to avoid variable
-    capture by shifting variable indices
-
-    For example, suppose that you were to normalize the following expression:
-
-> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
-
-    If you were to substitute @y@ with @x@ without shifting any variable
-    indices, then you would get the following incorrect result:
-
-> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
-
-    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
-    order to avoid being misinterpreted as the @x@ bound by the innermost
-    lambda.  If we perform that `shift` then we get the correct result:
-
-> λ(a : Type) → λ(x : a) → λ(x : a) → x@1
-
-    As a more worked example, suppose that you were to normalize the following
-    expression:
-
->     λ(a : Type)
-> →   λ(f : a → a → a)
-> →   λ(x : a)
-> →   λ(x : a)
-> →   (λ(x : a) → f x x@1) x@1
-
-    The correct normalized result would be:
-
->     λ(a : Type)
-> →   λ(f : a → a → a)
-> →   λ(x : a)
-> →   λ(x : a)
-> →   f x@1 x
-
-    The above example illustrates how we need to both increase and decrease
-    variable indices as part of substitution:
-
-    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
-      substitute it into the body of the innermost lambda expression in order
-      to avoid variable capture.  This substitution changes the body of the
-      lambda expression to @(f x\@2 x\@1)@
-
-    * We then remove the innermost lambda and therefore decrease the indices of
-      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
-      less @x@ variable is now bound within that scope
-
-    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
-    the indices of all variables named @x@ whose indices are greater than
-    @(n + m)@, where @m@ is the number of bound variables of the same name
-    within that scope
-
-    In practice, @d@ is always @1@ or @-1@ because we either:
-
-    * increment variables by @1@ to avoid variable capture during substitution
-    * decrement variables by @1@ when deleting lambdas after substitution
-
-    @n@ starts off at @0@ when substitution begins and increments every time we
-    descend into a lambda or let expression that binds a variable of the same
-    name in order to avoid shifting the bound variables by mistake.
--}
-shift :: Int -> Var -> Expr s a -> Expr s a
-shift d (V x n) (Var (V x' n')) = Var (V x' n'')
-  where
-    n'' = if x == x' && n <= n' then n' + d else n'
-shift d (V x n) (Lam cs (FunctionBinding src0 x' src1 src2 _A) b) =
-    Lam cs (FunctionBinding src0 x' src1 src2 _A') b'
-  where
-    _A' = shift d (V x n ) _A
-    b'  = shift d (V x n') b
-      where
-        n' = if x == x' then n + 1 else n
-shift d (V x n) (Pi cs x' _A _B) = Pi cs x' _A' _B'
-  where
-    _A' = shift d (V x n ) _A
-    _B' = shift d (V x n') _B
-      where
-        n' = if x == x' then n + 1 else n
-shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
-    Let (Binding src0 f src1 mt' src2 r') e'
-  where
-    e' = shift d (V x n') e
-      where
-        n' = if x == f then n + 1 else n
-
-    mt' = fmap (fmap (shift d (V x n))) mt
-    r'  =             shift d (V x n)  r
-shift d v expression = Lens.over subExpressions (shift d v) expression
-
--- | Desugar all @with@ expressions
-desugarWith :: Expr s a -> Expr s a
-desugarWith = Optics.rewriteOf subExpressions rewrite
-  where
-    rewrite e@(With record (key :| []) value) =
-        Just
-            (Prefer
-                mempty
-                (PreferFromWith e)
-                record
-                (RecordLit [ (key, makeRecordField value) ])
-            )
-    rewrite e@(With record (key0 :| key1 : keys) value) =
-        Just
-            (Let
-                (makeBinding "_" record)
-                (Prefer mempty (PreferFromWith e) "_"
-                    (RecordLit
-                        [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ]
-                    )
-                )
-            )
-    rewrite _ = Nothing
-
 _ERROR :: String
 _ERROR = "\ESC[1;31mError\ESC[0m"
 
diff --git a/dhall/src/Dhall/Syntax/Import.hs b/dhall/src/Dhall/Syntax/Import.hs
new file mode 100644
index 000000000..30d1e5dd7
--- /dev/null
+++ b/dhall/src/Dhall/Syntax/Import.hs
@@ -0,0 +1,248 @@
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RecordWildCards    #-}
+
+{-| This module contains the core syntax types for imports.
+-}
+
+module Dhall.Syntax.Import (
+      Directory(..)
+    , File(..)
+    , FilePrefix(..)
+    , Import(..)
+    , ImportHashed(..)
+    , ImportMode(..)
+    , ImportType(..)
+    , URL(..)
+    , Scheme(..)
+    , pathCharacter
+    ) where
+
+import Control.DeepSeq       (NFData)
+import Data.Text             (Text)
+import Dhall.Pretty.Internal (prettyEnvironmentVariable)
+import Dhall.Src             (Src (..))
+import Dhall.Syntax          (Expr)
+import GHC.Generics          (Generic)
+import Prettyprinter         (Doc, Pretty)
+
+import qualified Data.Text
+import qualified Dhall.Crypto
+import qualified Network.URI   as URI
+import qualified Prettyprinter as Pretty
+
+{-| Internal representation of a directory that stores the path components in
+    reverse order
+
+    In other words, the directory @\/foo\/bar\/baz@ is encoded as
+    @Directory { components = [ "baz", "bar", "foo" ] }@
+-}
+newtype Directory = Directory { components :: [Text] }
+    deriving stock (Eq, Generic, Ord, Show)
+    deriving anyclass NFData
+
+instance Semigroup Directory where
+    Directory components₀ <> Directory components₁ =
+        Directory (components₁ <> components₀)
+
+instance Pretty Directory where
+    pretty (Directory {..}) = foldMap prettyPathComponent (reverse components)
+
+prettyPathComponent :: Text -> Doc ann
+prettyPathComponent text
+    | Data.Text.all pathCharacter text =
+        "/" <> Pretty.pretty text
+    | otherwise =
+        "/\"" <> Pretty.pretty text <> "\""
+
+{-| A `File` is a `directory` followed by one additional path component
+    representing the `file` name
+-}
+data File = File
+    { directory :: Directory
+    , file      :: Text
+    } deriving (Eq, Generic, Ord, Show, NFData)
+
+instance Pretty File where
+    pretty (File {..}) =
+            Pretty.pretty directory
+        <>  prettyPathComponent file
+
+instance Semigroup File where
+    File directory₀ _ <> File directory₁ file =
+        File (directory₀ <> directory₁) file
+
+-- | The beginning of a file path which anchors subsequent path components
+data FilePrefix
+    = Absolute
+    -- ^ Absolute path
+    | Here
+    -- ^ Path relative to @.@
+    | Parent
+    -- ^ Path relative to @..@
+    | Home
+    -- ^ Path relative to @~@
+    deriving (Eq, Generic, Ord, Show, NFData)
+
+instance Pretty FilePrefix where
+    pretty Absolute = ""
+    pretty Here     = "."
+    pretty Parent   = ".."
+    pretty Home     = "~"
+
+-- | The URI scheme
+data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)
+
+-- | This type stores all of the components of a remote import
+data URL = URL
+    { scheme    :: Scheme
+    , authority :: Text
+    , path      :: File
+    , query     :: Maybe Text
+    , headers   :: Maybe (Expr Src Import)
+    } deriving (Eq, Generic, Ord, Show, NFData)
+
+instance Pretty URL where
+    pretty (URL {..}) =
+            schemeDoc
+        <>  "://"
+        <>  Pretty.pretty authority
+        <>  pathDoc
+        <>  queryDoc
+        <>  foldMap prettyHeaders headers
+      where
+        prettyHeaders h =
+          " using (" <> Pretty.unAnnotate (Pretty.pretty h) <> ")"
+
+        File {..} = path
+
+        Directory {..} = directory
+
+        pathDoc =
+                foldMap prettyURIComponent (reverse components)
+            <>  prettyURIComponent file
+
+        schemeDoc = case scheme of
+            HTTP  -> "http"
+            HTTPS -> "https"
+
+        queryDoc = case query of
+            Nothing -> ""
+            Just q  -> "?" <> Pretty.pretty q
+
+prettyURIComponent :: Text -> Doc ann
+prettyURIComponent text =
+        Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text
+
+-- | The type of import (i.e. local vs. remote vs. environment)
+data ImportType
+    = Local FilePrefix File
+    -- ^ Local path
+    | Remote URL
+    -- ^ URL of remote resource and optional headers stored in an import
+    | Env  Text
+    -- ^ Environment variable
+    | Missing
+    deriving (Eq, Generic, Ord, Show, NFData)
+
+parent :: File
+parent = File { directory = Directory { components = [ ".." ] }, file = "" }
+
+instance Semigroup ImportType where
+    Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁)
+
+    Remote (URL { path = path₀, ..}) <> Local Here path₁ =
+        Remote (URL { path = path₀ <> path₁, ..})
+
+    Local prefix file₀ <> Local Parent file₁ =
+        Local prefix (file₀ <> parent <> file₁)
+
+    Remote (URL { path = path₀, .. }) <> Local Parent path₁ =
+        Remote (URL { path = path₀ <> parent <> path₁, .. })
+
+    import₀ <> Remote (URL { headers = headers₀, .. }) =
+        Remote (URL { headers = headers₁, .. })
+      where
+        importHashed₀ = Import (ImportHashed Nothing import₀) Code
+
+        headers₁ = fmap (fmap (importHashed₀ <>)) headers₀
+
+    _ <> import₁ =
+        import₁
+
+instance Pretty ImportType where
+    pretty (Local prefix file) =
+        Pretty.pretty prefix <> Pretty.pretty file
+
+    pretty (Remote url) = Pretty.pretty url
+
+    pretty (Env env) = "env:" <> prettyEnvironmentVariable env
+
+    pretty Missing = "missing"
+
+-- | How to interpret the import's contents (i.e. as Dhall code or raw text)
+data ImportMode = Code | RawText | Location
+  deriving (Eq, Generic, Ord, Show, NFData)
+
+-- | A `ImportType` extended with an optional hash for semantic integrity checks
+data ImportHashed = ImportHashed
+    { hash       :: Maybe Dhall.Crypto.SHA256Digest
+    , importType :: ImportType
+    } deriving (Eq, Generic, Ord, Show, NFData)
+
+instance Semigroup ImportHashed where
+    ImportHashed _ importType₀ <> ImportHashed hash importType₁ =
+        ImportHashed hash (importType₀ <> importType₁)
+
+instance Pretty ImportHashed where
+    pretty (ImportHashed  Nothing p) =
+      Pretty.pretty p
+    pretty (ImportHashed (Just h) p) =
+      Pretty.group (Pretty.flatAlt long short)
+      where
+        long =
+            Pretty.align
+                (   Pretty.pretty p <> Pretty.hardline
+                <>  "  sha256:" <> Pretty.pretty (show h)
+                )
+
+        short = Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h)
+
+-- | Reference to an external resource
+data Import = Import
+    { importHashed :: ImportHashed
+    , importMode   :: ImportMode
+    } deriving (Eq, Generic, Ord, Show, NFData)
+
+instance Semigroup Import where
+    Import importHashed₀ _ <> Import importHashed₁ code =
+        Import (importHashed₀ <> importHashed₁) code
+
+instance Pretty Import where
+    pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix
+      where
+        suffix :: Text
+        suffix = case importMode of
+            RawText  -> " as Text"
+            Location -> " as Location"
+            Code     -> ""
+
+{-| Returns `True` if the given `Char` is valid within an unquoted path
+    component
+
+    This is exported for reuse within the @"Dhall.Parser.Token"@ module
+-}
+pathCharacter :: Char -> Bool
+pathCharacter c =
+         '\x21' == c
+    ||  ('\x24' <= c && c <= '\x27')
+    ||  ('\x2A' <= c && c <= '\x2B')
+    ||  ('\x2D' <= c && c <= '\x2E')
+    ||  ('\x30' <= c && c <= '\x3B')
+    ||  c == '\x3D'
+    ||  ('\x40' <= c && c <= '\x5A')
+    ||  ('\x5E' <= c && c <= '\x7A')
+    ||  c == '\x7C'
+    ||  c == '\x7E'
diff --git a/dhall/src/Dhall/Syntax/Optics.hs b/dhall/src/Dhall/Syntax/Optics.hs
new file mode 100644
index 000000000..7394a2e9d
--- /dev/null
+++ b/dhall/src/Dhall/Syntax/Optics.hs
@@ -0,0 +1,87 @@
+{-| This module provides optics for the core syntax types.
+-}
+
+module Dhall.Syntax.Optics (
+      subExpressions
+    , subExpressionsWith
+    , unsafeSubExpressions
+    , chunkExprs
+    , bindingExprs
+    , recordFieldExprs
+    , functionBindingExprs
+    ) where
+
+import Dhall.Syntax
+    ( Binding (..)
+    , Expr (..)
+    , FunctionBinding (..)
+    , RecordField (..)
+    , chunkExprs
+    , unsafeSubExpressions
+    )
+
+-- | A traversal over the immediate sub-expressions of an expression.
+subExpressions
+    :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
+subExpressions = subExpressionsWith (pure . Embed)
+{-# INLINABLE subExpressions #-}
+
+{-| A traversal over the immediate sub-expressions of an expression which
+    allows mapping embedded values
+-}
+subExpressionsWith
+    :: Applicative f => (a -> f (Expr s b)) -> (Expr s a -> f (Expr s b)) -> Expr s a -> f (Expr s b)
+subExpressionsWith h _ (Embed a) = h a
+subExpressionsWith _ f (Note a b) = Note a <$> f b
+subExpressionsWith _ f (Let a b) = Let <$> bindingExprs f a <*> f b
+subExpressionsWith _ f (Record a) = Record <$> traverse (recordFieldExprs f) a
+subExpressionsWith _ f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a
+subExpressionsWith _ f (Lam cs fb e) = Lam cs <$> functionBindingExprs f fb <*> f e
+subExpressionsWith _ f (Field a b) = Field <$> f a <*> pure b
+subExpressionsWith _ f expression = unsafeSubExpressions f expression
+{-# INLINABLE subExpressionsWith #-}
+
+{-| Traverse over the immediate 'Expr' children in a 'Binding'.
+-}
+bindingExprs
+  :: (Applicative f)
+  => (Expr s a -> f (Expr s b))
+  -> Binding s a -> f (Binding s b)
+bindingExprs f (Binding s0 n s1 t s2 v) =
+  Binding
+    <$> pure s0
+    <*> pure n
+    <*> pure s1
+    <*> traverse (traverse f) t
+    <*> pure s2
+    <*> f v
+{-# INLINABLE bindingExprs #-}
+
+{-| Traverse over the immediate 'Expr' children in a 'RecordField'.
+-}
+recordFieldExprs
+    :: Applicative f
+    => (Expr s a -> f (Expr s b))
+    -> RecordField s a -> f (RecordField s b)
+recordFieldExprs f (RecordField s0 e s1 s2) =
+    RecordField
+        <$> pure s0
+        <*> f e
+        <*> pure s1
+        <*> pure s2
+{-# INLINABLE recordFieldExprs #-}
+
+{-| Traverse over the immediate 'Expr' children in a 'FunctionBinding'.
+-}
+functionBindingExprs
+    :: Applicative f
+    => (Expr s a -> f (Expr s b))
+    -> FunctionBinding s a -> f (FunctionBinding s b)
+functionBindingExprs f (FunctionBinding s0 label s1 s2 type_) =
+    FunctionBinding
+        <$> pure s0
+        <*> pure label
+        <*> pure s1
+        <*> pure s2
+        <*> f type_
+{-# INLINABLE functionBindingExprs #-}
diff --git a/dhall/src/Dhall/URL.hs b/dhall/src/Dhall/URL.hs
index d969341e0..aaae29643 100644
--- a/dhall/src/Dhall/URL.hs
+++ b/dhall/src/Dhall/URL.hs
@@ -5,7 +5,7 @@ module Dhall.URL where
 
 import Data.Text (Text)
 
-import Dhall.Syntax (Directory (..), File (..), Scheme (..), URL (..))
+import Dhall.Syntax.Import (Directory (..), File (..), Scheme (..), URL (..))
 
 import qualified Network.URI.Encode as URI.Encode
 
diff --git a/dhall/src/Dhall/Util.hs b/dhall/src/Dhall/Util.hs
index 6f6cb68e5..1b27100bd 100644
--- a/dhall/src/Dhall/Util.hs
+++ b/dhall/src/Dhall/Util.hs
@@ -36,7 +36,8 @@ import Data.Text              (Text)
 import Dhall.Parser           (Header (..), ParseError)
 import Dhall.Pretty           (Ann, CharacterSet)
 import Dhall.Src              (Src)
-import Dhall.Syntax           (Expr, Import)
+import Dhall.Syntax           (Expr)
+import Dhall.Syntax.Import    (Import)
 import Prettyprinter          (Doc, Pretty)
 
 import qualified Control.Exception