dhall 1.8.2 → 1.9.0

raw patch · 30 files changed

+890/−452 lines, 30 filesdep +deepseqdep ~prettyprinterdep ~tastyPVP ok

version bump matches the API change (PVP)

Dependencies added: deepseq

Dependency ranges changed: prettyprinter, tasty

API changes (from Hackage documentation)

Files

• CHANGELOG.md +42/−0
• dhall-format/Main.hs +0/−1
• dhall.cabal +7/−2
• src/Dhall.hs +88/−9
• src/Dhall/Core.hs +292/−150
• src/Dhall/Import.hs +73/−52
• src/Dhall/Parser.hs +56/−60
• src/Dhall/Tutorial.hs +42/−44
• src/Dhall/TypeCheck.hs +164/−132
• tests/Parser.hs +3/−0
• tests/Regression.hs +42/−0
• tests/Tutorial.hs +16/−0
• tests/Util.hs +7/−0
• tests/parser/constructors.dhall +1/−0
• tests/parser/quotedLabel.dhall +1/−2
• tests/regression/issue201.dhall +1/−0
• tests/regression/issue209.dhall +1/−0
• tests/regression/issue216a.dhall +5/−0
• tests/regression/issue216b.dhall +10/−0
• tests/tutorial/process.dhall +6/−0
• tests/tutorial/unions0A.dhall +1/−0
• tests/tutorial/unions0B.dhall +1/−0
• tests/tutorial/unions1A.dhall +1/−0
• tests/tutorial/unions1B.dhall +1/−0
• tests/tutorial/unions2A.dhall +8/−0
• tests/tutorial/unions2B.dhall +5/−0
• tests/tutorial/unions3A.dhall +5/−0
• tests/tutorial/unions3B.dhall +4/−0
• tests/tutorial/unions4A.dhall +1/−0
• tests/tutorial/unions4B.dhall +6/−0

@@ -1,3 +1,45 @@+1.9.0++* Feature: BREAKING CHANGE TO LANGUAGE AND API: Add `constructors` keyword+    * This new keyword generates constructors from a union type+        * See the updated Haskell tutorial for more details+    * This means that `constructors` is now a reserved keyword+    * This adds a new `Constructors` constructor to the `Expr` type+    * See: https://github.com/dhall-lang/dhall-haskell/pull/199+* Feature: BREAKING CHANGE TO THE API: `dhall-format` preserves interpolation+    * This changes the `TextLit` constructor to represent an interpolated `Text`+      literal+    * See: https://github.com/dhall-lang/dhall-haskell/pull/220+* Feature: You can now define type synonyms using `let`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/202+* Feature: Extend valid set of quoted labels+    * See: https://github.com/dhall-lang/dhall-lang/pull/65+    * See: https://github.com/dhall-lang/dhall-lang/pull/77+* Performance: Improve startup time when importing files, but not URLs+    * See: https://github.com/dhall-lang/dhall-haskell/pull/194+* Security: `localhost`/`127.0.0.1` imports no longer count as local imports+    * Specifically: they cannot import environment variables or files+    * See: https://github.com/dhall-lang/dhall-haskell/pull/197+* Security: Fix potential type-checking bug+    * See: https://github.com/dhall-lang/dhall-haskell/pull/198+* Fix: BREAKING CHANGE TO API: Improve localization of error messages+    * This required fixing the type of `normalize`/`shift`/`subst` to preserve+      the first type parameter of `Expr` (i.e. they no longer delete `Note`+      constructors)+    * A new `denote` function was added for the explicit purpose of deleting+      `Note` constructors+    * See: https://github.com/dhall-lang/dhall-haskell/pull/218+* Expose `MissingEnvironmentVariable` exception type+    * See: https://github.com/dhall-lang/dhall-haskell/pull/196+* Add `genericAuto`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/195+* Add `inputWith`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/222+* Add`loadWithContext`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/215+* Add `pair`/`unit`/`string`/`list`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/227+ 1.8.2  * Add `typeWithA` for type-checking custom `Embed`ded values

@@ -20,7 +20,6 @@           subexpressions then you will need to split them into a separate           file for now     * Preserving multi-line strings (this reduces them to ordinary strings)-    * Preserving string interpolation (this expands interpolation to @++@)      See the @Dhall.Tutorial@ module for example usage -}

@@ -1,5 +1,5 @@ Name: dhall-Version: 1.8.2+Version: 1.9.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1@@ -83,6 +83,7 @@     Prelude/Text/concatSep     tests/parser/*.dhall     tests/regression/*.dhall+    tests/tutorial/*.dhall  Source-Repository head     Type: git@@ -162,6 +163,8 @@         optparse-generic >= 1.1.1    && < 1.3,         trifecta         >= 1.6      && < 1.8,         text             >= 0.11.1.0 && < 1.3+    Other-Modules:+        Paths_dhall  Test-Suite test     Type: exitcode-stdio-1.0@@ -178,8 +181,10 @@     Build-Depends:         base               >= 4        && < 5   ,         containers         >= 0.5.0.0  && < 0.6 ,+        deepseq            >= 1.2.0.1  && < 1.5 ,         dhall                                   ,-        tasty              >= 0.11.2   && < 0.13,+        prettyprinter                           ,+        tasty              >= 0.11.2   && < 1.1 ,         tasty-hunit        >= 0.9.2    && < 0.11,         text               >= 0.11.1.0 && < 1.3 ,         vector             >= 0.11.0.0 && < 0.13

@@ -5,6 +5,7 @@ {-# LANGUAGE FlexibleInstances   #-} {-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE RankNTypes          #-} {-# LANGUAGE RecordWildCards     #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving  #-}@@ -18,6 +19,7 @@     (     -- * Input       input+    , inputWith     , detailed      -- * Types@@ -26,6 +28,7 @@     , Interpret(..)     , InvalidType(..)     , auto+    , genericAuto     , InterpretOptions(..)     , defaultInterpretOptions     , bool@@ -36,6 +39,10 @@     , strictText     , maybe     , vector+    , list+    , unit+    , string+    , pair     , GenericInterpret(..)      , Inject(..)@@ -61,7 +68,7 @@ import Data.Typeable (Typeable) import Data.Vector (Vector) import Data.Word (Word8, Word16, Word32, Word64)-import Dhall.Core (Expr(..))+import Dhall.Core (Expr(..), Chunks(..)) import Dhall.Import (Imported(..)) import Dhall.Parser (Src(..)) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)@@ -81,6 +88,7 @@ import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding import qualified Data.Vector+import qualified Dhall.Context import qualified Dhall.Core import qualified Dhall.Import import qualified Dhall.Parser@@ -133,10 +141,26 @@     -- ^ The Dhall program     -> IO a     -- ^ The decoded value in Haskell-input (Type {..}) txt = do+input ty txt =+  inputWith ty Dhall.Context.empty (const Nothing) txt++{-| Extend 'input' with a custom typing context and normalization process.++-}+inputWith+    :: Type a+    -- ^ The type of value to decode from Dhall to Haskell+    -> Dhall.Context.Context (Expr Src X)+    -- ^ The starting context for type-checking+    -> Dhall.Core.Normalizer X+    -> Text+    -- ^ The Dhall program+    -> IO a+    -- ^ The decoded value in Haskell+inputWith (Type {..}) ctx n txt = do     let delta = Directed "(input)" 0 0 0 0     expr  <- throws (Dhall.Parser.exprFromText delta txt)-    expr' <- Dhall.Import.load expr+    expr' <- Dhall.Import.loadWithContext ctx expr     let suffix =             ( Data.ByteString.Lazy.toStrict             . Data.Text.Lazy.Encoding.encodeUtf8@@ -150,8 +174,8 @@                 bytes' = bytes <> " : " <> suffix             _ ->                 Annot expr' expected-    _ <- throws (Dhall.TypeCheck.typeOf annot)-    case extract (Dhall.Core.normalize expr') of+    _ <- throws (Dhall.TypeCheck.typeWith ctx annot)+    case extract (Dhall.Core.normalizeWith n expr') of         Just x  -> return x         Nothing -> Control.Exception.throwIO InvalidType @@ -376,8 +400,8 @@ lazyText :: Type Text lazyText = Type {..}   where-    extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t)-    extract  _          = empty+    extract (TextLit (Chunks [] t)) = pure (Data.Text.Lazy.Builder.toLazyText t)+    extract  _                      = empty      expected = Text @@ -417,6 +441,52 @@      expectedOut = App List expectedIn +{-| Decode a list++>>> input (list integer) "[1, 2, 3]"+[1,2,3]+-}+list :: Type a -> Type [a]+list = fmap Data.Vector.toList . vector++{-| Decode `()` from an empty record.++>>> input unit "{=}"+()+-}+unit :: Type ()+unit = Type extractOut expectedOut+  where+    extractOut (RecordLit fields) | Data.Map.null fields = return ()+    extractOut _ = Nothing++    expectedOut = Record Data.Map.empty++{-| Decode a `String`++>>> input string "\"ABC\""+"ABC"++"-}+string :: Type String+string = Data.Text.Lazy.unpack <$> lazyText++{-| Given a pair of `Type`s, decode a tuple-record into their pairing.++>>> input (pair natural bool) "{ _1 = +42, _2 = False }"+(42, False)+-}+pair :: Type a -> Type b -> Type (a, b)+pair l r = Type extractOut expectedOut+  where+    extractOut (RecordLit fields) =+      (,) <$> ( Data.Map.lookup "_1" fields >>= extract l )+          <*> ( Data.Map.lookup "_2" fields >>= extract r )+    extractOut _ = Nothing++    expectedOut = Record (Data.Map.fromList [("_1", expected l)+                                            ,("_2", expected r)])+ {-| Any value that implements `Interpret` can be automatically decoded based on     the inferred return type of `input` @@ -482,6 +552,14 @@ auto :: Interpret a => Type a auto = autoWith defaultInterpretOptions +{-| `genericAuto` is the default implementation for `auto` if you derive+    `Interpret`.  The difference is that you can use `genericAuto` without+    having to explicitly provide an `Interpret` instance for a type as long as+    the type derives `Generic`+-}+genericAuto :: (Generic a, GenericInterpret (Rep a)) => Type a+genericAuto = fmap to (evalState (genericAutoWith defaultInterpretOptions) 1)+ {-| Use these options to tweak how Dhall derives a generic implementation of     `Interpret` -}@@ -692,14 +770,15 @@ instance Inject Text where     injectWith _ = InputType {..}       where-        embed text = TextLit (Data.Text.Lazy.Builder.fromLazyText text)+        embed text =+            TextLit (Chunks [] (Data.Text.Lazy.Builder.fromLazyText text))          declared = Text  instance Inject Data.Text.Text where     injectWith _ = InputType {..}       where-        embed text = TextLit (Data.Text.Lazy.Builder.fromText text)+        embed text = TextLit (Chunks [] (Data.Text.Lazy.Builder.fromText text))          declared = Text 

@@ -23,6 +23,7 @@     , PathMode(..)     , Path(..)     , Var(..)+    , Chunks(..)     , Expr(..)      -- * Normalization@@ -33,6 +34,7 @@     , shift     , isNormalized     , isNormalizedWith+    , denote      -- * Pretty-printing     , pretty@@ -40,6 +42,7 @@     -- * Miscellaneous     , internalError     , reservedIdentifiers+    , escapeText     ) where  #if MIN_VERSION_base(4,8,0)@@ -276,8 +279,8 @@     | DoubleShow     -- | > Text                                     ~  Text     | Text-    -- | > TextLit t                                ~  t-    | TextLit Builder+    -- | > TextLit (Chunks [(t1, e1), (t2, e2)] t3) ~  "t1${e1}t2${e2}t3"+    | TextLit (Chunks s a)     -- | > TextAppend x y                           ~  x ++ y     | TextAppend (Expr s a) (Expr s a)     -- | > List                                     ~  List@@ -325,6 +328,8 @@     -- | > Merge x y (Just t )                      ~  merge x y : t     -- | > Merge x y  Nothing                       ~  merge x y     | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))+    -- | > Constructors e                           ~  constructors e+    | Constructors (Expr s a)     -- | > Field e x                                ~  e.x     | Field (Expr s a) Text     -- | > Note s x                                 ~  e@@ -341,130 +346,146 @@ instance Monad (Expr s) where     return = pure -    Const a          >>= _ = Const a-    Var a            >>= _ = Var a-    Lam a b c        >>= k = Lam a (b >>= k) (c >>= k)-    Pi  a b c        >>= k = Pi a (b >>= k) (c >>= k)-    App a b          >>= k = App (a >>= k) (b >>= k)-    Let a b c d      >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)-    Annot a b        >>= k = Annot (a >>= k) (b >>= k)-    Bool             >>= _ = Bool-    BoolLit a        >>= _ = BoolLit a-    BoolAnd a b      >>= k = BoolAnd (a >>= k) (b >>= k)-    BoolOr  a b      >>= k = BoolOr  (a >>= k) (b >>= k)-    BoolEQ  a b      >>= k = BoolEQ  (a >>= k) (b >>= k)-    BoolNE  a b      >>= k = BoolNE  (a >>= k) (b >>= k)-    BoolIf a b c     >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)-    Natural          >>= _ = Natural-    NaturalLit a     >>= _ = NaturalLit a-    NaturalFold      >>= _ = NaturalFold-    NaturalBuild     >>= _ = NaturalBuild-    NaturalIsZero    >>= _ = NaturalIsZero-    NaturalEven      >>= _ = NaturalEven-    NaturalOdd       >>= _ = NaturalOdd-    NaturalToInteger >>= _ = NaturalToInteger-    NaturalShow      >>= _ = NaturalShow-    NaturalPlus  a b >>= k = NaturalPlus  (a >>= k) (b >>= k)-    NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)-    Integer          >>= _ = Integer-    IntegerLit a     >>= _ = IntegerLit a-    IntegerShow      >>= _ = IntegerShow-    Double           >>= _ = Double-    DoubleLit a      >>= _ = DoubleLit a-    DoubleShow       >>= _ = DoubleShow-    Text             >>= _ = Text-    TextLit a        >>= _ = TextLit a-    TextAppend a b   >>= k = TextAppend (a >>= k) (b >>= k)-    List             >>= _ = List-    ListLit a b      >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)-    ListAppend a b   >>= k = ListAppend (a >>= k) (b >>= k)-    ListBuild        >>= _ = ListBuild-    ListFold         >>= _ = ListFold-    ListLength       >>= _ = ListLength-    ListHead         >>= _ = ListHead-    ListLast         >>= _ = ListLast-    ListIndexed      >>= _ = ListIndexed-    ListReverse      >>= _ = ListReverse-    Optional         >>= _ = Optional-    OptionalLit a b  >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)-    OptionalFold     >>= _ = OptionalFold-    OptionalBuild    >>= _ = OptionalBuild-    Record    a      >>= k = Record (fmap (>>= k) a)-    RecordLit a      >>= k = RecordLit (fmap (>>= k) a)-    Union     a      >>= k = Union (fmap (>>= k) a)-    UnionLit a b c   >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)-    Combine a b      >>= k = Combine (a >>= k) (b >>= k)-    Prefer a b       >>= k = Prefer (a >>= k) (b >>= k)-    Merge a b c      >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)-    Field a b        >>= k = Field (a >>= k) b-    Note a b         >>= k = Note a (b >>= k)-    Embed a          >>= k = k a+    Const a              >>= _ = Const a+    Var a                >>= _ = Var a+    Lam a b c            >>= k = Lam a (b >>= k) (c >>= k)+    Pi  a b c            >>= k = Pi a (b >>= k) (c >>= k)+    App a b              >>= k = App (a >>= k) (b >>= k)+    Let a b c d          >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)+    Annot a b            >>= k = Annot (a >>= k) (b >>= k)+    Bool                 >>= _ = Bool+    BoolLit a            >>= _ = BoolLit a+    BoolAnd a b          >>= k = BoolAnd (a >>= k) (b >>= k)+    BoolOr  a b          >>= k = BoolOr  (a >>= k) (b >>= k)+    BoolEQ  a b          >>= k = BoolEQ  (a >>= k) (b >>= k)+    BoolNE  a b          >>= k = BoolNE  (a >>= k) (b >>= k)+    BoolIf a b c         >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)+    Natural              >>= _ = Natural+    NaturalLit a         >>= _ = NaturalLit a+    NaturalFold          >>= _ = NaturalFold+    NaturalBuild         >>= _ = NaturalBuild+    NaturalIsZero        >>= _ = NaturalIsZero+    NaturalEven          >>= _ = NaturalEven+    NaturalOdd           >>= _ = NaturalOdd+    NaturalToInteger     >>= _ = NaturalToInteger+    NaturalShow          >>= _ = NaturalShow+    NaturalPlus  a b     >>= k = NaturalPlus  (a >>= k) (b >>= k)+    NaturalTimes a b     >>= k = NaturalTimes (a >>= k) (b >>= k)+    Integer              >>= _ = Integer+    IntegerLit a         >>= _ = IntegerLit a+    IntegerShow          >>= _ = IntegerShow+    Double               >>= _ = Double+    DoubleLit a          >>= _ = DoubleLit a+    DoubleShow           >>= _ = DoubleShow+    Text                 >>= _ = Text+    TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b)+    TextAppend a b       >>= k = TextAppend (a >>= k) (b >>= k)+    List                 >>= _ = List+    ListLit a b          >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)+    ListAppend a b       >>= k = ListAppend (a >>= k) (b >>= k)+    ListBuild            >>= _ = ListBuild+    ListFold             >>= _ = ListFold+    ListLength           >>= _ = ListLength+    ListHead             >>= _ = ListHead+    ListLast             >>= _ = ListLast+    ListIndexed          >>= _ = ListIndexed+    ListReverse          >>= _ = ListReverse+    Optional             >>= _ = Optional+    OptionalLit a b      >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)+    OptionalFold         >>= _ = OptionalFold+    OptionalBuild        >>= _ = OptionalBuild+    Record    a          >>= k = Record (fmap (>>= k) a)+    RecordLit a          >>= k = RecordLit (fmap (>>= k) a)+    Union     a          >>= k = Union (fmap (>>= k) a)+    UnionLit a b c       >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)+    Combine a b          >>= k = Combine (a >>= k) (b >>= k)+    Prefer a b           >>= k = Prefer (a >>= k) (b >>= k)+    Merge a b c          >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)+    Constructors a       >>= k = Constructors (a >>= k)+    Field a b            >>= k = Field (a >>= k) b+    Note a b             >>= k = Note a (b >>= k)+    Embed a              >>= k = k a  instance Bifunctor Expr where-    first _ (Const a         ) = Const a-    first _ (Var a           ) = Var a-    first k (Lam a b c       ) = Lam a (first k b) (first k c)-    first k (Pi a b c        ) = Pi a (first k b) (first k c)-    first k (App a b         ) = App (first k a) (first k b)-    first k (Let a b c d     ) = Let a (fmap (first k) b) (first k c) (first k d)-    first k (Annot a b       ) = Annot (first k a) (first k b)-    first _  Bool              = Bool-    first _ (BoolLit a       ) = BoolLit a-    first k (BoolAnd a b     ) = BoolAnd (first k a) (first k b)-    first k (BoolOr a b      ) = BoolOr (first k a) (first k b)-    first k (BoolEQ a b      ) = BoolEQ (first k a) (first k b)-    first k (BoolNE a b      ) = BoolNE (first k a) (first k b)-    first k (BoolIf a b c    ) = BoolIf (first k a) (first k b) (first k c)-    first _  Natural           = Natural-    first _ (NaturalLit a    ) = NaturalLit a-    first _  NaturalFold       = NaturalFold-    first _  NaturalBuild      = NaturalBuild-    first _  NaturalIsZero     = NaturalIsZero-    first _  NaturalEven       = NaturalEven-    first _  NaturalOdd        = NaturalOdd-    first _  NaturalToInteger  = NaturalToInteger-    first _  NaturalShow       = NaturalShow-    first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)-    first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b)-    first _  Integer           = Integer-    first _ (IntegerLit a    ) = IntegerLit a-    first _  IntegerShow       = IntegerShow-    first _  Double            = Double-    first _ (DoubleLit a     ) = DoubleLit a-    first _  DoubleShow        = DoubleShow-    first _  Text              = Text-    first _ (TextLit a       ) = TextLit a-    first k (TextAppend a b  ) = TextAppend (first k a) (first k b)-    first _  List              = List-    first k (ListLit a b     ) = ListLit (fmap (first k) a) (fmap (first k) b)-    first k (ListAppend a b  ) = ListAppend (first k a) (first k b)-    first _  ListBuild         = ListBuild-    first _  ListFold          = ListFold-    first _  ListLength        = ListLength-    first _  ListHead          = ListHead-    first _  ListLast          = ListLast-    first _  ListIndexed       = ListIndexed-    first _  ListReverse       = ListReverse-    first _  Optional          = Optional-    first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)-    first _  OptionalFold      = OptionalFold-    first _  OptionalBuild     = OptionalBuild-    first k (Record a        ) = Record (fmap (first k) a)-    first k (RecordLit a     ) = RecordLit (fmap (first k) a)-    first k (Union a         ) = Union (fmap (first k) a)-    first k (UnionLit a b c  ) = UnionLit a (first k b) (fmap (first k) c)-    first k (Combine a b     ) = Combine (first k a) (first k b)-    first k (Prefer a b      ) = Prefer (first k a) (first k b)-    first k (Merge a b c     ) = Merge (first k a) (first k b) (fmap (first k) c)-    first k (Field a b       ) = Field (first k a) b-    first k (Note a b        ) = Note (k a) (first k b)-    first _ (Embed a         ) = Embed a+    first _ (Const a             ) = Const a+    first _ (Var a               ) = Var a+    first k (Lam a b c           ) = Lam a (first k b) (first k c)+    first k (Pi a b c            ) = Pi a (first k b) (first k c)+    first k (App a b             ) = App (first k a) (first k b)+    first k (Let a b c d         ) = Let a (fmap (first k) b) (first k c) (first k d)+    first k (Annot a b           ) = Annot (first k a) (first k b)+    first _  Bool                  = Bool+    first _ (BoolLit a           ) = BoolLit a+    first k (BoolAnd a b         ) = BoolAnd (first k a) (first k b)+    first k (BoolOr a b          ) = BoolOr (first k a) (first k b)+    first k (BoolEQ a b          ) = BoolEQ (first k a) (first k b)+    first k (BoolNE a b          ) = BoolNE (first k a) (first k b)+    first k (BoolIf a b c        ) = BoolIf (first k a) (first k b) (first k c)+    first _  Natural               = Natural+    first _ (NaturalLit a        ) = NaturalLit a+    first _  NaturalFold           = NaturalFold+    first _  NaturalBuild          = NaturalBuild+    first _  NaturalIsZero         = NaturalIsZero+    first _  NaturalEven           = NaturalEven+    first _  NaturalOdd            = NaturalOdd+    first _  NaturalToInteger      = NaturalToInteger+    first _  NaturalShow           = NaturalShow+    first k (NaturalPlus a b     ) = NaturalPlus (first k a) (first k b)+    first k (NaturalTimes a b    ) = NaturalTimes (first k a) (first k b)+    first _  Integer               = Integer+    first _ (IntegerLit a        ) = IntegerLit a+    first _  IntegerShow           = IntegerShow+    first _  Double                = Double+    first _ (DoubleLit a         ) = DoubleLit a+    first _  DoubleShow            = DoubleShow+    first _  Text                  = Text+    first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b)+    first k (TextAppend a b      ) = TextAppend (first k a) (first k b)+    first _  List                  = List+    first k (ListLit a b         ) = ListLit (fmap (first k) a) (fmap (first k) b)+    first k (ListAppend a b      ) = ListAppend (first k a) (first k b)+    first _  ListBuild             = ListBuild+    first _  ListFold              = ListFold+    first _  ListLength            = ListLength+    first _  ListHead              = ListHead+    first _  ListLast              = ListLast+    first _  ListIndexed           = ListIndexed+    first _  ListReverse           = ListReverse+    first _  Optional              = Optional+    first k (OptionalLit a b     ) = OptionalLit (first k a) (fmap (first k) b)+    first _  OptionalFold          = OptionalFold+    first _  OptionalBuild         = OptionalBuild+    first k (Record a            ) = Record (fmap (first k) a)+    first k (RecordLit a         ) = RecordLit (fmap (first k) a)+    first k (Union a             ) = Union (fmap (first k) a)+    first k (UnionLit a b c      ) = UnionLit a (first k b) (fmap (first k) c)+    first k (Combine a b         ) = Combine (first k a) (first k b)+    first k (Prefer a b          ) = Prefer (first k a) (first k b)+    first k (Merge a b c         ) = Merge (first k a) (first k b) (fmap (first k) c)+    first k (Constructors a      ) = Constructors (first k a)+    first k (Field a b           ) = Field (first k a) b+    first k (Note a b            ) = Note (k a) (first k b)+    first _ (Embed a             ) = Embed a      second = fmap  instance IsString (Expr s a) where     fromString str = Var (fromString str) +data Chunks s a = Chunks [(Builder, Expr s a)] Builder+    deriving (Functor, Foldable, Traversable, Show, Eq)++instance Monoid (Chunks s a) where+    mempty = Chunks [] mempty++    mappend (Chunks xysL zL) (Chunks         []    zR) =+        Chunks xysL (zL <> zR)+    mappend (Chunks xysL zL) (Chunks ((x, y):xysR) zR) =+        Chunks (xysL ++ (zL <> x, y):xysR) zR++instance IsString (Chunks s a) where+    fromString str = Chunks [] (fromString str)+ {-  There is a one-to-one correspondence between the builders in this section     and the sub-parsers in "Dhall.Parser".  Each builder is named after the     corresponding parser and the relationship between builders exactly matches@@ -573,9 +594,11 @@  prettyLabel :: Text -> Doc ann prettyLabel a =-    if Data.HashSet.member a reservedIdentifiers+    if Data.HashSet.member a reservedIdentifiers || Text.any predicate a     then "`" <> Pretty.pretty a <> "`"     else Pretty.pretty a+  where+    predicate c = c == ':' || c == '.'  prettyNumber :: Integer -> Doc ann prettyNumber = Pretty.pretty@@ -586,9 +609,14 @@ prettyDouble :: Double -> Doc ann prettyDouble = Pretty.pretty -prettyText :: Builder -> Doc ann-prettyText a = Pretty.pretty (Builder.toLazyText (buildText a))+prettyChunks :: Pretty a => Chunks s a -> Doc ann+prettyChunks (Chunks a b) =+    "\"" <> foldMap prettyChunk a <> prettyText b <> "\""+  where+    prettyChunk (c, d) = prettyText c <> "${" <> prettyExprA d <> "}" +    prettyText t = Pretty.pretty (Builder.toLazyText (escapeText t))+ prettyConst :: Const -> Doc ann prettyConst Type = "Type" prettyConst Kind = "Kind"@@ -897,16 +925,19 @@     prettyExprD a0  prettyExprD :: Pretty a => Expr s a -> Doc ann-prettyExprD a0@(App _ _) =-    enclose' "" "" " " "" (fmap duplicate (reverse (docs a0)))+prettyExprD a0 = case a0 of+    App _ _        -> result+    Constructors _ -> result+    Note _ b       -> prettyExprD b+    _              -> prettyExprE a0   where-    docs (App  a b) = prettyExprE b : docs a-    docs (Note _ b) = docs b-    docs         b  = [ prettyExprE b ]-prettyExprD (Note _ b) = prettyExprD b-prettyExprD a0 =-    prettyExprE a0+    result = enclose' "" "" " " "" (fmap duplicate (reverse (docs a0))) +    docs (App        a b) = prettyExprE b : docs a+    docs (Constructors b) = [ prettyExprE b , "constructors" ]+    docs (Note       _ b) = docs b+    docs               b  = [ prettyExprE b ]+ prettyExprE :: Pretty a => Expr s a -> Doc ann prettyExprE (Field a b) = prettyExprE a <> "." <> prettyLabel b prettyExprE (Note  _ b) = prettyExprE b@@ -978,7 +1009,7 @@ prettyExprF (DoubleLit a) =     prettyDouble a prettyExprF (TextLit a) =-    prettyText a+    prettyChunks a prettyExprF (Record a) =     prettyRecord a prettyExprF (RecordLit a) =@@ -1059,9 +1090,11 @@ -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder buildLabel label =-    if Data.HashSet.member label reservedIdentifiers+    if Data.HashSet.member label reservedIdentifiers || Text.any predicate label     then "`" <> build label <> "`"     else build label+  where+    predicate c = c == ':' || c == '.'  -- | Builder corresponding to the @number@ token in "Dhall.Parser" buildNumber :: Integer -> Builder@@ -1076,9 +1109,17 @@ buildDouble a = build (show a)  -- | Builder corresponding to the @text@ token in "Dhall.Parser"-buildText :: Builder -> Builder-buildText a = "\"" <> Builder.fromLazyText (Text.concatMap adapt text) <> "\""+buildChunks :: Buildable a => Chunks s a -> Builder+buildChunks (Chunks a b) = "\"" <> foldMap buildChunk a <> escapeText b <> "\""   where+    buildChunk (c, d) = escapeText c <> "${" <> buildExprA d <> "}"++-- | Escape a `Builder` literal using Dhall's escaping rules+--+-- Note that the result does not include surrounding quotes+escapeText :: Builder -> Builder+escapeText a = Builder.fromLazyText (Text.concatMap adapt text)+  where     adapt c         | '\x20' <= c && c <= '\x21' = Text.singleton c         | '\x23' <= c && c <= '\x5B' = Text.singleton c@@ -1239,9 +1280,10 @@  -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser" buildExprD :: Buildable a => Expr s a -> Builder-buildExprD (App  a b) = buildExprD a <> " " <> buildExprE b-buildExprD (Note _ b) = buildExprD b-buildExprD  a         = buildExprE a+buildExprD (App        a b) = buildExprD a <> " " <> buildExprE b+buildExprD (Constructors b) = "constructors " <> buildExprE b+buildExprD (Note       _ b) = buildExprD b+buildExprD  a               = buildExprE a  -- | Builder corresponding to the @exprE@ parser in "Dhall.Parser" buildExprE :: Buildable a => Expr s a -> Builder@@ -1316,7 +1358,7 @@ buildExprF (DoubleLit a) =     buildDouble a buildExprF (TextLit a) =-    buildText a+    buildChunks a buildExprF (Record a) =     buildRecord a buildExprF (RecordLit a) =@@ -1491,7 +1533,7 @@     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 :: Integer -> Var -> Expr s a -> Expr t a+shift :: Integer -> Var -> Expr s a -> Expr s a shift _ _ (Const a) = Const a shift d (V x n) (Var (V x' n')) = Var (V x' n'')   where@@ -1571,7 +1613,9 @@ shift _ _ (DoubleLit a) = DoubleLit a shift _ _ DoubleShow = DoubleShow shift _ _ Text = Text-shift _ _ (TextLit a) = TextLit a+shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b)+  where+    a' = fmap (fmap (shift d v)) a shift d v (TextAppend a b) = TextAppend a' b'   where     a' = shift d v a@@ -1625,10 +1669,13 @@     a' =       shift d v  a     b' =       shift d v  b     c' = fmap (shift d v) c+shift d v (Constructors a) = Constructors a'+  where+    a' = shift d v  a shift d v (Field a b) = Field a' b   where     a' = shift d v a-shift d v (Note _ b) = b'+shift d v (Note a b) = Note a b'   where     b' = shift d v b -- The Dhall compiler enforces that all embedded values are closed expressions@@ -1639,7 +1686,7 @@  > subst x C B  ~  B[x := C] -}-subst :: Var -> Expr s a -> Expr t a -> Expr s a+subst :: Var -> Expr s a -> Expr s a -> Expr s a subst _ _ (Const a) = Const a subst (V x n) e (Lam y _A b) = Lam y _A' b'   where@@ -1715,7 +1762,9 @@ subst _ _ (DoubleLit a) = DoubleLit a subst _ _ DoubleShow = DoubleShow subst _ _ Text = Text-subst _ _ (TextLit a) = TextLit a+subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b)+  where+    a' = fmap (fmap (subst x e)) a subst x e (TextAppend a b) = TextAppend a' b'   where     a' = subst x e a@@ -1760,10 +1809,13 @@     a' =       subst x e  a     b' =       subst x e  b     c' = fmap (subst x e) c+subst x e (Constructors a) = Constructors a'+  where+    a' = subst x e  a subst x e (Field a b) = Field a' b   where     a' = subst x e a-subst x e (Note _ b) = b'+subst x e (Note a b) = Note a b'   where     b' = subst x e b -- The Dhall compiler enforces that all embedded values are closed expressions@@ -1804,6 +1856,68 @@ boundedType (Union kvs)      = all boundedType kvs boundedType _                = False +-- | Remove all `Note` constructors from an `Expr` (i.e. de-`Note`)+denote :: Expr s a -> Expr t a+denote (Note _ b            ) = denote b+denote (Const a             ) = Const a+denote (Var a               ) = Var a+denote (Lam a b c           ) = Lam a (denote b) (denote c)+denote (Pi a b c            ) = Pi a (denote b) (denote c)+denote (App a b             ) = App (denote a) (denote b)+denote (Let a b c d         ) = Let a (fmap denote b) (denote c) (denote d)+denote (Annot a b           ) = Annot (denote a) (denote b)+denote  Bool                  = Bool+denote (BoolLit a           ) = BoolLit a+denote (BoolAnd a b         ) = BoolAnd (denote a) (denote b)+denote (BoolOr a b          ) = BoolOr (denote a) (denote b)+denote (BoolEQ a b          ) = BoolEQ (denote a) (denote b)+denote (BoolNE a b          ) = BoolNE (denote a) (denote b)+denote (BoolIf a b c        ) = BoolIf (denote a) (denote b) (denote c)+denote  Natural               = Natural+denote (NaturalLit a        ) = NaturalLit a+denote  NaturalFold           = NaturalFold+denote  NaturalBuild          = NaturalBuild+denote  NaturalIsZero         = NaturalIsZero+denote  NaturalEven           = NaturalEven+denote  NaturalOdd            = NaturalOdd+denote  NaturalToInteger      = NaturalToInteger+denote  NaturalShow           = NaturalShow+denote (NaturalPlus a b     ) = NaturalPlus (denote a) (denote b)+denote (NaturalTimes a b    ) = NaturalTimes (denote a) (denote b)+denote  Integer               = Integer+denote (IntegerLit a        ) = IntegerLit a+denote  IntegerShow           = IntegerShow+denote  Double                = Double+denote (DoubleLit a         ) = DoubleLit a+denote  DoubleShow            = DoubleShow+denote  Text                  = Text+denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b)+denote (TextAppend a b      ) = TextAppend (denote a) (denote b)+denote  List                  = List+denote (ListLit a b         ) = ListLit (fmap denote a) (fmap denote b)+denote (ListAppend a b      ) = ListAppend (denote a) (denote b)+denote  ListBuild             = ListBuild+denote  ListFold              = ListFold+denote  ListLength            = ListLength+denote  ListHead              = ListHead+denote  ListLast              = ListLast+denote  ListIndexed           = ListIndexed+denote  ListReverse           = ListReverse+denote  Optional              = Optional+denote (OptionalLit a b     ) = OptionalLit (denote a) (fmap denote b)+denote  OptionalFold          = OptionalFold+denote  OptionalBuild         = OptionalBuild+denote (Record a            ) = Record (fmap denote a)+denote (RecordLit a         ) = RecordLit (fmap denote a)+denote (Union a             ) = Union (fmap denote a)+denote (UnionLit a b c      ) = UnionLit a (denote b) (fmap denote c)+denote (Combine a b         ) = Combine (denote a) (denote b)+denote (Prefer a b          ) = Prefer (denote a) (denote b)+denote (Merge a b c         ) = Merge (denote a) (denote b) (fmap denote c)+denote (Constructors a      ) = Constructors (denote a)+denote (Field a b           ) = Field (denote a) b+denote (Embed a             ) = Embed a+ {-| Reduce an expression to its normal form, performing beta reduction and applying     any custom definitions.    @@ -1820,7 +1934,7 @@     -} normalizeWith :: Normalizer a -> Expr s a -> Expr t a-normalizeWith ctx e0 = loop (shift 0 "_" e0)+normalizeWith ctx e0 = loop (denote e0)  where     -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of     -- `loop`.  In theory, this might change a failing repro case into@@ -1891,9 +2005,12 @@             App NaturalEven (NaturalLit n) -> BoolLit (even n)             App NaturalOdd (NaturalLit n) -> BoolLit (odd n)             App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n)-            App NaturalShow (NaturalLit n) -> TextLit ("+" <> buildNatural n)-            App IntegerShow (IntegerLit n) -> TextLit (buildNumber n)-            App DoubleShow (DoubleLit n) -> TextLit (buildDouble n)+            App NaturalShow (NaturalLit n) ->+                TextLit (Chunks [] ("+" <> buildNatural n))+            App IntegerShow (IntegerLit n) ->+                TextLit (Chunks [] (buildNumber n))+            App DoubleShow (DoubleLit n) ->+                TextLit (Chunks [] (buildDouble n))             App (App OptionalBuild t) k                 | check     -> OptionalLit t k'                 | otherwise -> App f' a'@@ -2064,7 +2181,16 @@     DoubleLit n -> DoubleLit n     DoubleShow -> DoubleShow     Text -> Text-    TextLit t -> TextLit t+    TextLit (Chunks xys z) ->+        case mconcat chunks of+            Chunks [("", x)] "" -> x+            c                   -> TextLit c+      where+        chunks = concatMap process xys ++ [Chunks [] z]++        process (x, y) = case loop y of+            TextLit c -> [Chunks [] x, c]+            y'        -> [Chunks [(x, y')] mempty]     TextAppend x y   ->         case x' of             TextLit xt ->@@ -2151,6 +2277,18 @@         x' =      loop x         y' =      loop y         t' = fmap loop t+    Constructors t   ->+        case t' of+            Union kts -> RecordLit kvs+              where+                kvs = Data.Map.mapWithKey adapt kts++                adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)+                  where+                    rest = Data.Map.delete k kts+            _ -> Constructors t'+      where+        t' = loop t     Field r x        ->         case loop r of             RecordLit kvs ->@@ -2175,7 +2313,7 @@  -- | Quickly check if an expression is in normal form isNormalized :: Expr s a -> Bool-isNormalized e = case shift 0 "_" e of  -- `shift` is a hack to delete `Note`+isNormalized e = case denote e of     Const _ -> True     Var _ -> True     Lam _ a b -> isNormalized a && isNormalized b@@ -2305,7 +2443,7 @@     DoubleLit _ -> True     DoubleShow -> True     Text -> True-    TextLit _ -> True+    TextLit (Chunks xys _) -> all (all isNormalized) xys     TextAppend x y -> isNormalized x && isNormalized y &&         case x of             TextLit _ ->@@ -2361,6 +2499,10 @@                             Nothing -> True                     _ -> True             _ -> True+    Constructors t -> isNormalized t &&+        case t of+            Union _ -> False+            _       -> True     Field r x -> isNormalized r &&         case r of             RecordLit kvs ->

@@ -104,6 +104,7 @@       exprFromPath     , load     , loadWith+    , loadWithContext     , hashExpression     , hashExpressionToCode     , Cycle(..)@@ -111,6 +112,7 @@     , Imported(..)     , PrettyHttpException(..)     , MissingFile(..)+    , MissingEnvironmentVariable(..)     ) where  import Control.Applicative (empty)@@ -119,7 +121,6 @@ import Control.Lens (Lens', zoom) import Control.Monad (join) import Control.Monad.Catch (throwM, MonadCatch(catch))-import Control.Monad.Trans.Class (lift) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT) import Data.ByteString.Lazy (ByteString)@@ -137,6 +138,7 @@ import Filesystem.Path ((</>), FilePath) import Dhall.Core     ( Expr(..)+    , Chunks(..)     , HasHome(..)     , PathHashed(..)     , PathMode(..)@@ -338,6 +340,9 @@     , _manager :: Maybe Manager     } +emptyStatus :: Status+emptyStatus = Status [] Map.empty Nothing+ canonicalizeAll :: [Path] -> [Path] canonicalizeAll = map canonicalizePath . List.tails @@ -491,8 +496,8 @@   :: Expr s a   -> Maybe (CI Data.ByteString.ByteString, Data.ByteString.ByteString) toHeader (RecordLit m) = do-    TextLit keyBuilder   <- Map.lookup "header" m-    TextLit valueBuilder <- Map.lookup "value"  m+    TextLit (Chunks [] keyBuilder  ) <- Map.lookup "header" m+    TextLit (Chunks [] valueBuilder) <- Map.lookup "value"  m     let keyText   = Text.toStrict (Builder.toLazyText keyBuilder  )     let valueText = Text.toStrict (Builder.toLazyText valueBuilder)     let keyBytes   = Data.Text.Encoding.encodeUtf8 keyText@@ -582,12 +587,12 @@     bytesPath = Data.Text.Encoding.encodeUtf8 textPath  -- | Parse an expression from a `Path` containing a Dhall program-exprFromPath :: Manager -> Path -> IO (Expr Src Path)-exprFromPath m (Path {..}) = case pathType of-    File hasHome file -> do+exprFromPath :: Path -> StateT Status IO (Expr Src Path)+exprFromPath (Path {..}) = case pathType of+    File hasHome file -> liftIO (do         path <- case hasHome of             Home -> do-                home <- liftIO Filesystem.getHomeDirectory+                home <- Filesystem.getHomeDirectory                 return (home </> file)             Homeless -> do                 return file@@ -597,7 +602,7 @@                 exists <- Filesystem.isFile path                 if exists                     then return ()-                    else Control.Exception.throwIO (MissingFile path)+                    else throwIO (MissingFile path)                  -- Unfortunately, GHC throws an `InappropriateType` exception                 -- when trying to read a directory, but does not export the@@ -618,9 +623,10 @@             RawText -> do                 let pathString = Filesystem.Path.CurrentOS.encodeString path                 text <- Data.Text.IO.readFile pathString-                return (TextLit (build text))+                return (TextLit (Chunks [] (build text))) )     URL url headerPath -> do-        request <- HTTP.parseUrlThrow (Text.unpack url)+        m       <- needManager+        request <- liftIO (HTTP.parseUrlThrow (Text.unpack url))          let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString) #if MIN_VERSION_http_client(0,5,0)@@ -637,7 +643,7 @@         requestWithHeaders <- case headerPath of             Nothing   -> return request             Just path -> do-                expr <- load (Embed (Path path Code))+                expr <- loadStaticIO Dhall.Context.empty (Path path Code)                 let expected :: Expr Src X                     expected =                         App List@@ -660,22 +666,24 @@                         _ ->                             Annot expr expected                 case Dhall.TypeCheck.typeOf annot of-                    Left err -> Control.Exception.throwIO err+                    Left err -> liftIO (throwIO err)                     Right _  -> return ()                 let expr' = Dhall.Core.normalize expr                 headers <- case toHeaders expr' of-                    Just headers -> return headers-                    Nothing      -> Control.Exception.throwIO InternalError+                    Just headers -> do+                        return headers+                    Nothing      -> do+                        liftIO (throwIO InternalError)                 let requestWithHeaders = request                         { HTTP.requestHeaders = headers                         }                 return requestWithHeaders-        response <- HTTP.httpLbs requestWithHeaders m `catch` handler+        response <- liftIO (HTTP.httpLbs requestWithHeaders m `catch` handler)          let bytes = HTTP.responseBody response          text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of-            Left  err  -> throwIO err+            Left  err  -> liftIO (throwIO err)             Right text -> return text          case pathMode of@@ -690,27 +698,26 @@                         -- a directory list                         let err' = ParseError (Text.Trifecta._errDoc err) -                        request' <- HTTP.parseUrlThrow (Text.unpack url)+                        request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url))                          let request'' =                                 request'                                     { HTTP.path = HTTP.path request' <> "/@" }-                        response' <- HTTP.httpLbs request'' m-                            `onException` throwIO err'+                        response' <- liftIO (HTTP.httpLbs request'' m `onException` throwIO err' )                          let bytes' = HTTP.responseBody response'                          text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of-                            Left  _     -> throwIO err'+                            Left  _     -> liftIO (throwIO err')                             Right text' -> return text'                          case Text.Trifecta.parseString parser delta (Text.unpack text') of-                            Failure _    -> throwIO err'+                            Failure _    -> liftIO (throwIO err')                             Success expr -> return expr                     Success expr -> return expr             RawText -> do-                return (TextLit (build text))-    Env env -> do+                return (TextLit (Chunks [] (build text)))+    Env env -> liftIO (do         x <- System.Environment.lookupEnv (Text.unpack env)         case x of             Just str -> do@@ -724,8 +731,8 @@                                 throwIO (ParseError (Text.Trifecta._errDoc errInfo))                             Success expr    -> do                                 return expr-                    RawText -> return (TextLit (build str))-            Nothing  -> throwIO (MissingEnvironmentVariable env)+                    RawText -> return (TextLit (Chunks [] (build str)))+            Nothing  -> throwIO (MissingEnvironmentVariable env) )   where     PathHashed {..} = pathHashed @@ -740,41 +747,56 @@     This also returns the true final path (i.e. explicit "/@" at the end for     directories) -}-loadDynamic :: forall m . MonadCatch m => (Path -> m (Expr Src Path))-    -> Path -> StateT Status m (Expr Src Path)+loadDynamic+    :: forall m . MonadCatch m+    => (Path -> StateT Status m (Expr Src Path))+    -> Path+    -> StateT Status m (Expr Src Path) loadDynamic from_path p = do     paths <- zoom stack State.get -    let handler :: SomeException -> m (Expr Src Path)+    let handler :: SomeException -> StateT Status m (Expr Src Path)         handler e = throwM (Imported (p:paths) e) -    lift (from_path (canonicalizePath (p:paths)) `catch` handler)+    from_path (canonicalizePath (p:paths)) `catch` handler -loadStaticIO :: Dhall.Context.Context (Expr Src X) -> Path -> StateT Status IO (Expr Src X)-loadStaticIO ctx path = do-    m <- needManager-    loadStaticWith (exprFromPath m) ctx path+loadStaticIO+    :: Dhall.Context.Context (Expr Src X)+    -> Path+    -> StateT Status IO (Expr Src X)+loadStaticIO = loadStaticWith exprFromPath  -- | Resolve all imports within an expression using a custom typing context and Path -- resolving callback in arbitrary `MonadCatch` monad.-loadWith :: MonadCatch m => (Path -> m (Expr Src Path))-    -> Dhall.Context.Context (Expr Src X) -> Expr Src Path -> m (Expr Src X)+loadWith+    :: MonadCatch m+    => (Path -> StateT Status m (Expr Src Path))+    -> Dhall.Context.Context (Expr Src X)+    -> Expr Src Path+    -> m (Expr Src X) loadWith from_path ctx = evalStatus (loadStaticWith from_path ctx) -loadStaticWith :: MonadCatch m => (Path -> m (Expr Src Path))-    -> Dhall.Context.Context (Expr Src X) -> Path -> StateT Status m (Expr Src X)+-- | Resolve all imports within an expression using a custom typing context.+--+-- @load = loadWithContext Dhall.Context.empty@+loadWithContext+    :: Dhall.Context.Context (Expr Src X)+    -> Expr Src Path+    -> IO (Expr Src X)+loadWithContext ctx = evalStatus (loadStaticIO ctx)++loadStaticWith+    :: MonadCatch m+    => (Path -> StateT Status m (Expr Src Path))+    -> Dhall.Context.Context (Expr Src X)+    -> Path+    -> StateT Status m (Expr Src X) loadStaticWith from_path ctx path = do     paths <- zoom stack State.get -    let local (Path (PathHashed _ (URL url _)) _) =-            case HTTP.parseUrlThrow (Text.unpack url) of-                Nothing      -> False-                Just request -> case HTTP.host request of-                    "127.0.0.1" -> True-                    "localhost" -> True-                    _           -> False-        local (Path (PathHashed _ (File _ _ )) _) = True-        local (Path (PathHashed _ (Env  _   )) _) = True+    let local (Path (PathHashed _ (URL _ _ )) _) = False+        local (Path (PathHashed _ (File _ _)) _) = True+        local (Path (PathHashed _ (Env  _  )) _) = True      let parent = canonicalizePath paths     let here   = canonicalizePath (path:paths)@@ -831,15 +853,14 @@      return expr -evalStatus :: (Traversable f, Monad m, Monad f) =>-                    (a -> StateT Status m (f b)) -> f a -> m (f b)-evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) status-  where-    status = Status [] Map.empty Nothing+evalStatus+    :: (Traversable f, Monad m, Monad f)+    => (a -> StateT Status m (f b)) -> f a -> m (f b)+evalStatus cb expr = State.evalStateT (fmap join (traverse cb expr)) emptyStatus  -- | Resolve all imports within an expression load :: Expr Src Path -> IO (Expr Src X)-load = evalStatus (loadStaticIO Dhall.Context.empty)+load = loadWithContext Dhall.Context.empty  -- | Hash a fully resolved expression hashExpression :: Expr s X -> Data.ByteString.ByteString

@@ -237,16 +237,12 @@  simpleLabel :: Parser Text simpleLabel = try (do-    text <- quotedLabel-    Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers))-    return text )--quotedLabel :: Parser Text-quotedLabel = try (do     c  <- Text.Parser.Char.satisfy headCharacter     cs <- many (Text.Parser.Char.satisfy tailCharacter)     let string = c:cs-    return (Data.Text.Lazy.pack string) )+    let text = Data.Text.Lazy.pack string+    Control.Monad.guard (not (Data.HashSet.member text reservedIdentifiers))+    return text )   where     headCharacter c = alpha c || c == '_' @@ -255,9 +251,11 @@ backtickLabel :: Parser Text backtickLabel = do     _ <- Text.Parser.Char.char '`'-    t <- quotedLabel+    t <- some (Text.Parser.Char.satisfy predicate)     _ <- Text.Parser.Char.char '`'-    return t+    return (Data.Text.Lazy.pack t)+  where+    predicate c = alpha c || digit c || elem c ("-/_:." :: String)  label :: Parser Text label = (do@@ -265,16 +263,7 @@     whitespace     return t ) <?> "label" --- | Combine consecutive chunks to eliminate gratuitous appends-textAppend :: Expr Src a -> Expr Src a -> Expr Src a-textAppend (TextLit a) (TextLit b) =-    TextLit (a <> b)-textAppend (TextLit a) (TextAppend (TextLit b) c) =-    TextAppend (TextLit (a <> b)) c-textAppend a b =-    TextAppend a b--doubleQuotedChunk :: Parser a -> Parser (Expr Src a)+doubleQuotedChunk :: Parser a -> Parser (Chunks Src a) doubleQuotedChunk embedded =     choice         [ interpolation@@ -286,11 +275,11 @@         _ <- Text.Parser.Char.text "${"         e <- expression embedded         _ <- Text.Parser.Char.char '}'-        return e+        return (Chunks [(mempty, e)] mempty)      unescapedCharacter = do         c <- Text.Parser.Char.satisfy predicate-        return (TextLit (Data.Text.Lazy.Builder.singleton c))+        return (Chunks [] (Data.Text.Lazy.Builder.singleton c))       where         predicate c =                 ('\x20' <= c && c <= '\x21'    )@@ -311,7 +300,7 @@             , tab             , unicode             ]-        return (TextLit (Data.Text.Lazy.Builder.singleton c))+        return (Chunks [] (Data.Text.Lazy.Builder.singleton c))       where         quotationMark = Text.Parser.Char.char '"' @@ -340,25 +329,29 @@             let n = ((n0 * 16 + n1) * 16 + n2) * 16 + n3             return (Data.Char.chr n) -doubleQuotedLiteral :: Parser a -> Parser (Expr Src a)+doubleQuotedLiteral :: Parser a -> Parser (Chunks Src a) doubleQuotedLiteral embedded = do     _      <- Text.Parser.Char.char '"'     chunks <- many (doubleQuotedChunk embedded)     _      <- Text.Parser.Char.char '"'-    return (foldr textAppend (TextLit "") chunks)+    return (mconcat chunks) -dedent :: Expr Src a -> Expr Src a-dedent expr0 = process trimBegin expr0+-- | Similar to `Dhall.Core.buildChunks` except that this doesn't bother to+-- render interpolated expressions to avoid a `Buildable a` constraint.  The+-- interpolated contents are not necessary for computing how much to dedent a+-- multi-line string+--+-- This also doesn't include the surrounding quotes since they would interfere+-- with the whitespace detection+buildChunks :: Chunks s a -> Builder+buildChunks (Chunks a b) = foldMap buildChunk a <> escapeText b   where-    -- This treats variable interpolation as breaking leading whitespace for the-    -- purposes of computing the shortest leading whitespace.  The "${x}"-    -- could really be any text that breaks whitespace-    concatFragments (TextAppend (TextLit t) e) = t      <> concatFragments e-    concatFragments (TextAppend  _          e) = "${x}" <> concatFragments e-    concatFragments (TextLit t)                = t-    concatFragments  _                         = mempty+    buildChunk (c, _) = escapeText c <> "${x}" -    builder0 = concatFragments expr0+dedent :: Chunks Src a -> Chunks Src a+dedent chunks0 = process chunks0+  where+    builder0 = buildChunks chunks0      text0 = Data.Text.Lazy.Builder.toLazyText builder0 @@ -375,9 +368,9 @@         [] -> 0         _  -> minimum (map indentLength nonEmptyLines) -    -- The purpose of this complicated `trim0`/`trim1` is to ensure that we-    -- strip leading whitespace without stripping whitespace after variable-    -- interpolation+    -- The purpose of this complicated `trimBegin`/`trimContinue` is to ensure+    -- that we strip leading whitespace without stripping whitespace after+    -- variable interpolation      -- This is the trim function we use up until the first variable     -- interpolation, dedenting all lines@@ -402,16 +395,14 @@     -- This is the loop that drives whether or not to use `trimBegin` or     -- `trimContinue`.  We call this function with `trimBegin`, but after the     -- first interpolation we switch permanently to `trimContinue`-    process trim (TextAppend (TextLit t) e) =-        TextAppend (TextLit (trim t)) (process trimContinue e)-    process _    (TextAppend e0 e1) =-        TextAppend e0 (process trimContinue e1)-    process trim (TextLit t) =-        TextLit (trim t)-    process _     e =-        e+    process (Chunks ((x0, y0):xys) z) =+        Chunks ((trimBegin x0, y0):xys') (trimContinue z)+      where+        xys' = [ (trimContinue x, y) | (x, y) <- xys ]+    process (Chunks [] z) =+        Chunks [] (trimBegin z) -singleQuoteContinue :: Parser a -> Parser (Expr Src a)+singleQuoteContinue :: Parser a -> Parser (Chunks Src a) singleQuoteContinue embedded =     choice         [ escapeSingleQuotes@@ -424,44 +415,44 @@         ]   where         escapeSingleQuotes = do-            a <- fmap TextLit "'''"+            _ <- "'''" :: Parser Builder             b <- singleQuoteContinue embedded-            return (textAppend a b)+            return ("''" <> b)          interpolation = do             _ <- Text.Parser.Char.text "${"             a <- expression embedded             _ <- Text.Parser.Char.char '}'             b <- singleQuoteContinue embedded-            return (textAppend a b)+            return (Chunks [(mempty, a)] mempty <> b)          escapeInterpolation = do             _ <- Text.Parser.Char.text "''${"             b <- singleQuoteContinue embedded-            return (textAppend (TextLit "${") b)+            return ("${" <> b)          endLiteral = do             _ <- Text.Parser.Char.text "''"-            return (TextLit "")+            return mempty          unescapedCharacter = do-            a <- fmap TextLit (satisfy predicate)+            a <- satisfy predicate             b <- singleQuoteContinue embedded-            return (textAppend a b)+            return (Chunks [] a <> b)           where             predicate c = '\x20' <= c && c <= '\x10FFFF'          endOfLine = do-            a <- fmap TextLit "\n" <|> fmap TextLit "\r\n"+            a <- "\n" <|> "\r\n"             b <- singleQuoteContinue embedded-            return (textAppend a b)+            return (Chunks [] a <> b)          tab = do             _ <- Text.Parser.Char.char '\t'             b <- singleQuoteContinue embedded-            return (textAppend (TextLit "\t") b)+            return ("\t" <> b) -singleQuoteLiteral :: Parser a -> Parser (Expr Src a)+singleQuoteLiteral :: Parser a -> Parser (Chunks Src a) singleQuoteLiteral embedded = do     _ <- Text.Parser.Char.text "''" @@ -482,7 +473,7 @@ textLiteral embedded = (do     literal <- doubleQuotedLiteral embedded <|> singleQuoteLiteral embedded     whitespace-    return literal ) <?> "text literal"+    return (TextLit literal) ) <?> "text literal"  reserved :: Data.Text.Text -> Parser () reserved x = do _ <- Text.Parser.Char.text x; whitespace@@ -511,6 +502,9 @@ _merge :: Parser () _merge = reserved "merge" +_constructors :: Parser ()+_constructors = reserved "constructors"+ _NaturalFold :: Parser () _NaturalFold = reserved "Natural/fold" @@ -1151,8 +1145,10 @@  applicationExpression :: Parser a -> Parser (Expr Src a) applicationExpression embedded = do-    a <- some (noted (selectorExpression embedded))-    return (foldl1 app a)+    f <- (do _constructors; return Constructors) <|> return id+    a <- noted (selectorExpression embedded)+    b <- many (noted (selectorExpression embedded))+    return (foldl app (f a) b)   where     app nL@(Note (Src before _ bytesL) _) nR@(Note (Src _ after bytesR) _) =         Note (Src before after (bytesL <> bytesR)) (App nL nR)

@@ -923,30 +923,6 @@ -- > -- > "haha" ----- Every @let@ expression of the form:------ > let x : t = y in e------ ... is exactly equivalent to:------ > (λ(x : t) → e) y------ So for example, this @let@ expression:------ > let x : Text = "ha" in x ++ x------ ... is equivalent to:------ > (λ(x : Text) → x ++ x) "ha"------ ... which in turn reduces to:------ > "ha" ++ "ha"------ ... which in turn reduces to:------ > "haha"--- -- You need to nest @let@ expressions if you want to define more than one value -- in this way: --@@ -997,6 +973,13 @@ -- >  -- > False --+-- ... or to define synonyms for types:+--+-- > $ dhall <<< 'let Name : Type = Text in [ "John", "Mary" ] : List Name'+-- > List Text+-- > +-- > [ "John", "Mary" ]+-- -- __Exercise:__ What do you think the following code will normalize to? -- -- >     let x = 1@@ -1128,6 +1111,36 @@ -- >     ,   Empty -- >     ] --+-- ... and Dhall even provides the @constructors@ keyword to automate this+-- common pattern:+--+-- >     let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >+-- > in  [   MyType.Empty {}+-- >     ,   MyType.Person { name = "John", age = +23 }+-- >     ,   MyType.Person { name = "Amy" , age = +25 }+-- >     ]+--+-- The @constructors@ keyword takes a union type argument and returns a record+-- with one field per union type constructor:+--+-- > $ dhall --pretty+-- > constructors < Empty : {} | Person : { name : Text, age : Natural } >+-- > <Ctrl-D>+-- >+-- > { Empty  :+-- >     ∀(Empty : {}) → < Empty : {} | Person : { age : Natural, name : Text } >+-- > , Person :+-- >       ∀(Person : { age : Natural, name : Text })+-- >     → < Empty : {} | Person : { age : Natural, name : Text } >+-- > }+-- >+-- > { Empty  =+-- >     λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >+-- > , Person =+-- >       λ(Person : { age : Natural, name : Text })+-- >     → < Person = Person | Empty : {} >+-- > }+-- -- You can also extract fields during pattern matching such as in the following -- function which renders each value to `Text`: --@@ -2678,25 +2691,10 @@ -- the above polymorphic function then you'd get the unexpected behavior where -- a list literal is a function if the list has 0 elements but not a function -- otherwise.------ * Does Dhall support type synonyms like Haskell?------ No.  For example, the following expression will not type-check:------ > let MyType = Integer in 1 : MyType------ Haskell can support type synonyms because Haskell does not allow type-level--- functions like Dhall does.  Dhall's support for type-level computation means--- that type synonyms cannot be safely substituted until after the type-checking--- phase, otherwise type-checking might infinitely loop------ You can work around this limitation using Dhall's import system by saving the--- type synonym to a path and importing that path, like this:------ > cat ./MyType--- > Integer+-- +-- * Does Dhall support user-defined recursive types? ----- > 1 : ./MyType  -- This will type-check+-- No, but you can translate recursive code to non-recursive code by following+-- this guide: ----- This is because import resolution precedes type-checking and does not run the--- risk of causing the type-checker to diverge+-- <https://github.com/dhall-lang/dhall-lang/wiki/How-to-translate-recursive-code-to-Dhall How to translate recursive code to Dhall>

@@ -30,7 +30,7 @@ import Data.Text.Prettyprint.Doc (Pretty(..)) import Data.Traversable (forM) import Data.Typeable (Typeable)-import Dhall.Core (Const(..), Expr(..), Var(..))+import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..)) import Dhall.Context (Context)  import qualified Control.Monad.Trans.State.Strict as State@@ -137,7 +137,9 @@     loop ctx e@(Var (V x n)     ) = do         case Dhall.Context.lookup x n ctx of             Nothing -> Left (TypeError ctx e (UnboundVariable x))-            Just a  -> return a+            Just a  -> do+                _ <- loop ctx a+                return a     loop ctx   (Lam x _A  b     ) = do         _ <- loop ctx _A         let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx)@@ -177,45 +179,23 @@                 let nf_A  = Dhall.Core.normalize _A                 let nf_A' = Dhall.Core.normalize _A'                 Left (TypeError ctx e (TypeMismatch f nf_A a nf_A'))-    loop ctx e@(Let f mt r b ) = do-        tR  <- loop ctx r-        ttR <- fmap Dhall.Core.normalize (loop ctx tR)-        kR  <- case ttR of-            Const k -> return k-            -- Don't bother to provide a `let`-specific version of this error-            -- message because this should never happen anyway-            _       -> Left (TypeError ctx e (InvalidInputType tR))--        let ctx' = fmap (Dhall.Core.shift 1 (V f 0)) (Dhall.Context.insert f tR ctx)-        tB  <- loop ctx' b-        ttB <- fmap Dhall.Core.normalize (loop ctx' tB)-        kB  <- case ttB of-            Const k -> return k-            -- Don't bother to provide a `let`-specific version of this error-            -- message because this should never happen anyway-            _       -> Left (TypeError ctx e (InvalidOutputType tB))--        case rule kR kB of-            Left () -> Left (TypeError ctx e (NoDependentLet tR tB))-            Right _ -> return ()--        case mt of-            Nothing -> do-                return ()-            Just t  -> do-                _ <- loop ctx t-                let nf_t  = Dhall.Core.normalize t-                let nf_tR = Dhall.Core.normalize tR-                if propEqual nf_tR nf_t+    loop ctx e@(Let x mA a0 b0) = do+        _A1 <- loop ctx a0+        case mA of+            Just _A0 -> do+                _ <- loop ctx _A0+                let nf_A0 = Dhall.Core.normalize _A0+                let nf_A1 = Dhall.Core.normalize _A1+                if propEqual _A0 _A1                     then return ()-                    else Left (TypeError ctx e (AnnotMismatch r nf_t nf_tR))--        let r'   = Dhall.Core.shift 1 (V f 0) r-        let tB'  = Dhall.Core.subst (V f 0) r' (Dhall.Core.normalize tB)-        let tB'' = Dhall.Core.shift (-1) (V f 0) tB'-        return tB''+                    else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1))+            Nothing -> return ()+        let a1 = Dhall.Core.normalize a0+        let a2 = Dhall.Core.shift 1 (V x 0) a1+        let b1 = Dhall.Core.subst (V x 0) a2 b0+        let b2 = Dhall.Core.shift (-1) (V x 0) b1+        loop ctx b2     loop ctx e@(Annot x t       ) = do-        -- This is mainly just to check that `t` is not `Kind`         _ <- loop ctx t          t' <- loop ctx x@@ -362,7 +342,13 @@         return (Pi "_" Double Text)     loop _      Text              = do         return (Const Type)-    loop _     (TextLit _       ) = do+    loop ctx e@(TextLit (Chunks xys _)) = do+        let process (_, y) = do+                ty <- fmap Dhall.Core.normalize (loop ctx y)+                case ty of+                    Text -> return ()+                    _    -> Left (TypeError ctx e (CantInterpolate y ty))+        mapM_ process xys         return Text     loop ctx e@(TextAppend l r  ) = do         tl <- fmap Dhall.Core.normalize (loop ctx l)@@ -496,15 +482,15 @@         mapM_ process (Data.Map.toList kts)         return (Const Type)     loop ctx e@(RecordLit kvs   ) = do-        let process (k, v) = do+        let process k v = do                 t <- loop ctx v                 s <- fmap Dhall.Core.normalize (loop ctx t)                 case s of                     Const Type -> return ()                     _          -> Left (TypeError ctx e (InvalidField k v))-                return (k, t)-        kts <- mapM process (Data.Map.toAscList kvs)-        return (Record (Data.Map.fromAscList kts))+                return t+        kts <- Data.Map.traverseWithKey process kvs+        return (Record kts)     loop ctx e@(Union     kts   ) = do         let process (k, t) = do                 s <- fmap Dhall.Core.normalize (loop ctx t)@@ -561,6 +547,8 @@             _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY))         return (Record (Data.Map.union ktsY ktsX))     loop ctx e@(Merge kvsX kvsY (Just t)) = do+        _ <- loop ctx t+         tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)         ktsX  <- case tKvsX of             Record kts -> return kts@@ -634,10 +622,22 @@                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))         mapM_ process (Data.Map.toList ktsY)         return t+    loop ctx e@(Constructors t  ) = do+        _ <- loop ctx t++        kts <- case Dhall.Core.normalize t of+            Union kts -> return kts+            t'        -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))++        let adapt k t_ = Pi k t_ (Union kts)++        return (Record (Data.Map.mapWithKey adapt kts))     loop ctx e@(Field r x       ) = do         t <- fmap Dhall.Core.normalize (loop ctx r)         case t of-            Record kts ->+            Record kts -> do+                _ <- loop ctx t+                 case Data.Map.lookup x kts of                     Just t' -> return t'                     Nothing -> Left (TypeError ctx e (MissingField x t))@@ -706,17 +706,18 @@     | InvalidHandlerOutputType Text (Expr s a) (Expr s a)     | MissingMergeType     | HandlerNotAFunction Text (Expr s a)+    | ConstructorsRequiresAUnionType (Expr s a) (Expr s a)     | NotARecord Text (Expr s a) (Expr s a)     | MissingField Text (Expr s a)     | CantAnd (Expr s a) (Expr s a)     | CantOr (Expr s a) (Expr s a)     | CantEQ (Expr s a) (Expr s a)     | CantNE (Expr s a) (Expr s a)+    | CantInterpolate (Expr s a) (Expr s a)     | CantTextAppend (Expr s a) (Expr s a)     | CantListAppend (Expr s a) (Expr s a)     | CantAdd (Expr s a) (Expr s a)     | CantMultiply (Expr s a) (Expr s a)-    | NoDependentLet (Expr s a) (Expr s a)     | NoDependentTypes (Expr s a) (Expr s a)     deriving (Show) @@ -1725,7 +1726,7 @@         \    └───────────────┘                                                           \n\         \                                                                                \n\         \                                                                                \n\-        \Your first ❰List❱ elements has this type:                                       \n\+        \Your first ❰List❱ element has this type:                                        \n\         \                                                                                \n\         \↳ " <> txt0 <> "                                                                \n\         \                                                                                \n\@@ -2746,6 +2747,58 @@         txt0 = build k         txt1 = build expr0 +prettyTypeMessage (ConstructorsRequiresAUnionType expr0 expr1) = ErrorMessages {..}+  where+    short = "❰constructors❱ requires a union type"++    long =+        "Explanation: You can only use the ❰constructors❱ keyword on an argument that is \n\+        \a union type literal, like this:                                                \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌───────────────────────────────────────────────┐                           \n\+        \    │ constructors < Left : Natural, Right : Bool > │                           \n\+        \    └───────────────────────────────────────────────┘                           \n\+        \                                                                                \n\+        \                                                                                \n\+        \... but you cannot use the ❰constructors❱ keyword on any other type of argument.\n\+        \For example, you cannot use a variable argument:                                \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────┐                                            \n\+        \    │ λ(t : Type) → constructors t │  Invalid: ❰t❱ might not be a union type    \n\+        \    └──────────────────────────────┘                                            \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌─────────────────────────────────────────────────┐                         \n\+        \    │ let t : Type = < Left : Natural, Right : Bool > │  Invalid: Type-checking \n\+        \    │ in  constructors t                              │  precedes normalization \n\+        \    └─────────────────────────────────────────────────┘                         \n\+        \                                                                                \n\+        \                                                                                \n\+        \However, you can import the union type argument:                                \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌────────────────────────────────┐                                          \n\+        \    │ constructors ./unionType.dhall │ Valid: Import resolution precedes        \n\+        \    └────────────────────────────────┘ type-checking                            \n\+        \                                                                                \n\+        \                                                                                \n\+        \────────────────────────────────────────────────────────────────────────────────\n\+        \                                                                                \n\+        \You tried to supply the following argument:                                     \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... which normalized to:                                                        \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n\+        \                                                                                \n\+        \... which is not a union type literal                                           \n"+      where+        txt0 = build expr0+        txt1 = build expr1+  prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..}   where     short = "Not a record"@@ -2858,6 +2911,70 @@ prettyTypeMessage (CantNE expr0 expr1) =         buildBooleanOperator "/=" expr0 expr1 +prettyTypeMessage (CantInterpolate expr0 expr1) = ErrorMessages {..}+  where+    short = "You can only interpolate ❰Text❱"++    long =+        "Explanation: Text interpolation only works on expressions of type ❰Text❱        \n\+        \                                                                                \n\+        \For example, these are all valid uses of string interpolation:                  \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────┐                                                        \n\+        \    │ \"ABC${\"DEF\"}GHI\" │                                                    \n\+        \    └──────────────────┘                                                        \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌────────────────────────────┐                                              \n\+        \    │ λ(x : Text) → \"ABC${x}GHI\" │                                            \n\+        \    └────────────────────────────┘                                              \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌───────────────────────────────────────────────────────────────────┐       \n\+        \    │ λ(age : Natural) → \"Age: ${Integer/show (Natural/toInteger age)}\" │     \n\+        \    └───────────────────────────────────────────────────────────────────┘       \n\+        \                                                                                \n\+        \                                                                                \n\+        \Some common reasons why you might get this error:                               \n\+        \                                                                                \n\+        \● You might have thought that string interpolation automatically converts the   \n\+        \  interpolated value to a ❰Text❱ representation of that value:                  \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────────┐                                        \n\+        \    │ λ(age : Natural) → \"Age: ${age}\" │                                      \n\+        \    └──────────────────────────────────┘                                        \n\+        \                                  ⇧                                             \n\+        \                                  Invalid: ❰age❱ has type ❰Natural❱             \n\+        \                                                                                \n\+        \                                                                                \n\+        \● You might have forgotten to escape a string interpolation that you wanted     \n\+        \  Dhall to ignore and pass through:                                             \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌────────────────┐                                                          \n\+        \    │ \"echo ${HOME}\" │                                                        \n\+        \    └────────────────┘                                                          \n\+        \             ⇧                                                                  \n\+        \             ❰HOME❱ is not in scope and this might have meant to use ❰\\${HOME}❱\n\+        \                                                                                \n\+        \                                                                                \n\+        \────────────────────────────────────────────────────────────────────────────────\n\+        \                                                                                \n\+        \You interpolated this expression:                                               \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... which does not have type ❰Text❱ but instead has type:                       \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n"+      where+        txt0 = build expr0+        txt1 = build expr1++ + prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..}   where     short = "❰++❱ only works on ❰Text❱"@@ -2974,91 +3091,6 @@         \↳ " <> txt1 <> "                                                                \n\         \                                                                                \n\         \... which makes this a forbidden dependent function type                        \n"-      where-        txt0 = build expr0-        txt1 = build expr1--prettyTypeMessage (NoDependentLet expr0 expr1) = ErrorMessages {..}-  where-    short = "No dependent ❰let❱"--    long =-        "Explanation: The Dhall programming language does not allow ❰let❱ expressions    \n\-        \from terms to types.  These ❰let❱ expressions are also known as \"dependent ❰let❱\n\-        \expressions\" because you have a type whose value depends on the value of a term.\n\-        \                                                                                \n\-        \The Dhall language forbids these dependent ❰let❱ expressions in order to        \n\-        \guarantee that ❰let❱ expressions of the form:                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌────────────────────┐                                                      \n\-        \    │ let x : t = r in e │                                                      \n\-        \    └────────────────────┘                                                      \n\-        \                                                                                \n\-        \                                                                                \n\-        \... are always equivalent to:                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌──────────────────┐                                                        \n\-        \    │ (λ(x : t) → e) r │                                                        \n\-        \    └──────────────────┘                                                        \n\-        \                                                                                \n\-        \                                                                                \n\-        \This means that both expressions should normalize to the same result and if one \n\-        \of the two fails to type check then the other should fail to type check, too.   \n\-        \                                                                                \n\-        \For this reason, the following is " <> _NOT <> " legal code:                    \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────┐                                                       \n\-        \    │ let x = 2 in Text │                                                       \n\-        \    └───────────────────┘                                                       \n\-        \                                                                                \n\-        \                                                                                \n\-        \... because the above ❰let❱ expression is equivalent to:                        \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌─────────────────────────────┐                                             \n\-        \    │ let x : Integer = 2 in Text │                                             \n\-        \    └─────────────────────────────┘                                             \n\-        \                                                                                \n\-        \                                                                                \n\-        \... which in turn must be equivalent to:                                        \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────────┐                                               \n\-        \    │ (λ(x : Integer) → Text) 2 │                                               \n\-        \    └───────────────────────────┘                                               \n\-        \                                                                                \n\-        \                                                                                \n\-        \... which in turn fails to type check because this sub-expression:              \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────┐                                                   \n\-        \    │ λ(x : Integer) → Text │                                                   \n\-        \    └───────────────────────┘                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \... has type:                                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────┐                                                   \n\-        \    │ ∀(x : Integer) → Text │                                                   \n\-        \    └───────────────────────┘                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \... which is a forbidden dependent function type (i.e. a function from a term to\n\-        \a type).  Therefore the equivalent ❰let❱ expression is also forbidden.          \n\-        \                                                                                \n\-        \Your ❰let❱ expression is invalid because the input has type:                    \n\-        \                                                                                \n\-        \↳ " <> txt0 <> "                                                                \n\-        \                                                                                \n\-        \... and the output has kind:                                                    \n\-        \                                                                                \n\-        \↳ " <> txt1 <> "                                                                \n\-        \                                                                                \n\-        \... which makes this a forbidden dependent ❰let❱ expression                     \n"       where         txt0 = build expr0         txt1 = build expr1

@@ -108,6 +108,9 @@                 "merge"                 "./tests/parser/merge.dhall"             , shouldPass+                "constructors"+                "./tests/parser/constructors.dhall"+            , shouldPass                 "fields"                 "./tests/parser/fields.dhall"             , shouldPass

@@ -7,13 +7,18 @@  import qualified Control.Exception import qualified Data.Map+import qualified Data.Text.Lazy.IO+import qualified Data.Text.Prettyprint.Doc+import qualified Data.Text.Prettyprint.Doc.Render.Text import qualified Dhall import qualified Dhall.Core import qualified Dhall.Parser+import qualified System.Timeout import qualified Test.Tasty import qualified Test.Tasty.HUnit import qualified Util +import Control.DeepSeq (($!!)) import Dhall.Import (Imported) import Dhall.Parser (Src) import Dhall.TypeCheck (TypeError, X)@@ -27,6 +32,9 @@         , issue126         , issue151         , issue164+        , issue201+        , issue209+        , issue216         , parsing0         , typeChecking0         , typeChecking1@@ -114,6 +122,40 @@     -- single-quoted string     _ <- Util.code "./tests/regression/issue164.dhall"     return () )++issue201 :: TestTree+issue201 = Test.Tasty.HUnit.testCase "Issue #201" (do+    -- Verify that type synonyms work+    _ <- Util.code "./tests/regression/issue201.dhall"+    return () )++issue209 :: TestTree+issue209 = Test.Tasty.HUnit.testCase "Issue #209" (do+    -- Verify that pretty-printing `constructors` doesn't trigger an infinite+    -- loop+    e <- Util.code "./tests/regression/issue209.dhall"+    let text = Dhall.Core.pretty e+    Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $!! text)+    return () )++opts :: Data.Text.Prettyprint.Doc.LayoutOptions+opts =+    Data.Text.Prettyprint.Doc.defaultLayoutOptions+        { Data.Text.Prettyprint.Doc.layoutPageWidth =+            Data.Text.Prettyprint.Doc.AvailablePerLine 80 1.0+        }++issue216 :: TestTree+issue216 = Test.Tasty.HUnit.testCase "Issue #216" (do+    -- Verify that pretty-printing preserves string interpolation+    e <- Util.code "./tests/regression/issue216a.dhall"+    let doc       = Data.Text.Prettyprint.Doc.pretty e+    let docStream = Data.Text.Prettyprint.Doc.layoutSmart opts doc+    let text0 = Data.Text.Prettyprint.Doc.Render.Text.renderLazy docStream++    text1 <- Data.Text.Lazy.IO.readFile "./tests/regression/issue216b.dhall"++    Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 )  parsing0 :: TestTree parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do

@@ -10,8 +10,11 @@ import qualified Test.Tasty.HUnit import qualified Util +import Data.Monoid ((<>))+import Data.Text (Text) import Dhall (Inject) import GHC.Generics (Generic)+import Numeric.Natural (Natural) import Test.Tasty (TestTree) import Test.Tasty.HUnit ((@?=)) @@ -27,6 +30,13 @@             , _Functions_1             , _Functions_2             ]+        , Test.Tasty.testGroup "Unions"+            [ example 0 "./tests/tutorial/unions0A.dhall" "./tests/tutorial/unions0B.dhall"+            , example 1 "./tests/tutorial/unions1A.dhall" "./tests/tutorial/unions1B.dhall"+            , example 2 "./tests/tutorial/unions2A.dhall" "./tests/tutorial/unions2B.dhall"+            , example 3 "./tests/tutorial/unions3A.dhall" "./tests/tutorial/unions3B.dhall"+            , example 4 "./tests/tutorial/unions4A.dhall" "./tests/tutorial/unions4B.dhall"+            ]         ]  _Interpolation_0 :: TestTree@@ -67,3 +77,9 @@     f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar"     f (Example0 { foo = True, bar = False }) @?= False     f (Example0 { foo = True, bar = True  }) @?= True )++example :: Natural -> Text -> Text -> TestTree+example n text0 text1 =+    Test.Tasty.HUnit.testCase+        ("Example #" <> show n)+        (Util.equivalent text0 text1)

@@ -3,6 +3,7 @@ module Util     ( code     , codeWith+    , equivalent     , normalize'     , normalizeWith'     , assertNormalizesTo@@ -47,6 +48,12 @@         Left typeError -> Control.Exception.throwIO typeError         Right _        -> return ()     return expr1++equivalent :: Data.Text.Text -> Data.Text.Text -> IO ()+equivalent text0 text1 = do+    expr0 <- fmap Dhall.Core.normalize (Util.code text0) :: IO (Expr X X)+    expr1 <- fmap Dhall.Core.normalize (Util.code text1) :: IO (Expr X X)+    assertEqual "Expressions are not equivalent" expr0 expr1  assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO () assertNormalizesTo e expected = do 

@@ -0,0 +1,1 @@+constructors < Left : Natural | Right : Bool >

@@ -1,2 +1,1 @@-let `let` = 1-in  `let`+{ example1 = let `let` = 1 in `let`, example2 = let `:.` = 1 in `:.` }

@@ -0,0 +1,1 @@+let Foo = {} in {=} : Foo

@@ -0,0 +1,1 @@+constructors <>

@@ -0,0 +1,5 @@+let GitHubProject : Type = { owner : Text, repo : Text } in+let gitHubProject = \( github : GitHubProject ) ->+     let gitHubRoot = "https://github.com/${github.owner}/${github.repo}"+	 in { bugReports = "${gitHubRoot}/issues"  }+in gitHubProject

@@ -0,0 +1,10 @@+    let GitHubProject : Type = { owner : Text, repo : Text }++in  let gitHubProject =+            λ(github : GitHubProject)+          →     let gitHubRoot =+                      "https://github.com/${github.owner}/${github.repo}"+            +            in  { bugReports = "${gitHubRoot}/issues" }++in  gitHubProject

@@ -0,0 +1,6 @@+    λ(union : < Left : Natural | Right : Bool >)+→   let handlers =+            { Left  = Natural/even  -- Natural/even is a built-in function+            , Right = λ(b : Bool) → b+            }+in  merge handlers union : Bool

@@ -0,0 +1,1 @@+./process.dhall < Left = +3 | Right : Bool >

@@ -0,0 +1,1 @@+False

@@ -0,0 +1,1 @@+./process.dhall < Right = True | Left : Natural >

@@ -0,0 +1,1 @@+True

@@ -0,0 +1,8 @@+    let Empty  = < Empty = {=} | Person : { name : Text, age : Natural } >+in  let Person =+        λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} >+in  [   Empty+    ,   Person { name = "John", age = +23 }+    ,   Person { name = "Amy" , age = +25 }+    ,   Empty+    ]

@@ -0,0 +1,5 @@+[ < Empty = {=} | Person : { age : Natural, name : Text } >+, < Person = { age = +23, name = "John" } | Empty : {} >+, < Person = { age = +25, name = "Amy" } | Empty : {} >+, < Empty = {=} | Person : { age : Natural, name : Text } >+]

@@ -0,0 +1,5 @@+    let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >+in  [   MyType.Empty {=}+    ,   MyType.Person { name = "John", age = +23 }+    ,   MyType.Person { name = "Amy" , age = +25 }+    ]

@@ -0,0 +1,4 @@+[ < Empty = {=} | Person : { age : Natural, name : Text } >+, < Person = { age = +23, name = "John" } | Empty : {} >+, < Person = { age = +25, name = "Amy" } | Empty : {} >+]

@@ -0,0 +1,1 @@+constructors < Empty : {} | Person : { name : Text, age : Natural } >

@@ -0,0 +1,6 @@+{ Empty  =+    λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >+, Person =+      λ(Person : { age : Natural, name : Text })+    → < Person = Person | Empty : {} >+}