diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,24 @@
+1.38.0
+
+* [BREAKING CHANGE: Detect preferred character set from input](https://github.com/dhall-lang/dhall-haskell/pull/2108)
+    * `dhall format` will now preserve the character set of the formatted file
+      by default.  In other words, if the file uses ASCII punctuation then
+      `dhall format` will format the file using ASCII punctuation.
+    * If the file contains both ASCII and Unicode punctuation it will prefer
+      Unicode by default
+    * This is a breaking change because the `Lam` / `Pi` / `Combine` /
+      `CombineTypes`, and `Prefer` constructors now take an additional argument
+      to record which character set was used
+* [BUG FIX: Fix CORS compliance check](https://github.com/dhall-lang/dhall-haskell/pull/2121)
+    * Previous versions were not correctly enforcing CORS compliance
+    * This implies that some imports that would have worked previously by
+      accident will now fail; specifically: an import from one domain
+      transitively importing something from another domain that has not opted
+      into CORS
+* [Add `ToDhall (Fix f)` instance](https://github.com/dhall-lang/dhall-haskell/pull/2122)
+* Fixes and improvements to error messages
+    * [#2130](https://github.com/dhall-lang/dhall-haskell/pull/2130)
+
 1.37.1
 
 * [Fix performance regression for `with` expressions](https://github.com/dhall-lang/dhall-haskell/pull/2112)
diff --git a/benchmark/deep-nested-large-record/Main.hs b/benchmark/deep-nested-large-record/Main.hs
--- a/benchmark/deep-nested-large-record/Main.hs
+++ b/benchmark/deep-nested-large-record/Main.hs
@@ -54,7 +54,7 @@
                         Nothing
                         (prelude `Core.Field` types `Core.Field` big)
                     )
-                    (Core.Prefer Core.PreferFromSource "big" "big")
+                    (Core.Prefer mempty Core.PreferFromSource "big" "big")
                 )
             )
             "x"
diff --git a/dhall.cabal b/dhall.cabal
--- a/dhall.cabal
+++ b/dhall.cabal
@@ -1,5 +1,5 @@
 Name: dhall
-Version: 1.37.1
+Version: 1.38.0
 Cabal-Version: >=1.10
 Build-Type: Simple
 Tested-With: GHC == 8.4.3, GHC == 8.6.1
@@ -679,11 +679,11 @@
         serialise                                      ,
         special-values                           < 0.2 ,
         spoon                                    < 0.4 ,
-        tasty                     >= 0.11.2   && < 1.4 ,
+        tasty                     >= 0.11.2   && < 1.5 ,
         tasty-expected-failure                   < 0.13,
         tasty-hunit               >= 0.10     && < 0.11,
         tasty-quickcheck          >= 0.9.2    && < 0.11,
-        tasty-silver                             < 3.2 ,
+        tasty-silver                             < 3.3 ,
         template-haskell                               ,
         text                      >= 0.11.1.0 && < 1.3 ,
         transformers                                   ,
diff --git a/ghc-src/Dhall/Import/HTTP.hs b/ghc-src/Dhall/Import/HTTP.hs
--- a/ghc-src/Dhall/Import/HTTP.hs
+++ b/ghc-src/Dhall/Import/HTTP.hs
@@ -11,6 +11,7 @@
 import Data.ByteString                  (ByteString)
 import Data.CaseInsensitive             (CI)
 import Data.Dynamic                     (toDyn)
+import Data.List.NonEmpty               (NonEmpty(..))
 import Dhall.Core
     ( Import (..)
     , ImportHashed (..)
@@ -29,7 +30,6 @@
 
 import qualified Control.Exception
 import qualified Control.Monad.Trans.State.Strict as State
-import qualified Data.List.NonEmpty               as NonEmpty
 import qualified Data.Text                        as Text
 import qualified Data.Text.Encoding
 import qualified Data.Text.Lazy
@@ -266,11 +266,15 @@
 
     Status {..} <- State.get
 
-    let Chained parentImport = NonEmpty.head _stack
-
-    let parentImportType = importType (importHashed parentImport)
+    case _stack of
+        -- We ignore the first import in the stack since that is the same import
+        -- as the `childUrl`
+        _ :| Chained parentImport : _ -> do
+            let parentImportType = importType (importHashed parentImport)
 
-    corsCompliant parentImportType childURL (HTTP.responseHeaders response)
+            corsCompliant parentImportType childURL (HTTP.responseHeaders response)
+        _ -> do
+            return ()
 
     let bytes = HTTP.responseBody response
 
diff --git a/src/Dhall.hs b/src/Dhall.hs
--- a/src/Dhall.hs
+++ b/src/Dhall.hs
@@ -353,14 +353,15 @@
     show InvalidDecoder { .. } =
         _ERROR <> ": Invalid Dhall.Decoder                                               \n\
         \                                                                                \n\
-        \Every Decoder must provide an extract function that succeeds if an expression   \n\
-        \matches the expected type.  You provided a Decoder that disobeys this contract  \n\
+        \Every Decoder must provide an extract function that does not fail with a type   \n\
+        \error if an expression matches the expected type.  You provided a Decoder that  \n\
+        \disobeys this contract                                                          \n\
         \                                                                                \n\
         \The Decoder provided has the expected dhall type:                               \n\
         \                                                                                \n\
         \" <> show txt0 <> "\n\
         \                                                                                \n\
-        \and it couldn't extract a value from the well-typed expression:                 \n\
+        \and it threw a type error during extraction from the well-typed expression:     \n\
         \                                                                                \n\
         \" <> show txt1 <> "\n\
         \                                                                                \n"
@@ -1074,7 +1075,7 @@
         Success o  -> o
         Failure _e -> error "FromDhall: You cannot decode a function if it does not have the correct type" )
 
-    expectedOut = Pi "_" declared <$> expectedIn
+    expectedOut = Pi mempty "_" declared <$> expectedIn
 
 {-| Decode a `Data.Set.Set` from a `List`
 
@@ -1442,6 +1443,9 @@
 resultToFix :: Functor f => Result f -> Fix f
 resultToFix (Result x) = Fix (fmap resultToFix x)
 
+fixToResult :: Functor f => Fix f -> Result f
+fixToResult (Fix x) = Result (fmap fixToResult x)
+
 instance FromDhall (f (Result f)) => FromDhall (Result f) where
     autoWith inputNormalizer = Decoder {..}
       where
@@ -1451,6 +1455,12 @@
 
         expected = pure "result"
 
+instance ToDhall (f (Result f)) => ToDhall (Result f) where
+    injectWith inputNormalizer = Encoder {..}
+      where
+        embed = App "Make" . Dhall.embed (injectWith inputNormalizer) . _unResult
+        declared = "result"
+
 -- | You can use this instance to marshal recursive types from Dhall to Haskell.
 --
 -- Here is an example use of this instance:
@@ -1532,11 +1542,11 @@
           where
             die = typeError expected expr0
 
-            extract0 (Lam (FunctionBinding { functionBindingVariable = x }) expr) =
+            extract0 (Lam _ (FunctionBinding { functionBindingVariable = x }) expr) =
                 extract1 (rename x "result" expr)
             extract0  _             = die
 
-            extract1 (Lam (FunctionBinding { functionBindingVariable = y }) expr) =
+            extract1 (Lam _ (FunctionBinding { functionBindingVariable = y }) expr) =
                 extract2 (rename y "Make" expr)
             extract1  _             = die
 
@@ -1546,8 +1556,22 @@
                 | a /= b    = Core.subst (V a 0) (Var (V b 0)) (Core.shift 1 (V b 0) expr)
                 | otherwise = expr
 
-        expected = (\x -> Pi "result" (Const Core.Type) (Pi "Make" (Pi "_" x "result") "result"))
+        expected = (\x -> Pi mempty "result" (Const Core.Type) (Pi mempty "Make" (Pi mempty "_" x "result") "result"))
             <$> Dhall.expected (autoWith inputNormalizer :: Decoder (f (Result f)))
+
+instance forall f. (Functor f, ToDhall (f (Result f))) => ToDhall (Fix f) where
+    injectWith inputNormalizer = Encoder {..}
+      where
+        embed fixf =
+          Lam Nothing (Core.makeFunctionBinding "result" (Const Core.Type)) $
+            Lam Nothing (Core.makeFunctionBinding "Make" makeType) $
+              embed' . fixToResult $ fixf
+
+        declared = Pi Nothing "result" (Const Core.Type) $ Pi Nothing "_" makeType "result"
+
+        makeType = Pi Nothing "_" declared' "result"
+        Encoder embed' _ = injectWith @(Dhall.Result f) inputNormalizer
+        Encoder _ declared' = injectWith @(f (Dhall.Result f)) inputNormalizer
 
 {-| `genericAuto` is the default implementation for `auto` if you derive
     `FromDhall`.  The difference is that you can use `genericAuto` without
diff --git a/src/Dhall/Binary.hs b/src/Dhall/Binary.hs
--- a/src/Dhall/Binary.hs
+++ b/src/Dhall/Binary.hs
@@ -260,7 +260,7 @@
 
                                         b <- go
 
-                                        return (Lam (Syntax.makeFunctionBinding "_" _A) b)
+                                        return (Lam mempty (Syntax.makeFunctionBinding "_" _A) b)
 
                                     4 -> do
                                         x <- Decoding.decodeString
@@ -273,7 +273,7 @@
 
                                         b <- go
 
-                                        return (Lam (Syntax.makeFunctionBinding x _A) b)
+                                        return (Lam mempty (Syntax.makeFunctionBinding x _A) b)
 
                                     _ ->
                                         die ("Incorrect number of tokens used to encode a λ expression: " <> show len)
@@ -285,7 +285,7 @@
 
                                         _B <- go
 
-                                        return (Pi "_" _A _B)
+                                        return (Pi mempty "_" _A _B)
 
                                     4 -> do
                                         x <- Decoding.decodeString
@@ -298,7 +298,7 @@
 
                                         _B <- go
 
-                                        return (Pi x _A _B)
+                                        return (Pi mempty x _A _B)
 
                                     _ ->
                                         die ("Incorrect number of tokens used to encode a ∀ expression: " <> show len)
@@ -315,9 +315,9 @@
                                     5  -> return NaturalTimes
                                     6  -> return TextAppend
                                     7  -> return ListAppend
-                                    8  -> return (Combine Nothing)
-                                    9  -> return (Prefer PreferFromSource)
-                                    10 -> return CombineTypes
+                                    8  -> return (Combine mempty Nothing)
+                                    9  -> return (Prefer mempty PreferFromSource)
+                                    10 -> return (CombineTypes mempty)
                                     11 -> return ImportAlt
                                     12 -> return Equivalent
                                     13 -> return RecordCompletion
@@ -730,26 +730,26 @@
           where
             (function, arguments) = unApply a
 
-        Lam (FunctionBinding { functionBindingVariable = "_", functionBindingAnnotation = _A }) b ->
+        Lam _ (FunctionBinding { functionBindingVariable = "_", functionBindingAnnotation = _A }) b ->
             encodeList3
                 (Encoding.encodeInt 1)
                 (go _A)
                 (go b)
 
-        Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b ->
+        Lam _ (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b ->
             encodeList4
                 (Encoding.encodeInt 1)
                 (Encoding.encodeString x)
                 (go _A)
                 (go b)
 
-        Pi "_" _A _B ->
+        Pi _ "_" _A _B ->
             encodeList3
                 (Encoding.encodeInt 2)
                 (go _A)
                 (go _B)
 
-        Pi x _A _B ->
+        Pi _ x _A _B ->
             encodeList4
                 (Encoding.encodeInt 2)
                 (Encoding.encodeString x)
@@ -780,13 +780,13 @@
         ListAppend l r ->
             encodeOperator 7 l r
 
-        Combine _ l r ->
+        Combine _ _ l r ->
             encodeOperator 8 l r
 
-        Prefer _ l r ->
+        Prefer _ _ l r ->
             encodeOperator 9 l r
 
-        CombineTypes l r ->
+        CombineTypes _ l r ->
             encodeOperator 10 l r
 
         ImportAlt l r ->
diff --git a/src/Dhall/Diff.hs b/src/Dhall/Diff.hs
--- a/src/Dhall/Diff.hs
+++ b/src/Dhall/Diff.hs
@@ -356,7 +356,7 @@
 
     diffTextSkeleton = difference textSkeleton textSkeleton
 
-    chunks = zipWith chunkDiff (toEitherList cL) (toEitherList cR) 
+    chunks = zipWith chunkDiff (toEitherList cL) (toEitherList cR)
 
     chunkDiff a b =
       case (a, b) of
@@ -647,8 +647,8 @@
     enclosed' "  " (rarrow <> " ") (docs l r)
   where
     docs
-        (Lam (FunctionBinding { functionBindingVariable = aL, functionBindingAnnotation = bL }) cL)
-        (Lam (FunctionBinding { functionBindingVariable = aR, functionBindingAnnotation = bR }) cR) =
+        (Lam _ (FunctionBinding { functionBindingVariable = aL, functionBindingAnnotation = bL }) cL)
+        (Lam _ (FunctionBinding { functionBindingVariable = aR, functionBindingAnnotation = bR }) cR) =
         Data.List.NonEmpty.cons (align doc) (docs cL cR)
       where
         doc =   lambda
@@ -707,7 +707,7 @@
 diff l@(Pi {}) r@(Pi {}) =
     enclosed' "  " (rarrow <> " ") (docs l r)
   where
-    docs (Pi aL bL cL) (Pi aR bR cR) =
+    docs (Pi _ aL bL cL) (Pi _ aR bR cR) =
         Data.List.NonEmpty.cons (align doc) (docs cL cR)
       where
         doc | same docA && same docB = ignore
@@ -901,7 +901,7 @@
 diffCombineExpression l@(Combine {}) r@(Combine {}) =
     enclosed' "  " (operator "∧" <> " ") (docs l r)
   where
-    docs (Combine _ aL bL) (Combine _ aR bR) =
+    docs (Combine _ _ aL bL) (Combine _ _ aR bR) =
         Data.List.NonEmpty.cons (diffPreferExpression aL aR) (docs bL bR)
     docs aL aR =
         pure (diffPreferExpression aL aR)
@@ -916,7 +916,7 @@
 diffPreferExpression l@(Prefer {}) r@(Prefer {}) =
     enclosed' "  " (operator "⫽" <> " ") (docs l r)
   where
-    docs (Prefer _ aL bL) (Prefer _ aR bR) =
+    docs (Prefer _ _ aL bL) (Prefer _ _ aR bR) =
         Data.List.NonEmpty.cons (diffCombineTypesExpression aL aR) (docs bL bR)
     docs aL aR =
         pure (diffCombineTypesExpression aL aR)
@@ -931,7 +931,7 @@
 diffCombineTypesExpression l@(CombineTypes {}) r@(CombineTypes {}) =
     enclosed' "  " (operator "*" <> " ") (docs l r)
   where
-    docs (CombineTypes aL bL) (CombineTypes aR bR) =
+    docs (CombineTypes _ aL bL) (CombineTypes _ aR bR) =
         Data.List.NonEmpty.cons (diffTimesExpression aL aR) (docs bL bR)
     docs aL aR =
         pure (diffTimesExpression aL aR)
diff --git a/src/Dhall/Eval.hs b/src/Dhall/Eval.hs
--- a/src/Dhall/Eval.hs
+++ b/src/Dhall/Eval.hs
@@ -424,9 +424,9 @@
             VConst k
         Var v ->
             vVar env v
-        Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t ->
+        Lam _ (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t ->
             VLam (eval env a) (Closure x env t)
-        Pi x a b ->
+        Pi _ x a b ->
             VPi (eval env a) (Closure x env b)
         App t u ->
             vApp (eval env t) (eval env u)
@@ -733,14 +733,14 @@
             VRecordLit (Map.sort (eval env . recordFieldValue <$> kts))
         Union kts ->
             VUnion (Map.sort (fmap (fmap (eval env)) kts))
-        Combine mk t u ->
+        Combine _ mk t u ->
             vCombine mk (eval env t) (eval env u)
-        CombineTypes t u ->
+        CombineTypes _ t u ->
             vCombineTypes (eval env t) (eval env u)
-        Prefer _ t u ->
+        Prefer _ _ t u ->
             vPrefer env (eval env t) (eval env u)
         RecordCompletion t u ->
-            eval env (Annot (Prefer PreferFromCompletion (Field t def) u) (Field t typ))
+            eval env (Annot (Prefer mempty PreferFromCompletion (Field t def) u) (Field t typ))
           where
             def = Syntax.makeFieldSelection "default"
             typ = Syntax.makeFieldSelection "Type"
@@ -1054,21 +1054,23 @@
             quote env t `qApp` u
         VLam a (freshClosure -> (x, v, t)) ->
             Lam
+                mempty
                 (Syntax.makeFunctionBinding x (quote env a))
                 (quoteBind x (instantiate t v))
         VHLam i t ->
             case i of
                 Typed (fresh -> (x, v)) a ->
                     Lam
+                        mempty
                         (Syntax.makeFunctionBinding x (quote env a))
                         (quoteBind x (t v))
                 Prim                      -> quote env (t VPrimVar)
                 NaturalSubtractZero       -> App NaturalSubtract (NaturalLit 0)
 
         VPi a (freshClosure -> (x, v, b)) ->
-            Pi x (quote env a) (quoteBind x (instantiate b v))
+            Pi mempty x (quote env a) (quoteBind x (instantiate b v))
         VHPi (fresh -> (x, v)) a b ->
-            Pi x (quote env a) (quoteBind x (b v))
+            Pi mempty x (quote env a) (quoteBind x (b v))
         VBool ->
             Bool
         VBoolLit b ->
@@ -1168,11 +1170,11 @@
         VUnion m ->
             Union (fmap (fmap (quote env)) m)
         VCombine mk t u ->
-            Combine mk (quote env t) (quote env u)
+            Combine mempty mk (quote env t) (quote env u)
         VCombineTypes t u ->
-            CombineTypes (quote env t) (quote env u)
+            CombineTypes mempty (quote env t) (quote env u)
         VPrefer t u ->
-            Prefer PreferFromSource (quote env t) (quote env u)
+            Prefer mempty PreferFromSource (quote env t) (quote env u)
         VMerge t u ma ->
             Merge (quote env t) (quote env u) (fmap (quote env) ma)
         VToMap t ma ->
@@ -1243,10 +1245,10 @@
                 Const k
             Var (V x i) ->
                 goVar e0 x i
-            Lam (FunctionBinding src0 x src1 src2 t) u ->
-                Lam (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u)
-            Pi x a b ->
-                Pi "_" (go a) (goBind x b)
+            Lam cs (FunctionBinding src0 x src1 src2 t) u ->
+                Lam cs (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u)
+            Pi cs x a b ->
+                Pi cs "_" (go a) (goBind x b)
             App t u ->
                 App (go t) (go u)
             Let (Binding src0 x src1 mA src2 a) b ->
@@ -1351,12 +1353,12 @@
                 RecordLit (goRecordField <$> kts)
             Union kts ->
                 Union (fmap (fmap go) kts)
-            Combine m t u ->
-                Combine m (go t) (go u)
-            CombineTypes t u ->
-                CombineTypes (go t) (go u)
-            Prefer b t u ->
-                Prefer b (go t) (go u)
+            Combine cs m t u ->
+                Combine cs m (go t) (go u)
+            CombineTypes cs t u ->
+                CombineTypes cs (go t) (go u)
+            Prefer cs b t u ->
+                Prefer cs b (go t) (go u)
             RecordCompletion t u ->
                 RecordCompletion (go t) (go u)
             Merge x y ma ->
diff --git a/src/Dhall/Format.hs b/src/Dhall/Format.hs
--- a/src/Dhall/Format.hs
+++ b/src/Dhall/Format.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE NamedFieldPuns    #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards   #-}
 
@@ -10,8 +12,8 @@
     ) where
 
 import Data.Foldable (for_)
-import Dhall.Pretty  (CharacterSet (..), annToAnsiStyle)
-
+import Data.Maybe    (fromMaybe)
+import Dhall.Pretty  (CharacterSet, annToAnsiStyle, detectCharacterSet)
 import Dhall.Util
     ( Censor
     , CheckFailed (..)
@@ -36,10 +38,10 @@
 
 -- | Arguments to the `format` subcommand
 data Format = Format
-    { characterSet :: CharacterSet
-    , censor       :: Censor
-    , input        :: PossiblyTransitiveInput
-    , outputMode   :: OutputMode
+    { chosenCharacterSet :: Maybe CharacterSet
+    , censor             :: Censor
+    , input              :: PossiblyTransitiveInput
+    , outputMode         :: OutputMode
     }
 
 -- | Implementation of the @dhall format@ subcommand
@@ -56,6 +58,8 @@
         let status = Dhall.Import.emptyStatus directory
 
         let layoutHeaderAndExpr (Header header, expr) =
+                let characterSet = fromMaybe (detectCharacterSet expr) chosenCharacterSet
+                in
                 Dhall.Pretty.layout
                     (   Pretty.pretty header
                     <>  Dhall.Pretty.prettyCharacterSet characterSet expr
diff --git a/src/Dhall/Freeze.hs b/src/Dhall/Freeze.hs
--- a/src/Dhall/Freeze.hs
+++ b/src/Dhall/Freeze.hs
@@ -22,7 +22,8 @@
     ) where
 
 import Data.Foldable       (for_)
-import Dhall.Pretty        (CharacterSet)
+import Data.Maybe          (fromMaybe)
+import Dhall.Pretty        (CharacterSet, detectCharacterSet)
 import Dhall.Syntax
     ( Expr (..)
     , Import (..)
@@ -142,7 +143,7 @@
     -> PossiblyTransitiveInput
     -> Scope
     -> Intent
-    -> CharacterSet
+    -> Maybe CharacterSet
     -> Censor
     -> IO ()
 freeze = freezeWithManager Dhall.Import.defaultNewManager
@@ -154,10 +155,10 @@
     -> PossiblyTransitiveInput
     -> Scope
     -> Intent
-    -> CharacterSet
+    -> Maybe CharacterSet
     -> Censor
     -> IO ()
-freezeWithManager newManager outputMode input0 scope intent characterSet censor = go input0
+freezeWithManager newManager outputMode input0 scope intent chosenCharacterSet censor = go input0
   where
     go input = do
         let directory = case input of
@@ -180,6 +181,8 @@
                 return (text, NonTransitive)
 
         (Header header, parsedExpression) <- Util.getExpressionAndHeaderFromStdinText censor originalText
+
+        let characterSet = fromMaybe (detectCharacterSet parsedExpression) chosenCharacterSet
 
         case transitivity of
             Transitive ->
diff --git a/src/Dhall/Import.hs b/src/Dhall/Import.hs
--- a/src/Dhall/Import.hs
+++ b/src/Dhall/Import.hs
@@ -124,6 +124,8 @@
     , chainedChangeMode
     , emptyStatus
     , emptyStatusWithManager
+    , remoteStatus
+    , remoteStatusWithManager
     , stack
     , cache
     , Depends(..)
@@ -1062,8 +1064,50 @@
 
 -- | See 'emptyStatus'.
 emptyStatusWithManager :: IO Manager -> FilePath -> Status
-emptyStatusWithManager newManager = emptyStatusWith newManager fetchRemote
+emptyStatusWithManager newManager rootDirectory =
+    emptyStatusWith newManager fetchRemote rootImport
+  where
+    prefix = if FilePath.isRelative rootDirectory
+      then Here
+      else Absolute
 
+    pathComponents =
+        fmap Text.pack (reverse (FilePath.splitDirectories rootDirectory))
+
+    directoryAsFile = File (Directory pathComponents) "."
+
+    rootImport = Import
+      { importHashed = ImportHashed
+        { hash = Nothing
+        , importType = Local prefix directoryAsFile
+        }
+      , importMode = Code
+      }
+
+{-| Default `Status` appropriate for a server interpreting Dhall code
+
+    Using this `Status` ensures that interpreted Dhall code cannot access
+    server-local resources (like files or environment variables)
+-}
+remoteStatus
+    :: URL
+    -- ^ Public address of the server
+    -> Status
+remoteStatus = remoteStatusWithManager defaultNewManager
+
+-- | See `remoteStatus`
+remoteStatusWithManager :: IO Manager -> URL -> Status
+remoteStatusWithManager newManager url =
+    emptyStatusWith newManager fetchRemote rootImport
+  where
+    rootImport = Import
+      { importHashed = ImportHashed
+        { hash = Nothing
+        , importType = Remote url
+        }
+      , importMode = Code
+      }
+
 {-| Generalized version of `load`
 
     You can configure the desired behavior through the initial `Status` that you
@@ -1124,7 +1168,7 @@
   Let a b              -> Let <$> bindingExprs loadWith a <*> loadWith b
   Record m             -> Record <$> traverse (recordFieldExprs loadWith) m
   RecordLit m          -> RecordLit <$> traverse (recordFieldExprs loadWith) m
-  Lam a b              -> Lam <$> functionBindingExprs loadWith a <*> loadWith b
+  Lam cs a b           -> Lam cs <$> functionBindingExprs loadWith a <*> loadWith b
   Field a b            -> Field <$> loadWith a <*> pure b
   expression           -> Syntax.unsafeSubExpressions loadWith expression
 
diff --git a/src/Dhall/Import/Types.hs b/src/Dhall/Import/Types.hs
--- a/src/Dhall/Import/Types.hs
+++ b/src/Dhall/Import/Types.hs
@@ -14,21 +14,14 @@
 import Data.Void                        (Void)
 import Dhall.Context                    (Context)
 import Dhall.Core
-    ( Directory (..)
-    , Expr
-    , File (..)
-    , FilePrefix (..)
+    ( Expr
     , Import (..)
-    , ImportHashed (..)
-    , ImportMode (..)
-    , ImportType (..)
     , ReifiedNormalizer (..)
     , URL
     )
 import Dhall.Map                        (Map)
 import Dhall.Parser                     (Src)
 import Lens.Family                      (LensLike')
-import System.FilePath                  (isRelative, splitDirectories)
 
 #ifdef WITH_HTTP
 import qualified Dhall.Import.Manager
@@ -124,10 +117,14 @@
     --   cache directory
     }
 
--- | Initial `Status`, parameterised over the HTTP 'Manager' and the remote resolver,
---   importing relative to the given directory.
-emptyStatusWith :: IO Manager -> (URL -> StateT Status IO Data.Text.Text) -> FilePath -> Status
-emptyStatusWith _newManager _remote rootDirectory = Status {..}
+-- | Initial `Status`, parameterised over the HTTP 'Manager' and the remote
+--   resolver, importing relative to the given root import.
+emptyStatusWith
+    :: IO Manager
+    -> (URL -> StateT Status IO Data.Text.Text)
+    -> Import
+    -> Status
+emptyStatusWith _newManager _remote rootImport = Status {..}
   where
     _stack = pure (Chained rootImport)
 
@@ -146,23 +143,6 @@
     _semanticCacheMode = UseSemanticCache
 
     _cacheWarning = CacheNotWarned
-
-    prefix = if isRelative rootDirectory
-      then Here
-      else Absolute
-    pathComponents =
-        fmap Data.Text.pack (reverse (splitDirectories rootDirectory))
-
-    dirAsFile = File (Directory pathComponents) "."
-
-    -- Fake import to set the directory we're relative to.
-    rootImport = Import
-      { importHashed = ImportHashed
-        { hash = Nothing
-        , importType = Local prefix dirAsFile
-        }
-      , importMode = Code
-      }
 
 -- | Lens from a `Status` to its `_stack` field
 stack :: Functor f => LensLike' f Status (NonEmpty Chained)
diff --git a/src/Dhall/Main.hs b/src/Dhall/Main.hs
--- a/src/Dhall/Main.hs
+++ b/src/Dhall/Main.hs
@@ -24,6 +24,7 @@
 import Control.Applicative       (optional, (<|>))
 import Control.Exception         (Handler (..), SomeException)
 import Data.Foldable             (for_)
+import Data.Maybe                (fromMaybe)
 import Data.List.NonEmpty        (NonEmpty (..))
 import Data.Text                 (Text)
 import Data.Text.Prettyprint.Doc (Doc, Pretty)
@@ -36,7 +37,7 @@
     , _semanticCacheMode
     )
 import Dhall.Parser              (Src)
-import Dhall.Pretty              (Ann, CharacterSet (..), annToAnsiStyle)
+import Dhall.Pretty              (Ann, CharacterSet (..), annToAnsiStyle, detectCharacterSet)
 import Dhall.Schemas             (Schemas (..))
 import Dhall.TypeCheck
     ( Censored (..)
@@ -112,11 +113,11 @@
 
 -- | Top-level program options
 data Options = Options
-    { mode    :: Mode
-    , explain :: Bool
-    , plain   :: Bool
-    , ascii   :: Bool
-    , censor  :: Censor
+    { mode               :: Mode
+    , explain            :: Bool
+    , plain              :: Bool
+    , chosenCharacterSet :: Maybe CharacterSet
+    , censor             :: Censor
     }
 
 -- | The subcommands for the @dhall@ executable
@@ -194,7 +195,7 @@
     <$> parseMode
     <*> switch "explain" "Explain error messages in more detail"
     <*> switch "plain" "Disable syntax highlighting"
-    <*> switch "ascii" "Format code using only ASCII syntax"
+    <*> parseCharacterSet
     <*> parseCensor
   where
     switch name description =
@@ -208,6 +209,19 @@
         f True  = Censor
         f False = NoCensor
 
+    parseCharacterSet =
+            Options.Applicative.flag'
+                (Just Unicode)
+                (   Options.Applicative.long "unicode"
+                <>  Options.Applicative.help "Format code using only Unicode syntax"
+                )
+        <|> Options.Applicative.flag'
+                (Just ASCII)
+                (   Options.Applicative.long "ascii"
+                <>  Options.Applicative.help "Format code using only ASCII syntax"
+                )
+        <|> pure Nothing
+
 subcommand :: Group -> String -> String -> Parser a -> Parser a
 subcommand group name description parser =
     Options.Applicative.hsubparser
@@ -542,10 +556,6 @@
 -- | Run the command specified by the `Options` type
 command :: Options -> IO ()
 command (Options {..}) = do
-    let characterSet = case ascii of
-            True  -> ASCII
-            False -> Unicode
-
     GHC.IO.Encoding.setLocaleEncoding System.IO.utf8
 
     let rootDirectory = \case
@@ -556,6 +566,16 @@
 
     let getExpression = Dhall.Util.getExpression censor
 
+    -- The characterSet detection used here only works on the source
+    -- expression, before any transformation is applied. This helper is there
+    -- make sure the detection is done on the correct expr.
+    let getExpressionAndCharacterSet file = do
+            expr <- getExpression file
+
+            let characterSet = fromMaybe (detectCharacterSet expr) chosenCharacterSet
+
+            return (expr, characterSet)
+
     let handle io =
             Control.Exception.catches io
                 [ Handler handleTypeError
@@ -612,8 +632,8 @@
             Pretty.renderIO h ansiStream
             Data.Text.IO.hPutStrLn h ""
 
-    let render :: Pretty a => Handle -> Expr Src a -> IO ()
-        render h expression = do
+    let render :: Pretty a => Handle -> CharacterSet -> Expr Src a -> IO ()
+        render h characterSet expression = do
             let doc = Dhall.Pretty.prettyCharacterSet characterSet expression
 
             renderDoc h doc
@@ -635,7 +655,7 @@
                     Exit.exitSuccess
                 else return ()
 
-            expression <- getExpression file
+            (expression, characterSet) <- getExpressionAndCharacterSet file
 
             resolvedExpression <-
                 Dhall.Import.loadRelativeTo (rootDirectory file) semanticCacheMode expression
@@ -655,7 +675,7 @@
                         else alphaNormalizedExpression
 
             case output of
-                StandardOutput -> render System.IO.stdout annotatedExpression
+                StandardOutput -> render System.IO.stdout characterSet annotatedExpression
 
                 OutputFile file_ ->
                     writeDocToFile
@@ -714,15 +734,15 @@
                  $   _cache
 
         Resolve { resolveMode = Nothing, ..} -> do
-            expression <- getExpression file
+            (expression, characterSet) <- getExpressionAndCharacterSet file
 
             resolvedExpression <-
                 Dhall.Import.loadRelativeTo (rootDirectory file) semanticCacheMode expression
 
-            render System.IO.stdout resolvedExpression
+            render System.IO.stdout characterSet resolvedExpression
 
         Normalize {..} -> do
-            expression <- getExpression file
+            (expression, characterSet) <- getExpressionAndCharacterSet file
 
             resolvedExpression <- Dhall.Import.assertNoImports expression
 
@@ -735,10 +755,10 @@
                     then Dhall.Core.alphaNormalize normalizedExpression
                     else normalizedExpression
 
-            render System.IO.stdout alphaNormalizedExpression
+            render System.IO.stdout characterSet alphaNormalizedExpression
 
         Type {..} -> do
-            expression <- getExpression file
+            (expression, characterSet) <- getExpressionAndCharacterSet file
 
             resolvedExpression <-
                 Dhall.Import.loadRelativeTo (rootDirectory file) semanticCacheMode expression
@@ -747,10 +767,12 @@
 
             if quiet
                 then return ()
-                else render System.IO.stdout inferredType
+                else render System.IO.stdout characterSet inferredType
 
         Repl ->
-            Dhall.Repl.repl characterSet explain
+            Dhall.Repl.repl
+                (fromMaybe Unicode chosenCharacterSet) -- Default to Unicode if no characterSet specified
+                explain
 
         Diff {..} -> do
             expression1 <- Dhall.inputExpr expr1
@@ -774,7 +796,7 @@
 
             let intent = if cache then Cache else Secure
 
-            Dhall.Freeze.freeze outputMode possiblyTransitiveInput scope intent characterSet censor
+            Dhall.Freeze.freeze outputMode possiblyTransitiveInput scope intent chosenCharacterSet censor
 
         Hash {..} -> do
             expression <- getExpression file
@@ -815,6 +837,8 @@
                 (Header header, parsedExpression) <-
                     Dhall.Util.getExpressionAndHeaderFromStdinText censor originalText
 
+                let characterSet = fromMaybe (detectCharacterSet parsedExpression) chosenCharacterSet
+
                 case transitivity of
                     Transitive ->
                         for_ parsedExpression $ \import_ -> do
@@ -899,7 +923,7 @@
                 else do
                     let doc =
                             Dhall.Pretty.prettyCharacterSet
-                                characterSet
+                                (fromMaybe Unicode chosenCharacterSet) -- default to Unicode
                                 (Dhall.Core.renote expression :: Expr Src Import)
 
                     renderDoc System.IO.stdout doc
diff --git a/src/Dhall/Normalize.hs b/src/Dhall/Normalize.hs
--- a/src/Dhall/Normalize.hs
+++ b/src/Dhall/Normalize.hs
@@ -65,13 +65,13 @@
 -}
 subst :: Var -> Expr s a -> Expr s a -> Expr s a
 subst _ _ (Const a) = Const a
-subst (V x n) e (Lam (FunctionBinding src0 y src1 src2 _A) b) =
-    Lam (FunctionBinding src0 y src1 src2 _A') b'
+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
     n'  = if x == y then n + 1 else n
-subst (V x n) e (Pi y _A _B) = Pi y _A' _B'
+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
@@ -114,8 +114,8 @@
     using De Bruijn indices to distinguish them
 
 >>> mfb = Syntax.makeFunctionBinding
->>> alphaNormalize (Lam (mfb "a" (Const Type)) (Lam (mfb "b" (Const Type)) (Lam (mfb "x" "a") (Lam (mfb "y" "b") "x"))))
-Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1)))))
+>>> alphaNormalize (Lam mempty (mfb "a" (Const Type)) (Lam mempty (mfb "b" (Const Type)) (Lam mempty (mfb "x" "a") (Lam mempty (mfb "y" "b") "x"))))
+Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam Nothing (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1)))))
 
     α-normalization does not affect free variables:
 
@@ -174,12 +174,12 @@
  loop =  \case
     Const k -> pure (Const k)
     Var v -> pure (Var v)
-    Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b ->
-        Lam <$> (Syntax.makeFunctionBinding x <$> _A') <*> b'
+    Lam cs (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b ->
+        Lam cs <$> (Syntax.makeFunctionBinding x <$> _A') <*> b'
       where
         _A' = loop _A
         b'  = loop b
-    Pi x _A _B -> Pi x <$> _A' <*> _B'
+    Pi cs x _A _B -> Pi cs x <$> _A' <*> _B'
       where
         _A' = loop _A
         _B' = loop _B
@@ -191,7 +191,7 @@
               f' <- loop f
               a' <- loop a
               case f' of
-                Lam (FunctionBinding _ x _ _ _A) b₀ -> do
+                Lam _ (FunctionBinding _ x _ _ _A) b₀ -> do
 
                     let a₂ = Syntax.shift 1 (V x 0) a'
                     let b₁ = subst (V x 0) a₂ b₀
@@ -218,7 +218,7 @@
                         lazyLoop !n = App succ' (lazyLoop (n - 1))
                     App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)
                       where
-                        succ = Lam (Syntax.makeFunctionBinding "n" Natural) (NaturalPlus "n" (NaturalLit 1))
+                        succ = Lam mempty (Syntax.makeFunctionBinding "n" Natural) (NaturalPlus "n" (NaturalLit 1))
 
                         zero = NaturalLit 0
                     App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0))
@@ -260,8 +260,8 @@
                         list = App List _A₀
 
                         cons =
-                            Lam (Syntax.makeFunctionBinding "a" _A₀)
-                                (Lam
+                            Lam mempty (Syntax.makeFunctionBinding "a" _A₀)
+                                (Lam mempty
                                     (Syntax.makeFunctionBinding "as" (App List _A₁))
                                     (ListAppend (ListLit Nothing (pure "a")) "as")
                                 )
@@ -515,7 +515,7 @@
     Union kts -> Union . Dhall.Map.sort <$> kts'
       where
         kts' = traverse (traverse loop) kts
-    Combine mk x y -> decide <$> loop x <*> loop y
+    Combine cs mk x y -> decide <$> loop x <*> loop y
       where
         decide (RecordLit m) r | Data.Foldable.null m =
             r
@@ -527,8 +527,8 @@
             f (RecordField _ expr _ _) (RecordField _ expr' _ _) =
               Syntax.makeRecordField $ decide expr expr'
         decide l r =
-            Combine mk l r
-    CombineTypes x y -> decide <$> loop x <*> loop y
+            Combine cs mk l r
+    CombineTypes cs x y -> decide <$> loop x <*> loop y
       where
         decide (Record m) r | Data.Foldable.null m =
             r
@@ -540,8 +540,8 @@
             f (RecordField _ expr _ _) (RecordField _ expr' _ _) =
               Syntax.makeRecordField $ decide expr expr'
         decide l r =
-            CombineTypes l r
-    Prefer _ x y -> decide <$> loop x <*> loop y
+            CombineTypes cs l r
+    Prefer cs _ x y -> decide <$> loop x <*> loop y
       where
         decide (RecordLit m) r | Data.Foldable.null m =
             r
@@ -552,9 +552,9 @@
         decide l r | Eval.judgmentallyEqual l r =
             l
         decide l r =
-            Prefer PreferFromSource l r
+            Prefer cs PreferFromSource l r
     RecordCompletion x y ->
-        loop (Annot (Prefer PreferFromCompletion (Field x def) y) (Field x typ))
+        loop (Annot (Prefer mempty PreferFromCompletion (Field x def) y) (Field x typ))
       where
         def = Syntax.makeFieldSelection "default"
         typ = Syntax.makeFieldSelection "Type"
@@ -626,17 +626,17 @@
                     Just v  -> pure $ recordFieldValue v
                     Nothing -> Field <$> (RecordLit <$> traverse (Syntax.recordFieldExprs loop) kvs) <*> pure k
             Project r_ _ -> loop (Field r_ k)
-            Prefer _ (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
-                Just v -> pure (Field (Prefer PreferFromSource (singletonRecordLit v) 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)
                 Nothing -> loop (Field r_ k)
-            Prefer _ l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
+            Prefer _ _ l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
                 Just v -> pure $ recordFieldValue v
                 Nothing -> loop (Field l k)
-            Combine m (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
-                Just v -> pure (Field (Combine m (singletonRecordLit v) r_) k)
+            Combine cs m (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
+                Just v -> pure (Field (Combine cs m (singletonRecordLit v) r_) k)
                 Nothing -> loop (Field r_ k)
-            Combine m l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
-                Just v -> pure (Field (Combine m l (singletonRecordLit v)) k)
+            Combine cs m l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
+                Just v -> pure (Field (Combine cs m l (singletonRecordLit v)) k)
                 Nothing -> loop (Field l k)
             _ -> pure (Field r' k)
     Project x (Left fields)-> do
@@ -647,11 +647,11 @@
                 pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet))
             Project y _ ->
                 loop (Project y (Left fields))
-            Prefer _ l (RecordLit rKvs) -> do
+            Prefer cs _ l (RecordLit rKvs) -> do
                 let rKs = Dhall.Map.keysSet rKvs
                 let l' = Project l (Left (Data.Set.toList (Data.Set.difference fieldsSet rKs)))
                 let r' = RecordLit (Dhall.Map.restrictKeys rKvs fieldsSet)
-                loop (Prefer PreferFromSource l' r')
+                loop (Prefer cs PreferFromSource l' r')
             _ | null fields -> pure (RecordLit mempty)
               | otherwise   -> pure (Project x' (Left (Data.Set.toList (Data.Set.fromList fields))))
     Project r (Right e1) -> do
@@ -731,11 +731,11 @@
     loop e = case e of
       Const _ -> True
       Var _ -> True
-      Lam (FunctionBinding Nothing _ Nothing Nothing a) b -> loop a && loop b
-      Lam _ _ -> False
-      Pi _ a b -> loop a && loop b
+      Lam _ (FunctionBinding Nothing _ Nothing Nothing a) b -> loop a && loop b
+      Lam _ _ _ -> False
+      Pi _ _ a b -> loop a && loop b
       App f a -> loop f && loop a && case App f a of
-          App (Lam _ _) _ -> False
+          App (Lam _ _ _) _ -> False
           App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
           App NaturalBuild _ -> False
           App NaturalIsZero (NaturalLit _) -> False
@@ -866,19 +866,19 @@
           decide (RecordField Nothing exp' Nothing Nothing) = loop exp'
           decide _ = False
       Union kts -> Dhall.Map.isSorted kts && all (all loop) kts
-      Combine _ x y -> loop x && loop y && decide x y
+      Combine _ _ x y -> loop x && loop y && decide x y
         where
           decide (RecordLit m) _ | Data.Foldable.null m = False
           decide _ (RecordLit n) | Data.Foldable.null n = False
           decide (RecordLit _) (RecordLit _) = False
           decide  _ _ = True
-      CombineTypes x y -> loop x && loop y && decide x y
+      CombineTypes _ x y -> loop x && loop y && decide x y
         where
           decide (Record m) _ | Data.Foldable.null m = False
           decide _ (Record n) | Data.Foldable.null n = False
           decide (Record _) (Record _) = False
           decide  _ _ = True
-      Prefer _ x y -> loop x && loop y && decide x y
+      Prefer _ _ x y -> loop x && loop y && decide x y
         where
           decide (RecordLit m) _ | Data.Foldable.null m = False
           decide _ (RecordLit n) | Data.Foldable.null n = False
@@ -899,10 +899,10 @@
       Field r (FieldSelection Nothing k Nothing) -> case r of
           RecordLit _ -> False
           Project _ _ -> False
-          Prefer _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
-          Prefer _ _ (RecordLit _) -> False
-          Combine _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
-          Combine _ _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
+          Prefer _ _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
+          Prefer _ _ _ (RecordLit _) -> False
+          Combine _ _ (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
+          Combine _ _ _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
           _ -> loop r
       Field _ _ -> False
       Project r p -> loop r &&
@@ -910,7 +910,7 @@
               Left s -> case r of
                   RecordLit _ -> False
                   Project _ _ -> False
-                  Prefer _ _ (RecordLit _) -> False
+                  Prefer _ _ _ (RecordLit _) -> False
                   _ -> not (null s) && Data.Set.toList (Data.Set.fromList s) == s
               Right e' -> case e' of
                   Record _ -> False
@@ -928,7 +928,7 @@
 True
 >>> "x" `freeIn` "y"
 False
->>> "x" `freeIn` Lam (Syntax.makeFunctionBinding "x" (Const Type)) "x"
+>>> "x" `freeIn` Lam mempty (Syntax.makeFunctionBinding "x" (Const Type)) "x"
 False
 -}
 freeIn :: Eq a => Var -> Expr s a -> Bool
diff --git a/src/Dhall/Optics.hs b/src/Dhall/Optics.hs
--- a/src/Dhall/Optics.hs
+++ b/src/Dhall/Optics.hs
@@ -4,17 +4,24 @@
 -}
 
 module Dhall.Optics
-    ( -- * Utilities
-      rewriteOf
+    ( Optic
+    , Optic'
+       -- * Utilities
+    , rewriteOf
     , transformOf
     , rewriteMOf
     , transformMOf
     , mapMOf
+    , cosmosOf
+    , to
+    , foldOf
     ) where
 
-import Control.Applicative    (WrappedMonad (..))
-import Data.Profunctor.Unsafe (( #. ))
-import Lens.Family            (ASetter, LensLike, over)
+import Control.Applicative        (Const (..), WrappedMonad (..))
+import Data.Functor.Contravariant (Contravariant (contramap))
+import Data.Profunctor            (Profunctor (dimap))
+import Data.Profunctor.Unsafe     (( #. ))
+import Lens.Family                (ASetter, LensLike, LensLike', over)
 
 -- | Identical to @"Control.Lens".`Control.Lens.rewriteOf`@
 rewriteOf :: ASetter a b a b -> (b -> Maybe a) -> a -> b
@@ -51,3 +58,27 @@
 mapMOf :: LensLike (WrappedMonad m) s t a b -> (a -> m b) -> s -> m t
 mapMOf l cmd = unwrapMonad #. l (WrapMonad #. cmd)
 {-# INLINE mapMOf #-}
+
+-- | Identical to @"Control.Lens.Plated".`Control.Lens.Plated.cosmosOf`@
+cosmosOf :: (Applicative f, Contravariant f) => LensLike' f a a -> LensLike' f a a
+cosmosOf d f s = f s *> d (cosmosOf d f) s
+{-# INLINE cosmosOf #-}
+
+-- | Identical to @"Control.Lens.Type".`Control.Lens.Type.Optic`@
+type Optic p f s t a b = p a (f b) -> p s (f t)
+
+-- | Identical to @"Control.Lens.Type".`Control.Lens.Type.Optic'`@
+type Optic' p f s a = Optic p f s s a a
+
+-- | Identical to @"Control.Lens.Getter".`Control.Lens.Getter.to`@
+to :: (Profunctor p, Contravariant f) => (s -> a) -> Optic' p f s a
+to k = dimap k (contramap k)
+{-# INLINE to #-}
+
+-- | Identical to @"Control.Lens.Getter".`Control.Lens.Getter.Getting`@
+type Getting r s a = (a -> Const r a) -> s -> Const r s
+
+-- | Identical to @"Control.Lens.Fold".`Control.Lens.Fold.foldOf`@
+foldOf :: Getting a s a -> s -> a
+foldOf l = getConst #. l Const
+{-# INLINE foldOf #-}
diff --git a/src/Dhall/Parser/Expression.hs b/src/Dhall/Parser/Expression.hs
--- a/src/Dhall/Parser/Expression.hs
+++ b/src/Dhall/Parser/Expression.hs
@@ -109,7 +109,7 @@
     , importExpression_   :: Parser (Expr Src a)
     }
 
--- | Given a parser for imports, 
+-- | Given a parser for imports,
 parsers :: forall a. Parser a -> Parsers a
 parsers embedded = Parsers {..}
   where
@@ -128,7 +128,7 @@
             ) <?> "expression"
       where
         alternative0 = do
-            _lambda
+            cs <- _lambda
             whitespace
             _openParens
             src0 <- src whitespace
@@ -140,10 +140,10 @@
             whitespace
             _closeParens
             whitespace
-            _arrow
+            cs' <- _arrow
             whitespace
             c <- expression
-            return (Lam (FunctionBinding (Just src0) a (Just src1) (Just src2) b) c)
+            return (Lam (Just (cs <> cs')) (FunctionBinding (Just src0) a (Just src1) (Just src2) b) c)
 
         alternative1 = do
             try (_if *> nonemptyWhitespace)
@@ -211,7 +211,7 @@
             return (Dhall.Syntax.wrapInLets as b)
 
         alternative3 = do
-            try (_forall *> whitespace *> _openParens)
+            cs <- try (_forall <* whitespace <* _openParens)
             whitespace
             a <- label
             whitespace
@@ -221,10 +221,10 @@
             whitespace
             _closeParens
             whitespace
-            _arrow
+            cs' <- _arrow
             whitespace
             c <- expression
-            return (Pi a b c)
+            return (Pi (Just (cs <> cs')) a b c)
 
         alternative4 = do
             try (_assert *> whitespace *> _colon)
@@ -266,11 +266,11 @@
                     whitespace
 
                     let alternative5B0 = do
-                            _arrow
+                            cs <- _arrow
                             whitespace
                             b <- expression
                             whitespace
-                            return (Pi "_" a b)
+                            return (Pi (Just cs) "_" a b)
 
                     let alternative5B1 = do
                             _colon
@@ -341,20 +341,20 @@
 
     operatorParsers :: [Parser (Expr s a -> Expr s a -> Expr s a)]
     operatorParsers =
-        [ Equivalent              <$ _equivalent   <* whitespace
-        , ImportAlt               <$ _importAlt    <* nonemptyWhitespace
-        , BoolOr                  <$ _or           <* whitespace
-        , NaturalPlus             <$ _plus         <* nonemptyWhitespace
-        , TextAppend              <$ _textAppend   <* whitespace
-        , ListAppend              <$ _listAppend   <* whitespace
-        , BoolAnd                 <$ _and          <* whitespace
-        , Combine Nothing         <$ _combine      <* whitespace
-        , Prefer PreferFromSource <$ _prefer       <* whitespace
-        , CombineTypes            <$ _combineTypes <* whitespace
-        , NaturalTimes            <$ _times        <* whitespace
+        [ Equivalent                  <$ _equivalent    <* whitespace
+        , ImportAlt                   <$ _importAlt     <* nonemptyWhitespace
+        , BoolOr                      <$ _or            <* whitespace
+        , NaturalPlus                 <$ _plus          <* nonemptyWhitespace
+        , TextAppend                  <$ _textAppend    <* whitespace
+        , ListAppend                  <$ _listAppend    <* whitespace
+        , BoolAnd                     <$ _and           <* whitespace
+        , (\cs -> Combine (Just cs) Nothing)         <$> _combine <* whitespace
+        , (\cs -> Prefer (Just cs) PreferFromSource) <$> _prefer  <* whitespace
+        , (CombineTypes . Just)       <$> _combineTypes <* whitespace
+        , NaturalTimes                <$ _times         <* whitespace
         -- Make sure that `==` is not actually the prefix of `===`
-        , BoolEQ                  <$ try (_doubleEqual <* Text.Megaparsec.notFollowedBy (char '=')) <* whitespace
-        , BoolNE                  <$ _notEqual     <* whitespace
+        , BoolEQ                      <$ try (_doubleEqual <* Text.Megaparsec.notFollowedBy (char '=')) <* whitespace
+        , BoolNE                      <$ _notEqual      <* whitespace
         ]
 
     applicationExpression = snd <$> applicationExpressionWithInfo
@@ -678,7 +678,7 @@
 
                     let fourCharacterEscapeSequence = do
                             ns <- Control.Monad.replicateM 4 hexNumber
-                            
+
                             let number = toNumber ns
 
                             Control.Monad.guard (validCodepoint number)
@@ -883,7 +883,7 @@
 
                     whitespace
 
-                    let combine k = liftA2 $ \rf rf' -> makeRecordField $ Combine (Just k)
+                    let combine k = liftA2 $ \rf rf' -> makeRecordField $ Combine mempty (Just k)
                                                             (recordFieldValue rf')
                                                             (recordFieldValue rf)
 
diff --git a/src/Dhall/Parser/Token.hs b/src/Dhall/Parser/Token.hs
--- a/src/Dhall/Parser/Token.hs
+++ b/src/Dhall/Parser/Token.hs
@@ -139,8 +139,8 @@
 -- | Returns `True` if the given `Int` is a valid Unicode codepoint
 validCodepoint :: Int -> Bool
 validCodepoint c =
-    not (category == Char.Surrogate 
-      || c .&. 0xFFFE == 0xFFFE 
+    not (category == Char.Surrogate
+      || c .&. 0xFFFE == 0xFFFE
       || c .&. 0xFFFF == 0xFFFF)
   where
     category = Char.generalCategory (Char.chr c)
@@ -266,7 +266,7 @@
     a    <- naturalLiteral
     return (sign (fromIntegral a)) ) <?> "literal"
 
-{-| Parse a `Dhall.Syntax.Natural` literal 
+{-| Parse a `Dhall.Syntax.Natural` literal
 
     This corresponds to the @natural-literal@ rule from the official grammar
 -}
@@ -1221,32 +1221,40 @@
 _importAlt = operatorChar '?'
 
 -- | Parse the record combine operator (@/\\@ or @∧@)
-_combine :: Parser ()
-_combine = (void (char '∧' <?> "\"∧\"") <|> void (text "/\\")) <?> "operator"
+_combine :: Parser CharacterSet
+_combine =
+        (Unicode <$ char '∧' <?> "\"∧\"")
+    <|> (ASCII <$ text "/\\" <?> "/\\")
 
 -- | Parse the record type combine operator (@//\\\\@ or @⩓@)
-_combineTypes :: Parser ()
-_combineTypes = (void (char '⩓' <?> "\"⩓\"") <|> void (text "//\\\\")) <?> "operator"
+_combineTypes :: Parser CharacterSet
+_combineTypes =
+        (Unicode <$ char '⩓' <?> "\"⩓\"")
+    <|> (ASCII <$ text "//\\\\" <?> "//\\\\")
 
 -- | Parse the record \"prefer\" operator (@//@ or @⫽@)
-_prefer :: Parser ()
-_prefer = (void (char '⫽' <?> "\"⫽\"") <|> void (text "//")) <?> "operator"
+_prefer :: Parser CharacterSet
+_prefer =
+        (Unicode <$ char '⫽' <?> "\"⫽\"")
+    <|> (ASCII <$ text "//" <?> "//")
 
 -- | Parse a lambda (@\\@ or @λ@)
-_lambda :: Parser ()
-_lambda = void (Text.Parser.Char.satisfy predicate) <?> "\\"
-  where
-    predicate 'λ'  = True
-    predicate '\\' = True
-    predicate _    = False
+_lambda :: Parser CharacterSet
+_lambda =
+        (Unicode <$ char 'λ' <?> "\"λ\"")
+    <|> (ASCII <$ char '\\' <?> "\\")
 
 -- | Parse a forall (@forall@ or @∀@)
-_forall :: Parser ()
-_forall = (void (char '∀' <?> "\"∀\"") <|> void (text "forall")) <?> "forall"
+_forall :: Parser CharacterSet
+_forall =
+        (Unicode <$ char '∀' <?> "\"∀\"")
+    <|> (ASCII <$ text "forall" <?> "forall")
 
 -- | Parse a right arrow (@->@ or @→@)
-_arrow :: Parser ()
-_arrow = (void (char '→' <?> "\"→\"") <|> void (text "->")) <?> "->"
+_arrow :: Parser CharacterSet
+_arrow =
+        (Unicode <$ char '→' <?> "\"→\"")
+    <|> (ASCII <$ text "->" <?> "->")
 
 -- | Parse a double colon (@::@)
 _doubleColon :: Parser ()
diff --git a/src/Dhall/Pretty.hs b/src/Dhall/Pretty.hs
--- a/src/Dhall/Pretty.hs
+++ b/src/Dhall/Pretty.hs
@@ -8,6 +8,7 @@
     , prettyExpr
 
     , CharacterSet(..)
+    , detectCharacterSet
     , prettyCharacterSet
 
     , Dhall.Pretty.Internal.layout
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
@@ -1,7 +1,11 @@
-{-# LANGUAGE LambdaCase        #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards   #-}
-{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE DeriveLift         #-}
+{-# LANGUAGE LambdaCase         #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RecordWildCards    #-}
+{-# LANGUAGE ViewPatterns       #-}
 
 {-# OPTIONS_GHC -Wall #-}
 
@@ -16,6 +20,7 @@
     , prettySrcExpr
 
     , CharacterSet(..)
+    , detectCharacterSet
     , prettyCharacterSet
     , prettyImportExpression
 
@@ -65,14 +70,21 @@
     , rparen
     ) where
 
+import Control.DeepSeq            (NFData)
+import Data.Aeson                 (FromJSON (..), Value (String))
+import Data.Aeson.Types           (typeMismatch, unexpected)
+import Data.Data                  (Data)
 import Data.Foldable
-import Data.List.NonEmpty        (NonEmpty (..))
-import Data.Text                 (Text)
-import Data.Text.Prettyprint.Doc (Doc, Pretty, space)
-import Dhall.Map                 (Map)
-import Dhall.Src                 (Src (..))
+import Data.List.NonEmpty         (NonEmpty (..))
+import Data.Text                  (Text)
+import Data.Text.Prettyprint.Doc  (Doc, Pretty, space)
+import Dhall.Map                  (Map)
+import Dhall.Optics               (cosmosOf, foldOf, to)
+import Dhall.Src                  (Src (..))
 import Dhall.Syntax
-import Numeric.Natural           (Natural)
+import GHC.Generics               (Generic)
+import Language.Haskell.TH.Syntax (Lift)
+import Numeric.Natural            (Natural)
 
 import qualified Data.Char
 import qualified Data.HashSet
@@ -110,8 +122,39 @@
 annToAnsiStyle Operator = Terminal.bold <> Terminal.colorDull Terminal.Green
 
 -- | This type determines whether to render code as `ASCII` or `Unicode`
-data CharacterSet = ASCII | Unicode deriving Show
+data CharacterSet = ASCII | Unicode
+    deriving (Eq, Ord, Show, Data, Generic, Lift, NFData)
 
+-- | Since ASCII is a subset of Unicode, if either argument is Unicode, the
+-- result is Unicode
+instance Semigroup CharacterSet where
+    Unicode <> _ = Unicode
+    _ <> other = other
+
+instance Monoid CharacterSet where
+    mempty = ASCII
+
+instance FromJSON CharacterSet where
+  parseJSON (String "unicode") = pure Unicode
+  parseJSON (String "ascii") = pure ASCII
+  parseJSON v@(String _) = unexpected v
+  parseJSON v = typeMismatch "String" v
+
+-- | Detect which character set is used for the syntax of an expression
+-- 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)
+  where
+    exprToCharacterSet = \case
+        Embed _ -> mempty -- Don't go down the embed route, otherwise: <<loop>>
+        Lam (Just Unicode) _ _ -> Unicode
+        Pi (Just Unicode) _ _ _ -> Unicode
+        Combine (Just Unicode) _ _ _ -> Unicode
+        CombineTypes (Just Unicode) _ _ -> Unicode
+        Prefer (Just Unicode) _ _ _ -> Unicode
+        _ -> mempty
+
 -- | Pretty print an expression
 prettyExpr :: Pretty a => Expr s a -> Doc Ann
 prettyExpr = prettySrcExpr . denote
@@ -600,10 +643,10 @@
     prettyCompleteExpression expression =
         Pretty.group (prettyExpression expression)
 
-    prettyExpression a0@(Lam _ _) =
+    prettyExpression a0@(Lam _ _ _) =
         arrows characterSet (docs a0)
       where
-        docs (Lam (FunctionBinding { functionBindingVariable = a, functionBindingAnnotation = b }) c) =
+        docs (Lam _ (FunctionBinding { functionBindingVariable = a, functionBindingAnnotation = b }) c) =
             Pretty.group (Pretty.flatAlt long short) : docs c
           where
             long =  (lambda characterSet <> space)
@@ -736,11 +779,11 @@
             ( keyword "in" <> " " <> prettyExpression b
             , keyword "in" <> "  "  <> prettyExpression b
             )
-    prettyExpression a0@(Pi _ _ _) =
+    prettyExpression a0@(Pi _ _ _ _) =
         arrows characterSet (docs a0)
       where
-        docs (Pi "_" b c) = prettyOperatorExpression b : docs c
-        docs (Pi a   b c) = Pretty.group (Pretty.flatAlt long short) : docs c
+        docs (Pi _ "_" b c) = prettyOperatorExpression b : docs c
+        docs (Pi _ a   b c) = Pretty.group (Pretty.flatAlt long short) : docs c
           where
             long =  forall characterSet <> space
                 <>  Pretty.align
@@ -1024,10 +1067,10 @@
             prettyCombineExpression a
 
     prettyCombineExpression :: Pretty a => Expr Src a -> Doc Ann
-    prettyCombineExpression a0@(Combine _ _ _) =
+    prettyCombineExpression a0@(Combine _ _ _ _) =
         prettyOperator (combine characterSet) (docs a0)
       where
-        docs (Combine _ a b) = prettyPreferExpression b : docs a
+        docs (Combine _ _ a b) = prettyPreferExpression b : docs a
         docs a
             | Just doc <- preserveSource a =
                 [ doc ]
@@ -1047,7 +1090,7 @@
     prettyPreferExpression a0@(Prefer {}) =
         prettyOperator (prefer characterSet) (docs a0)
       where
-        docs (Prefer _ a b) = prettyCombineTypesExpression b : docs a
+        docs (Prefer _ _ a b) = prettyCombineTypesExpression b : docs a
         docs a
             | Just doc <- preserveSource a =
                 [ doc ]
@@ -1064,10 +1107,10 @@
             prettyCombineTypesExpression a
 
     prettyCombineTypesExpression :: Pretty a => Expr Src a -> Doc Ann
-    prettyCombineTypesExpression a0@(CombineTypes _ _) =
+    prettyCombineTypesExpression a0@(CombineTypes _ _ _) =
         prettyOperator (combineTypes characterSet) (docs a0)
       where
-        docs (CombineTypes a b) = prettyTimesExpression b : docs a
+        docs (CombineTypes _ a b) = prettyTimesExpression b : docs a
         docs a
             | Just doc <- preserveSource a =
                 [ doc ]
@@ -1679,7 +1722,7 @@
         , [ KeyValue keys mSrc2' val' ] <- concatMap adapt (Map.toList m) =
             [ KeyValue (NonEmpty.cons (mSrc0, key, mSrc1) keys) mSrc2' val' ]
 
-        | Combine (Just _) l r <- e =
+        | Combine _ (Just _) l r <- e =
             adapt (key, makeRecordField l) <> adapt (key, makeRecordField r)
         | otherwise =
             [ KeyValue (pure (mSrc0, key, mSrc1)) mSrc2 val ]
diff --git a/src/Dhall/Pretty/Internal.hs-boot b/src/Dhall/Pretty/Internal.hs-boot
--- a/src/Dhall/Pretty/Internal.hs-boot
+++ b/src/Dhall/Pretty/Internal.hs-boot
@@ -1,12 +1,26 @@
 module Dhall.Pretty.Internal where
 
+import Control.DeepSeq (NFData)
+import Data.Data (Data)
 import Data.Text (Text)
 import Data.Text.Prettyprint.Doc (Pretty, Doc)
 import Dhall.Src (Src)
+import Language.Haskell.TH.Syntax (Lift)
 
 import {-# SOURCE #-} Dhall.Syntax
 
 data Ann
+
+data CharacterSet = ASCII | Unicode
+
+instance Eq CharacterSet
+instance Ord CharacterSet
+instance Show CharacterSet
+instance Data CharacterSet
+instance Lift CharacterSet
+instance NFData CharacterSet
+instance Semigroup CharacterSet
+instance Monoid CharacterSet
 
 prettyVar :: Var -> Doc Ann
 
diff --git a/src/Dhall/Schemas.hs b/src/Dhall/Schemas.hs
--- a/src/Dhall/Schemas.hs
+++ b/src/Dhall/Schemas.hs
@@ -17,11 +17,12 @@
 
 import Control.Applicative (empty)
 import Control.Exception   (Exception)
+import Data.Maybe          (fromMaybe)
 import Data.Text           (Text)
 import Data.Void           (Void)
 import Dhall.Crypto        (SHA256Digest)
 import Dhall.Map           (Map)
-import Dhall.Pretty        (CharacterSet (..))
+import Dhall.Pretty        (CharacterSet (..), detectCharacterSet)
 import Dhall.Src           (Src)
 import Dhall.Syntax        (Expr (..), Import, Var (..))
 import Dhall.Util
@@ -57,11 +58,11 @@
 
 -- | Arguments to the @rewrite-with-schemas@ subcommand
 data Schemas = Schemas
-    { characterSet :: CharacterSet
-    , censor       :: Censor
-    , input        :: Input
-    , outputMode   :: OutputMode
-    , schemas      :: Text
+    { chosenCharacterSet :: Maybe CharacterSet
+    , censor             :: Censor
+    , input              :: Input
+    , outputMode         :: OutputMode
+    , schemas            :: Text
     }
 
 -- | Implementation of the @dhall rewrite-with-schemas@ subcommand
@@ -72,6 +73,8 @@
         StandardInput  -> Text.IO.getContents
 
     (Header header, expression) <- Util.getExpressionAndHeaderFromStdinText censor originalText
+
+    let characterSet = fromMaybe (detectCharacterSet expression) chosenCharacterSet
 
     schemasRecord <- Core.throws (Parser.exprFromText "(schemas)" schemas)
 
diff --git a/src/Dhall/Syntax.hs b/src/Dhall/Syntax.hs
--- a/src/Dhall/Syntax.hs
+++ b/src/Dhall/Syntax.hs
@@ -1,16 +1,17 @@
-{-# LANGUAGE DeriveAnyClass     #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE DeriveLift         #-}
-{-# LANGUAGE DeriveTraversable  #-}
-{-# LANGUAGE LambdaCase         #-}
-{-# LANGUAGE OverloadedLists    #-}
-{-# LANGUAGE OverloadedStrings  #-}
-{-# LANGUAGE PatternSynonyms    #-}
-{-# LANGUAGE RankNTypes         #-}
-{-# LANGUAGE RecordWildCards    #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE UnicodeSyntax      #-}
+{-# LANGUAGE DeriveAnyClass             #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DeriveLift                 #-}
+{-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE GeneralisedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE OverloadedLists            #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RecordWildCards            #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE UnicodeSyntax              #-}
 
 {-| This module contains the core syntax types and optics for them.
 
@@ -24,6 +25,7 @@
     , Var(..)
     , Binding(..)
     , makeBinding
+    , CharacterSet(..)
     , Chunks(..)
     , DhallDouble(..)
     , PreferAnnotation(..)
@@ -225,7 +227,8 @@
 -- | This wrapper around 'Prelude.Double' exists for its 'Eq' instance which is
 -- defined via the binary encoding of Dhall @Double@s.
 newtype DhallDouble = DhallDouble { getDhallDouble :: Double }
-    deriving (Show, Data, Lift, NFData, Generic)
+    deriving stock (Show, Data, Lift, Generic)
+    deriving anyclass NFData
 
 -- | This instance satisfies all the customary 'Eq' laws except substitutivity.
 --
@@ -438,10 +441,10 @@
     --   > Var (V x n)                              ~  x@n
     | Var Var
     -- | > Lam (FunctionBinding _ "x" _ _ A) b      ~  λ(x : A) -> b
-    | Lam (FunctionBinding s a) (Expr s a)
+    | Lam (Maybe CharacterSet) (FunctionBinding s a) (Expr s a)
     -- | > Pi "_" A B                               ~        A  -> B
     --   > Pi x   A B                               ~  ∀(x : A) -> B
-    | Pi  Text (Expr s a) (Expr s a)
+    | Pi  (Maybe CharacterSet) Text (Expr s a) (Expr s a)
     -- | > App f a                                  ~  f a
     | App (Expr s a) (Expr s a)
     -- | > Let (Binding _ x _  Nothing  _ r) e      ~  let x     = r in e
@@ -588,14 +591,14 @@
     --   >              _
     --   >              (Combine (Just k) x y)
     --   >            )]
-    | Combine (Maybe Text) (Expr s a) (Expr s a)
+    | Combine (Maybe CharacterSet) (Maybe Text) (Expr s a) (Expr s a)
     -- | > CombineTypes x y                         ~  x ⩓ y
-    | CombineTypes (Expr s a) (Expr s a)
+    | CombineTypes (Maybe CharacterSet) (Expr s a) (Expr s a)
     -- | > Prefer False x y                         ~  x ⫽ y
     --
     -- The first field is a `True` when the `Prefer` operator is introduced as a
     -- result of desugaring a @with@ expression
-    | Prefer (PreferAnnotation s a) (Expr s a) (Expr s a)
+    | Prefer (Maybe CharacterSet) (PreferAnnotation s a) (Expr s a) (Expr s a)
     -- | > RecordCompletion x y                     ~  x::y
     | RecordCompletion (Expr s a) (Expr s a)
     -- | > Merge x y (Just t )                      ~  merge x y : t
@@ -648,7 +651,7 @@
   fmap f (Note s e1) = Note s (fmap f e1)
   fmap f (Record a) = Record $ fmap f <$> a
   fmap f (RecordLit a) = RecordLit $ fmap f <$> a
-  fmap f (Lam fb e) = Lam (f <$> fb) (f <$> e)
+  fmap f (Lam cs fb e) = Lam cs (f <$> fb) (f <$> e)
   fmap f (Field a b) = Field (f <$> a) b
   fmap f expression = Lens.over unsafeSubExpressions (fmap f) expression
   {-# INLINABLE fmap #-}
@@ -667,7 +670,7 @@
         Note a b    -> Note a (b >>= k)
         Record a    -> Record $ bindRecordKeyValues <$> a
         RecordLit a -> RecordLit $ bindRecordKeyValues <$> a
-        Lam a b     -> Lam (adaptFunctionBinding a) (b >>= k)
+        Lam cs a b  -> Lam cs (adaptFunctionBinding a) (b >>= k)
         Field a b   -> Field (a >>= k) b
         _ -> Lens.over unsafeSubExpressions (>>= k) expression
       where
@@ -688,7 +691,7 @@
     first k (Let a b    ) = Let (first k a) (first k b)
     first k (Record a   ) = Record $ first k <$> a
     first k (RecordLit a) = RecordLit $ first k <$> a
-    first k (Lam a b    ) = Lam (first k a) (first k b)
+    first k (Lam cs a b ) = Lam cs (first k a) (first k b)
     first k (Field a b  ) = Field (first k a) (k <$> b)
     first k  expression  = Lens.over unsafeSubExpressions (first k) expression
 
@@ -759,7 +762,7 @@
 subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b
 subExpressions f (Record a) = Record <$> traverse (recordFieldExprs f) a
 subExpressions f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a
-subExpressions f (Lam fb e) = Lam <$> functionBindingExprs f fb <*> f e
+subExpressions f (Lam cs fb e) = Lam cs <$> functionBindingExprs f fb <*> f e
 subExpressions f (Field a b) = Field <$> f a <*> pure b
 subExpressions f expression = unsafeSubExpressions f expression
 {-# INLINABLE subExpressions #-}
@@ -775,7 +778,7 @@
     :: Applicative f => (Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b)
 unsafeSubExpressions _ (Const c) = pure (Const c)
 unsafeSubExpressions _ (Var v) = pure (Var v)
-unsafeSubExpressions f (Pi a b c) = Pi a <$> f b <*> f c
+unsafeSubExpressions f (Pi cs a b c) = Pi cs a <$> f b <*> f c
 unsafeSubExpressions f (App a b) = App <$> f a <*> f b
 unsafeSubExpressions f (Annot a b) = Annot <$> f a <*> f b
 unsafeSubExpressions _ Bool = pure Bool
@@ -826,9 +829,9 @@
 unsafeSubExpressions f (Some a) = Some <$> f a
 unsafeSubExpressions _ None = pure None
 unsafeSubExpressions f (Union a) = Union <$> traverse (traverse f) a
-unsafeSubExpressions f (Combine a b c) = Combine a <$> f b <*> f c
-unsafeSubExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b
-unsafeSubExpressions f (Prefer a b c) = Prefer <$> a' <*> f b <*> f c
+unsafeSubExpressions f (Combine cs a b c) = Combine cs a <$> f b <*> f c
+unsafeSubExpressions f (CombineTypes cs a b) = CombineTypes cs <$> f a <*> f b
+unsafeSubExpressions f (Prefer cs a b c) = Prefer cs <$> a' <*> f b <*> f c
   where
     a' = case a of
         PreferFromSource     -> pure PreferFromSource
@@ -918,7 +921,8 @@
     @Directory { components = [ "baz", "bar", "foo" ] }@
 -}
 newtype Directory = Directory { components :: [Text] }
-    deriving (Eq, Generic, Ord, Show, NFData)
+    deriving stock (Eq, Generic, Ord, Show)
+    deriving anyclass NFData
 
 instance Semigroup Directory where
     Directory components₀ <> Directory components₁ =
@@ -1117,15 +1121,20 @@
     ||  c == '\x7E'
 
 -- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)
+--
+-- This also remove CharacterSet annotations.
 denote :: Expr s a -> Expr t a
 denote = \case
-    Note _ b      -> denote b
-    Let a b       -> Let (denoteBinding a) (denote b)
-    Embed a       -> Embed a
-    Combine _ b c -> Combine Nothing (denote b) (denote c)
+    Note _ b -> denote b
+    Let a b -> Let (denoteBinding a) (denote b)
+    Embed a -> Embed a
+    Combine _ _ b c -> Combine Nothing Nothing (denote b) (denote c)
+    CombineTypes _ b c -> CombineTypes Nothing (denote b) (denote c)
+    Prefer _ a b c -> Lens.over unsafeSubExpressions denote $ Prefer Nothing a b c
     Record a -> Record $ denoteRecordField <$> a
     RecordLit a -> RecordLit $ denoteRecordField <$> a
-    Lam a b -> Lam (denoteFunctionBinding a) (denote b)
+    Lam _ a b -> Lam Nothing (denoteFunctionBinding a) (denote b)
+    Pi _ t a b -> Pi Nothing t (denote a) (denote b)
     Field a (FieldSelection _ b _) -> Field (denote a) (FieldSelection Nothing b Nothing)
     expression -> Lens.over unsafeSubExpressions denote expression
   where
@@ -1376,14 +1385,14 @@
 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 (FunctionBinding src0 x' src1 src2 _A) b) =
-    Lam (FunctionBinding src0 x' src1 src2 _A') b'
+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 x' _A _B) = Pi x' _A' _B'
+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
@@ -1407,6 +1416,7 @@
     rewrite e@(With record (key :| []) value) =
         Just
             (Prefer
+                mempty
                 (PreferFromWith e)
                 record
                 (RecordLit [ (key, makeRecordField value) ])
@@ -1415,7 +1425,7 @@
         Just
             (Let
                 (makeBinding "_" record)
-                (Prefer (PreferFromWith e) "_"
+                (Prefer mempty (PreferFromWith e) "_"
                     (RecordLit
                         [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ]
                     )
diff --git a/src/Dhall/TH.hs b/src/Dhall/TH.hs
--- a/src/Dhall/TH.hs
+++ b/src/Dhall/TH.hs
@@ -128,7 +128,7 @@
         _   | Just haskellType <- List.find predicate haskellTypes -> do
                 let name = Syntax.mkName (Text.unpack (typeName haskellType))
 
-                return (ConT name) 
+                return (ConT name)
             | otherwise -> do
             let document =
                     mconcat
diff --git a/src/Dhall/TypeCheck.hs b/src/Dhall/TypeCheck.hs
--- a/src/Dhall/TypeCheck.hs
+++ b/src/Dhall/TypeCheck.hs
@@ -188,7 +188,7 @@
 {-| `typeWithA` is implemented internally in terms of @infer@ in order to speed
     up equivalence checking.
 
-    Specifically, we extend the `Context` to become a @Ctx@, which can store 
+    Specifically, we extend the `Context` to become a @Ctx@, which can store
     the entire contents of a `let` expression (i.e. the type *and* the value
     of the bound variable).  By storing this extra information in the @Ctx@ we
     no longer need to substitute `let` expressions at all (which is very
@@ -228,7 +228,7 @@
 
             go types n0
 
-        Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b -> do
+        Lam _ (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b -> do
             tA' <- loop ctx _A
 
             case tA' of
@@ -251,7 +251,7 @@
 
             return (VHPi x _A' (\u -> Eval.eval (Extend values x u) _B''))
 
-        Pi x _A _B -> do
+        Pi _ x _A _B -> do
             tA' <- loop ctx _A
 
             kA <- case tA' of
@@ -767,7 +767,7 @@
 
             Max c <- fmap Foldable.fold (Dhall.Map.unorderedTraverseWithKey process xTs)
             return (VConst c)
-        Combine mk l r -> do
+        Combine _ mk l r -> do
             _L' <- loop ctx l
 
             let l'' = quote names (eval values l)
@@ -816,7 +816,7 @@
 
             combineTypes [] xLs' xRs'
 
-        CombineTypes l r -> do
+        CombineTypes _ l r -> do
             _L' <- loop ctx l
 
             let l' = eval values l
@@ -863,7 +863,7 @@
 
             return (VConst c)
 
-        Prefer a l r -> do
+        Prefer _ a l r -> do
             _L' <- loop ctx l
 
             _R' <- loop ctx r
@@ -898,13 +898,13 @@
             _L' <- loop ctx l
 
             case _L' of
-                VRecord xLs' 
+                VRecord xLs'
                   | not (Dhall.Map.member "default" xLs')
                      -> die (InvalidRecordCompletion "default" l)
                   | not (Dhall.Map.member "Type" xLs')
                      -> die (InvalidRecordCompletion "Type" l)
                   | otherwise
-                     -> loop ctx (Annot (Prefer PreferFromCompletion (Field l def) r) (Field l typ))
+                     -> loop ctx (Annot (Prefer mempty PreferFromCompletion (Field l def) r) (Field l typ))
                 _ -> die (CompletionSchemaMustBeARecord l (quote names _L'))
 
               where
@@ -2582,11 +2582,11 @@
         txt0 = insert expr0
         txt1 = insert expr1
 
-prettyTypeMessage (CompletionSchemaMustBeARecord expr0 expr1) = ErrorMessages {..} 
+prettyTypeMessage (CompletionSchemaMustBeARecord expr0 expr1) = ErrorMessages {..}
  where
-   short = "The completion schema must be a record" 
+   short = "The completion schema must be a record"
 
-   long = 
+   long =
         "Explanation: You can complete records using the ❰::❱ operator:                  \n\
         \                                                                                \n\
         \    ┌─────────────────────────────────────────────────────────────────────────┐ \n\
@@ -2606,11 +2606,11 @@
         txt0 = insert expr0
         txt1 = insert expr1
 
-prettyTypeMessage (InvalidRecordCompletion fieldName expr0) = ErrorMessages {..} 
+prettyTypeMessage (InvalidRecordCompletion fieldName expr0) = ErrorMessages {..}
  where
    short = "Completion schema is missing a field: " <> pretty fieldName
 
-   long = 
+   long =
         "Explanation: You can complete records using the ❰::❱ operator like this:\n\
         \                                                                                \n\
         \    ┌─────────────────────────────────────────────────────────────────────────┐ \n\
@@ -3213,7 +3213,7 @@
   where
     short = case Data.Set.toList ks of
          []       -> "Missing handler: " <> Dhall.Pretty.Internal.prettyLabel exemplar
-         xs@(_:_) -> "Missing handlers: " <> (Pretty.hsep . Pretty.punctuate Pretty.comma 
+         xs@(_:_) -> "Missing handlers: " <> (Pretty.hsep . Pretty.punctuate Pretty.comma
                                              . map Dhall.Pretty.Internal.prettyLabel $ exemplar:xs)
 
     long =
@@ -4589,9 +4589,9 @@
         MustUpdateARecord <$> f a <*> f b <*> f c
     MustCombineARecord a b c ->
         MustCombineARecord <$> pure a <*> f b <*> f c
-    InvalidRecordCompletion a l -> 
+    InvalidRecordCompletion a l ->
         InvalidRecordCompletion a <$> f l
-    CompletionSchemaMustBeARecord l r -> 
+    CompletionSchemaMustBeARecord l r ->
         CompletionSchemaMustBeARecord <$> f l <*> f r
     CombineTypesRequiresRecordType a b ->
         CombineTypesRequiresRecordType <$> f a <*> f b
diff --git a/tests/Dhall/Test/Dhall.hs b/tests/Dhall/Test/Dhall.hs
--- a/tests/Dhall/Test/Dhall.hs
+++ b/tests/Dhall/Test/Dhall.hs
@@ -13,21 +13,22 @@
 
 module Dhall.Test.Dhall where
 
-import Control.Exception    (SomeException, try)
-import Data.Fix             (Fix (..))
-import Data.Functor.Classes (Eq1(..), Show1(..))
-import Data.List.NonEmpty   (NonEmpty (..))
-import Data.Maybe           (isJust)
-import Data.Scientific      (Scientific)
-import Data.Sequence        (Seq)
-import Data.Text            (Text)
-import Data.Vector          (Vector)
-import Data.Void            (Void)
-import Dhall                (FromDhall, ToDhall)
-import Dhall.Core           (Expr (..))
-import GHC.Generics         (Generic, Rep)
-import Numeric.Natural      (Natural)
-import System.Timeout       (timeout)
+import Control.Exception      (SomeException, throwIO, try)
+import Data.Either.Validation (validationToEither)
+import Data.Fix               (Fix (..))
+import Data.Functor.Classes   (Eq1(..), Show1(..))
+import Data.List.NonEmpty     (NonEmpty (..))
+import Data.Maybe             (isJust)
+import Data.Scientific        (Scientific)
+import Data.Sequence          (Seq)
+import Data.Text              (Text)
+import Data.Vector            (Vector)
+import Data.Void              (Void)
+import Dhall                  (FromDhall, ToDhall)
+import Dhall.Core             (Expr (..))
+import GHC.Generics           (Generic, Rep)
+import Numeric.Natural        (Natural)
+import System.Timeout         (timeout)
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -43,7 +44,7 @@
    = LitF Natural
    | AddF expr expr
    | MulF expr expr
-   deriving (Eq, Functor, Generic, FromDhall, Show)
+   deriving (Eq, Functor, Generic, FromDhall, ToDhall, Show)
 
 instance Eq1 ExprF where
     liftEq _  (LitF aL) (LitF aR) = aL == aR
@@ -91,14 +92,15 @@
   let expectedMsg =
         "\ESC[1;31mError\ESC[0m: Invalid Dhall.Decoder                                               \n\
         \                                                                                \n\
-        \Every Decoder must provide an extract function that succeeds if an expression   \n\
-        \matches the expected type.  You provided a Decoder that disobeys this contract  \n\
+        \Every Decoder must provide an extract function that does not fail with a type   \n\
+        \error if an expression matches the expected type.  You provided a Decoder that  \n\
+        \disobeys this contract                                                          \n\
         \                                                                                \n\
         \The Decoder provided has the expected dhall type:                               \n\
         \                                                                                \n\
         \↳ { bar : Natural, foo : Text }\n\
         \                                                                                \n\
-        \and it couldn't extract a value from the well-typed expression:                 \n\
+        \and it threw a type error during extraction from the well-typed expression:     \n\
         \                                                                                \n\
         \↳ { bar = 0, foo = \"foo\" }\n\
         \                                                                                \n"
@@ -141,6 +143,11 @@
 shouldHaveWorkingRecursiveFromDhall = testGroup "recursive FromDhall instance"
     [ testCase "works for a recursive expression" $ do
         actual <- Dhall.input Dhall.auto "./tests/recursive/expr0.dhall"
+
+        expected @=? actual
+    , testCase "roundtrips (one-way)" $ do
+        let expr = Dhall.embed Dhall.inject expected
+        actual <- either throwIO pure . validationToEither . Dhall.extract Dhall.auto $ expr
 
         expected @=? actual
     , testCase "passes a shadowing sanity check" $ do
diff --git a/tests/Dhall/Test/Normalization.hs b/tests/Dhall/Test/Normalization.hs
--- a/tests/Dhall/Test/Normalization.hs
+++ b/tests/Dhall/Test/Normalization.hs
@@ -67,7 +67,7 @@
     let tyCtx =
             Context.insert
                 "min"
-                (Pi "_" Natural (Pi "_" Natural Natural))
+                (Pi mempty "_" Natural (Pi mempty "_" Natural Natural))
                 Context.empty
 
         valCtx e =
diff --git a/tests/Dhall/Test/QuickCheck.hs b/tests/Dhall/Test/QuickCheck.hs
--- a/tests/Dhall/Test/QuickCheck.hs
+++ b/tests/Dhall/Test/QuickCheck.hs
@@ -305,8 +305,8 @@
             standardizedExpression
       where
         customGens
-            :: ConstrGen "Lam" 0 (FunctionBinding s a)
-            :+ ConstrGen "Pi" 0 Text
+            :: ConstrGen "Lam" 1 (FunctionBinding s a)
+            :+ ConstrGen "Pi" 1 Text
             :+ ConstrGen "Field" 1 (FieldSelection s)
             :+ ConstrGen "Project" 1 (Either [Text] (Expr s a))
             :+ Gen Integer  -- Generates all Integer fields in Expr
@@ -417,13 +417,13 @@
     Data.Sequence.null xs
 standardizedExpression (Note _ _) =
     False
-standardizedExpression (Combine (Just _) _ _) =
+standardizedExpression (Combine _ (Just _) _ _) =
     False
 standardizedExpression With{} =
     False
-standardizedExpression (Prefer PreferFromCompletion _ _) =
+standardizedExpression (Prefer _ PreferFromCompletion _ _) =
     False
-standardizedExpression (Prefer (PreferFromWith _) _ _) =
+standardizedExpression (Prefer _ (PreferFromWith _) _ _) =
     False
 -- The following three expressions are valid ASTs, but they can never be parsed,
 -- because the annotation will associate with `Merge`/`ListLit`/`ToMap` with