dhall 1.12.0 → 1.13.0

raw patch · 24 files changed

+2407/−425 lines, 24 filesdep +megaparsecdep +optparse-applicativedep +semigroupsdep −ansi-wl-pprintdep −base16-bytestringdep −optparse-genericdep ~ansi-terminaldep ~basedep ~transformersPVP ok

version bump matches the API change (PVP)

Dependencies added: megaparsec, optparse-applicative, semigroups

Dependencies removed: ansi-wl-pprint, base16-bytestring, optparse-generic, trifecta

Dependency ranges changed: ansi-terminal, base, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +53/−0
• dhall-format/Main.hs +36/−18
• dhall-hash/Main.hs +34/−17
• dhall-repl/Main.hs +6/−4
• dhall.cabal +28/−22
• dhall/Main.hs +136/−47
• src/Dhall.hs +113/−26
• src/Dhall/Context.hs +3/−6
• src/Dhall/Core.hs +83/−6
• src/Dhall/Diff.hs +1120/−0
• src/Dhall/Import.hs +24/−63
• src/Dhall/Parser.hs +115/−61
• src/Dhall/Pretty/Internal.hs +79/−21
• src/Dhall/Tutorial.hs +80/−50
• src/Dhall/TypeCheck.hs +464/−79
• tests/Normalization.hs +11/−3
• tests/Parser.hs +3/−0
• tests/normalization/tutorial/combineTypes/0A.dhall +1/−0
• tests/normalization/tutorial/combineTypes/0B.dhall +1/−0
• tests/normalization/tutorial/projection/0A.dhall +1/−0
• tests/normalization/tutorial/projection/0B.dhall +1/−0
• tests/parser/template.dhall +13/−0
• tests/typecheck/fieldsAreTypesA.dhall +1/−1
• tests/typecheck/fieldsAreTypesB.dhall +1/−1

@@ -1,3 +1,56 @@+1.13.0++* BUG FIX: Fix semantic integrity hashing support+    * Both parsing and pretty-printing semantic hashes were broken since version+      1.11.0+    * See: https://github.com/dhall-lang/dhall-haskell/pull/345+* BUG FIX: Allow leading whitespace in interpolated expresssions+    * See: https://github.com/dhall-lang/dhall-haskell/pull/369+* BUG FIX: Fix `deriving (Interpret)` for sum types+    * The types of alternatives were not correctly included in the corresponding+      Dhall type+    * See: https://github.com/dhall-lang/dhall-haskell/pull/348+* BREAKING CHANGE TO LANGUAGE: Records cannot store both types and terms+    * Records can also not store type-level functions (like `List`)+        * Records might be allowed to store type-level functions again in the+          future+    * This fixes a potential soundness bug+    * The primarily practical consequence of this change is that if you are+      hosting a "package" then you will need to split terms and types from your+      package into different records for your users to import+    * This also implies removing the `./Monoid` type-level function from the+      `./Prelude/package.dhall` record+    * See: https://github.com/dhall-lang/dhall-haskell/pull/335+* BREAKING CHANGE TO THE API: Replace `trifecta` with `megaparsec`+    * This change the API to use the `Parser` type from `megaparsec`+    * This also slightly changes the type of `exprFromText`+    * If you program using the type classes provided by the `parsers` library+      then this is not a breaking change as that interface is preserved+    * See: https://github.com/dhall-lang/dhall-haskell/pull/268+* BREAKING CHANGE TO THE API: New `⩓` operator for merging record types+    * Example: `{ foo : Text } ⩓ { bar : Bool } = { foo : Text, bar : Bool }`+    * This is breaking because it adds a new constructor to the `Expr` type+    * See: https://github.com/dhall-lang/dhall-haskell/pull/342+* BREAKING CHANGE TO THE API: New support for projecting a subset of fields+    * Example: `{ x = 1, y = 2, z = 3 }.{ x, y } = { x = 1, y = 2 }`+    * This is breaking because it adds a new constructor to the `Expr` type+    * See: https://github.com/dhall-lang/dhall-haskell/pull/350+* API+UX feature: New support for pretty-printing diffs of Dhall expressions+    * Error messages also use this feature to simplify large type mismatches+    * There is also a new `Dhall.Diff` module+    * See: https://github.com/dhall-lang/dhall-haskell/pull/336+* Add `version`, `resolve`, `type`, and `normalize` sub-commands to interpreter+    * See: https://github.com/dhall-lang/dhall-haskell/pull/352+* Support GHC 7.10.3+    * See: https://github.com/dhall-lang/dhall-haskell/pull/340+* `:type` command in `dhall-repl` now only displays the type+    * Before it would also display the original expression+    * See: https://github.com/dhall-lang/dhall-haskell/pull/344+* Trim dependency tree+    * See: https://github.com/dhall-lang/dhall-haskell/pull/351+    * See: https://github.com/dhall-lang/dhall-haskell/pull/268+    * See: https://github.com/dhall-lang/dhall-haskell/pull/355+ 1.12.0  * Additional changes to support GHC 8.4

@@ -1,10 +1,5 @@-{-# LANGUAGE DataKinds          #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE FlexibleInstances  #-}-{-# LANGUAGE OverloadedStrings  #-}-{-# LANGUAGE RecordWildCards    #-}-{-# LANGUAGE TypeOperators      #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards   #-}  {-| Utility executable for pretty-printing Dhall code @@ -27,16 +22,16 @@ -} module Main where +import Control.Applicative (optional) import Control.Exception (SomeException) import Control.Monad (when) import Data.Monoid ((<>)) import Data.Version (showVersion) import Dhall.Parser (exprAndHeaderFromText) import Dhall.Pretty (annToAnsiStyle, prettyExpr)-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))+import Options.Applicative (Parser, ParserInfo) import System.IO (stderr) import System.Exit (exitFailure, exitSuccess)-import Text.Trifecta.Delta (Delta(..))  import qualified Paths_dhall as Meta @@ -46,25 +41,48 @@ import qualified Data.Text.Lazy.IO import qualified Data.Text.Prettyprint.Doc                 as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty-import qualified Options.Generic+import qualified Options.Applicative import qualified System.Console.ANSI import qualified System.IO -data Options w = Options-    { version :: w ::: Bool           <?> "Display version and exit"-    , inplace :: w ::: Maybe FilePath <?> "Modify the specified file in-place"-    } deriving (Generic)+data Options = Options+    { version :: Bool+    , inplace :: Maybe FilePath+    } -instance ParseRecord (Options Wrapped)+parseOptions :: Parser Options+parseOptions = Options <$> parseVersion <*> optional parseInplace+  where+    parseVersion =+        Options.Applicative.switch+        (   Options.Applicative.long "version"+        <>  Options.Applicative.help "Display version and exit"+        ) +    parseInplace =+        Options.Applicative.strOption+        (   Options.Applicative.long "inplace"+        <>  Options.Applicative.help "Modify the specified file in-place"+        <>  Options.Applicative.metavar "FILE"+        )+ opts :: Pretty.LayoutOptions opts =     Pretty.defaultLayoutOptions         { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } +parserInfo :: ParserInfo Options+parserInfo =+    Options.Applicative.info+        (Options.Applicative.helper <*> parseOptions)+        (   Options.Applicative.progDesc "Formatter for the Dhall language"+        <>  Options.Applicative.fullDesc+        )+ main :: IO () main = do-    Options {..} <- Options.Generic.unwrapRecord "Formatter for the Dhall language"+    Options {..} <- Options.Applicative.execParser parserInfo+     when version $ do       putStrLn (showVersion Meta.version)       exitSuccess@@ -80,7 +98,7 @@             Just file -> do                 strictText <- Data.Text.IO.readFile file                 let lazyText = Data.Text.Lazy.fromStrict strictText-                (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) lazyText of+                (header, expr) <- case exprAndHeaderFromText "(stdin)" lazyText of                     Left  err -> Control.Exception.throwIO err                     Right x   -> return x @@ -92,7 +110,7 @@                 System.IO.hSetEncoding System.IO.stdin System.IO.utf8                 inText <- Data.Text.Lazy.IO.getContents -                (header, expr) <- case exprAndHeaderFromText (Directed "(stdin)" 0 0 0 0) inText of+                (header, expr) <- case exprAndHeaderFromText "(stdin)" inText of                     Left  err -> Control.Exception.throwIO err                     Right x   -> return x 

@@ -1,43 +1,60 @@-{-# LANGUAGE DataKinds          #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE FlexibleInstances  #-}-{-# LANGUAGE OverloadedStrings  #-}-{-# LANGUAGE RecordWildCards    #-}-{-# LANGUAGE TypeOperators      #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards   #-}  module Main where  import Control.Exception (SomeException) import Control.Monad (when)+import Data.Monoid ((<>)) import Data.Version (showVersion) import Dhall.Core (normalize) import Dhall.Import (Imported(..), hashExpressionToCode, load) import Dhall.Parser (Src, exprFromText) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))+import Options.Applicative (Parser, ParserInfo) import System.IO (stderr) import System.Exit (exitFailure, exitSuccess)-import Text.Trifecta.Delta (Delta(..))  import qualified Paths_dhall as Meta  import qualified Control.Exception import qualified Data.Text.Lazy.IO import qualified Dhall.TypeCheck-import qualified Options.Generic+import qualified Options.Applicative import qualified System.IO -data Options w = Options-    { explain :: w ::: Bool <?> "Explain error messages in more detail"-    , version :: w ::: Bool <?> "Display version and exit"-    } deriving (Generic)+data Options = Options+    { explain :: Bool+    , version :: Bool+    } -instance ParseRecord (Options Wrapped)+parseOptions :: Parser Options+parseOptions = Options <$> parseExplain <*> parseVersion+  where+    parseExplain =+        Options.Applicative.switch+            (   Options.Applicative.long "explain"+            <>  Options.Applicative.help "Explain error messages in more detail"+            ) +    parseVersion =+        Options.Applicative.switch+            (   Options.Applicative.long "version"+            <>  Options.Applicative.help "Display version and exit"+            )++parserInfo :: ParserInfo Options+parserInfo =+    Options.Applicative.info+        (Options.Applicative.helper <*> parseOptions)+        (   Options.Applicative.progDesc "Compute semantic hashes for Dhall expressions"+        <>  Options.Applicative.fullDesc+        )+ main :: IO () main = do-    Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"+    Options {..} <- Options.Applicative.execParser parserInfo+     when version $ do       putStrLn (showVersion Meta.version)       exitSuccess@@ -74,7 +91,7 @@         System.IO.hSetEncoding System.IO.stdin System.IO.utf8         inText <- Data.Text.Lazy.IO.getContents -        expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of+        expr <- case exprFromText "(stdin)" inText of             Left  err  -> Control.Exception.throwIO err             Right expr -> return expr 

@@ -24,7 +24,6 @@ import qualified System.Console.Haskeline.MonadException as Haskeline import qualified System.Console.Repline as Repline import qualified System.IO-import qualified Text.Trifecta.Delta as Trifecta   main :: IO ()@@ -75,7 +74,7 @@   => String -> m ( Dhall.Expr Dhall.Src Dhall.X ) parseAndLoad src = do   parsed <--    case Dhall.exprFromText ( Trifecta.Columns 0 0 ) ( LazyText.pack src ) of+    case Dhall.exprFromText "(stdin)" ( LazyText.pack src ) of       Left e ->         liftIO ( throwIO e ) @@ -117,7 +116,7 @@   exprType' <-     normalize exprType -  output System.IO.stdout ( Expr.Annot loaded exprType' )+  output System.IO.stdout exprType'   @@ -233,6 +232,8 @@     :: (Pretty.Pretty a, MonadIO m)     => System.IO.Handle -> Dhall.Expr s a -> m () output handle expr = do+  liftIO (System.IO.hPutStrLn handle "")  -- Visual spacing+   let opts =           Pretty.defaultLayoutOptions               { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }@@ -245,5 +246,6 @@           else Pretty.unAnnotateS stream    liftIO (Pretty.renderIO handle ansiStream)+  liftIO (System.IO.hPutStrLn handle "") -- Pretty printing doesn't end with a new line -  liftIO (putStrLn "") -- Pretty printing doesn't end with a new line+  liftIO (System.IO.hPutStrLn handle "")  -- Visual spacing

@@ -1,5 +1,5 @@ Name: dhall-Version: 1.12.0+Version: 1.13.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1@@ -82,6 +82,8 @@     Prelude/Text/concatMapSep     Prelude/Text/concatSep     tests/format/*.dhall+    tests/normalization/tutorial/combineTypes/*.dhall+    tests/normalization/tutorial/projection/*.dhall     tests/normalization/*.dhall     tests/normalization/examples/Bool/and/*.dhall     tests/normalization/examples/Bool/build/*.dhall@@ -153,9 +155,8 @@ Library     Hs-Source-Dirs: src     Build-Depends:-        base                        >= 4.9.0.0  && < 5   ,-        ansi-wl-pprint                           < 0.7 ,-        base16-bytestring                        < 0.2 ,+        base                        >= 4.8.2.0  && < 5   ,+        ansi-terminal               >= 0.6.3.1  && < 0.8 ,         bytestring                               < 0.11,         case-insensitive                         < 1.3 ,         containers                  >= 0.5.0.0  && < 0.6 ,@@ -169,6 +170,7 @@         http-client-tls             >= 0.2.0    && < 0.4 ,         insert-ordered-containers   >= 0.1.0.1  && < 0.3 ,         lens-family-core            >= 1.0.0    && < 1.3 ,+        megaparsec                  >= 6.1.1    && < 6.5 ,         memory                      >= 0.14     && < 0.15,         parsers                     >= 0.12.4   && < 0.13,         prettyprinter               >= 1.2.0.1  && < 1.3 ,@@ -176,13 +178,16 @@         scientific                  >= 0.3.0.0  && < 0.4 ,         text                        >= 0.11.1.0 && < 1.3 ,         transformers                >= 0.2.0.0  && < 0.6 ,-        trifecta                    >= 1.6      && < 1.8 ,         unordered-containers        >= 0.1.3.0  && < 0.3 ,         vector                      >= 0.11.0.0 && < 0.13+    if !impl(ghc >= 8.0)+      Build-Depends: semigroups == 0.18.*+     Exposed-Modules:         Dhall,         Dhall.Context,         Dhall.Core,+        Dhall.Diff         Dhall.Import,         Dhall.Parser,         Dhall.Pretty,@@ -190,7 +195,7 @@         Dhall.TypeCheck     Other-Modules:         Dhall.Pretty.Internal-    GHC-Options: -Wall -Wcompat+    GHC-Options: -Wall  Executable dhall     Hs-Source-Dirs: dhall@@ -199,12 +204,12 @@         ansi-terminal               >= 0.6.3.1  && < 0.9 ,         base                        >= 4        && < 5   ,         dhall                                            ,-        optparse-generic            >= 1.1.1    && < 1.4 ,+        optparse-applicative                       < 0.15,         prettyprinter                                    ,         prettyprinter-ansi-terminal >= 1.1.1    && < 1.2 ,-        trifecta                    >= 1.6      && < 1.8 ,+        megaparsec                  >= 6.1.1    && < 6.5 ,         text                        >= 0.11.1.0 && < 1.3-    GHC-Options: -Wall -Wcompat+    GHC-Options: -Wall     Other-Modules:         Paths_dhall @@ -220,9 +225,10 @@         repline          >= 0.1.6.0  && < 0.2 ,         prettyprinter                         ,         prettyprinter-ansi-terminal           ,-        text                                  ,-        trifecta-    GHC-Options: -Wall -Wcompat+        text+    if !impl(ghc >= 8.0)+      Build-Depends: transformers == 0.4.2.*+    GHC-Options: -Wall  Executable dhall-format     Hs-Source-Dirs: dhall-format@@ -230,13 +236,13 @@     Build-Depends:         base                        >= 4        && < 5   ,         ansi-terminal               >= 0.6.3.1  && < 0.9 ,-        dhall                                ,-        optparse-generic            >= 1.1.1    && < 1.4 ,+        dhall                                            ,+        megaparsec                  >= 6.1.1    && < 6.5 ,+        optparse-applicative                       < 0.15,         prettyprinter               >= 1.2.0.1  && < 1.3 ,         prettyprinter-ansi-terminal >= 1.1.1    && < 1.2 ,-        trifecta                    >= 1.6      && < 1.8 ,         text                        >= 0.11.1.0 && < 1.3-    GHC-Options: -Wall -Wcompat+    GHC-Options: -Wall     Other-Modules:         Paths_dhall @@ -244,11 +250,11 @@     Hs-Source-Dirs: dhall-hash     Main-Is: Main.hs     Build-Depends:-        base             >= 4        && < 5  ,-        dhall                                ,-        optparse-generic >= 1.1.1    && < 1.4,-        trifecta         >= 1.6      && < 1.8,-        text             >= 0.11.1.0 && < 1.3+        base                 >= 4        && < 5   ,+        dhall                                     ,+        optparse-applicative                < 0.15,+        megaparsec           >= 6.1.1    && < 6.5 ,+        text                 >= 0.11.1.0 && < 1.3     Other-Modules:         Paths_dhall @@ -256,7 +262,7 @@     Type: exitcode-stdio-1.0     Hs-Source-Dirs: tests     Main-Is: Tests.hs-    GHC-Options: -Wall -Wcompat+    GHC-Options: -Wall     Other-Modules:         Format         Normalization

@@ -1,25 +1,24 @@-{-# LANGUAGE DataKinds          #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE FlexibleInstances  #-}+{-# LANGUAGE DeriveAnyClass     #-}+{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings  #-} {-# LANGUAGE RecordWildCards    #-}-{-# LANGUAGE TypeOperators      #-}  module Main where -import Control.Exception (SomeException)-import Control.Monad (when)-import Data.Monoid (mempty)+import Control.Applicative ((<|>))+import Control.Exception (Exception, SomeException)+import Data.Monoid (mempty, (<>))+import Data.Text.Prettyprint.Doc (Pretty)+import Data.Typeable (Typeable) import Data.Version (showVersion)-import Dhall.Core (normalize)+import Dhall.Core (Expr, Path) import Dhall.Import (Imported(..), load) import Dhall.Parser (Src) import Dhall.Pretty (annToAnsiStyle, prettyExpr) import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)-import Options.Generic (Generic, ParseRecord, Wrapped, type (<?>)(..), (:::))-import System.Exit (exitFailure, exitSuccess)-import Text.Trifecta.Delta (Delta(..))+import Options.Applicative (Parser)+import System.Exit (exitFailure)+import System.IO (Handle)  import qualified Paths_dhall as Meta @@ -27,32 +26,97 @@ import qualified Data.Text.Lazy.IO import qualified Data.Text.Prettyprint.Doc                 as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty+import qualified Dhall.Core import qualified Dhall.Parser import qualified Dhall.TypeCheck-import qualified Options.Generic+import qualified Options.Applicative import qualified System.Console.ANSI import qualified System.IO -data Options w = Options-    { explain :: w ::: Bool <?> "Explain error messages in more detail"-    , version :: w ::: Bool <?> "Display version and exit"-    , plain   :: w ::: Bool <?> "Disable syntax highlighting"-    } deriving (Generic)+data Options = Options+    { mode    :: Mode+    , explain :: Bool+    , plain   :: Bool+    } -instance ParseRecord (Options Wrapped)+data Mode = Default | Version | Resolve | Type | Normalize +parseOptions :: Parser Options+parseOptions = Options <$> parseMode <*> parseExplain <*> parsePlain+  where+    parseExplain =+        Options.Applicative.switch+            (   Options.Applicative.long "explain"+            <>  Options.Applicative.help "Explain error messages in more detail"+            )++    parsePlain =+        Options.Applicative.switch+            (   Options.Applicative.long "plain"+            <>  Options.Applicative.help "Disable syntax highlighting"+            )++parseMode :: Parser Mode+parseMode =+        subcommand "version"   "Display version"                 Version+    <|> subcommand "resolve"   "Resolve an expression's imports" Resolve+    <|> subcommand "type"      "Infer an expression's type"      Type+    <|> subcommand "normalize" "Normalize an expression"         Normalize+    <|> pure Default+  where+    subcommand name description mode =+        Options.Applicative.subparser+            (   Options.Applicative.command name parserInfo+            <>  Options.Applicative.metavar name+            )+      where+        parserInfo =+            Options.Applicative.info parser+                (   Options.Applicative.fullDesc+                <>  Options.Applicative.progDesc description+                )++        parser =+            Options.Applicative.helper <*> pure mode+ opts :: Pretty.LayoutOptions opts =     Pretty.defaultLayoutOptions         { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } +data ImportResolutionDisabled =+    ImportResolutionDisabled deriving (Exception, Typeable)++instance Show ImportResolutionDisabled where+    show _ = "\nImport resolution is disabled"++throws :: Exception e => Either e a -> IO a+throws (Left  e) = Control.Exception.throwIO e+throws (Right a) = return a++getExpression :: IO (Expr Src Path)+getExpression = do+    inText <- Data.Text.Lazy.IO.getContents++    throws (Dhall.Parser.exprFromText "(stdin)" inText)++assertNoImports :: Expr Src Path -> IO (Expr Src X)+assertNoImports expression =+    throws (traverse (\_ -> Left ImportResolutionDisabled) expression)+ main :: IO () main = do-    Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"-    when version $ do-      putStrLn (showVersion Meta.version)-      exitSuccess+    let parserInfo =+            Options.Applicative.info+                (Options.Applicative.helper <*> parseOptions)+                (   Options.Applicative.progDesc "Interpreter for the Dhall language"+                <>  Options.Applicative.fullDesc+                ) +    Options {..} <- Options.Applicative.execParser parserInfo++    System.IO.hSetEncoding System.IO.stdin System.IO.utf8+     let handle =                 Control.Exception.handle handler2             .   Control.Exception.handle handler1@@ -82,36 +146,61 @@                 System.IO.hPrint System.IO.stderr e                 System.Exit.exitFailure -    handle (do-        System.IO.hSetEncoding System.IO.stdin System.IO.utf8-        inText <- Data.Text.Lazy.IO.getContents+    let render :: Pretty a => Handle -> Expr s a -> IO ()+        render h e = do+            let doc = prettyExpr e -        expr <- case Dhall.Parser.exprFromText (Directed "(stdin)" 0 0 0 0) inText of-            Left  err -> Control.Exception.throwIO err-            Right x   -> return x+            let layoutOptions = opts -        let render h e = do-                let doc = prettyExpr e+            let stream = Pretty.layoutSmart layoutOptions doc -                let layoutOptions = opts-                let stream = Pretty.layoutSmart layoutOptions doc+            supportsANSI <- System.Console.ANSI.hSupportsANSI h+            let ansiStream =+                    if supportsANSI && not plain+                    then fmap annToAnsiStyle stream+                    else Pretty.unAnnotateS stream -                supportsANSI <- System.Console.ANSI.hSupportsANSI h-                let ansiStream =-                        if supportsANSI && not plain-                        then fmap annToAnsiStyle stream-                        else Pretty.unAnnotateS stream+            Pretty.renderIO h ansiStream+            Data.Text.Lazy.IO.hPutStrLn h "" -                Pretty.renderIO h ansiStream-                Data.Text.Lazy.IO.hPutStrLn h ""+    handle $ case mode of+        Version -> do+            putStrLn (showVersion Meta.version) +        Default -> do+            expression <- getExpression -        expr' <- load expr+            resolvedExpression <- load expression -        typeExpr <- case Dhall.TypeCheck.typeOf expr' of-            Left  err      -> Control.Exception.throwIO err-            Right typeExpr -> return typeExpr+            inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression) -        render System.IO.stderr (normalize typeExpr)-        Data.Text.Lazy.IO.hPutStrLn System.IO.stderr mempty-        render System.IO.stdout (normalize expr') )+            render System.IO.stderr (Dhall.Core.normalize inferredType)++            Data.Text.Lazy.IO.hPutStrLn System.IO.stderr mempty++            render System.IO.stdout (Dhall.Core.normalize resolvedExpression)++        Resolve -> do+            expression <- getExpression++            resolvedExpression <- load expression++            render System.IO.stdout resolvedExpression++        Normalize -> do+            expression <- getExpression++            resolvedExpression <- assertNoImports expression++            _ <- throws (Dhall.TypeCheck.typeOf resolvedExpression)++            render System.IO.stdout (Dhall.Core.normalize resolvedExpression)++        Type -> do+            expression <- getExpression++            resolvedExpression <- assertNoImports expression++            inferredType <- throws (Dhall.TypeCheck.typeOf resolvedExpression)++            render System.IO.stdout (Dhall.Core.normalize inferredType)

@@ -1,16 +1,15 @@-{-# LANGUAGE DefaultSignatures   #-}-{-# LANGUAGE DeriveAnyClass      #-}-{-# LANGUAGE DeriveFunctor       #-}-{-# LANGUAGE DeriveGeneric       #-}-{-# LANGUAGE FlexibleInstances   #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE RecordWildCards     #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving  #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE DefaultSignatures          #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings          #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE RecordWildCards            #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE StandaloneDeriving         #-}+{-# LANGUAGE TypeOperators              #-}  {-| Please read the "Dhall.Tutorial" module, which contains a tutorial explaining     how to use the language, the compiler, and this library@@ -25,6 +24,7 @@      -- * Types     , Type(..)+    , RecordType(..)     , InputType(..)     , Interpret(..)     , InvalidType(..)@@ -46,6 +46,8 @@     , unit     , string     , pair+    , record+    , field     , GenericInterpret(..)     , GenericInject(..) @@ -82,11 +84,12 @@ import GHC.Generics import Numeric.Natural (Natural) import Prelude hiding (maybe, sequence)-import Text.Trifecta.Delta (Delta(..)) +import qualified Control.Applicative import qualified Control.Exception-import qualified Data.ByteString.Lazy import qualified Data.Foldable+import qualified Data.Functor.Compose+import qualified Data.Functor.Product import qualified Data.HashMap.Strict.InsOrd import qualified Data.Scientific import qualified Data.Sequence@@ -94,7 +97,6 @@ import qualified Data.Text import qualified Data.Text.Lazy import qualified Data.Text.Lazy.Builder-import qualified Data.Text.Lazy.Encoding import qualified Data.Vector import qualified Dhall.Context import qualified Dhall.Core@@ -166,13 +168,10 @@     -> IO a     -- ^ The decoded value in Haskell inputWith (Type {..}) ctx n txt = do-    let delta = Directed "(input)" 0 0 0 0-    expr  <- throws (Dhall.Parser.exprFromText delta txt)+    expr  <- throws (Dhall.Parser.exprFromText "(input)" txt)     expr' <- Dhall.Import.loadWithContext ctx expr     let suffix =-            ( Data.ByteString.Lazy.toStrict-            . Data.Text.Lazy.Encoding.encodeUtf8-            . Data.Text.Lazy.Builder.toLazyText+            ( Data.Text.Lazy.Builder.toLazyText             . build             ) expected     let annot = case expr' of@@ -580,7 +579,7 @@          Type extractIn expectedIn = autoWith opts -deriving instance (Interpret a, Interpret b) => Interpret (a, b)+instance (Interpret a, Interpret b) => Interpret (a, b)  {-| Use the default options for interpreting a configuration file @@ -884,7 +883,7 @@  instance Inject Double where     injectWith =-        fmap (contramap (Data.Scientific.fromFloatDigits @Double)) injectWith+        fmap (contramap (Data.Scientific.fromFloatDigits :: Double -> Scientific)) injectWith  instance Inject () where     injectWith _ = InputType {..}@@ -923,7 +922,7 @@ instance Inject a => Inject (Data.Set.Set a) where     injectWith = fmap (contramap Data.Set.toList) injectWith -deriving instance (Inject a, Inject b) => Inject (a, b)+instance (Inject a, Inject b) => Inject (a, b)  {-| This is the underlying class that powers the `Interpret` class's support     for automatically deriving a generic implementation@@ -945,10 +944,10 @@     genericInjectWith options@(InterpretOptions {..}) = pure (InputType {..})       where         embed (L1 (M1 l)) =-            UnionLit keyL (embedL l) Data.HashMap.Strict.InsOrd.empty+            UnionLit keyL (embedL l) (Data.HashMap.Strict.InsOrd.singleton keyR declaredR)          embed (R1 (M1 r)) =-            UnionLit keyR (embedR r) Data.HashMap.Strict.InsOrd.empty+            UnionLit keyR (embedR r) (Data.HashMap.Strict.InsOrd.singleton keyL declaredL)          declared =             Union (Data.HashMap.Strict.InsOrd.fromList [(keyL, declaredL), (keyR, declaredR)])@@ -1058,3 +1057,91 @@         n = undefined          InputType embedIn declaredIn = injectWith opts++{-| The 'RecordType' applicative functor allows you to build a 'Type' parser+    from a Dhall record.++    For example, let's take the following Haskell data type:++> data Project = Project+>   { projectName :: Text+>   , projectDescription :: Text+>   , projectStars :: Natural+>   }++    And assume that we have the following Dhall record that we would like to+    parse as a @Project@:++> { name =+>     "dhall-haskell"+> , description =+>     "A configuration language guaranteed to terminate"+> , stars =+>     +289+> }++    Our parser has type 'Type' @Project@, but we can't build that out of any+    smaller parsers, as 'Type's cannot be combined (they are only 'Functor's).+    However, we can use a 'RecordType' to build a 'Type' for @Project@:++> project :: Type Project+> project =+>   record+>     ( Project <$> field "name" string+>               <*> field "description" string+>               <*> field "stars" natural+>     )++-}++newtype RecordType a =+  RecordType+    ( Data.Functor.Product.Product+        ( Control.Applicative.Const+            ( Data.HashMap.Strict.InsOrd.InsOrdHashMap+                Data.Text.Lazy.Text+                ( Expr Src X )+            )+        )+        ( Data.Functor.Compose.Compose+            ( (->) ( Expr Src X ) )+            Maybe+        )+        a+    )+  deriving (Functor, Applicative)+++-- | Run a 'RecordType' parser to build a 'Type' parser.+record :: RecordType a -> Dhall.Type a+record ( RecordType ( Data.Functor.Product.Pair ( Control.Applicative.Const fields ) ( Data.Functor.Compose.Compose extractF ) ) ) =+  Type+    { extract =+        extractF+    , expected =+        Record fields+    }+++-- | Parse a single field of a record.+field :: Data.Text.Lazy.Text -> Type a -> RecordType a+field key valueType =+  let+    extractBody expr = do+      RecordLit fields <-+        return expr++      Data.HashMap.Strict.InsOrd.lookup key fields+        >>= extract valueType++  in+    RecordType+      ( Data.Functor.Product.Pair+          ( Control.Applicative.Const+              ( Data.HashMap.Strict.InsOrd.singleton+                  key+                  ( Dhall.expected valueType )+              )+          )+          ( Data.Functor.Compose.Compose extractBody )+      )

@@ -1,6 +1,4 @@-{-# LANGUAGE BangPatterns               #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveFunctor #-}  -- | This is a utility module that consolidates all `Context`-related operations @@ -50,7 +48,6 @@ match :: Context a -> Maybe (Text, a, Context a) match (Context ((k, v) : kvs)) = Just (k, v, Context kvs) match (Context           []  ) = Nothing- {-# INLINABLE match #-}  {-| Look up a key by name and index@@ -61,9 +58,9 @@ > lookup k n (insert j v c) = lookup k  n      c  -- k /= j -} lookup :: Text -> Integer -> Context a -> Maybe a-lookup _ !_ (Context         []  ) =+lookup _ _ (Context         []  ) =     Nothing-lookup x !n (Context ((k, v):kvs)) =+lookup x n (Context ((k, v):kvs)) =     if x == k     then if n == 0          then Just v

@@ -60,8 +60,9 @@ import Data.HashSet (HashSet) import Data.String (IsString(..)) import Data.Scientific (Scientific)-import Data.Sequence (Seq, ViewL(..), ViewR(..)) import Data.Semigroup (Semigroup(..))+import Data.Sequence (Seq, ViewL(..), ViewR(..))+import Data.Set (Set) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) import Data.Text.Prettyprint.Doc (Pretty)@@ -76,6 +77,7 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet import qualified Data.Sequence+import qualified Data.Set import qualified Data.Text import qualified Data.Text.Lazy                        as Text import qualified Data.Text.Lazy.Builder                as Builder@@ -111,7 +113,7 @@     = File HasHome FilePath     -- ^ Local path     | URL  Text (Maybe PathHashed)-    -- ^ URL of emote resource and optional headers stored in a path+    -- ^ URL of remote resource and optional headers stored in a path     | Env  Text     -- ^ Environment variable     deriving (Eq, Ord, Show)@@ -305,16 +307,18 @@     | OptionalFold     -- | > OptionalBuild                            ~  Optional/build     | OptionalBuild-    -- | > Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }+    -- | > Record       [(k1, t1), (k2, t2)]        ~  { k1 : t1, k2 : t1 }     | Record    (InsOrdHashMap Text (Expr s a))-    -- | > RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }+    -- | > RecordLit    [(k1, v1), (k2, v2)]        ~  { k1 = v1, k2 = v2 }     | RecordLit (InsOrdHashMap Text (Expr s a))-    -- | > Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1 | k2 : t2 >+    -- | > Union        [(k1, t1), (k2, t2)]        ~  < k1 : t1 | k2 : t2 >     | Union     (InsOrdHashMap Text (Expr s a))-    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1 | k2 : t2 | k3 : t3 >+    -- | > UnionLit k v [(k1, t1), (k2, t2)]        ~  < k = v | k1 : t1 | k2 : t2 >     | UnionLit Text (Expr s a) (InsOrdHashMap Text (Expr s a))     -- | > Combine x y                              ~  x ∧ y     | Combine (Expr s a) (Expr s a)+    -- | > CombineTypes x y                         ~  x ⩓ y+    | CombineTypes (Expr s a) (Expr s a)     -- | > CombineRight x y                         ~  x ⫽ y     | Prefer (Expr s a) (Expr s a)     -- | > Merge x y (Just t )                      ~  merge x y : t@@ -324,6 +328,8 @@     | Constructors (Expr s a)     -- | > Field e x                                ~  e.x     | Field (Expr s a) Text+    -- | > Project e xs                             ~  e.{ xs }+    | Project (Expr s a) (Set Text)     -- | > Note s x                                 ~  e     | Note s (Expr s a)     -- | > Embed path                               ~  path@@ -391,10 +397,12 @@     Union     a          >>= k = Union (fmap (>>= k) a)     UnionLit a b c       >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)     Combine a b          >>= k = Combine (a >>= k) (b >>= k)+    CombineTypes a b     >>= k = CombineTypes (a >>= k) (b >>= k)     Prefer a b           >>= k = Prefer (a >>= k) (b >>= k)     Merge a b c          >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)     Constructors a       >>= k = Constructors (a >>= k)     Field a b            >>= k = Field (a >>= k) b+    Project a b          >>= k = Project (a >>= k) b     Note a b             >>= k = Note a (b >>= k)     Embed a              >>= k = k a @@ -452,10 +460,12 @@     first k (Union a             ) = Union (fmap (first k) a)     first k (UnionLit a b c      ) = UnionLit a (first k b) (fmap (first k) c)     first k (Combine a b         ) = Combine (first k a) (first k b)+    first k (CombineTypes a b    ) = CombineTypes (first k a) (first k b)     first k (Prefer a b          ) = Prefer (first k a) (first k b)     first k (Merge a b c         ) = Merge (first k a) (first k b) (fmap (first k) c)     first k (Constructors a      ) = Constructors (first k a)     first k (Field a b           ) = Field (first k a) b+    first k (Project a b         ) = Project (first k a) b     first k (Note a b            ) = Note (k a) (first k b)     first _ (Embed a             ) = Embed a @@ -690,6 +700,10 @@   where     a' = shift d v a     b' = shift d v b+shift d v (CombineTypes a b) = CombineTypes a' b'+  where+    a' = shift d v a+    b' = shift d v b shift d v (Prefer a b) = Prefer a' b'   where     a' = shift d v a@@ -705,6 +719,9 @@ shift d v (Field a b) = Field a' b   where     a' = shift d v a+shift d v (Project a b) = Project a' b+  where+    a' = shift d v a shift d v (Note a b) = Note a b'   where     b' = shift d v b@@ -830,6 +847,10 @@   where     a' = subst x e a     b' = subst x e b+subst x e (CombineTypes a b) = CombineTypes a' b'+  where+    a' = subst x e a+    b' = subst x e b subst x e (Prefer a b) = Prefer a' b'   where     a' = subst x e a@@ -845,6 +866,9 @@ subst x e (Field a b) = Field a' b   where     a' = subst x e a+subst x e (Project a b) = Project a' b+  where+    a' = subst x e a subst x e (Note a b) = Note a b'   where     b' = subst x e b@@ -1075,6 +1099,12 @@     l₁ = alphaNormalize l₀      r₁ = alphaNormalize r₀+alphaNormalize (CombineTypes l₀ r₀) =+    CombineTypes l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀ alphaNormalize (Prefer l₀ r₀) =     Prefer l₁ r₁   where@@ -1097,6 +1127,10 @@     Field e₁ a   where     e₁ = alphaNormalize e₀+alphaNormalize (Project e₀ a) =+    Project e₁ a+  where+    e₁ = alphaNormalize e₀ alphaNormalize (Note s e₀) =     Note s e₁   where@@ -1194,10 +1228,12 @@ denote (Union a             ) = Union (fmap denote a) denote (UnionLit a b c      ) = UnionLit a (denote b) (fmap denote c) denote (Combine a b         ) = Combine (denote a) (denote b)+denote (CombineTypes a b    ) = CombineTypes (denote a) (denote b) denote (Prefer a b          ) = Prefer (denote a) (denote b) denote (Merge a b c         ) = Merge (denote a) (denote b) (fmap denote c) denote (Constructors a      ) = Constructors (denote a) denote (Field a b           ) = Field (denote a) b+denote (Project a b         ) = Project (denote a) b denote (Embed a             ) = Embed a  {-| Reduce an expression to its normal form, performing beta reduction and applying@@ -1493,6 +1529,17 @@             RecordLit (Data.HashMap.Strict.InsOrd.unionWith decide m n)         decide l r =             Combine l r+    CombineTypes x y -> decide (loop x) (loop y)+      where+        decide (Record m) r | Data.HashMap.Strict.InsOrd.null m =+            r+        decide l (Record n) | Data.HashMap.Strict.InsOrd.null n =+            l+        decide (Record m) (Record n) =+            Record (Data.HashMap.Strict.InsOrd.unionWith decide m n)+        decide l r =+            CombineTypes l r+     Prefer x y -> decide (loop x) (loop y)       where         decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m =@@ -1536,6 +1583,21 @@                     Just v  -> loop v                     Nothing -> Field (RecordLit (fmap loop kvs)) x             r' -> Field r' x+    Project r xs     ->+        case loop r of+            RecordLit kvs ->+                case traverse adapt (Data.Set.toList xs) of+                    Just s  ->+                        loop (RecordLit kvs')+                      where+                        kvs' = Data.HashMap.Strict.InsOrd.fromList s+                    Nothing ->+                        Project (RecordLit (fmap loop kvs)) xs+              where+                adapt x = do+                    v <- Data.HashMap.Strict.InsOrd.lookup x kvs+                    return (x, v)+            r' -> Project r' xs     Note _ e' -> loop e'     Embed a -> Embed a @@ -1704,6 +1766,13 @@                 RecordLit _ -> False                 _ -> True             _ -> True+    CombineTypes x y -> isNormalized x && isNormalized y && combine+      where+        combine = case x of+            Record _ -> case y of+                Record _ -> False+                _ -> True+            _ -> True     Prefer x y -> isNormalized x && isNormalized y && combine       where         combine = case x of@@ -1725,12 +1794,20 @@         case t of             Union _ -> False             _       -> True+     Field r x -> isNormalized r &&         case r of             RecordLit kvs ->                 case Data.HashMap.Strict.InsOrd.lookup x kvs of                     Just _  -> False                     Nothing -> True+            _ -> True+    Project r xs -> isNormalized r &&+        case r of+            RecordLit kvs ->+                if all (flip Data.HashMap.Strict.InsOrd.member kvs) xs+                    then False+                    else True             _ -> True     Note _ e' -> isNormalized e'     Embed _ -> True

@@ -0,0 +1,1120 @@+{-# LANGUAGE CPP               #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards   #-}++{-| This module provides functionality for concisely displaying the difference+    between two expressions++    For example, this is used in type errors to explain why the actual type does+    not match the expected type+-}++module Dhall.Diff (+    -- * Diff+      diffNormalized+    , Dhall.Diff.diff+    ) where++import Data.Foldable (fold)+import Data.HashMap.Strict.InsOrd (InsOrdHashMap)+import Data.Monoid (Any(..))+import Data.Scientific (Scientific)+import Data.Semigroup+import Data.Set (Set)+import Data.String (IsString(..))+import Data.Text.Lazy (Text)+import Data.Text.Prettyprint.Doc (Doc, Pretty)+import Data.List.NonEmpty (NonEmpty(..))+import Dhall.Core (Const(..), Expr(..), Var(..))+import Dhall.Pretty.Internal (Ann)+import Numeric.Natural (Natural)++import qualified Data.HashMap.Strict.InsOrd as HashMap+import qualified Data.List.NonEmpty+import qualified Data.Set+import qualified Data.Text.Prettyprint.Doc  as Pretty+import qualified Dhall.Core+import qualified Dhall.Pretty.Internal      as Internal++data Diff =+    Diff+        { same :: Bool+        , doc  :: Doc Ann+        }++instance Data.Semigroup.Semigroup Diff where+    Diff sameL docL <> Diff sameR docR = Diff (sameL && sameR) (docL <> docR)++instance Monoid (Diff) where+    mempty = Diff {..}+      where+        same = True++        doc = mempty++#if !(MIN_VERSION_base(4,11,0))+    mappend = (<>)+#endif++instance IsString (Diff) where+    fromString string = Diff {..}+      where+        same = True++        doc = fromString string++ignore :: Diff+ignore = "…"++align :: Diff -> Diff+align (Diff {doc = docOld, ..}) = Diff {doc = Pretty.align docOld, .. }++hardline :: Diff+hardline = token Pretty.hardline++minus :: Diff -> Diff+minus l = ("- " <> l) { same = False }++plus :: Diff -> Diff+plus r = ("+ " <> r) { same = False }++difference :: Diff -> Diff -> Diff+difference l r = align (minus l <> hardline <> plus r)++token :: Doc Ann -> Diff+token doc = Diff {..}+  where+    same = True++format :: Diff -> Diff -> Diff+format suffix doc = doc <> (if same doc then suffix else hardline)++builtin :: Doc Ann -> Diff+builtin doc = token (Internal.builtin doc)++keyword :: Doc Ann -> Diff+keyword doc = token (Internal.keyword doc)++operator :: Doc Ann -> Diff+operator doc = token (Internal.operator doc)++colon :: Diff+colon = token Internal.colon++comma :: Diff+comma = token Internal.comma++dot :: Diff+dot = token Internal.dot++equals :: Diff+equals = token Internal.equals++forall :: Diff+forall = token Internal.forall++lambda :: Diff+lambda = token Internal.lambda++langle :: Diff+langle = token Internal.langle++lbrace :: Diff+lbrace = token Internal.lbrace++lbracket :: Diff+lbracket = token Internal.lbracket++lparen :: Diff+lparen = token Internal.lparen++pipe :: Diff+pipe = token Internal.pipe++rangle :: Diff+rangle = token Internal.rangle++rarrow :: Diff+rarrow = token Internal.rarrow++rbrace :: Diff+rbrace = token Internal.rbrace++rbracket :: Diff+rbracket = token Internal.rbracket++rparen :: Diff+rparen = token Internal.rparen++-- | Render the difference between the normal form of two expressions+diffNormalized :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann+diffNormalized l0 r0 = Dhall.Diff.diff l1 r1+  where+    l1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize l0)+    r1 = Dhall.Core.alphaNormalize (Dhall.Core.normalize r0)++-- | Render the difference between two expressions+diff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann+diff l0 r0 = doc+  where+    Diff {..} = diffExprA l0 r0++diffPrimitive :: Eq a => (a -> Diff) -> a -> a -> Diff+diffPrimitive f l r+    | l == r    = ignore+    | otherwise = difference (f l) (f r)++diffLabel :: Text -> Text -> Diff+diffLabel = diffPrimitive (token . Internal.prettyLabel)++diffLabels :: Set Text -> Set Text -> Diff+diffLabels ksL ksR =+    braced (diffFieldNames <> (if anyEqual then [ ignore ] else []))+  where+    extraL = Data.Set.difference ksL ksR+    extraR = Data.Set.difference ksR ksL++    diffFieldNames = foldMap (adapt minus) extraL <> foldMap (adapt plus) extraR+      where+        adapt sign key = [ sign (token (Internal.prettyLabel key)) ]++    anyEqual = not (Data.Set.null (Data.Set.intersection ksL ksR))++diffNatural :: Natural -> Natural -> Diff+diffNatural = diffPrimitive (token . Internal.prettyNatural)++diffScientific :: Scientific -> Scientific -> Diff+diffScientific = diffPrimitive (token . Internal.prettyScientific)++diffConst :: Const -> Const -> Diff+diffConst = diffPrimitive (token . Internal.prettyConst)++diffBool :: Bool -> Bool -> Diff+diffBool = diffPrimitive bool+  where+    bool True  = builtin "True"+    bool False = builtin "False"++diffInteger :: Integer -> Integer -> Diff+diffInteger = diffPrimitive (token . Internal.prettyNumber)++diffVar :: Var -> Var -> Diff+diffVar (V xL nL) (V xR nR) = format mempty label <> "@" <> natural+  where+    label = diffLabel xL xR++    natural = diffInteger nL nR++diffMaybe :: Diff -> (a -> a -> Diff) -> (Maybe a -> Maybe a -> Diff)+diffMaybe _ _ Nothing Nothing =+    mempty+diffMaybe prefix _ Nothing (Just _) =+    difference mempty (prefix <> ignore)+diffMaybe prefix _ (Just _) Nothing =+    difference (prefix <> ignore) mempty+diffMaybe prefix f (Just l) (Just r) =+    prefix <> f l r++enclosed+    :: Diff+    -> Diff+    -> Diff+    -> [Diff]+    -> Diff+enclosed l _ r []   = l <> r+enclosed l m r docs = align (fold (zipWith (<>) prefixes docs) <> suffix)+  where+    prefixes = l : repeat (hardline <> m)++    suffix = hardline <> r++enclosed'+    :: Diff+    -> Diff+    -> NonEmpty (Diff)+    -> Diff+enclosed' l m docs =+    align (fold (Data.List.NonEmpty.zipWith (<>) prefixes docs))+  where+    prefixes = l :| repeat (hardline <> m)++diffKeyVals+    :: Pretty a+    => Diff+    -> InsOrdHashMap Text (Expr s a)+    -> InsOrdHashMap Text (Expr s a)+    -> [Diff]+diffKeyVals assign kvsL kvsR =+    diffFieldNames <> diffFieldValues <> (if anyEqual then [ ignore ] else [])+  where+    ksL = Data.Set.fromList (HashMap.keys kvsL)+    ksR = Data.Set.fromList (HashMap.keys kvsR)++    extraL = Data.Set.difference ksL ksR+    extraR = Data.Set.difference ksR ksL++    diffFieldNames = foldMap (adapt minus) extraL <> foldMap (adapt plus) extraR+      where+        adapt sign key =+            [   sign (token (Internal.prettyLabel key))+            <>  " "+            <>  assign+            <>  " "+            <>  ignore+            ]++    shared = HashMap.intersectionWith diffExprA kvsL kvsR++    diffFieldValues =+        filter (not . same) (HashMap.foldMapWithKey adapt shared)+      where+        adapt key doc =+            [   (if ksL == ksR then mempty else "  ")+            <>  token (Internal.prettyLabel key)+            <>  " "+            <>  assign+            <>  " "+            <>  doc+            ]++    anyEqual = getAny (foldMap (Any . same) shared)++braced :: [Diff] -> Diff+braced = enclosed (lbrace <> " ") (comma <> " ") rbrace++angled :: [Diff] -> Diff+angled = enclosed (langle <> " ") (pipe <> " ") rangle++diffRecord+    :: Pretty a+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff+diffRecord kvsL kvsR = braced (diffKeyVals colon kvsL kvsR)++diffRecordLit+    :: Pretty a+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff+diffRecordLit kvsL kvsR = braced (diffKeyVals equals kvsL kvsR)++diffUnion+    :: Pretty a+    => InsOrdHashMap Text (Expr s a) -> InsOrdHashMap Text (Expr s a) -> Diff+diffUnion kvsL kvsR = angled (diffKeyVals colon kvsL kvsR)++diffUnionLit+    :: Pretty a+    => Text+    -> Text+    -> Expr s a+    -> Expr s a+    -> InsOrdHashMap Text (Expr s a)+    -> InsOrdHashMap Text (Expr s a)+    -> Diff+diffUnionLit kL kR vL vR kvsL kvsR =+        langle+    <>  " "+    <>  format " " (diffLabel kL kR)+    <>  equals+    <>  " "+    <>  format " " (diffExprA vL vR)+    <>  halfAngled (diffKeyVals equals kvsL kvsR)+  where+    halfAngled = enclosed (pipe <> " ") (pipe <> " ") rangle++skeleton :: Pretty a => Expr s a -> Diff+skeleton (Lam {}) =+        lambda+    <>  lparen+    <>  ignore+    <>  " "+    <>  colon+    <>  " "+    <>  ignore+    <>  rparen+    <>  " "+    <>  rarrow+    <>  " "+    <>  ignore+skeleton (Pi {}) =+        forall+    <>  lparen+    <>  ignore+    <>  " "+    <>  colon+    <>  " "+    <>  ignore+    <>  rparen+    <>  " "+    <>  rarrow+    <>  " "+    <>  ignore+skeleton (App {}) =+        ignore+    <>  " "+    <>  ignore+skeleton (Let {}) =+        keyword "let"+    <>  " "+    <>  ignore+    <>  " "+    <>  equals+    <>  " "+    <>  ignore+    <>  " "+    <>  keyword "in"+    <>  " "+    <>  ignore+skeleton (Annot {}) =+        ignore+    <>  " "+    <>  colon+    <>  " "+    <>  ignore+skeleton (BoolAnd {}) =+        ignore+    <>  " "+    <>  operator "&&"+    <>  " "+    <>  ignore+skeleton (BoolOr {}) =+        ignore+    <>  " "+    <>  operator "||"+    <>  " "+    <>  ignore+skeleton (BoolEQ {}) =+        ignore+    <>  " "+    <>  operator "=="+    <>  " "+    <>  ignore+skeleton (BoolNE {}) =+        ignore+    <>  " "+    <>  operator "!="+    <>  " "+    <>  ignore+skeleton (BoolIf {}) =+        keyword "if"+    <>  " "+    <>  ignore+    <>  " "+    <>  keyword "then"+    <>  " "+    <>  ignore+    <>  " "+    <>  keyword "else"+    <>  " "+    <>  ignore+skeleton (NaturalPlus {}) =+        ignore+    <>  " "+    <>  operator "+"+    <>  " "+    <>  ignore+skeleton (NaturalTimes {}) =+        ignore+    <>  " "+    <>  operator "*"+    <>  " "+    <>  ignore+skeleton (TextLit {}) =+        "\""+    <>  ignore+    <>  "\""+skeleton (TextAppend {}) =+        ignore+    <>  " "+    <>  operator "++"+    <>  " "+    <>  ignore+skeleton (ListLit {}) =+        lbracket+    <>  " "+    <>  ignore+    <>  " "+    <>  rbracket+    <>  " "+    <>  colon+    <>  " "+    <>  builtin "List"+    <>  " "+    <>  ignore+skeleton (ListAppend {}) =+        ignore+    <>  " "+    <>  operator "#"+    <>  " "+    <>  ignore+skeleton (OptionalLit {}) =+        lbracket+    <>  " "+    <>  ignore+    <>  " "+    <>  rbracket+    <>  " "+    <>  colon+    <>  " "+    <>  builtin "Optional"+    <>  " "+    <>  ignore+skeleton (Record {}) =+        lbrace+    <>  " "+    <>  ignore+    <>  " "+    <>  colon+    <>  " "+    <>  ignore+    <>  " "+    <>  rbrace+skeleton (RecordLit {}) =+        lbrace+    <>  " "+    <>  ignore+    <>  " "+    <>  equals+    <>  " "+    <>  ignore+    <>  " "+    <>  rbrace+skeleton (Union {}) =+        langle+    <>  " "+    <>  ignore+    <>  " "+    <>  colon+    <>  " "+    <>  ignore+    <>  " "+    <>  rangle+skeleton (UnionLit {}) =+        langle+    <>  " "+    <>  ignore+    <>  " "+    <>  equals+    <>  " "+    <>  ignore+    <>  " "+    <>  rangle+skeleton (Combine {}) =+        ignore+    <>  " "+    <>  operator "∧"+    <>  " "+    <>  ignore+skeleton (CombineTypes {}) =+        ignore+    <>  " "+    <>  operator "⩓"+    <>  " "+    <>  ignore+skeleton (Prefer {}) =+        ignore+    <>  " "+    <>  operator "⫽"+    <>  " "+    <>  ignore+skeleton (Merge {}) =+        keyword "merge"+    <>  " "+    <>  ignore+    <>  " "+    <>  ignore+skeleton (Constructors {}) =+        keyword "constructors"+    <>  " "+    <>  ignore+skeleton (Field {}) =+        ignore+    <>  dot+    <>  ignore+skeleton (Project {}) =+        ignore+    <>  dot+    <>  lbrace+    <>  " "+    <>  ignore+    <>  " "+    <>  rbrace+skeleton x = token (Pretty.pretty x)++mismatch :: Pretty a => Expr s a -> Expr s a -> Diff+mismatch l r = difference (skeleton l) (skeleton r)++diffExprA :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprA l@(Annot {}) r@(Annot {}) =+    enclosed' "  " (colon <> " ") (docs l r)+  where+    docs (Annot aL bL) (Annot aR bR) =+        Data.List.NonEmpty.cons (align doc) (docs bL bR)+      where+        doc = diffExprB aL aR+    docs aL aR =+        diffExprB aL aR :| []+diffExprA l@(Annot {}) r =+    mismatch l r+diffExprA l r@(Annot {}) =+    mismatch l r+diffExprA l r =+    diffExprB l r++diffExprB :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprB l@(Lam {}) r@(Lam {}) =+    enclosed' "  " (rarrow <> " ") (docs l r)+  where+    docs (Lam aL bL cL) (Lam aR bR cR) =+        Data.List.NonEmpty.cons (align doc) (docs cL cR)+      where+        doc =   lambda+            <>  lparen+            <>  format " " (diffLabel aL aR)+            <>  colon+            <>  " "+            <>  format mempty (diffExprA bL bR)+            <>  rparen++    docs aL aR =+        pure (diffExprC aL aR)+diffExprB l@(Lam {}) r =+    mismatch l r+diffExprB l r@(Lam {}) =+    mismatch l r+diffExprB l@(BoolIf {}) r@(BoolIf {}) =+    enclosed' "      " (keyword "else" <> "  ") (docs l r)+  where+    docs (BoolIf aL bL cL) (BoolIf aR bR cR) =+        Data.List.NonEmpty.cons (align doc) (docs cL cR)+      where+        doc =   keyword "if"+            <>  " "+            <>  format " " (diffExprA aL aR)+            <>  keyword "then"+            <>  " "+            <>  diffExprA bL bR+    docs aL aR =+        pure (diffExprB aL aR)+diffExprB l@(BoolIf {}) r =+    mismatch l r+diffExprB l r@(BoolIf {}) =+    mismatch l r+diffExprB l@(Pi {}) r@(Pi {}) =+    enclosed' "  " (rarrow <> " ") (docs l r)+  where+    docs (Pi aL bL cL) (Pi aR bR cR) =+        Data.List.NonEmpty.cons (align doc) (docs cL cR)+      where+        doc =   forall+            <>  lparen+            <>  format " " (diffLabel aL aR)+            <>  colon+            <>  " "+            <>  format mempty (diffExprA bL bR)+            <>  rparen+    docs aL aR = pure (diffExprB aL aR)+diffExprB l@(Pi {}) r =+    mismatch l r+diffExprB l r@(Pi {}) =+    mismatch l r+diffExprB l@(Let {}) r@(Let {}) =+    enclosed' "    " (keyword "in" <> "  ") (docs l r)+  where+    docs (Let aL bL cL dL) (Let aR bR cR dR) =+        Data.List.NonEmpty.cons (align doc) (docs dL dR)+      where+        doc =   keyword "let"+            <>  " "+            <>  format " " (diffLabel aL aR)+            <>  format " " (diffMaybe (colon <> " ") diffExprA bL bR)+            <>  equals+            <>  " "+            <>  diffExprA cL cR+    docs aL aR = pure (diffExprB aL aR)+diffExprB l@(Let {}) r =+    mismatch l r+diffExprB l r@(Let {}) =+    mismatch l r+-- TODO: Implement proper list diff+diffExprB l@(ListLit {}) r@(ListLit {}) =+    mismatch l r+diffExprB l@(ListLit {}) r =+    mismatch l r+diffExprB l r@(ListLit {}) =+    mismatch l r+diffExprB (OptionalLit aL bL) (OptionalLit aR bR) = align doc+  where+    doc =   lbracket+        <>  " "+        <>  format " " (diffMaybe mempty diffExprA bL bR)+        <>  rbracket+        <>  " "+        <>  colon+        <>  " "+        <>  diffExprD (App Optional aL) (App Optional aR)+diffExprB l@(OptionalLit {}) r =+    mismatch l r+diffExprB l r@(OptionalLit {}) =+    mismatch l r+diffExprB (Merge aL bL cL) (Merge aR bR cR) = align doc+  where+    doc =   keyword "merge"+        <>  " "+        <>  format " " (diffExprE aL aR)+        <>  format " " (diffExprE bL bR)+        <>  diffMaybe (colon <> " ") diffExprE cL cR+diffExprB l@(Merge {}) r =+    mismatch l r+diffExprB l r@(Merge {}) =+    mismatch l r+diffExprB l r =+    diffExprC l r++diffExprC :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprC = diffBoolOr++diffBoolOr :: Pretty a => Expr s a -> Expr s a -> Diff+diffBoolOr l@(BoolOr {}) r@(BoolOr {}) =+    enclosed' "    " (operator "||" <> "  ") (docs l r)+  where+    docs (BoolOr aL bL) (BoolOr aR bR) =+        Data.List.NonEmpty.cons (diffTextAppend aL aR) (docs bL bR)+    docs aL aR =+        pure (diffTextAppend aL aR)+diffBoolOr l@(BoolOr {}) r =+    mismatch l r+diffBoolOr l r@(BoolOr {}) =+    mismatch l r+diffBoolOr l r =+    diffTextAppend l r++diffTextAppend :: Pretty a => Expr s a -> Expr s a -> Diff+diffTextAppend l@(TextAppend {}) r@(TextAppend {}) =+    enclosed' "    " (operator "++" <> "  ") (docs l r)+  where+    docs (TextAppend aL bL) (TextAppend aR bR) =+        Data.List.NonEmpty.cons (diffNaturalPlus aL aR) (docs bL bR)+    docs aL aR =+        pure (diffNaturalPlus aL aR)+diffTextAppend l@(TextAppend {}) r =+    mismatch l r+diffTextAppend l r@(TextAppend {}) =+    mismatch l r+diffTextAppend l r =+    diffNaturalPlus l r++diffNaturalPlus :: Pretty a => Expr s a -> Expr s a -> Diff+diffNaturalPlus l@(NaturalPlus {}) r@(NaturalPlus {}) =+    enclosed' "  " (operator "+" <> " ") (docs l r)+  where+    docs (NaturalPlus aL bL) (NaturalPlus aR bR) =+        Data.List.NonEmpty.cons (diffListAppend aL aR) (docs bL bR)+    docs aL aR =+        pure (diffListAppend aL aR)+diffNaturalPlus l@(NaturalPlus {}) r =+    mismatch l r+diffNaturalPlus l r@(NaturalPlus {}) =+    mismatch l r+diffNaturalPlus l r =+    diffListAppend l r++diffListAppend :: Pretty a => Expr s a -> Expr s a -> Diff+diffListAppend l@(ListAppend {}) r@(ListAppend {}) =+    enclosed' "  " (operator "#" <> " ") (docs l r)+  where+    docs (ListAppend aL bL) (ListAppend aR bR) =+        Data.List.NonEmpty.cons (diffBoolAnd aL aR) (docs bL bR)+    docs aL aR =+        pure (diffBoolAnd aL aR)+diffListAppend l@(ListAppend {}) r =+    mismatch l r+diffListAppend l r@(ListAppend {}) =+    mismatch l r+diffListAppend l r =+    diffBoolAnd l r++diffBoolAnd :: Pretty a => Expr s a -> Expr s a -> Diff+diffBoolAnd l@(BoolAnd {}) r@(BoolAnd {}) =+    enclosed' "    " (operator "&&" <> "  ") (docs l r)+  where+    docs (BoolAnd aL bL) (BoolAnd aR bR) =+        Data.List.NonEmpty.cons (diffCombine aL aR) (docs bL bR)+    docs aL aR =+        pure (diffCombine aL aR)+diffBoolAnd l@(BoolAnd {}) r =+    mismatch l r+diffBoolAnd l r@(BoolAnd {}) =+    mismatch l r+diffBoolAnd l r =+    diffCombine l r++diffCombine :: Pretty a => Expr s a -> Expr s a -> Diff+diffCombine l@(Combine {}) r@(Combine {}) =+    enclosed' "  " (operator "∧" <> " ") (docs l r)+  where+    docs (Combine aL bL) (Combine aR bR) =+        Data.List.NonEmpty.cons (diffPrefer aL aR) (docs bL bR)+    docs aL aR =+        pure (diffPrefer aL aR)+diffCombine l@(Combine {}) r =+    mismatch l r+diffCombine l r@(Combine {}) =+    mismatch l r+diffCombine l r =+    diffPrefer l r++diffPrefer :: Pretty a => Expr s a -> Expr s a -> Diff+diffPrefer l@(Prefer {}) r@(Prefer {}) =+    enclosed' "  " (operator "⫽" <> " ") (docs l r)+  where+    docs (Prefer aL bL) (Prefer aR bR) =+        Data.List.NonEmpty.cons (diffCombineTypes aL aR) (docs bL bR)+    docs aL aR =+        pure (diffCombineTypes aL aR)+diffPrefer l@(Prefer {}) r =+    mismatch l r+diffPrefer l r@(Prefer {}) =+    mismatch l r+diffPrefer l r =+    diffCombineTypes l r++diffCombineTypes :: Pretty a => Expr s a -> Expr s a -> Diff+diffCombineTypes l@(CombineTypes {}) r@(CombineTypes {}) =+    enclosed' "  " (operator "*" <> " ") (docs l r)+  where+    docs (CombineTypes aL bL) (CombineTypes aR bR) =+        Data.List.NonEmpty.cons (diffNaturalTimes aL aR) (docs bL bR)+    docs aL aR =+        pure (diffNaturalTimes aL aR)+diffCombineTypes l@(CombineTypes {}) r =+    mismatch l r+diffCombineTypes l r@(CombineTypes {}) =+    mismatch l r+diffCombineTypes l r =+    diffNaturalTimes l r++diffNaturalTimes :: Pretty a => Expr s a -> Expr s a -> Diff+diffNaturalTimes l@(NaturalTimes {}) r@(NaturalTimes {}) =+    enclosed' "  " (operator "*" <> " ") (docs l r)+  where+    docs (NaturalTimes aL bL) (NaturalTimes aR bR) =+        Data.List.NonEmpty.cons (diffBoolEQ aL aR) (docs bL bR)+    docs aL aR =+        pure (diffBoolEQ aL aR)+diffNaturalTimes l@(NaturalTimes {}) r =+    mismatch l r+diffNaturalTimes l r@(NaturalTimes {}) =+    mismatch l r+diffNaturalTimes l r =+    diffBoolEQ l r++diffBoolEQ :: Pretty a => Expr s a -> Expr s a -> Diff+diffBoolEQ l@(BoolEQ {}) r@(BoolEQ {}) =+    enclosed' "    " (operator "==" <> "  ") (docs l r)+  where+    docs (BoolEQ aL bL) (BoolEQ aR bR) =+        Data.List.NonEmpty.cons (diffBoolNE aL aR) (docs bL bR)+    docs aL aR =+        pure (diffBoolNE aL aR)+diffBoolEQ l@(BoolEQ {}) r =+    mismatch l r+diffBoolEQ l r@(BoolEQ {}) =+    mismatch l r+diffBoolEQ l r =+    diffBoolNE l r++diffBoolNE :: Pretty a => Expr s a -> Expr s a -> Diff+diffBoolNE l@(BoolNE {}) r@(BoolNE {}) =+    enclosed' "    " (operator "!=" <> "  ") (docs l r)+  where+    docs (BoolNE aL bL) (BoolNE aR bR) =+        Data.List.NonEmpty.cons (diffExprD aL aR) (docs bL bR)+    docs aL aR =+        pure (diffExprD aL aR)+diffBoolNE l@(BoolNE {}) r =+    mismatch l r+diffBoolNE l r@(BoolNE {}) =+    mismatch l r+diffBoolNE l r =+    diffExprD l r++diffExprD :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprD l@(App {}) r@(App {}) =+    enclosed' mempty mempty (Data.List.NonEmpty.reverse (docs l r))+  where+    docs (App aL bL) (App aR bR) =+        Data.List.NonEmpty.cons (diffExprE bL bR) (docs aL aR)+    docs (Constructors aL) (Constructors aR) =+        diffExprE aL aR :| [ keyword "constructors" ]+    docs aL@(App {}) aR@(Constructors {}) =+        pure (mismatch aL aR)+    docs aL@(Constructors {}) aR@(App {}) =+        pure (mismatch aL aR)+    docs aL aR =+        pure (diffExprE aL aR)+diffExprD l@(App {}) r =+    mismatch l r+diffExprD l r@(App {}) =+    mismatch l r+diffExprD l@(Constructors {}) r@(Constructors {}) =+    enclosed' mempty mempty (keyword "constructors" :| [ diffExprE l r ])+diffExprD l@(Constructors {}) r =+    mismatch l r+diffExprD l r@(Constructors {}) =+    mismatch l r+diffExprD l r =+    diffExprE l r++diffExprE :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprE l@(Field {}) r@(Field {}) =+    enclosed' "  " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r))+  where+    docs (Field aL bL) (Field aR bR) =+        Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR)+    docs (Project aL bL) (Project aR bR) =+        Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)+    docs aL aR =+        pure (diffExprF aL aR)+diffExprE l@(Field {}) r =+    mismatch l r+diffExprE l r@(Field {}) =+    mismatch l r+diffExprE l@(Project {}) r@(Project {}) =+    enclosed' "  " (dot <> " ") (Data.List.NonEmpty.reverse (docs l r))+  where+    docs (Field aL bL) (Field aR bR) =+        Data.List.NonEmpty.cons (diffLabel bL bR) (docs aL aR)+    docs (Project aL bL) (Project aR bR) =+        Data.List.NonEmpty.cons (diffLabels bL bR) (docs aL aR)+    docs aL aR =+        pure (diffExprF aL aR)+diffExprE l@(Project {}) r =+    mismatch l r+diffExprE l r@(Project {}) =+    mismatch l r+diffExprE l r =+    diffExprF l r++diffExprF :: Pretty a => Expr s a -> Expr s a -> Diff+diffExprF (Var aL) (Var aR) =+    diffVar aL aR+diffExprF l@(Var {}) r =+    mismatch l r+diffExprF l r@(Var {}) =+    mismatch l r+diffExprF (Const aL) (Const aR) =+    diffConst aL aR+diffExprF l@(Const {}) r =+    mismatch l r+diffExprF l r@(Const {}) =+    mismatch l r+diffExprF Bool Bool =+    "…"+diffExprF l@Bool r =+    mismatch l r+diffExprF l r@Bool =+    mismatch l r+diffExprF Natural Natural =+    "…"+diffExprF l@Natural r =+    mismatch l r+diffExprF l r@Natural =+    mismatch l r+diffExprF NaturalFold NaturalFold =+    "…"+diffExprF l@NaturalFold r =+    mismatch l r+diffExprF l r@NaturalFold =+    mismatch l r+diffExprF NaturalBuild NaturalBuild =+    "…"+diffExprF l@NaturalBuild r =+    mismatch l r+diffExprF l r@NaturalBuild =+    mismatch l r+diffExprF NaturalIsZero NaturalIsZero =+    "…"+diffExprF l@NaturalIsZero r =+    mismatch l r+diffExprF l r@NaturalIsZero =+    mismatch l r+diffExprF NaturalEven NaturalEven =+    "…"+diffExprF l@NaturalEven r =+    mismatch l r+diffExprF l r@NaturalEven =+    mismatch l r+diffExprF NaturalOdd NaturalOdd =+    "…"+diffExprF l@NaturalOdd r =+    mismatch l r+diffExprF l r@NaturalOdd =+    mismatch l r+diffExprF NaturalToInteger NaturalToInteger =+    "…"+diffExprF l@NaturalToInteger r =+    mismatch l r+diffExprF l r@NaturalToInteger =+    mismatch l r+diffExprF NaturalShow NaturalShow =+    "…"+diffExprF l@NaturalShow r =+    mismatch l r+diffExprF l r@NaturalShow =+    mismatch l r+diffExprF Integer Integer =+    "…"+diffExprF l@Integer r =+    mismatch l r+diffExprF l r@Integer =+    mismatch l r+diffExprF IntegerShow IntegerShow =+    "…"+diffExprF l@IntegerShow r =+    mismatch l r+diffExprF l r@IntegerShow =+    mismatch l r+diffExprF Double Double =+    "…"+diffExprF l@Double r =+    mismatch l r+diffExprF l r@Double =+    mismatch l r+diffExprF DoubleShow DoubleShow =+    "…"+diffExprF l@DoubleShow r =+    mismatch l r+diffExprF l r@DoubleShow =+    mismatch l r+diffExprF Text Text =+    "…"+diffExprF l@Text r =+    mismatch l r+diffExprF l r@Text =+    mismatch l r+diffExprF List List =+    "…"+diffExprF l@List r =+    mismatch l r+diffExprF l r@List =+    mismatch l r+diffExprF ListBuild ListBuild =+    "…"+diffExprF l@ListBuild r =+    mismatch l r+diffExprF l r@ListBuild =+    mismatch l r+diffExprF ListFold ListFold =+    "…"+diffExprF l@ListFold r =+    mismatch l r+diffExprF l r@ListFold =+    mismatch l r+diffExprF ListLength ListLength =+    "…"+diffExprF l@ListLength r =+    mismatch l r+diffExprF l r@ListLength =+    mismatch l r+diffExprF ListHead ListHead =+    "…"+diffExprF l@ListHead r =+    mismatch l r+diffExprF l r@ListHead =+    mismatch l r+diffExprF ListLast ListLast =+    "…"+diffExprF l@ListLast r =+    mismatch l r+diffExprF l r@ListLast =+    mismatch l r+diffExprF ListIndexed ListIndexed =+    "…"+diffExprF l@ListIndexed r =+    mismatch l r+diffExprF l r@ListIndexed =+    mismatch l r+diffExprF ListReverse ListReverse =+    "…"+diffExprF l@ListReverse r =+    mismatch l r+diffExprF l r@ListReverse =+    mismatch l r+diffExprF Optional Optional =+    "…"+diffExprF l@Optional r =+    mismatch l r+diffExprF l r@Optional =+    mismatch l r+diffExprF OptionalFold OptionalFold =+    "…"+diffExprF l@OptionalFold r =+    mismatch l r+diffExprF l r@OptionalFold =+    mismatch l r+diffExprF OptionalBuild OptionalBuild =+    "…"+diffExprF l@OptionalBuild r =+    mismatch l r+diffExprF l r@OptionalBuild =+    mismatch l r+diffExprF (BoolLit aL) (BoolLit aR) =+    diffBool aL aR+diffExprF l@(BoolLit {}) r =+    mismatch l r+diffExprF l r@(BoolLit {}) =+    mismatch l r+diffExprF (IntegerLit aL) (IntegerLit aR) =+    diffInteger aL aR+diffExprF l@(IntegerLit {}) r =+    mismatch l r+diffExprF l r@(IntegerLit {}) =+    mismatch l r+diffExprF (NaturalLit aL) (NaturalLit aR) =+    token (Internal.literal "+") <> diffNatural aL aR+diffExprF l@(NaturalLit {}) r =+    mismatch l r+diffExprF l r@(NaturalLit {}) =+    mismatch l r+diffExprF (DoubleLit aL) (DoubleLit aR) =+    diffScientific aL aR+diffExprF l@(DoubleLit {}) r =+    mismatch l r+diffExprF l r@(DoubleLit {}) =+    mismatch l r+-- TODO: Implement proper textual diff+diffExprF l@(TextLit {}) r@(TextLit {}) =+    mismatch l r+diffExprF l@(TextLit {}) r =+    mismatch l r+diffExprF l r@(TextLit {}) =+    mismatch l r+diffExprF (Record aL) (Record aR) =+    diffRecord aL aR+diffExprF l@(Record {}) r =+    mismatch l r+diffExprF l r@(Record {}) =+    mismatch l r+diffExprF (RecordLit aL) (RecordLit aR) =+    diffRecordLit aL aR+diffExprF l@(RecordLit {}) r =+    mismatch l r+diffExprF l r@(RecordLit {}) =+    mismatch l r+diffExprF (Union aL) (Union aR) =+    diffUnion aL aR+diffExprF l@(Union {}) r =+    mismatch l r+diffExprF l r@(Union {}) =+    mismatch l r+diffExprF (UnionLit aL bL cL) (UnionLit aR bR cR) =+    diffUnionLit aL aR bL bR cL cR+diffExprF l@(UnionLit {}) r =+    mismatch l r+diffExprF l r@(UnionLit {}) =+    mismatch l r+diffExprF aL aR =+    if same doc+    then ignore+    else align ("( " <> doc <> hardline <> ")")+  where+    doc = diffExprA aL aR

@@ -157,15 +157,10 @@ #else import Network.HTTP.Client (HttpException(..), Manager) #endif-import Text.Trifecta (Result(..))-import Text.Trifecta.Delta (Delta(..))  import qualified Control.Monad.Trans.State.Strict as State import qualified Crypto.Hash-import qualified Data.ByteArray import qualified Data.ByteString-import qualified Data.ByteString.Char8-import qualified Data.ByteString.Lazy import qualified Data.CaseInsensitive import qualified Data.Foldable import qualified Data.List                        as List@@ -186,9 +181,9 @@ import qualified System.Environment import qualified System.Directory import qualified System.FilePath                  as FilePath+import qualified Text.Megaparsec import qualified Text.Parser.Combinators import qualified Text.Parser.Token-import qualified Text.Trifecta  builderToString :: Builder -> String builderToString = Text.unpack . Builder.toLazyText@@ -554,23 +549,6 @@         <>  "\n"         <>  "↳ " <> show actualHash <> "\n" -parseFromFileEx-    :: Text.Trifecta.Parser a-    -> FilePath-    -> IO (Text.Trifecta.Result a)-parseFromFileEx parser path = do-    text <- Data.Text.Lazy.IO.readFile path--    let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 text--    let strictBytes = Data.ByteString.Lazy.toStrict lazyBytes--    let delta = Directed bytesPath 0 0 0 0--    return (Text.Trifecta.parseByteString parser delta strictBytes)-  where-    bytesPath = Data.ByteString.Char8.pack path- -- | Parse an expression from a `Path` containing a Dhall program exprFromPath :: Path -> StateT Status IO (Expr Src Path) exprFromPath (Path {..}) = case pathType of@@ -592,18 +570,18 @@                 -- Unfortunately, GHC throws an `InappropriateType` exception                 -- when trying to read a directory, but does not export the                 -- exception, so I must resort to a more heavy-handed `catch`-                let handler :: IOException -> IO (Result (Expr Src Path))+                let handler :: IOException -> IO Text                     handler e = do                         -- If the fallback fails, reuse the original exception                         -- to avoid user confusion-                        parseFromFileEx parser (path </> "@")+                        Data.Text.Lazy.IO.readFile (path </> "@")                             `onException` throwIO e -                x <- parseFromFileEx parser path `catch` handler-                case x of-                    Failure errInfo -> do-                        throwIO (ParseError (Text.Trifecta._errDoc errInfo))-                    Success expr -> do+                text <- Data.Text.Lazy.IO.readFile path `catch` handler+                case Text.Megaparsec.parse parser path text of+                    Left errInfo -> do+                        throwIO (ParseError errInfo text)+                    Right expr -> do                         return expr             RawText -> do                 text <- Data.Text.IO.readFile path@@ -637,9 +615,7 @@                                 )                             )                 let suffix =-                        ( Data.ByteString.Lazy.toStrict-                        . Data.Text.Lazy.Encoding.encodeUtf8-                        . Builder.toLazyText+                        ( Builder.toLazyText                         . build                         ) expected                 let annot = case expr of@@ -671,16 +647,13 @@             Right text -> return text          case pathMode of-            Code -> do-                let urlBytes = Data.Text.Lazy.Encoding.encodeUtf8 url-                let delta =-                        Directed (Data.ByteString.Lazy.toStrict urlBytes) 0 0 0 0-                case Text.Trifecta.parseString parser delta (Text.unpack text) of-                    Failure err -> do+            Code ->+                case Text.Megaparsec.parse parser (Text.unpack url) text of+                    Left err -> do                         -- Also try the fallback in case of a parse error, since                         -- the parse error might signify that this URL points to                         -- a directory list-                        let err' = ParseError (Text.Trifecta._errDoc err)+                        let err' = ParseError err text                          request' <- liftIO (HTTP.parseUrlThrow (Text.unpack url)) @@ -695,25 +668,23 @@                             Left  _     -> liftIO (throwIO err')                             Right text' -> return text' -                        case Text.Trifecta.parseString parser delta (Text.unpack text') of-                            Failure _    -> liftIO (throwIO err')-                            Success expr -> return expr-                    Success expr -> return expr+                        case Text.Megaparsec.parse parser (Text.unpack url) text' of+                            Left _     -> liftIO (throwIO err')+                            Right expr -> return expr+                    Right expr -> return expr             RawText -> do                 return (TextLit (Chunks [] (build text)))     Env env -> liftIO (do         x <- System.Environment.lookupEnv (Text.unpack env)         case x of             Just str -> do+                let text = Text.pack str                 case pathMode of-                    Code -> do-                        let envBytes = Data.Text.Lazy.Encoding.encodeUtf8 env-                        let delta =-                                Directed (Data.ByteString.Lazy.toStrict envBytes) 0 0 0 0-                        case Text.Trifecta.parseString parser delta str of-                            Failure errInfo -> do-                                throwIO (ParseError (Text.Trifecta._errDoc errInfo))-                            Success expr    -> do+                    Code ->+                        case Text.Megaparsec.parse parser (Text.unpack env) text of+                            Left errInfo -> do+                                throwIO (ParseError errInfo text)+                            Right expr   -> do                                 return expr                     RawText -> return (TextLit (Chunks [] (build str)))             Nothing  -> throwIO (MissingEnvironmentVariable env) )@@ -860,14 +831,4 @@     source code to add an integrity check to an import -} hashExpressionToCode :: Expr s X -> Text-hashExpressionToCode expr = "sha256:" <> lazyText-  where-    bytes = hashExpression expr--    bytes16 = Data.ByteArray.convert bytes--    -- Notes that `decodeUtf8` is partial, but the base16-encoded bytestring-    -- should always successfully decode-    text = Data.Text.Encoding.decodeUtf8 bytes16--    lazyText = Text.fromStrict text+hashExpressionToCode expr = "sha256:" <> Text.pack (show (hashExpression expr))

@@ -23,76 +23,69 @@ import Control.Applicative (Alternative(..), liftA2, optional) import Control.Exception (Exception) import Control.Monad (MonadPlus)-import Data.ByteString (ByteString)+import Data.ByteArray.Encoding (Base(..)) import Data.Functor (void) import Data.HashMap.Strict.InsOrd (InsOrdHashMap)-import Data.Sequence (ViewL(..))-import Data.Semigroup (Semigroup(..)) import Data.Scientific (Scientific)+import Data.Semigroup (Semigroup(..))+import Data.Sequence (ViewL(..))+import Data.Set (Set) import Data.String (IsString(..)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder)-import Data.Typeable (Typeable)+import Data.Void (Void) import Dhall.Core import Formatting.Buildable (Buildable(..)) import Numeric.Natural (Natural) import Prelude hiding (const, pi)-import Text.PrettyPrint.ANSI.Leijen (Doc) import Text.Parser.Combinators (choice, try, (<?>)) import Text.Parser.Token (TokenParsing(..))-import Text.Trifecta-    (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..))-import Text.Trifecta.Delta (Delta)  import qualified Control.Monad import qualified Crypto.Hash+import qualified Data.ByteArray.Encoding+import qualified Data.ByteString import qualified Data.ByteString.Lazy import qualified Data.Char import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet import qualified Data.List import qualified Data.Sequence+import qualified Data.Set import qualified Data.Text-import qualified Data.Text.Encoding import qualified Data.Text.Lazy import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding+import qualified Text.Megaparsec+import qualified Text.Megaparsec.Char import qualified Text.Parser.Char import qualified Text.Parser.Combinators import qualified Text.Parser.Token import qualified Text.Parser.Token.Style-import qualified Text.PrettyPrint.ANSI.Leijen-import qualified Text.Trifecta  -- | Source code extract-data Src = Src Delta Delta ByteString deriving (Eq, Show)+data Src = Src Text.Megaparsec.SourcePos Text.Megaparsec.SourcePos Text+  deriving (Eq, Show)  instance Buildable Src where-    build (Src begin _ bytes) =+    build (Src begin _ text) =             build text <> "\n"         <>  "\n"-        <>  build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin))+        <>  build (Text.Megaparsec.sourcePosPretty begin)         <>  "\n"-      where-        bytes' = Data.ByteString.Lazy.fromStrict bytes -        text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes')- {-| A `Parser` that is almost identical to-    @"Text.Trifecta".`Text.Trifecta.Parser`@ except treating Haskell-style+    @"Text.Megaparsec".`Text.Megaparsec.Parsec`@ except treating Haskell-style     comments as whitespace -}-newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a }+newtype Parser a = Parser { unParser :: Text.Megaparsec.Parsec Void Text a }     deriving     (   Functor     ,   Applicative     ,   Monad     ,   Alternative     ,   MonadPlus-    ,   Parsing-    ,   CharParsing-    ,   DeltaParsing-    ,   MarkParsing Delta+    ,   Text.Megaparsec.MonadParsec Void Text     )  instance Data.Semigroup.Semigroup a => Data.Semigroup.Semigroup (Parser a) where@@ -106,26 +99,52 @@ #endif  instance IsString a => IsString (Parser a) where-    fromString x = fmap fromString (Text.Parser.Char.string x)+    fromString x = fromString x <$ Text.Megaparsec.Char.string (fromString x) +instance Text.Parser.Combinators.Parsing Parser where+  try = Text.Megaparsec.try++  (<?>) = (Text.Megaparsec.<?>)++  skipMany = Text.Megaparsec.skipMany++  skipSome = Text.Megaparsec.skipSome++  unexpected = fail++  eof = Parser Text.Megaparsec.eof++  notFollowedBy = Text.Megaparsec.notFollowedBy++instance Text.Parser.Char.CharParsing Parser where+  satisfy = Parser . Text.Megaparsec.Char.satisfy++  char = Text.Megaparsec.Char.char++  notChar = Text.Megaparsec.Char.char++  anyChar = Text.Megaparsec.Char.anyChar++  string = fmap Data.Text.Lazy.unpack . Text.Megaparsec.Char.string . fromString++  text = fmap Data.Text.Lazy.toStrict . Text.Megaparsec.Char.string . Data.Text.Lazy.fromStrict+ instance TokenParsing Parser where     someSpace =         Text.Parser.Token.Style.buildSomeSpaceParser-            (Parser someSpace)+            (Parser (Text.Megaparsec.skipSome (Text.Megaparsec.Char.satisfy Data.Char.isSpace)))             Text.Parser.Token.Style.haskellCommentStyle -    nesting (Parser m) = Parser (nesting m)--    semi = Parser semi+    highlight _ = id -    highlight h (Parser m) = Parser (highlight h m)+    semi = token (Text.Megaparsec.Char.char ';' <?> ";")  noted :: Parser (Expr Src a) -> Parser (Expr Src a) noted parser = do-    before     <- Text.Trifecta.position-    (e, bytes) <- Text.Trifecta.slicedWith (,) parser-    after      <- Text.Trifecta.position-    return (Note (Src before after bytes) e)+    before      <- Text.Megaparsec.getPosition+    (tokens, e) <- Text.Megaparsec.match parser+    after       <- Text.Megaparsec.getPosition+    return (Note (Src before after tokens) e)  count :: (Semigroup a, Monoid a) => Int -> Parser a -> Parser a count n parser = mconcat (replicate n parser)@@ -269,6 +288,29 @@     whitespace     return t ) <?> "label" +noDuplicates :: Ord a => [a] -> Parser (Set a)+noDuplicates = go Data.Set.empty+  where+    go found    []  = return found+    go found (x:xs) =+        if Data.Set.member x found+        then fail "Duplicate key"+        else go (Data.Set.insert x found) xs++labels :: Parser (Set Text)+labels = do+    _openBrace+    xs <- nonEmptyLabels <|> emptyLabels+    _closeBrace+    return xs+  where+    emptyLabels = pure Data.Set.empty++    nonEmptyLabels = do+        x  <- label+        xs <- many (do _ <- _comma; label)+        noDuplicates (x : xs)+ doubleQuotedChunk :: Parser a -> Parser (Chunks Src a) doubleQuotedChunk embedded =     choice@@ -279,7 +321,7 @@   where     interpolation = do         _ <- Text.Parser.Char.text "${"-        e <- expression embedded+        e <- completeExpression embedded         _ <- Text.Parser.Char.char '}'         return (Chunks [(mempty, e)] mempty) @@ -427,7 +469,7 @@          interpolation = do             _ <- Text.Parser.Char.text "${"-            a <- expression embedded+            a <- completeExpression embedded             _ <- Text.Parser.Char.char '}'             b <- singleQuoteContinue embedded             return (Chunks [(mempty, a)] mempty <> b)@@ -669,6 +711,11 @@     void (Text.Parser.Char.char '∧' <?> "\"∧\"") <|> void (Text.Parser.Char.text "/\\")     whitespace +_combineTypes :: Parser ()+_combineTypes = do+    void (Text.Parser.Char.char '⩓' <?> "\"⩓\"") <|> void (Text.Parser.Char.text "//\\\\")+    whitespace+ _prefer :: Parser () _prefer = do     void (Text.Parser.Char.char '⫽' <?> "\"⫽\"") <|> void (Text.Parser.Char.text "//")@@ -1135,8 +1182,12 @@  preferExpression :: Parser a -> Parser (Expr Src a) preferExpression =-    makeOperatorExpression timesExpression _prefer Prefer+    makeOperatorExpression combineTypesExpression _prefer Prefer +combineTypesExpression :: Parser a -> Parser (Expr Src a)+combineTypesExpression =+    makeOperatorExpression timesExpression _combineTypes CombineTypes+ timesExpression :: Parser a -> Parser (Expr Src a) timesExpression =     makeOperatorExpression equalExpression _times NaturalTimes@@ -1164,9 +1215,12 @@ selectorExpression :: Parser a -> Parser (Expr Src a) selectorExpression embedded = noted (do     a <- primitiveExpression embedded-    b <- many (try (do _dot; label))-    return (foldl Field a b) ) +    let left  x  e = Field   e x+    let right xs e = Project e xs+    b <- many (try (do _dot; fmap left label <|> fmap right labels))+    return (foldl (\e k -> k e) a b) )+ primitiveExpression :: Parser a -> Parser (Expr Src a) primitiveExpression embedded =     noted@@ -1513,9 +1567,13 @@         _ <- Text.Parser.Char.text "sha256:"         builder <- count 64 (satisfy hexdig <?> "hex digit")         whitespace-        let lazyText = Data.Text.Lazy.Builder.toLazyText builder-        let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 lazyText-        case Crypto.Hash.digestFromByteString (Data.ByteString.Lazy.toStrict lazyBytes) of+        let lazyText    = Data.Text.Lazy.Builder.toLazyText builder+        let lazyBytes16 = Data.Text.Lazy.Encoding.encodeUtf8 lazyText+        let strictBytes16 = Data.ByteString.Lazy.toStrict lazyBytes16+        strictBytes <- case Data.ByteArray.Encoding.convertFromBase Base16 strictBytes16 of+            Left  string      -> fail string+            Right strictBytes -> return (strictBytes :: Data.ByteString.ByteString)+        case Crypto.Hash.digestFromByteString strictBytes of           Nothing -> fail "Invalid sha256 hash"           Just h -> pure h @@ -1531,16 +1589,19 @@         return RawText  -- | A parsing error-newtype ParseError = ParseError Doc deriving (Typeable)+data ParseError = ParseError+    { unwrap :: Text.Megaparsec.ParseError Char Void+    , input  :: Text+    }  instance Show ParseError where-    show (ParseError doc) =-      "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> show doc+    show (ParseError {..}) =+      "\n\ESC[1;31mError\ESC[0m: Invalid input\n\n" <> Text.Megaparsec.parseErrorPretty' input unwrap  instance Exception ParseError  -- | Parse an expression from `Text` containing a Dhall program-exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path)+exprFromText :: String -> Text -> Either ParseError (Expr Src Path) exprFromText delta text = fmap snd (exprAndHeaderFromText delta text)  {-| Like `exprFromText` but also returns the leading comments and whitespace@@ -1556,24 +1617,17 @@     This is used by @dhall-format@ to preserve leading comments and whitespace -} exprAndHeaderFromText-    :: Delta+    :: String     -> Text     -> Either ParseError (Text, Expr Src Path) exprAndHeaderFromText delta text = case result of-    Failure errInfo    -> Left (ParseError (Text.Trifecta._errDoc errInfo))-    Success (bytes, r) -> case Data.Text.Encoding.decodeUtf8' bytes of-        Left  errInfo -> Left (ParseError (fromString (show errInfo)))-        Right txt     -> do-            let stripped = Data.Text.dropWhileEnd (/= '\n') txt-            let lazyText = Data.Text.Lazy.fromStrict stripped-            Right (lazyText, r)+    Left errInfo   -> Left (ParseError { unwrap = errInfo, input = text })+    Right (txt, r) -> Right (Data.Text.Lazy.dropWhileEnd (/= '\n') txt, r)   where-    string = Data.Text.Lazy.unpack text--    parser = unParser (do-        bytes <- Text.Trifecta.slicedWith (\_ x -> x) whitespace+    parser = do+        (bytes, _) <- Text.Megaparsec.match whitespace         r <- expr-        Text.Parser.Combinators.eof-        return (bytes, r) )+        Text.Megaparsec.eof+        return (bytes, r) -    result = Text.Trifecta.parseString parser delta string+    result = Text.Megaparsec.parse (unParser parser) delta text

@@ -18,6 +18,36 @@     , buildScientific     , pretty     , escapeText++    , prettyConst+    , prettyLabel+    , prettyLabels+    , prettyNatural+    , prettyNumber+    , prettyScientific++    , builtin+    , keyword+    , literal+    , operator++    , colon+    , comma+    , dot+    , equals+    , forall+    , label+    , lambda+    , langle+    , lbrace+    , lbracket+    , lparen+    , pipe+    , rangle+    , rarrow+    , rbrace+    , rbracket+    , rparen     ) where  import {-# SOURCE #-} Dhall.Core@@ -30,6 +60,7 @@ import Data.HashMap.Strict.InsOrd (InsOrdHashMap) import Data.Monoid ((<>)) import Data.Scientific (Scientific)+import Data.Set (Set) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) import Data.Text.Prettyprint.Doc (Doc, Pretty, space)@@ -42,6 +73,7 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet import qualified Data.List+import qualified Data.Set import qualified Data.Text.Lazy                        as Text import qualified Data.Text.Lazy.Builder                as Builder import qualified Data.Text.Prettyprint.Doc             as Pretty@@ -248,6 +280,13 @@                         -> Pretty.pretty a                 _       -> backtick <> Pretty.pretty a <> backtick +prettyLabels :: Set Text -> Doc Ann+prettyLabels a+    | Data.Set.null a =+        lbrace <> rbrace+    | otherwise =+        braces (map (duplicate . prettyLabel) (Data.Set.toList a))+ prettyNumber :: Integer -> Doc Ann prettyNumber = literal . Pretty.pretty @@ -571,10 +610,10 @@     prettyExprC7 a0  prettyExprC7 :: Pretty a => Expr s a -> Doc Ann-prettyExprC7 a0@(NaturalTimes _ _) =-    enclose' "" "  " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))+prettyExprC7 a0@(CombineTypes _ _) =+    enclose' "" "  " (" " <> operator "⩓" <> " ") (operator "⩓" <> " ") (fmap duplicate (docs a0))   where-    docs (NaturalTimes a b) = prettyExprC8 a : docs b+    docs (CombineTypes a b) = prettyExprC8 a : docs b     docs (Note         _ b) = docs b     docs                 b  = [ prettyExprC8 b ] prettyExprC7 (Note _ a) =@@ -583,27 +622,39 @@     prettyExprC8 a0  prettyExprC8 :: Pretty a => Expr s a -> Doc Ann-prettyExprC8 a0@(BoolEQ _ _) =-    enclose' "" "    " (" " <> operator "==" <> " ") (operator "==" <> "  ") (fmap duplicate (docs a0))+prettyExprC8 a0@(NaturalTimes _ _) =+    enclose' "" "  " (" " <> operator "*" <> " ") (operator "*" <> " ") (fmap duplicate (docs a0))   where-    docs (BoolEQ a b) = prettyExprC9 a : docs b-    docs (Note   _ b) = docs b-    docs           b  = [ prettyExprC9 b ]+    docs (NaturalTimes a b) = prettyExprC9 a : docs b+    docs (Note         _ b) = docs b+    docs                 b  = [ prettyExprC9 b ] prettyExprC8 (Note _ a) =     prettyExprC8 a prettyExprC8 a0 =     prettyExprC9 a0  prettyExprC9 :: Pretty a => Expr s a -> Doc Ann-prettyExprC9 a0@(BoolNE _ _) =-    enclose' "" "    " (" " <> operator "!=" <> " ") (operator "!=" <> "  ") (fmap duplicate (docs a0))+prettyExprC9 a0@(BoolEQ _ _) =+    enclose' "" "    " (" " <> operator "==" <> " ") (operator "==" <> "  ") (fmap duplicate (docs a0))   where-    docs (BoolNE a b) = prettyExprD a : docs b+    docs (BoolEQ a b) = prettyExprC10 a : docs b     docs (Note   _ b) = docs b-    docs           b  = [ prettyExprD b ]+    docs           b  = [ prettyExprC10 b ] prettyExprC9 (Note _ a) =     prettyExprC9 a prettyExprC9 a0 =+    prettyExprC10 a0++prettyExprC10 :: Pretty a => Expr s a -> Doc Ann+prettyExprC10 a0@(BoolNE _ _) =+    enclose' "" "    " (" " <> operator "!=" <> " ") (operator "!=" <> "  ") (fmap duplicate (docs a0))+  where+    docs (BoolNE a b) = prettyExprD a : docs b+    docs (Note   _ b) = docs b+    docs           b  = [ prettyExprD b ]+prettyExprC10 (Note _ a) =+    prettyExprC10 a+prettyExprC10 a0 =     prettyExprD a0  prettyExprD :: Pretty a => Expr s a -> Doc Ann@@ -621,9 +672,10 @@     docs               b  = [ prettyExprE b ]  prettyExprE :: Pretty a => Expr s a -> Doc Ann-prettyExprE (Field a b) = prettyExprE a <> dot <> prettyLabel b-prettyExprE (Note  _ b) = prettyExprE b-prettyExprE  a          = prettyExprF a+prettyExprE (Field   a b) = prettyExprE a <> dot <> prettyLabel b+prettyExprE (Project a b) = prettyExprE a <> dot <> prettyLabels b+prettyExprE (Note    _ b) = prettyExprE b+prettyExprE  a            = prettyExprF a  prettyExprF :: Pretty a => Expr s a -> Doc Ann prettyExprF (Var a) =@@ -947,21 +999,27 @@  -- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser" buildExprC7 :: Buildable a => Expr s a -> Builder-buildExprC7 (NaturalTimes a b) = buildExprC8 a <> " * " <> buildExprC7 b+buildExprC7 (CombineTypes a b) = buildExprC8 a <> " ⩓ " <> buildExprC7 b buildExprC7 (Note         _ b) = buildExprC7 b buildExprC7  a                 = buildExprC8 a  -- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser" buildExprC8 :: Buildable a => Expr s a -> Builder-buildExprC8 (BoolEQ a b) = buildExprC9 a <> " == " <> buildExprC8 b-buildExprC8 (Note   _ b) = buildExprC8 b-buildExprC8  a           = buildExprC9 a+buildExprC8 (NaturalTimes a b) = buildExprC9 a <> " * " <> buildExprC8 b+buildExprC8 (Note         _ b) = buildExprC8 b+buildExprC8  a                 = buildExprC9 a  -- | Builder corresponding to the @exprC9@ parser in "Dhall.Parser" buildExprC9 :: Buildable a => Expr s a -> Builder-buildExprC9 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC9 b+buildExprC9 (BoolEQ a b) = buildExprC10 a <> " == " <> buildExprC9 b buildExprC9 (Note   _ b) = buildExprC9 b-buildExprC9  a           = buildExprD  a+buildExprC9  a           = buildExprC10 a++-- | Builder corresponding to the @exprC10@ parser in "Dhall.Parser"+buildExprC10 :: Buildable a => Expr s a -> Builder+buildExprC10 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC10 b+buildExprC10 (Note   _ b) = buildExprC10 b+buildExprC10  a           = buildExprD  a  -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser" buildExprD :: Buildable a => Expr s a -> Builder

@@ -602,6 +602,20 @@ -- > >>> input auto "{ foo = True, bar = 2, baz = 4.2 }.baz" :: IO Double -- > 4.2 --+-- ... and you can project out multiple fields into a new record using this+-- syntax:+--+-- > someRecord.{ field₀, field₁, … }+--+-- For example:+--+-- > $ dhall+-- > { x = 1, y = True, z = "ABC" }.{ x, y }+-- > <Ctrl-D>+-- > { x : Integer, y : Bool }+-- > +-- > { x = 1, y = True }+-- -- __Exercise__: What is the type of this record: -- -- > { foo = 1@@ -900,6 +914,21 @@ -- -- __Exercise__: Combine any record with the empty record.  What do you expect -- to happen?+--+-- You can analogously combine record types using the @//\\\\@ operator (or @(⩓)@ U+2A53):+--+-- > $ dhall+-- > { foo : Natural } ⩓ { bar : Text }+-- > <Ctrl-D>+-- > { foo : Natural, bar : Text }+--+-- ... which behaves the exact same, except at the type level, meaning that the+-- operator descends recursively into record types:+--+-- > $ dhall+-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }+-- > <Ctrl-D>+-- > { foo : { bar : Text, baz : Bool }, qux : Integer }  -- $let --@@ -1123,7 +1152,7 @@ -- The @constructors@ keyword takes a union type argument and returns a record -- with one field per union type constructor: ----- > $ dhall --pretty+-- > $ dhall -- > constructors < Empty : {} | Person : { name : Text, age : Natural } > -- > <Ctrl-D> -- >@@ -1615,55 +1644,8 @@ -- >     (List (List Integer)) -- >     (replicate +5 (List Integer) (replicate +5 Integer 1)) ----- If you want to evaluate and format an expression then you can use the--- @--pretty@ flag of the @dhall@ executable:------ > $ dhall --pretty--- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate --- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))--- > <Ctrl-D>--- > List (List (List Integer))--- > --- >   [   [ [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       ]--- >     : List (List Integer)--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       ]--- >     : List (List Integer)--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       ]--- >     : List (List Integer)--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       ]--- >     : List (List Integer)--- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       , [ 1, 1, 1, 1, 1 ] : List Integer--- >       ]--- >     : List (List Integer)--- >   ]--- > : List (List (List Integer))--- -- You can also use the formatter to modify files in place using the--- @--inplace@ flag:+-- @--inplace@ flag (i.e. for formatting source code): -- -- > $ dhall-format --inplace ./unformatted -- > $ cat ./unformatted@@ -1712,6 +1694,54 @@ -- > {- This comment will be preserved by the formatter -} -- > -- ... and this comment will be preserved, too -- > 1+--+-- Note that you do not need to use @dhall-format@ to format the output of the+-- @dhall@ interpreter.  The interpreter already automatically formats+-- multi-line expressions, too:+--+-- > $ dhall+-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate +-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))+-- > <Ctrl-D>+-- > List (List (List Integer))+-- > +-- >   [   [ [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       ]+-- >     : List (List Integer)+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       ]+-- >     : List (List Integer)+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       ]+-- >     : List (List Integer)+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       ]+-- >     : List (List Integer)+-- >   ,   [ [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       , [ 1, 1, 1, 1, 1 ] : List Integer+-- >       ]+-- >     : List (List Integer)+-- >   ]+-- > : List (List (List Integer))  -- $builtins --@@ -2682,7 +2712,7 @@ -- -- __Exercise__: Browse the Prelude by running: ----- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'+-- > $ dhall <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'  -- $conclusion --

@@ -28,7 +28,7 @@ import Data.Set (Set) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder)-import Data.Text.Prettyprint.Doc (Pretty(..))+import Data.Text.Prettyprint.Doc (Doc, Pretty(..)) import Data.Traversable (forM) import Data.Typeable (Typeable) import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..))@@ -39,15 +39,25 @@ import qualified Data.HashMap.Strict.InsOrd import qualified Data.Sequence import qualified Data.Set-import qualified Data.Text.Lazy                   as Text-import qualified Data.Text.Lazy.Builder           as Builder+import qualified Data.Text.Lazy                        as Text+import qualified Data.Text.Lazy.Builder                as Builder+import qualified Data.Text.Prettyprint.Doc             as Pretty+import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty import qualified Dhall.Context import qualified Dhall.Core+import qualified Dhall.Diff+import qualified Dhall.Pretty+import qualified Dhall.Pretty.Internal  traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f () traverseWithIndex_ k xs =     Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs) +docToLazyText :: Doc a -> Text+docToLazyText = Pretty.renderLazy . Pretty.layoutPretty opts+  where+    opts = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }+ axiom :: Const -> Either (TypeError s a) Const axiom Type = return Kind axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped)@@ -424,25 +434,69 @@                       (Pi "just" (Pi "_" "a" "optional")                           (Pi "nothing" "optional" "optional") )     loop ctx e@(Record    kts   ) = do-        let process (k, t) = do-                s <- fmap Dhall.Core.normalize (loop ctx t)-                case s of-                    Const Type -> return ()-                    Const Kind -> return ()-                    _          -> Left (TypeError ctx e (InvalidFieldType k t))-        mapM_ process (Data.HashMap.Strict.InsOrd.toList kts)-        return (Const Type)+        case Data.HashMap.Strict.InsOrd.toList kts of+            []            -> return (Const Type)+            (k0, t0):rest -> do+                s0 <- fmap Dhall.Core.normalize (loop ctx t0)+                c <- case s0 of+                    Const Type ->+                        return Type+                    Const Kind+                        | Dhall.Core.judgmentallyEqual t0 (Const Type) ->+                            return Kind+                    _ -> Left (TypeError ctx e (InvalidFieldType k0 t0))+                let process (k, t) = do+                        s <- fmap Dhall.Core.normalize (loop ctx t)+                        case s of+                            Const Type ->+                                if c == Type+                                then return ()+                                else Left (TypeError ctx e (FieldAnnotationMismatch k t k0 t0 Type))+                            Const Kind ->+                                if c == Kind+                                then+                                    if Dhall.Core.judgmentallyEqual t (Const Type)+                                    then return ()+                                    else Left (TypeError ctx e (InvalidFieldType k t))+                                else Left (TypeError ctx e (FieldAnnotationMismatch k t k0 t0 Kind))+                            _ ->+                                Left (TypeError ctx e (InvalidFieldType k t))+                mapM_ process rest+                return (Const c)     loop ctx e@(RecordLit kvs   ) = do-        let process k v = do-                t <- loop ctx v-                s <- fmap Dhall.Core.normalize (loop ctx t)-                case s of-                    Const Type -> return ()-                    Const Kind -> return ()-                    _          -> Left (TypeError ctx e (InvalidField k v))-                return t-        kts <- Data.HashMap.Strict.InsOrd.traverseWithKey process kvs-        return (Record kts)+        case Data.HashMap.Strict.InsOrd.toList kvs of+            []         -> return (Record Data.HashMap.Strict.InsOrd.empty)+            (k0, v0):_ -> do+                t0 <- loop ctx v0+                s0 <- fmap Dhall.Core.normalize (loop ctx t0)+                c <- case s0 of+                    Const Type ->+                        return Type+                    Const Kind+                        | Dhall.Core.judgmentallyEqual t0 (Const Type) ->+                            return Kind+                    _       -> Left (TypeError ctx e (InvalidField k0 v0))+                let process k v = do+                        t <- loop ctx v+                        s <- fmap Dhall.Core.normalize (loop ctx t)+                        case s of+                            Const Type ->+                                if c == Type+                                then return ()+                                else Left (TypeError ctx e (FieldMismatch k v k0 v0 Type))+                            Const Kind ->+                                if c == Kind+                                then+                                    if Dhall.Core.judgmentallyEqual t (Const Type)+                                    then return ()+                                    else Left (TypeError ctx e (InvalidFieldType k t))+                                else Left (TypeError ctx e (FieldMismatch k v k0 v0 Kind))+                            _ ->+                                Left (TypeError ctx e (InvalidField k t))++                        return t+                kts <- Data.HashMap.Strict.InsOrd.traverseWithKey process kvs+                return (Record kts)     loop ctx e@(Union     kts   ) = do         let process (k, t) = do                 s <- fmap Dhall.Core.normalize (loop ctx t)@@ -491,6 +545,52 @@                 return (Record (Data.HashMap.Strict.InsOrd.fromList kts))          combineTypes ktsX ktsY+    loop ctx e@(CombineTypes l r) = do+        tL <- loop ctx l+        let l' = Dhall.Core.normalize l+        cL <- case tL of+            Const cL -> return cL+            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))+        tR <- loop ctx r+        let r' = Dhall.Core.normalize r+        cR <- case tR of+            Const cR -> return cR+            _        -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))+        let decide Type Type =+                return Type+            decide Kind Kind =+                return Kind+            decide x y =+                Left (TypeError ctx e (RecordTypeMismatch x y l r))+        c <- decide cL cR++        ktsL0 <- case l' of+            Record kts -> return kts+            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType l l'))+        ktsR0 <- case r' of+            Record kts -> return kts+            _          -> Left (TypeError ctx e (CombineTypesRequiresRecordType r r'))++        let combineTypes ktsL ktsR = do+                let ksL =+                        Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsL)+                let ksR =+                        Data.Set.fromList (Data.HashMap.Strict.InsOrd.keys ktsR)+                let ks = Data.Set.union ksL ksR+                forM_ (toList ks) (\k -> do+                    case (Data.HashMap.Strict.InsOrd.lookup k ktsL, Data.HashMap.Strict.InsOrd.lookup k ktsR) of+                        (Just (Record ktsL'), Just (Record ktsR')) -> do+                            combineTypes ktsL' ktsR'+                        (Nothing, Just _) -> do+                            return ()+                        (Just _, Nothing) -> do+                            return ()+                        _ -> do+                            Left (TypeError ctx e (FieldCollision k)) )++        combineTypes ktsL0 ktsR0++        return (Const c)     loop ctx e@(Prefer kvsX kvsY) = do         tKvsX <- fmap Dhall.Core.normalize (loop ctx kvsX)         ktsX  <- case tKvsX of@@ -597,7 +697,24 @@                 case Data.HashMap.Strict.InsOrd.lookup x kts of                     Just t' -> return t'                     Nothing -> Left (TypeError ctx e (MissingField x t))-            _          -> Left (TypeError ctx e (NotARecord x r t))+            _ -> do+                let text = docToLazyText (Dhall.Pretty.Internal.prettyLabel x)+                Left (TypeError ctx e (NotARecord text r t))+    loop ctx e@(Project r xs    ) = do+        t <- fmap Dhall.Core.normalize (loop ctx r)+        case t of+            Record kts -> do+                _ <- loop ctx t++                let process k =+                        case Data.HashMap.Strict.InsOrd.lookup k kts of+                            Just t' -> return (k, t')+                            Nothing -> Left (TypeError ctx e (MissingField k t))+                let adapt = Record . Data.HashMap.Strict.InsOrd.fromList+                fmap adapt (traverse process (Data.Set.toList xs))+            _ -> do+                let text = docToLazyText (Dhall.Pretty.Internal.prettyLabels xs)+                Left (TypeError ctx e (NotARecord text r t))     loop ctx   (Note s e'       ) = case loop ctx e' of         Left (TypeError ctx' (Note s' e'') m) -> Left (TypeError ctx' (Note s' e'') m)         Left (TypeError ctx'          e''  m) -> Left (TypeError ctx' (Note s  e'') m)@@ -646,11 +763,15 @@     | IfBranchMustBeTerm Bool (Expr s a) (Expr s a) (Expr s a)     | InvalidField Text (Expr s a)     | InvalidFieldType Text (Expr s a)+    | FieldAnnotationMismatch Text (Expr s a) Text (Expr s a) Const+    | FieldMismatch Text (Expr s a) Text (Expr s a) Const     | InvalidAlternative Text (Expr s a)     | InvalidAlternativeType Text (Expr s a)     | ListAppendMismatch (Expr s a) (Expr s a)     | DuplicateAlternative Text     | MustCombineARecord Char (Expr s a) (Expr s a)+    | CombineTypesRequiresRecordType (Expr s a) (Expr s a)+    | RecordTypeMismatch Const Const (Expr s a) (Expr s a)     | FieldCollision Text     | MustMergeARecord (Expr s a) (Expr s a)     | MustMergeUnion (Expr s a) (Expr s a)@@ -676,13 +797,13 @@     | NoDependentTypes (Expr s a) (Expr s a)     deriving (Show) -shortTypeMessage :: Buildable a => TypeMessage s a -> Builder+shortTypeMessage :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> Builder shortTypeMessage msg =     "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"   where     ErrorMessages {..} = prettyTypeMessage msg -longTypeMessage :: Buildable a => TypeMessage s a -> Builder+longTypeMessage :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> Builder longTypeMessage msg =         "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"     <>  "\n"@@ -700,7 +821,22 @@ _NOT :: Builder _NOT = "\ESC[1mnot\ESC[0m" -prettyTypeMessage :: Buildable a => TypeMessage s a -> ErrorMessages+prettyDiff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Builder+prettyDiff exprL exprR = builder+  where+    doc =+        fmap Dhall.Pretty.annToAnsiStyle (Dhall.Diff.diffNormalized exprL exprR)++    opts = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }++    stream = Pretty.layoutPretty opts doc++    lazyText = Pretty.renderLazy stream++    builder = Builder.fromLazyText lazyText++prettyTypeMessage+    :: (Buildable a, Eq a, Pretty a) => TypeMessage s a -> ErrorMessages prettyTypeMessage (UnboundVariable _) = ErrorMessages {..}   -- We do not need to print variable name here. For the discussion see:   -- https://github.com/dhall-lang/dhall-haskell/pull/116@@ -1098,7 +1234,9 @@  prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}   where-    short = "Wrong type of function argument"+    short = "Wrong type of function argument\n"+        <>  "\n"+        <>  prettyDiff expr1 expr3      long =         "Explanation: Every function declares what type or kind of argument to accept    \n\@@ -1230,8 +1368,9 @@  prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}   where-    short = "Expression doesn't match annotation"-+    short = "Expression doesn't match annotation\n"+        <>  "\n"+        <>  prettyDiff expr1 expr2     long =         "Explanation: You can annotate an expression with its type or kind using the     \n\         \❰:❱ symbol, like this:                                                          \n\@@ -1511,7 +1650,9 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =     ErrorMessages {..}   where-    short = "❰if❱ branches must have matching types"+    short = "❰if❱ branches must have matching types\n"+        <>  "\n"+        <>  prettyDiff expr1 expr3      long =         "Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which\n\@@ -1660,7 +1801,9 @@ prettyTypeMessage (MismatchedListElements i expr0 _expr1 expr2) =     ErrorMessages {..}   where-    short = "List elements should all have the same type"+    short = "List elements should all have the same type\n"+        <>  "\n"+        <>  prettyDiff expr0 expr2      long =         "Explanation: Every element in a list must have the same type                    \n\@@ -1696,7 +1839,9 @@ prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =     ErrorMessages {..}   where-    short = "List element has the wrong type"+    short = "List element has the wrong type\n"+        <>  "\n"+        <>  prettyDiff expr0 expr2      long =         "Explanation: Every element in the list must have a type matching the type       \n\@@ -1783,7 +1928,9 @@  prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..}   where-    short = "❰Optional❱ element has the wrong type"+    short = "❰Optional❱ element has the wrong type\n"+        <>  "\n"+        <>  prettyDiff expr0 expr2      long =         "Explanation: An ❰Optional❱ element must have a type matching the type annotation\n\@@ -1825,32 +1972,75 @@     short = "Invalid field type"      long =-        "Explanation: Every record type documents the type of each field, like this:     \n\+        "Explanation: Every record type annotates each field with a ❰Type❱ or a ❰Kind❱,  \n\+        \like this:                                                                      \n\         \                                                                                \n\+        \                                                                                \n\         \    ┌──────────────────────────────────────────────┐                            \n\-        \    │ { foo : Integer, bar : Integer, baz : Text } │                            \n\-        \    └──────────────────────────────────────────────┘                            \n\+        \    │ { foo : Integer, bar : Integer, baz : Text } │  Every field is annotated  \n\+        \    └──────────────────────────────────────────────┘  with a ❰Type❱             \n\         \                                                                                \n\-        \However, fields cannot be annotated with expressions other than types           \n\         \                                                                                \n\-        \For example, these record types are " <> _NOT <> " valid:                       \n\+        \    ┌────────────────────────────┐                                              \n\+        \    │ { foo : Type, bar : Type } │  Every field is annotated                    \n\+        \    └────────────────────────────┘  with a ❰Kind❱                               \n\         \                                                                                \n\         \                                                                                \n\+        \However, the types of fields may " <> _NOT <> " be term-level values:           \n\+        \                                                                                \n\+        \                                                                                \n\         \    ┌────────────────────────────┐                                              \n\-        \    │ { foo : Integer, bar : 1 } │                                              \n\+        \    │ { foo : Integer, bar : 1 } │  Invalid record type                         \n\         \    └────────────────────────────┘                                              \n\         \                             ⇧                                                  \n\-        \                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱               \n\+        \                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱ or ❰Kind❱     \n\         \                                                                                \n\         \                                                                                \n\+        \You provided a record type with a field named:                                  \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... annotated with the following expression:                                    \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n\+        \                                                                                \n\+        \... which is neither a ❰Type❱ nor a ❰Kind❱                                      \n"+      where+        txt0 = build k+        txt1 = build expr0++prettyTypeMessage (FieldAnnotationMismatch k0 expr0 k1 expr1 c) = ErrorMessages {..}+  where+    short = "Field annotation mismatch"++    long =+        "Explanation: Every record type annotates each field with a ❰Type❱ or a ❰Kind❱,  \n\+        \like this:                                                                      \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────────────────────┐                            \n\+        \    │ { foo : Integer, bar : Integer, baz : Text } │  Every field is annotated  \n\+        \    └──────────────────────────────────────────────┘  with a ❰Type❱             \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌────────────────────────────┐                                              \n\+        \    │ { foo : Type, bar : Type } │  Every field is annotated                    \n\+        \    └────────────────────────────┘  with a ❰Kind❱                               \n\+        \                                                                                \n\+        \                                                                                \n\+        \However, you cannot have a record type with both a ❰Type❱ and ❰Kind❱ annotation:\n\+        \                                                                                \n\+        \                                                                                \n\+        \              This is a ❰Type❱ annotation                                       \n\+        \              ⇩                                                                 \n\         \    ┌───────────────────────────────┐                                           \n\-        \    │ { foo : Integer, bar : Type } │                                           \n\+        \    │ { foo : Integer, bar : Type } │  Invalid record type                      \n\         \    └───────────────────────────────┘                                           \n\         \                             ⇧                                                  \n\-        \                             ❰Type❱ is a ❰Kind❱ and not a ❰Type❱                \n\+        \                             ... but this is a ❰Kind❱ annotation                \n\         \                                                                                \n\         \                                                                                \n\-        \You provided a record type with a key named:                                    \n\+        \You provided a record type with a field named:                                  \n\         \                                                                                \n\         \↳ " <> txt0 <> "                                                                \n\         \                                                                                \n\@@ -1858,11 +2048,91 @@         \                                                                                \n\         \↳ " <> txt1 <> "                                                                \n\         \                                                                                \n\-        \... which is not a type                                                         \n"+        \... which is a " <> here <> " whereas another field named:                      \n\+        \                                                                                \n\+        \↳ " <> txt2 <> "                                                                \n\+        \                                                                                \n\+        \... annotated with the following expression:                                    \n\+        \                                                                                \n\+        \↳ " <> txt3 <> "                                                                \n\+        \                                                                                \n\+        \... is a " <> there <> ", which does not match                                  \n"       where-        txt0 = build k+        txt0 = build k0         txt1 = build expr0+        txt2 = build k1+        txt3 = build expr1 +        here = case c of+            Type -> "❰Type❱"+            Kind -> "❰Kind❱"++        there = case c of+            Type -> "❰Kind❱"+            Kind -> "❰Type❱"++prettyTypeMessage (FieldMismatch k0 expr0 k1 expr1 c) = ErrorMessages {..}+  where+    short = "Field mismatch"++    long =+        "Explanation: Every record has fields that can be either terms or types, like    \n\+        \this:                                                                           \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────────────┐                                    \n\+        \    │ { foo = 1, bar = True, baz = \"ABC\" } │  Every field is a term           \n\+        \    └──────────────────────────────────────┘                                    \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌───────────────────────────────┐                                           \n\+        \    │ { foo = Integer, bar = Text } │  Every field is a type                    \n\+        \    └───────────────────────────────┘                                           \n\+        \                                                                                \n\+        \                                                                                \n\+        \However, you cannot have a record that stores both terms and types:             \n\+        \                                                                                \n\+        \                                                                                \n\+        \              This is a term                                                    \n\+        \              ⇩                                                                 \n\+        \    ┌─────────────────────────┐                                                 \n\+        \    │ { foo = 1, bar = Bool } │  Invalid record                                 \n\+        \    └─────────────────────────┘                                                 \n\+        \                       ⇧                                                        \n\+        \                       ... but this is a type                                   \n\+        \                                                                                \n\+        \                                                                                \n\+        \You provided a record with a field named:                                       \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... whose value was:                                                            \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n\+        \                                                                                \n\+        \... which is a " <> here <> " whereas another field named:                      \n\+        \                                                                                \n\+        \↳ " <> txt2 <> "                                                                \n\+        \                                                                                \n\+        \... whose value was:                                                            \n\+        \                                                                                \n\+        \↳ " <> txt3 <> "                                                                \n\+        \                                                                                \n\+        \... is a " <> there <> ", which does not match                                  \n"+      where+        txt0 = build k0+        txt1 = build expr0+        txt2 = build k1+        txt3 = build expr1++        here = case c of+            Type -> "term"+            Kind -> "type"++        there = case c of+            Type -> "type"+            Kind -> "term"+ prettyTypeMessage (InvalidField k expr0) = ErrorMessages {..}   where     short = "Invalid field"@@ -1875,26 +2145,19 @@         \    │ { foo = 100, bar = True, baz = \"ABC\" } │                                \n\         \    └────────────────────────────────────────┘                                  \n\         \                                                                                \n\-        \However, fields can only be terms and cannot be types or kinds                  \n\-        \                                                                                \n\-        \For example, these record literals are " <> _NOT <> " valid:                    \n\-        \                                                                                \n\+        \However, fields can only be terms and or ❰Type❱s and not ❰Kind❱s                \n\         \                                                                                \n\-        \    ┌───────────────────────────┐                                               \n\-        \    │ { foo = 100, bar = Text } │                                               \n\-        \    └───────────────────────────┘                                               \n\-        \                         ⇧                                                      \n\-        \                         ❰Text❱ is a type and not a term                        \n\+        \For example, the following record literal is " <> _NOT <> " valid:              \n\         \                                                                                \n\         \                                                                                \n\-        \    ┌───────────────────────────┐                                               \n\-        \    │ { foo = 100, bar = Type } │                                               \n\-        \    └───────────────────────────┘                                               \n\-        \                         ⇧                                                      \n\-        \                         ❰Type❱ is a kind and not a term                        \n\+        \    ┌────────────────┐                                                          \n\+        \    │ { foo = Type } │                                                          \n\+        \    └────────────────┘                                                          \n\+        \              ⇧                                                                 \n\+        \              ❰Type❱ is a ❰Kind❱, which is not allowed                          \n\         \                                                                                \n\         \                                                                                \n\-        \You provided a record literal with a key named:                                 \n\+        \You provided a record literal with a field named:                               \n\         \                                                                                \n\         \↳ " <> txt0 <> "                                                                \n\         \                                                                                \n\@@ -1902,7 +2165,7 @@         \                                                                                \n\         \↳ " <> txt1 <> "                                                                \n\         \                                                                                \n\-        \... which is not a term                                                         \n"+        \... which is not a term or ❰Type❱                                               \n"       where         txt0 = build k         txt1 = build expr0@@ -2031,7 +2294,9 @@  prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}   where-    short = "You can only append ❰List❱s with matching element types"+    short = "You can only append ❰List❱s with matching element types\n"+        <>  "\n"+        <>  prettyDiff expr0 expr1      long =         "Explanation: You can append two ❰List❱s using the ❰#❱ operator, like this:      \n\@@ -2152,13 +2417,103 @@         txt0 = build expr0         txt1 = build expr1 +prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) =+    ErrorMessages {..}+  where+    short = "❰⩓❱ requires arguments that are record types"++    long =+        "Explanation: You can only use the ❰⩓❱ operator on arguments that are record type\n\+        \literals, like this:                                                            \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌─────────────────────────────────────┐                                     \n\+        \    │ { age : Natural } ⩓ { name : Text } │                                     \n\+        \    └─────────────────────────────────────┘                                     \n\+        \                                                                                \n\+        \                                                                                \n\+        \... but you cannot use the ❰⩓❱ operator on any other type of arguments.  For    \n\+        \example, you cannot use variable arguments:                                     \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌───────────────────────────────────┐                                       \n\+        \    │ λ(t : Type) → t ⩓ { name : Text } │  Invalid: ❰t❱ might not be a record   \n\+        \    └───────────────────────────────────┘  type                                 \n\+        \                                                                                \n\+        \                                                                                \n\+        \────────────────────────────────────────────────────────────────────────────────\n\+        \                                                                                \n\+        \You tried to supply the following argument:                                     \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... which normalized to:                                                        \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n\+        \                                                                                \n\+        \... which is not a record type literal                                          \n"+      where+        txt0 = build expr0+        txt1 = build expr1++prettyTypeMessage (RecordTypeMismatch const0 const1 expr0 expr1) =+    ErrorMessages {..}+  where+    short = "Record type mismatch"++    long =+        "Explanation: You can only use the ❰⩓❱ operator on record types if they are both \n\+        \ ❰Type❱s or ❰Kind❱s:                                                            \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌─────────────────────────────────────┐                                     \n\+        \    │ { age : Natural } ⩓ { name : Text } │  Valid: Both arguments are ❰Type❱s  \n\+        \    └─────────────────────────────────────┘                                     \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────────────┐                                    \n\+        \    │ { Input : Type } ⩓ { Output : Type } │  Valid: Both arguments are ❰Kind❱s \n\+        \    └──────────────────────────────────────┘                                    \n\+        \                                                                                \n\+        \                                                                                \n\+        \... but you cannot combine a ❰Type❱ and a ❰Kind❱:                               \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌────────────────────────────────────┐                                      \n\+        \    │ { Input : Type } ⩓ { name : Text } │  Invalid: The arguments do not match \n\+        \    └────────────────────────────────────┘                                      \n\+        \                                                                                \n\+        \                                                                                \n\+        \────────────────────────────────────────────────────────────────────────────────\n\+        \                                                                                \n\+        \You tried to combine the following record type:                                 \n\+        \                                                                                \n\+        \↳ " <> txt0 <> "                                                                \n\+        \                                                                                \n\+        \... with this record types:                                                     \n\+        \                                                                                \n\+        \↳ " <> txt1 <> "                                                                \n\+        \                                                                                \n\+        \... but the former record type is a:                                            \n\+        \                                                                                \n\+        \↳ " <> txt2 <> "                                                                \n\+        \                                                                                \n\+        \... but the latter record type is a:                                            \n\+        \                                                                                \n\+        \↳ " <> txt3 <> "                                                                \n"+      where+        txt0 = build expr0+        txt1 = build expr1+        txt2 = build const0+        txt3 = build const1+ prettyTypeMessage (FieldCollision k) = ErrorMessages {..}   where     short = "Field collision"      long =-        "Explanation: You can combine records if they don't share any fields in common,  \n\-        \like this:                                                                      \n\+        "Explanation: You can combine records or record types if they don't share any    \n\+        \fields in common, like this:                                                    \n\         \                                                                                \n\         \                                                                                \n\         \    ┌───────────────────────────────────────────┐                               \n\@@ -2166,21 +2521,45 @@         \    └───────────────────────────────────────────┘                               \n\         \                                                                                \n\         \                                                                                \n\+        \    ┌─────────────────────────────────┐                                         \n\+        \    │ { foo : Text } ⩓ { bar : Bool } │                                         \n\+        \    └─────────────────────────────────┘                                         \n\+        \                                                                                \n\+        \                                                                                \n\         \    ┌────────────────────────────────────────┐                                  \n\         \    │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │                                  \n\         \    └────────────────────────────────────────┘                                  \n\         \                                                                                \n\         \                                                                                \n\-        \... but you cannot merge two records that share the same field                  \n\+        \... but you cannot merge two records that share the same field unless the field \n\+        \is a record on both sides.                                                      \n\         \                                                                                \n\-        \For example, the following expression is " <> _NOT <> " valid:                  \n\+        \For example, the following expressions are " <> _NOT <> " valid:                \n\         \                                                                                \n\         \                                                                                \n\         \    ┌───────────────────────────────────────────┐                               \n\-        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱ fields\n\-        \    └───────────────────────────────────────────┘                               \n\+        \    │ { foo = 1, bar = \"ABC\" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱   \n\+        \    └───────────────────────────────────────────┘  fields                       \n\         \                                                                                \n\         \                                                                                \n\+        \    ┌─────────────────────────────────┐                                         \n\+        \    │ { foo : Bool } ∧ { foo : Text } │  Invalid: Colliding ❰foo❱ fields        \n\+        \    └─────────────────────────────────┘                                         \n\+        \                                                                                \n\+        \                                                                                \n\+        \... but the following expressions are valid:                                    \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌──────────────────────────────────────────────────┐                        \n\+        \    │ { foo = { bar = True } } ∧ { foo = { baz = 1 } } │  Valid: Both ❰foo❱     \n\+        \    └──────────────────────────────────────────────────┘  fields are records    \n\+        \                                                                                \n\+        \                                                                                \n\+        \    ┌─────────────────────────────────────────────────────┐                     \n\+        \    │ { foo : { bar : Bool } } ⩓ { foo : { baz : Text } } │  Valid: Both ❰foo❱  \n\+        \    └─────────────────────────────────────────────────────┘  fields are records \n\+        \                                                                                \n\+        \                                                                                \n\         \Some common reasons why you might get this error:                               \n\         \                                                                                \n\         \● You tried to use ❰∧❱ to update a field's value, like this:                    \n\@@ -2413,7 +2792,9 @@ prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =     ErrorMessages {..}   where-    short = "Wrong handler input type"+    short = "Wrong handler input type\n"+        <>  "\n"+        <>  prettyDiff expr1 expr2      long =         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\@@ -2473,7 +2854,9 @@ prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =     ErrorMessages {..}   where-    short = "Wrong handler output type"+    short = "Wrong handler output type\n"+        <>  "\n"+        <>  prettyDiff expr1 expr2      long =         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\@@ -2535,7 +2918,9 @@ prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =     ErrorMessages {..}   where-    short = "Handlers should have the same output type"+    short = "Handlers should have the same output type\n"+        <>  "\n"+        <>  prettyDiff expr0 expr1      long =         "Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\@@ -2680,7 +3065,7 @@         txt0 = build expr0         txt1 = build expr1  -prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..}+prettyTypeMessage (NotARecord lazyText0 expr0 expr1) = ErrorMessages {..}   where     short = "Not a record" @@ -2725,7 +3110,7 @@         \                                                                                \n\         \────────────────────────────────────────────────────────────────────────────────\n\         \                                                                                \n\-        \You tried to access a field named:                                              \n\+        \You tried to access the field(s):                                               \n\         \                                                                                \n\         \↳ " <> txt0 <> "                                                                \n\         \                                                                                \n\@@ -2737,7 +3122,7 @@         \                                                                                \n\         \↳ " <> txt2 <> "                                                                \n"       where-        txt0 = build k+        txt0 = build lazyText0         txt1 = build expr0         txt2 = build expr1 @@ -3073,12 +3458,12 @@     , typeMessage :: TypeMessage s a     } deriving (Typeable) -instance (Buildable a, Buildable s) => Show (TypeError s a) where+instance (Buildable a, Buildable s, Eq a, Pretty a) => Show (TypeError s a) where     show = Text.unpack . Builder.toLazyText . build -instance (Buildable a, Buildable s, Typeable a, Typeable s) => Exception (TypeError s a)+instance (Buildable a, Buildable s, Eq a, Pretty a, Typeable a, Typeable s) => Exception (TypeError s a) -instance (Buildable a, Buildable s) => Buildable (TypeError s a) where+instance (Buildable a, Buildable s, Eq a, Pretty a) => Buildable (TypeError s a) where     build (TypeError ctx expr msg)         =   "\n"         <>  (   if  Text.null (Builder.toLazyText (buildContext ctx))@@ -3107,12 +3492,12 @@ newtype DetailedTypeError s a = DetailedTypeError (TypeError s a)     deriving (Typeable) -instance (Buildable a, Buildable s) => Show (DetailedTypeError s a) where+instance (Buildable a, Buildable s, Eq a, Pretty a) => Show (DetailedTypeError s a) where     show = Text.unpack . Builder.toLazyText . build -instance (Buildable a, Buildable s, Typeable a, Typeable s) => Exception (DetailedTypeError s a)+instance (Buildable a, Buildable s, Eq a, Pretty a, Typeable a, Typeable s) => Exception (DetailedTypeError s a) -instance (Buildable a, Buildable s) => Buildable (DetailedTypeError s a) where+instance (Buildable a, Buildable s, Eq a, Pretty a) => Buildable (DetailedTypeError s a) where     build (DetailedTypeError (TypeError ctx expr msg))         =   "\n"         <>  (   if  Text.null (Builder.toLazyText (buildContext ctx))

@@ -24,7 +24,8 @@ normalizationTests :: TestTree normalizationTests =     testGroup "normalization"-        [ examples+        [ tutorialExamples+        , preludeExamples         , simplifications         , constantFolding         , conversions@@ -33,8 +34,15 @@         , shouldNormalize "a remote-systems.conf builder" "remoteSystems"         ] -examples :: TestTree-examples =+tutorialExamples :: TestTree+tutorialExamples =+    testGroup "Tutorial examples"+        [ shouldNormalize "⩓" "./tutorial/combineTypes/0"+        , shouldNormalize "projection" "./tutorial/projection/0"+        ]++preludeExamples :: TestTree+preludeExamples =     testGroup "Prelude examples"         [ shouldNormalize "Bool/and" "./examples/Bool/and/0"         , shouldNormalize "Bool/and" "./examples/Bool/and/1"

@@ -130,6 +130,9 @@             , shouldParse                 "names that begin with reserved identifiers"                 "./tests/parser/reservedPrefix.dhall"+            , shouldParse+                "interpolated expressions with leading whitespace"+                "./tests/parser/template.dhall"             ]         ] 

@@ -0,0 +1,1 @@+{ foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }

@@ -0,0 +1,1 @@+{ foo : { bar : Text, baz : Bool }, qux : Integer }

@@ -0,0 +1,1 @@+{ x = 1, y = True, z = "ABC" }.{ x, y }

@@ -0,0 +1,1 @@+{ x = 1, y = True }

@@ -0,0 +1,13 @@+    \(record : { name        : Text+               , value       : Double+               , taxed_value : Double+               , in_ca       : Bool+               }+     ) ->  ''+Hello ${record.name}+You have just won ${Double/show record.value} dollars!+${ if record.in_ca+   then "Well, ${Double/show record.taxed_value} dollars, after taxes"+   else ""+ }+''

@@ -1,1 +1,1 @@-{ x = Bool, y = List }+{ x = Bool, y = Text }

@@ -1,1 +1,1 @@-{ x : Type, y : Type → Type }+{ x : Type, y : Type }