dhall (empty) → 1.0.0
raw patch · 10 files changed
+6253/−0 lines, 10 filesdep +ansi-wl-pprintdep +basedep +bytestringsetup-changed
Dependencies added: ansi-wl-pprint, base, bytestring, containers, dhall, http-client, http-client-tls, microlens, microlens-mtl, neat-interpolation, optparse-generic, parsers, system-fileio, system-filepath, text, text-format, transformers, trifecta, unordered-containers, vector
Files
- LICENSE +24/−0
- Setup.hs +2/−0
- dhall.cabal +74/−0
- exec/Main.hs +83/−0
- src/Dhall.hs +618/−0
- src/Dhall/Context.hs +68/−0
- src/Dhall/Core.hs +1321/−0
- src/Dhall/Import.hs +486/−0
- src/Dhall/Parser.hs +708/−0
- src/Dhall/TypeCheck.hs +2869/−0
+ LICENSE view
@@ -0,0 +1,24 @@+Copyright (c) 2016 Gabriel Gonzalez+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright notice,+ this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.+ * Neither the name of Gabriel Gonzalez nor the names of other contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ dhall.cabal view
@@ -0,0 +1,74 @@+Name: dhall+Version: 1.0.0+Cabal-Version: >=1.8.0.2+Build-Type: Simple+Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2, GHC == 8.0.1+License: BSD3+License-File: LICENSE+Copyright: 2016 Gabriel Gonzalez+Author: Gabriel Gonzalez+Maintainer: Gabriel439@gmail.com+Bug-Reports: https://github.com/Gabriel439/Haskell-Dhall-Library/issues+Synopsis: A configuration language guaranteed to terminate+Description:+ Dhall is an explicitly typed configuration language that is not Turing+ complete. Despite being Turing incomplete, Dhall is a real programming+ language with a type-checker and evaluator.+ .+ Use this library to parse, type-check, evaluate, and pretty-print the Dhall+ configuration language. This package also includes an executable which+ type-checks a Dhall file and reduces the file to a fully evaluated normal+ form.+ .+ "Dhall.Core" contains the core syntax tree and evaluator+ .+ "Dhall.Import" contains logic for resolving remote file and URL references+ .+ "Dhall.TypeChecker" contains the type-checker+ .+ "Dhall.Parser" contains the parser+ .+ Read "Dhall.Tutorial" to learn how to use this library+Category: Compiler+Source-Repository head+ Type: git+ Location: https://github.com/Gabriel439/Haskell-Dhall-Library++Library+ Hs-Source-Dirs: src+ Build-Depends:+ base >= 4 && < 5 ,+ ansi-wl-pprint < 0.7 ,+ bytestring < 0.11,+ containers >= 0.5.0.0 && < 0.6 ,+ http-client >= 0.4.0 && < 0.5 ,+ http-client-tls >= 0.2.0 && < 0.3 ,+ microlens >= 0.2.0.0 && < 0.5 ,+ microlens-mtl >= 0.1.3.1 && < 0.2 ,+ neat-interpolation >= 0.3.2.1 && < 0.4 ,+ parsers >= 0.12.4 && < 0.13,+ system-filepath >= 0.3.1 && < 0.5 ,+ system-fileio >= 0.2.1 && < 0.4 ,+ text >= 0.11.1.0 && < 1.3 ,+ text-format < 0.4 ,+ transformers >= 0.2.0.0 && < 0.6 ,+ trifecta >= 1.6 && < 1.7 ,+ unordered-containers >= 0.1.3.0 && < 0.3 ,+ vector >= 0.11.0.0 && < 0.12+ Exposed-Modules:+ Dhall,+ Dhall.Context,+ Dhall.Core,+ Dhall.Import,+ Dhall.Parser,+ Dhall.TypeCheck++Executable dhall+ Hs-Source-Dirs: exec+ Main-Is: Main.hs+ Build-Depends:+ base >= 4 && < 5 ,+ dhall ,+ optparse-generic >= 1.1.1 && < 1.2,+ trifecta >= 1.6 && < 1.7,+ text >= 0.11.1.0 && < 1.3
+ exec/Main.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeOperators #-}++module Main where++import Control.Exception (SomeException)+import Data.Monoid (mempty)+import Data.Traversable+import Dhall.Core (pretty, normalize)+import Dhall.Import (Imported(..), load)+import Dhall.Parser (Src, exprFromText)+import Dhall.TypeCheck (DetailedTypeError(..), TypeError)+import Options.Generic (Generic, ParseRecord, type (<?>)(..))+import System.IO (stderr)+import System.Exit (exitFailure)+import Text.Trifecta.Delta (Delta(..))++import qualified Control.Exception+import qualified Data.Text.Lazy.IO+import qualified Dhall.TypeCheck+import qualified Options.Generic+import qualified System.Exit+import qualified System.IO++data Mode = Default | Resolve | TypeCheck | Normalize++data Options = Options+ { explain :: Bool <?> "Explain error messages in more detail"+ } deriving (Generic)++instance ParseRecord Options++main :: IO ()+main = do+ options <- Options.Generic.getRecord "Compiler for the Dhall language"++ let handle =+ Control.Exception.handle handler2+ . Control.Exception.handle handler1+ . Control.Exception.handle handler0+ where+ handler0 e = do+ let _ = e :: TypeError Src+ System.IO.hPutStrLn stderr ""+ if unHelpful (explain options)+ then Control.Exception.throwIO (DetailedTypeError e)+ else do+ Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"+ Control.Exception.throwIO e++ handler1 (Imported ps e) = do+ let _ = e :: TypeError Src+ System.IO.hPutStrLn stderr ""+ if unHelpful (explain options)+ then Control.Exception.throwIO (Imported ps (DetailedTypeError e))+ else do+ Data.Text.Lazy.IO.hPutStrLn stderr "\ESC[2mUse \"dhall --explain\" for detailed errors\ESC[0m"+ Control.Exception.throwIO (Imported ps e)++ handler2 e = do+ let _ = e :: SomeException+ System.IO.hPutStrLn stderr ""+ System.IO.hPrint stderr e+ System.Exit.exitFailure++ handle (do+ inText <- Data.Text.Lazy.IO.getContents++ expr <- case exprFromText (Directed "(stdin)" 0 0 0 0) inText of+ Left err -> Control.Exception.throwIO err+ Right expr -> return expr++ expr' <- load Nothing expr++ typeExpr <- case Dhall.TypeCheck.typeOf expr' of+ Left err -> Control.Exception.throwIO err+ Right typeExpr -> return typeExpr+ Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr))+ Data.Text.Lazy.IO.hPutStrLn stderr mempty+ Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) )
+ src/Dhall.hs view
@@ -0,0 +1,618 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}++-- | Dhall is a programming language specialized for configuration files.+--+-- The simplest possible way to use Dhall is to ignore the programming language+-- features and use it as a strongly typed configuration format. For example,+-- suppose that you have the following configuration file:+-- +-- > $ cat config+-- > < Example =+-- > { foo = 1+-- > , bar = [3.0, 4.0, 5.0] : List Double+-- > }+-- > >+-- +-- You can read the above configuration file into Haskell using the following+-- code:+-- +-- > $ cat example.hs+-- > {-# LANGUAGE DeriveGeneric #-}+-- > {-# LANGUAGE OverloadedStrings #-}+-- > +-- > import Dhall+-- > +-- > data Example = Example { foo :: Integer , bar :: Vector Double }+-- > deriving (Generic, Show)+-- > +-- > instance Interpret Example+-- > +-- > main :: IO ()+-- > main = do+-- > x <- input auto "./config"+-- > print (x :: Example)+-- +-- If you compile and run the above program, the program prints the+-- corresponding Haskell record:+-- +-- > $ ./example+-- > Example {foo = 1, bar = [3.0,4.0,5.0]}+--+-- In the above code, the @Example@ Haskell type represents the schema for our+-- configuration file. Suppose that we modify our configuration file to no+-- longer match the schema, like this:+--+-- > $ echo "1" > config+--+-- This then throws an exception when we try to load the configuration file:+--+-- > $ ./example+-- > example: +-- > Expression: 1 : { bar : List Double, foo : Integer }+-- > +-- > Error: Expression's inferred type does not match annotated type+-- > +-- > Explanation: You can annotate the type or kind of an expression like this:+-- > +-- > x : t -- `x` is the expression and `t` is the annotated type or kind of `x`+-- > +-- > Annotations are introduced in one of two ways:+-- > +-- > * You can manually annotate expressions to declare the type or kind you expect+-- > * The interpreter also implicitly inserts a top-level type annotation+-- > +-- > Annotations are optional because the compiler can infer the type of all+-- > expressions. However, if you or the interpreter inserts an annotation and the+-- > inferred type or kind does not match the annotation then type-checking fails.+-- > +-- > You or the interpreter annotated this expression:+-- > ↳ 1+-- > ... with this type or kind:+-- > ↳ { bar : List Double, foo : Integer }+-- > ... but the inferred type of the expression is actually this type or kind:+-- > ↳ Integer+--+-- The Dhall programming language is a statically typed language and the+-- above error message is the output of the language's type-checker. Every+-- expression we read into Haskell is type-checked against the expected schema.+--+-- The above error message says that the type-checker expected a record with+-- two fields: a field named @bar@ that is a `Vector` of `Double`s, and a+-- field named @foo@ that is an `Integer`. However, the type-checker found an+-- expression whose inferred type was an `Integer`. Since an `Integer` is not+-- the same thing as a record the type-checking step fails and Dhall does not+-- bother to marshal the configuration into Haskell.+--+-- Dhall is also a heavily restricted programming language. For example, we can+-- define a configuration file that is an anonymous function:+--+-- > $ cat > makeBools+-- > \(n : Bool) ->+-- > [ n && True, n && False, n || True, n || False ] : List Bool+-- > <Ctrl-D>+--+-- You can read this as a function of one argument named @n@ of type `Bool`+-- that returns a `Vector` of `Bool`s. Each element of the `Vector` depends+-- on the input argument.+--+-- This library comes with a command-line compiler named @dhall@ that you can+-- use to type-check configuration files and convert them to a normal form. For+-- example, we can ask the compiler what the type of our @makeBools@ file+-- is:+--+-- > $ dhall typecheck < makeBools+-- > ∀(n : Bool) → List Bool+--+-- This says that @makeBools@ is a function of one argument named @n@ of type+-- `Bool` that returns a `Vector` of `Bool`s.+--+-- We can apply our file to a `Bool` argument as if it were an ordinary+-- function, like this:+--+-- > {-# LANGUAGE OverloadedStrings #-}+-- >+-- > import Dhall+-- >+-- > main :: IO ()+-- > main = do+-- > x <- input auto "./makeBools True"+-- > print (x :: Vector Bool)+--+-- This produces the following output:+--+-- > $ ./example+-- > [True,False,True,True]+--+-- Notice how we can decode into some types \"out-of-the-box\" without declaring+-- a Haskell record to store the output. In the above example we marshalled+-- the result directly into a `Vector` of `Bool`s. The instances for the+-- `Interpret` class list all types that are automatically supported.+--+-- We can also test functions directly on the command line using the @dhall@+-- compiler. For example:+--+-- > $ dhall+-- > ./makeBools False+-- > <Ctrl-D>+-- > List Bool+-- > +-- > [False, False, True, False] : List Bool+--+-- The @dhall@ compiler with no arguments produces two output lines:+--+-- * The first output line is the type of the result+-- * The second output line is the normal form of the expression that we input+--+-- In the above example the type of the result is a `Vector` of `Bool`s and the+-- normal form of the expression just evaluates all functions.+--+-- You can also use the Dhall compiler to evaluate expressions which have no+-- file references. For example:+--+-- > $ dhall+-- > "Hello, " <> "world!"+-- > <Ctrl-D>+-- > Text+-- > +-- > "Hello, world!"+--+-- > $ dhall+-- > +10 * +10+-- > Natural+-- > +-- > +100+--+-- Dhall is a very restricted programming language that only supports simple+-- operations. For example, Dhall only support addition and subtraction on+-- `Natural` numbers (i.e. non-negative numbers), which are not the same type of+-- number as `Integer`s (which can be negative). A `Natural` number is a number+-- prefixed with the @+@ symbol. If you try to add or multiply two `Integer`s+-- (without the @+@ prefix) you will get a type error:+--+-- > $ dhall+-- > 2 + 2+-- > <Ctrl-D>+-- > dhall: +-- > Expression: 2 + 2+-- > +-- > Error: Cannot use `(+)` on a value that's not a `Natural`+-- > +-- > Explanation: The `(+)` operator expects two arguments of type `Natural`+-- > +-- > You provided this argument:+-- > +-- > 2 + ...+-- > +-- > ... whose type is not `Natural`. The type is actually:+-- > ↳ Integer+-- > +-- > An `Integer` is not the same thing as a `Natural` number. They are distinct+-- > types: `Integer`s can be negative, but `Natural` numbers must be non-negative+-- > +-- > You can prefix an `Integer` literal with a `+` to create a `Natural` literal+-- > +-- > Example:+-- > +-- > +2 + ...+--+-- The Dhall language doesn't just type-check the final schema; the language+-- also ensures that every expression is internally consistent. For example,+-- suppose that we call @./makeBools@ on a non-`Bool` argument:+--+--+-- > $ dhall+-- > ./makeBools "ABC"+-- > dhall: +-- > Expression: (λ(n : Bool) → [n && True, n && False, n || True, n || False] : List Bool) "ABC"+-- > +-- > Error: Function applied to the wrong type or kind of argument+-- > +-- > Explanation: Every function declares what type or kind of argument to accept+-- > +-- > λ(x : Bool) → x -- Anonymous function which only accepts `Bool` arguments+-- > +-- > let f (x : Bool) = x -- Named function which only accepts `Bool` arguments+-- > in f True+-- > +-- > λ(a : Type) → a -- Anonymous function which only accepts `Type` arguments+-- > +-- > You *cannot* apply a function to the wrong type or kind of argument:+-- > +-- > (λ(x : Bool) → x) "A" -- "A" is `Text`, but the function expects a `Bool`+-- > +-- > You tried to invoke a function which expects an argument of type or kind:+-- > ↳ Bool+-- > ... on an argument of type or kind:+-- > ↳ Text+--+-- We get a type error saying that our function expects a `Bool` argument, but+-- we supplied an argument of type `Text` instead.+--+-- Our `input` function also doesn't need to reference any files at all:+--+-- >>> input auto "True && False" :: IO Bool+-- False+--+-- Reading from an external configuration file is just a special case of Dhall's+-- support for embedding files as expressions. There's no limit to how many+-- files-as-expressions that you can nest this way. For example, we can define+-- one file that is a Dhall expression that in turn depends on another file+-- which is also a Dhall expression:+--+-- > $ echo './bool1 && ./bool2' > both+-- > $ echo 'True' > bool1+-- > $ echo 'False' > bool2+-- > $ dhall+-- > [ ./bool1 , ./bool2 , ./both ] : List Bool+-- > <Ctrl-D>+-- > List Bool+-- > +-- > [ True, False, False ] : List Bool+--+-- The only restriction is that the Dhall language will forbid cycles in these+-- file references:+--+-- > $ echo './bar' > foo+-- > $ echo './foo' > bar+-- > $ dhall < ./foo+-- > dhall: +-- > ⤷ ./bar +-- > ⤷ ./foo +-- > Cyclic import: ./bar +--+-- Dhall is a total programming language, which means that Dhall is not+-- Turing-complete and evaluation of every Dhall program is guaranteed to+-- eventually halt. There is no upper bound on how long the program might take+-- to evaluate, but the program is guaranteed to terminate in a finite amount of+-- time and not hang forever.+--+-- This guarantees that all Dhall programs can be safely reduced to a normal+-- form where all functions have been evaluated. In fact, Dhall expressions can+-- be evaluated even if all function arguments haven't been fully applied. For+-- example, the following program is an anonymous function:+--+-- > $ dhall+-- > \(n : Bool) -> +10 * +10+-- > <Ctrl-D>+-- > ∀(n : Bool) → Natural+-- > +-- > λ(n : Bool) → +100+--+-- ... and even though the function is still missing the first argument named+-- @n@ the compiler is smart enough to evaluate the body of the anonymous+-- function ahead of time before the function has even been invoked.+--+-- Similarly, you can use this normalization process to remove indirection+-- introduced by well-meaning software engineers over-architecting the+-- configuration file.++module Dhall+ (+ -- * Input+ input++ -- * Types+ , Type+ , Interpret(..)+ , bool+ , natural+ , integer+ , double+ , text+ , maybe+ , vector++ -- * Re-exports+ , Text+ , Vector+ , Generic+ ) where++import Control.Applicative (empty, liftA2, (<|>))+import Control.Exception (Exception)+import Data.Monoid ((<>))+import Data.Text.Lazy (Text)+import Data.Vector (Vector)+import Dhall.Core (Expr(..))+import Dhall.Parser (Src(..))+import Dhall.TypeCheck (X)+import GHC.Generics+import Numeric.Natural (Natural)+import Prelude hiding (maybe)+import Text.Trifecta.Delta (Delta(..))++import qualified Control.Exception+import qualified Data.ByteString.Lazy+import qualified Data.Map+import qualified Data.Text.Lazy+import qualified Data.Text.Lazy.Builder+import qualified Data.Text.Lazy.Encoding+import qualified Data.Vector+import qualified Dhall.Core+import qualified Dhall.Import+import qualified Dhall.Parser+import qualified Dhall.TypeCheck+import qualified GHC.Generics++throws :: Exception e => Either e a -> IO a+throws (Left e) = Control.Exception.throwIO e+throws (Right r) = return r++{-| Type-check and evaluate a Dhall program, decoding the result into Haskell++ The first argument determines the type of value that you decode:++>>> input integer "2"+2+>>> input (vector double) "[ 1.0, 2.0 ] : List Bool"+[1.0,2.0]++ Use `auto` to automatically select which type to decode based on the+ inferred return type:++>>> input auto "True" :: IO Bool+True+-}+input+ :: Type a+ -- ^ The type of value to decode from Dhall to Haskell+ -> Text+ -- ^ The Dhall program+ -> IO a+ -- ^ The decoded value in Haskell+input (Type {..}) text = do+ let delta = Directed "(input)" 0 0 0 0+ expr <- throws (Dhall.Parser.exprFromText delta text)+ expr' <- Dhall.Import.load Nothing expr+ let suffix =+ ( Data.ByteString.Lazy.toStrict+ . Data.Text.Lazy.Encoding.encodeUtf8+ . Data.Text.Lazy.Builder.toLazyText+ . Dhall.Core.buildExpr0+ ) expected+ let annot = case expr' of+ Note (Src begin end bytes) _ ->+ Note (Src begin end bytes') (Annot expr' expected)+ where+ bytes' = bytes <> " : " <> suffix+ _ ->+ Annot expr' expected+ typeExpr <- throws (Dhall.TypeCheck.typeOf annot)+ case extract (Dhall.Core.normalize expr') of+ Just x -> return x+ Nothing -> fail "input: malformed `Type`"++{-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall+ into Haskell++ You can produce `Type`s either explicitly:++> example :: Type (Vector Text)+> example = vector text++ ... or implicitly using `auto`:++> example :: Type (Vector Text)+> example = auto++ You can consume `Type`s using the `input` function:++> input :: Type a -> Text -> IO a+-}+data Type a = Type+ { extract :: Expr X X -> Maybe a+ , expected :: Expr Src X+ }+ deriving (Functor)++{-| Decode a `Bool`++>>> input bool "True"+True+-}+bool :: Type Bool+bool = Type {..}+ where+ extract (BoolLit b) = pure b+ extract _ = Nothing++ expected = Bool++{-| Decode a `Natural`++>>> input natural "+42"+42+-}+natural :: Type Natural+natural = Type {..}+ where+ extract (NaturalLit n) = pure n+ extract _ = empty++ expected = Natural++{-| Decode an `Integer`++>>> input integer "42"+42+-}+integer :: Type Integer+integer = Type {..}+ where+ extract (IntegerLit n) = pure n+ extract _ = empty++ expected = Integer++{-| Decode a `Double`++>>> input double "42.0"+42.0+-}+double :: Type Double+double = Type {..}+ where+ extract (DoubleLit n) = pure n+ extract _ = empty++ expected = Double++{-| Decode `Text`++>>> input text "\"Test\""+"Test"+-}+text :: Type Text+text = Type {..}+ where+ extract (TextLit t) = pure (Data.Text.Lazy.Builder.toLazyText t)+ extract _ = empty++ expected = Text++{-| Decode a `Maybe`++>>> input (maybe integer) "[] : Maybe Integer"+Nothing+-}+maybe :: Type a -> Type (Maybe a)+maybe (Type extractIn expectedIn) = Type extractOut expectedOut+ where+ extractOut (OptionalLit _ es) = traverse extractIn es'+ where+ es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)++ expectedOut = App Optional expectedIn++{-| Decode a `Vector`++>>> input (vector integer) "[ 1, 2, 3 ] : List Integer"+[1,2,3]+-}+vector :: Type a -> Type (Vector a)+vector (Type extractIn expectedIn) = Type extractOut expectedOut+ where+ extractOut (ListLit _ es) = traverse extractIn es++ expectedOut = App List expectedIn++{-| Any value that implements `Interpret` can be automatically decoded based on+ the inferred return type of `input`++>>> input auto "[1, 2, 3 ] : List Integer" :: IO (Vector Integer)+[1,2,3]++ This class auto-generates a default implementation for records that+ implement `Generic`. This does not auto-generate an instance for sum types+ nor recursive types.+-}+class Interpret a where+ auto :: Type a+ default auto :: (Generic a, GenericInterpret (Rep a)) => Type a+ auto = fmap GHC.Generics.to genericAuto++instance Interpret Bool where+ auto = bool++instance Interpret Natural where+ auto = natural++instance Interpret Integer where+ auto = integer++instance Interpret Double where+ auto = double++instance Interpret Text where+ auto = text++instance Interpret a => Interpret (Maybe a) where+ auto = maybe auto++instance Interpret a => Interpret (Vector a) where+ auto = vector auto++class GenericInterpret f where+ genericAuto :: Type (f a)++instance GenericInterpret f => GenericInterpret (M1 D d f) where+ genericAuto = fmap M1 genericAuto++instance GenericInterpret V1 where+ genericAuto = Type {..}+ where+ extract _ = Nothing++ expected = Union Data.Map.empty++instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :+: g) where+ genericAuto = Type {..}+ where+ extract e = fmap L1 (extractL e) <|> fmap R1 (extractR e)++ expected = Union (Data.Map.union expectedL expectedR)++ Type extractL (Union expectedL) = genericAuto+ Type extractR (Union expectedR) = genericAuto++instance (Constructor c, GenericInterpret f) => GenericInterpret (M1 C c f) where+ genericAuto = Type {..}+ where+ n :: M1 i c f a+ n = undefined++ name = Data.Text.Lazy.pack (conName n)++ extract (UnionLit name' e _)+ | name == name' = fmap M1 (extract' e)+ | otherwise = Nothing++ expected = Union (Data.Map.singleton name expected')++ Type extract' expected' = genericAuto++instance GenericInterpret U1 where+ genericAuto = Type {..}+ where+ extract _ = Just U1++ expected = Record (Data.Map.fromList [])++instance (GenericInterpret f, GenericInterpret g) => GenericInterpret (f :*: g) where+ genericAuto = Type {..}+ where+ extract = liftA2 (liftA2 (:*:)) extractL extractR++ expected = Record (Data.Map.union ktsL ktsR)+ where+ Record ktsL = expectedL+ Record ktsR = expectedR+ Type extractL expectedL = genericAuto+ Type extractR expectedR = genericAuto++instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where+ genericAuto = Type {..}+ where+ n :: M1 i s f a+ n = undefined++ extract (RecordLit m) = do+ case selName n of+ "" -> Nothing+ name -> do+ e <- Data.Map.lookup (Data.Text.Lazy.pack name) m+ fmap (M1 . K1) (extract' e)+ extract _ = Nothing++ expected = Record (Data.Map.fromList [(key, expected')])+ where+ key = Data.Text.Lazy.pack (selName n)++ Type extract' expected' = auto
+ src/Dhall/Context.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveFunctor #-}++-- | All `Context`-related operations++module Dhall.Context (+ -- * Context+ Context+ , empty+ , insert+ , lookup+ , toList+ ) where++import Data.Text.Lazy (Text)+import Prelude hiding (lookup)++{-| A @(Context a)@ associates `Text` labels with values of type @a@++ The `Context` is used for type-checking when @(a = Expr X)@++ * You create a `Context` using `empty` and `insert`+ * You transform a `Context` using `fmap`+ * You consume a `Context` using `lookup` and `toList`++ The difference between a `Context` and a `Map` is that a `Context` lets you+ have multiple occurrences of the same key and you can query for the @n@th+ occurrence of a given key.+-}+newtype Context a = Context { getContext :: [(Text, a)] }+ deriving (Functor)++-- | An empty context with no key-value pairs+empty :: Context a+empty = Context []++-- | Add a key-value pair to the `Context`+insert :: Text -> a -> Context a -> Context a+insert k v (Context kvs) = Context ((k, v) : kvs)+{-# INLINABLE insert #-}++{-| Look up a key by name and index++> lookup _ _ empty = Nothing+> lookup k 0 (insert k v c) = Just v+> lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n+> lookup k n (insert j v c) = lookup k n c -- k /= j+-}+lookup :: Text -> Integer -> Context a -> Maybe a+lookup _ !_ (Context [] ) =+ Nothing+lookup x !n (Context ((k, v):kvs)) =+ if x == k+ then if n == 0+ then Just v+ else lookup x (n - 1) (Context kvs)+ else lookup x n (Context kvs)+{-# INLINABLE lookup #-}++{-| Return all key-value associations as a list++> toList empty = []+> toList (insert k v ctx) = (k, v) : toList ctx+-}+toList :: Context a -> [(Text, a)]+toList = getContext+{-# INLINABLE toList #-}
+ src/Dhall/Core.hs view
@@ -0,0 +1,1321 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# OPTIONS_GHC -Wall #-}++-- | This module contains the core calculus for the Dhall language.++module Dhall.Core (+ -- * Syntax+ Const(..)+ , Path(..)+ , Var(..)+ , Expr(..)++ -- * Normalization+ , normalize+ , subst+ , shift++ -- * Builders+ -- $builders+ , pretty+ , buildExpr0+ , buildExpr1+ , buildExpr2+ , buildExpr3+ , buildExpr4+ , buildExpr5+ , buildExpr6+ , buildConst+ , buildVar+ , buildElems+ , buildRecordLit+ , buildFieldValues+ , buildFieldValue+ , buildRecord+ , buildFieldTypes+ , buildFieldType+ , buildUnion+ , buildAlternativeTypes+ , buildAlternativeType+ , buildUnionLit++ -- * Miscellaneous+ , internalError+ ) where++#if MIN_VERSION_base(4,8,0)+#else+import Control.Applicative (Applicative(..), (<$>))+#endif+import Data.Bifunctor (Bifunctor(..))+import Data.Foldable+import Data.Map (Map)+import Data.Monoid ((<>))+import Data.String (IsString(..))+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+import Data.Traversable+import Data.Vector (Vector)+import Filesystem.Path.CurrentOS (FilePath)+import Numeric.Natural (Natural)+import Prelude hiding (FilePath)++import qualified Control.Monad+import qualified Data.Map+import qualified Data.Maybe+import qualified Data.Text+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Vector+import qualified Data.Vector.Mutable+import qualified Filesystem.Path.CurrentOS as Filesystem+import qualified NeatInterpolation++{-| Constants for a pure type system++ The only axiom is:++> ⊦ Type : Kind++ ... and the valid rule pairs are:++> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)+> ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions)+> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors)++ These are the same rule pairs as System Fω++ Note that Dhall does not support functions from terms to types and therefore+ Dhall is not a dependently typed language+-}+data Const = Type | Kind deriving (Show, Bounded, Enum)++instance Buildable Const where+ build = buildConst++-- | Path to an external resource+data Path+ = File FilePath+ | URL Text+ deriving (Eq, Ord, Show)++instance Buildable Path where+ build (File file)+ | Text.isPrefixOf "./" txt+ || Text.isPrefixOf "/" txt+ || Text.isPrefixOf "../" txt+ = build txt <> " "+ | otherwise+ = "./" <> build txt <> " "+ where+ txt = Text.fromStrict (either id id (Filesystem.toText file))+ build (URL str ) = build str <> " "++{-| Label for a bound variable++ The `Text` field is the variable's name (i.e. \"@x@\").++ The `Int` field disambiguates variables with the same name if there are+ multiple bound variables of the same name in scope. Zero refers to the+ nearest bound variable and the index increases by one for each bound+ variable of the same name going outward. The following diagram may help:++> +-refers to-++> | |+> v |+> \(x : *) -> \(y : *) -> \(x : *) -> x@0+>+> +-------------refers to-------------++> | |+> v |+> \(x : *) -> \(y : *) -> \(x : *) -> x@1++ This `Int` behaves like a De Bruijn index in the special case where all+ variables have the same name.++ You can optionally omit the index if it is @0@:++> +refers to++> | |+> v |+> \(x : *) -> \(y : *) -> \(x : *) -> x++ Zero indices are omitted when pretty-printing `Var`s and non-zero indices+ appear as a numeric suffix.+-}+data Var = V Text !Integer+ deriving (Eq, Show)++instance IsString Var where+ fromString str = V (fromString str) 0++instance Buildable Var where+ build = buildVar++-- | Syntax tree for expressions+data Expr s a+ -- | > Const c ~ c+ = Const Const+ -- | > Var (V x 0) ~ x+ -- > Var (V x n) ~ x@n+ | Var Var + -- | > Lam x A b ~ λ(x : A) -> b+ | Lam Text (Expr s a) (Expr s a)+ -- | > Pi "_" A B ~ A -> B+ -- > Pi x A B ~ ∀(x : A) -> B+ | Pi Text (Expr s a) (Expr s a)+ -- | > App f a ~ f a+ | App (Expr s a) (Expr s a)+ -- | > Let x Nothing r e ~ let x = r in e+ -- > Let x (Just t) r e ~ let x : t = r in e+ | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)+ -- | > Annot x t ~ x : t+ | Annot (Expr s a) (Expr s a)+ -- | > Bool ~ Bool+ | Bool+ -- | > BoolLit b ~ b+ | BoolLit Bool+ -- | > BoolAnd x y ~ x && y+ | BoolAnd (Expr s a) (Expr s a)+ -- | > BoolOr x y ~ x || y+ | BoolOr (Expr s a) (Expr s a)+ -- | > BoolEQ x y ~ x == y+ | BoolEQ (Expr s a) (Expr s a)+ -- | > BoolNE x y ~ x /= y+ | BoolNE (Expr s a) (Expr s a)+ -- | > BoolIf x y z ~ if x then y else z+ | BoolIf (Expr s a) (Expr s a) (Expr s a)+ -- | > Natural ~ Natural+ | Natural+ -- | > NaturalLit n ~ +n+ | NaturalLit Natural+ -- | > NaturalFold ~ Natural/fold+ | NaturalFold+ -- | > NaturalBuild ~ Natural/build+ | NaturalBuild+ -- | > NaturalIsZero ~ Natural/isZero+ | NaturalIsZero+ -- | > NaturalEven ~ Natural/even+ | NaturalEven+ -- | > NaturalOdd ~ Natural/odd+ | NaturalOdd+ -- | > NaturalPlus x y ~ x + y+ | NaturalPlus (Expr s a) (Expr s a)+ -- | > NaturalTimes x y ~ x * y+ | NaturalTimes (Expr s a) (Expr s a)+ -- | > Integer ~ Integer+ | Integer+ -- | > IntegerLit n ~ n+ | IntegerLit Integer+ -- | > Double ~ Double+ | Double+ -- | > DoubleLit n ~ n+ | DoubleLit Double+ -- | > Text ~ Text+ | Text+ -- | > TextLit t ~ t+ | TextLit Builder+ -- | > TextAppend x y ~ x ++ y+ | TextAppend (Expr s a) (Expr s a)+ -- | > List ~ List+ | List+ -- | > ListLit t [x, y, z] ~ [x, y, z] : List t+ | ListLit (Expr s a) (Vector (Expr s a))+ -- | > ListBuild ~ List/build+ | ListBuild+ -- | > ListFold ~ List/fold+ | ListFold+ -- | > ListLength ~ List/length+ | ListLength+ -- | > ListHead ~ List/head+ | ListHead + -- | > ListLast ~ List/last+ | ListLast+ -- | > ListIndexed ~ List/indexed+ | ListIndexed+ -- | > ListReverse ~ List/reverse+ | ListReverse+ -- | > Optional ~ Optional+ | Optional+ -- | > OptionalLit t [e] ~ [e] : Optional t+ -- > OptionalLit t [] ~ [] : Optional t+ | OptionalLit (Expr s a) (Vector (Expr s a))+ -- | > OptionalFold ~ Optional/fold+ | OptionalFold+ -- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }+ | Record (Map Text (Expr s a))+ -- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }+ | RecordLit (Map Text (Expr s a))+ -- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >+ | Union (Map Text (Expr s a))+ -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 > + | UnionLit Text (Expr s a) (Map Text (Expr s a))+ -- | > Combine x y ~ x ∧ y+ | Combine (Expr s a) (Expr s a)+ -- | > Merge x y t ~ merge x y : t+ | Merge (Expr s a) (Expr s a) (Expr s a)+ -- | > Field e x ~ e.x+ | Field (Expr s a) Text+ -- | > Note s x ~ e+ | Note s (Expr s a)+ -- | > Embed path ~ path+ | Embed a+ deriving (Functor, Foldable, Traversable, Show)++instance Applicative (Expr s) where+ pure = Embed++ (<*>) = Control.Monad.ap++instance Monad (Expr s) where+ return = pure++ Const c >>= _ = Const c+ Var v >>= _ = Var v+ Lam x _A b >>= k = Lam x (_A >>= k) ( b >>= k)+ Pi x _A _B >>= k = Pi x (_A >>= k) (_B >>= k)+ App f a >>= k = App (f >>= k) (a >>= k)+ Let f mt r e >>= k = Let f (fmap (>>= k) mt) (r >>= k) (e >>= k)+ Annot x t >>= k = Annot (x >>= k) (t >>= k)+ Bool >>= _ = Bool+ BoolLit b >>= _ = BoolLit b+ BoolAnd l r >>= k = BoolAnd (l >>= k) (r >>= k)+ BoolOr l r >>= k = BoolOr (l >>= k) (r >>= k)+ BoolEQ l r >>= k = BoolEQ (l >>= k) (r >>= k)+ BoolNE l r >>= k = BoolNE (l >>= k) (r >>= k)+ BoolIf x y z >>= k = BoolIf (x >>= k) (y >>= k) (z >>= k)+ Natural >>= _ = Natural+ NaturalLit n >>= _ = NaturalLit n+ NaturalFold >>= _ = NaturalFold+ NaturalBuild >>= _ = NaturalBuild+ NaturalIsZero >>= _ = NaturalIsZero+ NaturalEven >>= _ = NaturalEven+ NaturalOdd >>= _ = NaturalOdd+ NaturalPlus l r >>= k = NaturalPlus (l >>= k) (r >>= k)+ NaturalTimes l r >>= k = NaturalTimes (l >>= k) (r >>= k)+ Integer >>= _ = Integer+ IntegerLit n >>= _ = IntegerLit n+ Double >>= _ = Double+ DoubleLit n >>= _ = DoubleLit n+ Text >>= _ = Text+ TextLit t >>= _ = TextLit t+ TextAppend l r >>= k = TextAppend (l >>= k) (r >>= k)+ List >>= _ = List+ ListLit t es >>= k = ListLit (t >>= k) (fmap (>>= k) es)+ ListBuild >>= _ = ListBuild+ ListFold >>= _ = ListFold+ ListLength >>= _ = ListLength+ ListHead >>= _ = ListHead+ ListLast >>= _ = ListLast+ ListIndexed >>= _ = ListIndexed+ ListReverse >>= _ = ListReverse+ Optional >>= _ = Optional+ OptionalLit t es >>= k = OptionalLit (t >>= k) (fmap (>>= k) es)+ OptionalFold >>= _ = OptionalFold+ Record kts >>= k = Record (fmap (>>= k) kts)+ RecordLit kvs >>= k = RecordLit (fmap (>>= k) kvs)+ Union kts >>= k = Union (fmap (>>= k) kts)+ UnionLit k' v kts >>= k = UnionLit k' (v >>= k) (fmap (>>= k) kts)+ Combine x y >>= k = Combine (x >>= k) (y >>= k)+ Merge x y t >>= k = Merge (x >>= k) (y >>= k) (t >>= k)+ Field r x >>= k = Field (r >>= k) x+ Note a b >>= k = Note a (b >>= k)+ Embed r >>= k = k r++instance Bifunctor Expr where+ first _ (Const a ) = Const a+ first _ (Var a ) = Var a+ first k (Lam a b c ) = Lam a (first k b) (first k c)+ first k (Pi a b c ) = Pi a (first k b) (first k c)+ first k (App a b ) = App (first k a) (first k b)+ first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d)+ first k (Annot a b ) = Annot (first k a) (first k b)+ first _ Bool = Bool+ first _ (BoolLit a ) = BoolLit a+ first k (BoolAnd a b ) = BoolAnd (first k a) (first k b)+ first k (BoolOr a b ) = BoolOr (first k a) (first k b)+ first k (BoolEQ a b ) = BoolEQ (first k a) (first k b)+ first k (BoolNE a b ) = BoolNE (first k a) (first k b)+ first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c)+ first _ Natural = Natural+ first _ (NaturalLit a ) = NaturalLit a+ first _ NaturalFold = NaturalFold+ first _ NaturalBuild = NaturalBuild+ first _ NaturalIsZero = NaturalIsZero+ first _ NaturalEven = NaturalEven+ first _ NaturalOdd = NaturalOdd+ first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)+ first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b)+ first _ Integer = Integer+ first _ (IntegerLit a ) = IntegerLit a+ first _ Double = Double+ first _ (DoubleLit a ) = DoubleLit a+ first _ Text = Text+ first _ (TextLit a ) = TextLit a+ first k (TextAppend a b ) = TextAppend (first k a) (first k b)+ first _ List = List+ first k (ListLit a b ) = ListLit (first k a) (fmap (first k) b)+ first _ ListBuild = ListBuild+ first _ ListFold = ListFold+ first _ ListLength = ListLength+ first _ ListHead = ListHead+ first _ ListLast = ListLast+ first _ ListIndexed = ListIndexed+ first _ ListReverse = ListReverse+ first _ Optional = Optional+ first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)+ first _ OptionalFold = OptionalFold+ first k (Record a ) = Record (fmap (first k) a)+ first k (RecordLit a ) = RecordLit (fmap (first k) a)+ first k (Union a ) = Union (fmap (first k) a)+ first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c)+ first k (Combine a b ) = Combine (first k a) (first k b)+ first k (Merge a b c ) = Merge (first k a) (first k b) (first k c)+ first k (Field a b ) = Field (first k a) b+ first k (Note a b ) = Note (k a) (first k b)+ first _ (Embed a ) = Embed a++ second = fmap++instance IsString (Expr s a)+ where+ fromString str = Var (fromString str)++{- $builders+ There is a one-to-one correspondence between the builders in this section+ and the sub-parsers in "Dhall.Parser". Each builder is named after the+ corresponding parser and the relationship between builders exactly matches+ the relationship between parsers. This leads to the nice emergent property+ of automatically getting all the parentheses and precedences right.++ This approach has one major disadvantage: you can get an infinite loop if+ you add a new constructor to the syntax tree without adding a matching+ case the corresponding builder.+-}++-- | Pretty-print a value+pretty :: Buildable a => a -> Text+pretty = Builder.toLazyText . build++-- | Builder corresponding to the @label@ token in "Dhall.Parser"+buildLabel :: Text -> Builder+buildLabel = build++-- | Builder corresponding to the @number@ token in "Dhall.Parser"+buildNumber :: Integer -> Builder+buildNumber a = build (show a)++-- | Builder corresponding to the @natural@ token in "Dhall.Parser"+buildNatural :: Natural -> Builder+buildNatural a = build (show a)++-- | Builder corresponding to the @double@ token in "Dhall.Parser"+buildDouble :: Double -> Builder+buildDouble a = build (show a)++-- | Builder corresponding to the @text@ token in "Dhall.Parser"+buildText :: Builder -> Builder+buildText a = build (show a)++-- | Builder corresponding to the @Expr0@ parser in "Dhall.Parser"+buildExpr0 :: Buildable a => Expr s a -> Builder+buildExpr0 (Annot a b) = buildExpr1 a <> " : " <> buildExpr0 b+buildExpr0 (Note _ b) = buildExpr0 b+buildExpr0 a = buildExpr1 a++-- | Builder corresponding to the @Expr1@ parser in "Dhall.Parser"+buildExpr1 :: Buildable a => Expr s a -> Builder+buildExpr1 (Lam a b c) =+ "λ("+ <> buildLabel a+ <> " : "+ <> buildExpr0 b+ <> ") → "+ <> buildExpr1 c+buildExpr1 (BoolIf a b c) =+ "if "+ <> buildExpr0 a+ <> " then "+ <> buildExpr1 b+ <> " else "+ <> buildExpr1 c+buildExpr1 (Pi "_" b c) =+ buildExpr2 b+ <> " → "+ <> buildExpr1 c+buildExpr1 (Pi a b c) =+ "∀("+ <> buildLabel a+ <> " : "+ <> buildExpr0 b+ <> ") → "+ <> buildExpr1 c+buildExpr1 (Let a Nothing c d) =+ "let "+ <> buildLabel a+ <> " = "+ <> buildExpr0 c+ <> " in "+ <> buildExpr1 d+buildExpr1 (Let a (Just b) c d) =+ "let "+ <> buildLabel a+ <> " : "+ <> buildExpr0 b+ <> " = "+ <> buildExpr0 c+ <> " in "+ <> buildExpr1 d+buildExpr1 (ListLit a b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : List " <> buildExpr6 a+buildExpr1 (OptionalLit a b) =+ "[" <> buildElems (Data.Vector.toList b) <> "] : Optional " <> buildExpr6 a+buildExpr1 (Merge a b c) =+ "merge " <> buildExpr6 a <> " " <> buildExpr6 b <> " : " <> buildExpr5 c+buildExpr1 (Note _ b) =+ buildExpr1 b+buildExpr1 a =+ buildExpr2 a++-- | Builder corresponding to the @Expr2@ parser in "Dhall.Parser"+buildExpr2 :: Buildable a => Expr s a -> Builder+buildExpr2 (BoolEQ a b) = buildExpr2 a <> " == " <> buildExpr2 b+buildExpr2 (BoolNE a b) = buildExpr2 a <> " /= " <> buildExpr2 b+buildExpr2 (Note _ b) = buildExpr2 b+buildExpr2 a = buildExpr3 a++-- | Builder corresponding to the @Expr3@ parser in "Dhall.Parser"+buildExpr3 :: Buildable a => Expr s a -> Builder+buildExpr3 (BoolOr a b) = buildExpr3 a <> " || " <> buildExpr3 b+buildExpr3 (NaturalPlus a b) = buildExpr3 a <> " + " <> buildExpr3 b+buildExpr3 (TextAppend a b) = buildExpr3 a <> " ++ " <> buildExpr3 b+buildExpr3 (Note _ b) = buildExpr3 b+buildExpr3 a = buildExpr4 a++-- | Builder corresponding to the @Expr4@ parser in "Dhall.Parser"+buildExpr4 :: Buildable a => Expr s a -> Builder+buildExpr4 (BoolAnd a b) = buildExpr4 a <> " && " <> buildExpr4 b+buildExpr4 (NaturalTimes a b) = buildExpr4 a <> " * " <> buildExpr4 b+buildExpr4 (Combine a b) = buildExpr4 a <> " ∧ " <> buildExpr4 b+buildExpr4 (Note _ b) = buildExpr4 b+buildExpr4 a = buildExpr5 a++-- | Builder corresponding to the @Expr5@ parser in "Dhall.Parser"+buildExpr5 :: Buildable a => Expr s a -> Builder+buildExpr5 (App a b) = buildExpr5 a <> " " <> buildExpr6 b+buildExpr5 (Note _ b) = buildExpr5 b+buildExpr5 a = buildExpr6 a++-- | Builder corresponding to the @Expr6@ parser in "Dhall.Parser"+buildExpr6 :: Buildable a => Expr s a -> Builder+buildExpr6 (Var a) =+ buildVar a+buildExpr6 (Const k) =+ buildConst k+buildExpr6 Bool =+ "Bool"+buildExpr6 Natural =+ "Natural"+buildExpr6 NaturalFold =+ "Natural/fold"+buildExpr6 NaturalBuild =+ "Natural/build"+buildExpr6 NaturalIsZero =+ "Natural/isZero"+buildExpr6 NaturalEven =+ "Natural/even"+buildExpr6 NaturalOdd =+ "Natural/odd"+buildExpr6 Integer =+ "Integer"+buildExpr6 Double =+ "Double"+buildExpr6 Text =+ "Text"+buildExpr6 List =+ "List"+buildExpr6 ListBuild =+ "List/build"+buildExpr6 ListFold =+ "List/fold"+buildExpr6 ListLength =+ "List/length"+buildExpr6 ListHead =+ "List/head"+buildExpr6 ListLast =+ "List/last"+buildExpr6 ListIndexed =+ "List/indexed"+buildExpr6 ListReverse =+ "List/reverse"+buildExpr6 Optional =+ "Optional"+buildExpr6 OptionalFold =+ "Optional/fold"+buildExpr6 (BoolLit True) =+ "True"+buildExpr6 (BoolLit False) =+ "False"+buildExpr6 (IntegerLit a) =+ buildNumber a+buildExpr6 (NaturalLit a) =+ "+" <> buildNatural a+buildExpr6 (DoubleLit a) =+ buildDouble a+buildExpr6 (TextLit a) =+ buildText a+buildExpr6 (Record a) =+ buildRecord a+buildExpr6 (RecordLit a) =+ buildRecordLit a+buildExpr6 (Union a) =+ buildUnion a+buildExpr6 (UnionLit a b c) =+ buildUnionLit a b c+buildExpr6 (Embed a) =+ build a+buildExpr6 (Field a b) =+ buildExpr6 a <> "." <> buildLabel b+buildExpr6 (Note _ b) =+ buildExpr6 b+buildExpr6 a =+ "(" <> buildExpr0 a <> ")"++-- | Builder corresponding to the @Const@ parser in "Dhall.Parser"+buildConst :: Const -> Builder+buildConst Type = "Type"+buildConst Kind = "Kind"++-- | Builder corresponding to the @Var@ parser in "Dhall.Parser"+buildVar :: Var -> Builder+buildVar (V x 0) = buildLabel x+buildVar (V x n) = buildLabel x <> "@" <> buildNumber n++-- | Builder corresponding to the @Elems@ parser in "Dhall.Parser"+buildElems :: Buildable a => [Expr s a] -> Builder+buildElems [] = ""+buildElems [a] = buildExpr0 a+buildElems (a:bs) = buildExpr0 a <> ", " <> buildElems bs++-- | Builder corresponding to the @RecordLit@ parser in "Dhall.Parser"+buildRecordLit :: Buildable a => Map Text (Expr s a) -> Builder+buildRecordLit a | Data.Map.null a =+ "{=}"+buildRecordLit a =+ "{ " <> buildFieldValues (Data.Map.toList a) <> " }"++-- | Builder corresponding to the @FieldValues@ parser in "Dhall.Parser"+buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder+buildFieldValues [] = ""+buildFieldValues [a] = buildFieldValue a+buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs++-- | Builder corresponding to the @FieldValue@ parser in "Dhall.Parser"+buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder+buildFieldValue (a, b) = buildLabel a <> " = " <> buildExpr0 b++-- | Builder corresponding to the @Record@ parser in "Dhall.Parser"+buildRecord :: Buildable a => Map Text (Expr s a) -> Builder+buildRecord a | Data.Map.null a =+ "{}"+buildRecord a =+ "{ " <> buildFieldTypes (Data.Map.toList a) <> " }"++-- | Builder corresponding to the @FieldTypes@ parser in "Dhall.Parser"+buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder+buildFieldTypes [] = ""+buildFieldTypes [a] = buildFieldType a+buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs++-- | Builder corresponding to the @FieldType@ parser in "Dhall.Parser"+buildFieldType :: Buildable a => (Text, Expr s a) -> Builder+buildFieldType (a, b) = buildLabel a <> " : " <> buildExpr0 b++-- | Builder corresponding to the @Union@ parser in "Dhall.Parser"+buildUnion :: Buildable a => Map Text (Expr s a) -> Builder+buildUnion a | Data.Map.null a =+ "<>"+buildUnion a =+ "< " <> buildAlternativeTypes (Data.Map.toList a) <> " >"++-- | Builder corresponding to the @AlternativeTypes@ parser in "Dhall.Parser"+buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder+buildAlternativeTypes [] =+ ""+buildAlternativeTypes [a] =+ buildAlternativeType a+buildAlternativeTypes (a:bs) =+ buildAlternativeType a <> " | " <> buildAlternativeTypes bs++-- | Builder corresponding to the @AlternativeType@ parser in "Dhall.Parser"+buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder+buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExpr0 b++-- | Builder corresponding to the @UnionLit@ parser in "Dhall.Parser"+buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder+buildUnionLit a b c+ | Data.Map.null c =+ "< "+ <> buildLabel a+ <> " = "+ <> buildExpr0 b+ <> " >"+ | otherwise =+ "< "+ <> buildLabel a+ <> " = "+ <> buildExpr0 b+ <> " | "+ <> buildAlternativeTypes (Data.Map.toList c)+ <> " >"++-- | Generates a syntactically valid Dhall program+instance Buildable a => Buildable (Expr s a)+ where+ build = buildExpr0++{-| `shift` is used by both normalization and type-checking to avoid variable+ capture by shifting variable indices++ For example, suppose that you were to normalize the following expression:++> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x++ If you were to substitute @y@ with @x@ without shifting any variable+ indices, then you would get the following incorrect result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form++ In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in+ order to avoid being misinterpreted as the @x@ bound by the innermost+ lambda. If we perform that `shift` then we get the correct result:++> λ(a : Type) → λ(x : a) → λ(x : a) → x@1++ As a more worked example, suppose that you were to normalize the following+ expression:++> λ(a : Type)+> → λ(f : a → a → a)+> → λ(x : a)+> → λ(x : a)+> → (λ(x : a) → f x x@1) x@1++ The correct normalized result would be:++> λ(a : Type)+> → λ(f : a → a → a)+> → λ(x : a)+> → λ(x : a)+> → f x@1 x++ The above example illustrates how we need to both increase and decrease+ variable indices as part of substitution:++ * We need to increase the index of the outer @x\@1@ to @x\@2@ before we+ substitute it into the body of the innermost lambda expression in order+ to avoid variable capture. This substitution changes the body of the+ lambda expression to @(f x\@2 x\@1)@++ * We then remove the innermost lambda and therefore decrease the indices of+ both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one+ less @x@ variable is now bound within that scope++ Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to+ the indices of all variables named @x@ whose indices are greater than+ @(n + m)@, where @m@ is the number of bound variables of the same name+ within that scope++ In practice, @d@ is always @1@ or @-1@ because we either:++ * increment variables by @1@ to avoid variable capture during substitution+ * decrement variables by @1@ when deleting lambdas after substitution++ @n@ starts off at @0@ when substitution begins and increments every time we+ descend into a lambda or let expression that binds a variable of the same+ name in order to avoid shifting the bound variables by mistake.+-}+shift :: Integer -> Var -> Expr s a -> Expr t a+shift _ _ (Const a) = Const a+shift d (V x n) (Var (V x' n')) = Var (V x' n'')+ where+ n'' = if x == x' && n <= n' then n' + d else n'+shift d (V x n) (Lam x' _A b) = Lam x' _A' b'+ where+ _A' = shift d (V x n ) _A+ b' = shift d (V x n') b+ where+ n' = if x == x' then n + 1 else n+shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'+ where+ _A' = shift d (V x n ) _A+ _B' = shift d (V x n') _B+ where+ n' = if x == x' then n + 1 else n+shift d v (App f a) = App f' a'+ where+ f' = shift d v f+ a' = shift d v a+shift d (V x n) (Let f mt r e) = Let f mt' r' e'+ where+ e' = shift d (V x n') e+ where+ n' = if x == f then n + 1 else n++ mt' = fmap (shift d (V x n)) mt+ r' = shift d (V x n) r+shift d v (Annot a b) = Annot a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ Bool = Bool+shift _ _ (BoolLit a) = BoolLit a+shift d v (BoolAnd a b) = BoolAnd a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolOr a b) = BoolOr a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolEQ a b) = BoolEQ a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolNE a b) = BoolNE a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (BoolIf a b c) = BoolIf a' b' c'+ where+ a' = shift d v a+ b' = shift d v b+ c' = shift d v c+shift _ _ Natural = Natural+shift _ _ (NaturalLit a) = NaturalLit a+shift _ _ NaturalFold = NaturalFold+shift _ _ NaturalBuild = NaturalBuild+shift _ _ NaturalIsZero = NaturalIsZero+shift _ _ NaturalEven = NaturalEven+shift _ _ NaturalOdd = NaturalOdd+shift d v (NaturalPlus a b) = NaturalPlus a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (NaturalTimes a b) = NaturalTimes a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ Integer = Integer+shift _ _ (IntegerLit a) = IntegerLit a+shift _ _ Double = Double+shift _ _ (DoubleLit a) = DoubleLit a+shift _ _ Text = Text+shift _ _ (TextLit a) = TextLit a+shift d v (TextAppend a b) = TextAppend a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift _ _ List = List+shift d v (ListLit a b) = ListLit a' b'+ where+ a' = shift d v a+ b' = fmap (shift d v) b+shift _ _ ListBuild = ListBuild+shift _ _ ListFold = ListFold+shift _ _ ListLength = ListLength+shift _ _ ListHead = ListHead+shift _ _ ListLast = ListLast+shift _ _ ListIndexed = ListIndexed+shift _ _ ListReverse = ListReverse+shift _ _ Optional = Optional+shift d v (OptionalLit a b) = OptionalLit a' b'+ where+ a' = shift d v a+ b' = fmap (shift d v) b+shift _ _ OptionalFold = OptionalFold+shift d v (Record a) = Record a'+ where+ a' = fmap (shift d v) a+shift d v (RecordLit a) = RecordLit a'+ where+ a' = fmap (shift d v) a+shift d v (Union a) = Union a'+ where+ a' = fmap (shift d v) a+shift d v (UnionLit a b c) = UnionLit a b' c'+ where+ b' = shift d v b+ c' = fmap (shift d v) c+shift d v (Combine a b) = Combine a' b'+ where+ a' = shift d v a+ b' = shift d v b+shift d v (Merge a b c) = Merge a' b' c'+ where+ a' = shift d v a+ b' = shift d v b+ c' = shift d v c+shift d v (Field a b) = Field a' b+ where+ a' = shift d v a+shift d v (Note _ b) = b'+ where+ b' = shift d v b+-- The Dhall compiler enforces that all embedded values are closed expressions+-- and `shift` does nothing to a closed expression+shift _ _ (Embed p) = Embed p++{-| Substitute all occurrences of a variable with an expression++> subst x C B ~ B[x := C]+-}+subst :: Var -> Expr s a -> Expr t a -> Expr s a+subst _ _ (Const a) = Const a+subst (V x n) e (Lam y _A b) = Lam y _A' b'+ where+ _A' = subst (V x n ) e _A+ b' = subst (V x n') (shift 1 (V y 0) e) b+ n' = if x == y then n + 1 else n+subst (V x n) e (Pi y _A _B) = Pi y _A' _B'+ where+ _A' = subst (V x n ) e _A+ _B' = subst (V x n') (shift 1 (V y 0) e) _B+ n' = if x == y then n + 1 else n+subst v e (App f a) = App f' a'+ where+ f' = subst v e f+ a' = subst v e a+subst v e (Var v') = if v == v' then e else Var v'+subst (V x n) e (Let f mt r b) = Let f mt' r' b'+ where+ b' = subst (V x n') (shift 1 (V f 0) e) b+ where+ n' = if x == f then n + 1 else n++ mt' = fmap (subst (V x n) e) mt+ r' = subst (V x n) e r+subst x e (Annot a b) = Annot a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ Bool = Bool+subst _ _ (BoolLit a) = BoolLit a+subst x e (BoolAnd a b) = BoolAnd a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolOr a b) = BoolOr a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolEQ a b) = BoolEQ a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolNE a b) = BoolNE a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (BoolIf a b c) = BoolIf a' b' c'+ where+ a' = subst x e a+ b' = subst x e b+ c' = subst x e c+subst _ _ Natural = Natural+subst _ _ (NaturalLit a) = NaturalLit a+subst _ _ NaturalFold = NaturalFold+subst _ _ NaturalBuild = NaturalBuild+subst _ _ NaturalIsZero = NaturalIsZero+subst _ _ NaturalEven = NaturalEven+subst _ _ NaturalOdd = NaturalOdd+subst x e (NaturalPlus a b) = NaturalPlus a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (NaturalTimes a b) = NaturalTimes a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ Integer = Integer+subst _ _ (IntegerLit a) = IntegerLit a+subst _ _ Double = Double+subst _ _ (DoubleLit a) = DoubleLit a+subst _ _ Text = Text+subst _ _ (TextLit a) = TextLit a+subst x e (TextAppend a b) = TextAppend a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst _ _ List = List+subst x e (ListLit a b) = ListLit a' b'+ where+ a' = subst x e a+ b' = fmap (subst x e) b+subst _ _ ListBuild = ListBuild+subst _ _ ListFold = ListFold+subst _ _ ListLength = ListLength+subst _ _ ListHead = ListHead+subst _ _ ListLast = ListLast+subst _ _ ListIndexed = ListIndexed+subst _ _ ListReverse = ListReverse+subst _ _ Optional = Optional+subst x e (OptionalLit a b) = OptionalLit a' b'+ where+ a' = subst x e a+ b' = fmap (subst x e) b+subst _ _ OptionalFold = OptionalFold+subst x e (Record kts) = Record (fmap (subst x e) kts)+subst x e (RecordLit kvs) = RecordLit (fmap (subst x e) kvs)+subst x e (Union kts) = Union (fmap (subst x e) kts)+subst x e (UnionLit a b kts) = UnionLit a (subst x e b) (fmap (subst x e) kts)+subst x e (Combine a b) = Combine a' b'+ where+ a' = subst x e a+ b' = subst x e b+subst x e (Merge a b c) = Merge a' b' c'+ where+ a' = subst x e a+ b' = subst x e b+ c' = subst x e c+subst x e (Field a b) = Field a' b+ where+ a' = subst x e a+subst x e (Note _ b) = b'+ where+ b' = subst x e b+-- The Dhall compiler enforces that all embedded values are closed expressions+-- and `subst` does nothing to a closed expression+subst _ _ (Embed p) = Embed p++{-| Reduce an expression to its normal form, performing beta reduction++ `normalize` does not type-check the expression. You may want to type-check+ expressions before normalizing them since normalization can convert an+ ill-typed expression into a well-typed expression.++ However, `normalize` will not fail if the expression is ill-typed and will+ leave ill-typed sub-expressions unevaluated.+-}+normalize :: Expr s a -> Expr t a+normalize e = case e of+ Const k -> Const k+ Var v -> Var v+ Lam x _A b -> Lam x _A' b'+ where+ _A' = normalize _A+ b' = normalize b+ Pi x _A _B -> Pi x _A' _B'+ where+ _A' = normalize _A+ _B' = normalize _B+ App f a -> case normalize f of+ Lam x _A b -> normalize b'' -- Beta reduce+ where+ a' = shift 1 (V x 0) a+ b' = subst (V x 0) a' b+ b'' = shift (-1) (V x 0) b'+ f' -> case App f' a' of+ -- fold/build fusion for `List`+ App (App ListBuild _) (App (App ListFold _) e') -> normalize e'+ App (App ListFold _) (App (App ListBuild _) e') -> normalize e'++ -- fold/build fusion for `Natural`+ App NaturalBuild (App NaturalFold e') -> normalize e'+ App NaturalFold (App NaturalBuild e') -> normalize e'++ App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->+ normalize (go n0)+ where+ go !0 = zero+ go !n = App succ' (go (n - 1))+ App NaturalBuild k+ | check -> NaturalLit n+ | otherwise -> App f' a'+ where+ labeled =+ normalize (App (App (App k Natural) "Succ") "Zero")++ n = go 0 labeled+ where+ go !m (App (Var "Succ") e') = go (m + 1) e'+ go !m (Var "Zero") = m+ go !_ _ = internalError text+ check = go labeled+ where+ go (App (Var "Succ") e') = go e'+ go (Var "Zero") = True+ go _ = False+ App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)+ App NaturalEven (NaturalLit n) -> BoolLit (even n)+ App NaturalOdd (NaturalLit n) -> BoolLit (odd n)+ App (App ListBuild t) k+ | check -> ListLit t (buildVector k')+ | otherwise -> App f' a'+ where+ labeled =+ normalize (App (App (App k (App List t)) "Cons") "Nil")++ k' cons nil = go labeled+ where+ go (App (App (Var "Cons") x) e') = cons x (go e')+ go (Var "Nil") = nil+ go _ = internalError text+ check = go labeled+ where+ go (App (App (Var "Cons") _) e') = go e'+ go (Var "Nil") = True+ go _ = False+ App (App (App (App (App ListFold _) (ListLit _ xs)) _) cons) nil ->+ normalize (Data.Vector.foldr cons' nil xs)+ where+ cons' y ys = App (App cons y) ys+ App (App ListLength _) (ListLit _ ys) ->+ NaturalLit (fromIntegral (Data.Vector.length ys))+ App (App ListHead _) (ListLit t ys) ->+ normalize (OptionalLit t (Data.Vector.take 1 ys))+ App (App ListLast _) (ListLit t ys) ->+ normalize (OptionalLit t y)+ where+ y = if Data.Vector.null ys+ then Data.Vector.empty+ else Data.Vector.singleton (Data.Vector.last ys)+ App (App ListIndexed _) (ListLit t xs) ->+ normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))+ where+ t' = Record (Data.Map.fromList kts)+ where+ kts = [ ("index", Natural)+ , ("value", t)+ ]+ adapt (n, x) = RecordLit (Data.Map.fromList kvs)+ where+ kvs = [ ("index", NaturalLit (fromIntegral n))+ , ("value", x)+ ]+ App (App ListReverse _) (ListLit t xs) ->+ normalize (ListLit t (Data.Vector.reverse xs))+ App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->+ normalize (maybe nothing just' (toMaybe xs))+ where+ just' y = App just y+ toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList+ _ -> App f' a'+ where+ a' = normalize a+ Let f _ r b -> normalize b''+ where+ r' = shift 1 (V f 0) r+ b' = subst (V f 0) r' b+ b'' = shift (-1) (V f 0) b'+ Annot x _ -> normalize x+ Bool -> Bool+ BoolLit b -> BoolLit b+ BoolAnd x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn && yn)+ _ -> BoolAnd x' y'+ _ -> BoolAnd x' y'+ where+ x' = normalize x+ y' = normalize y+ BoolOr x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn || yn)+ _ -> BoolOr x' y'+ _ -> BoolOr x' y'+ where+ x' = normalize x+ y' = normalize y+ BoolEQ x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn == yn)+ _ -> BoolEQ x' y'+ _ -> BoolEQ x' y'+ where+ x' = normalize x+ y' = normalize y+ BoolNE x y ->+ case x' of+ BoolLit xn ->+ case y' of+ BoolLit yn -> BoolLit (xn /= yn)+ _ -> BoolNE x' y'+ _ -> BoolNE x' y'+ where+ x' = normalize x+ y' = normalize y+ BoolIf b true false -> case normalize b of+ BoolLit True -> true'+ BoolLit False -> false'+ b' -> BoolIf b' true' false'+ where+ true' = normalize true+ false' = normalize false+ Natural -> Natural+ NaturalLit n -> NaturalLit n+ NaturalFold -> NaturalFold+ NaturalBuild -> NaturalBuild+ NaturalIsZero -> NaturalIsZero+ NaturalEven -> NaturalEven+ NaturalOdd -> NaturalOdd+ NaturalPlus x y ->+ case x' of+ NaturalLit xn ->+ case y' of+ NaturalLit yn -> NaturalLit (xn + yn)+ _ -> NaturalPlus x' y'+ _ -> NaturalPlus x' y'+ where+ x' = normalize x+ y' = normalize y+ NaturalTimes x y ->+ case x' of+ NaturalLit xn ->+ case y' of+ NaturalLit yn -> NaturalLit (xn * yn)+ _ -> NaturalTimes x' y'+ _ -> NaturalTimes x' y'+ where+ x' = normalize x+ y' = normalize y+ Integer -> Integer+ IntegerLit n -> IntegerLit n+ Double -> Double+ DoubleLit n -> DoubleLit n+ Text -> Text+ TextLit t -> TextLit t+ TextAppend x y ->+ case x' of+ TextLit xt ->+ case y' of+ TextLit yt -> TextLit (xt <> yt)+ _ -> TextAppend x' y'+ _ -> TextAppend x' y'+ where+ x' = normalize x+ y' = normalize y+ List -> List+ ListLit t es -> ListLit t' es'+ where+ t' = normalize t+ es' = fmap normalize es+ ListBuild -> ListBuild+ ListFold -> ListFold+ ListLength -> ListLength+ ListHead -> ListHead+ ListLast -> ListLast+ ListIndexed -> ListIndexed+ ListReverse -> ListReverse+ Optional -> Optional+ OptionalLit t es -> OptionalLit t' es'+ where+ t' = normalize t+ es' = fmap normalize es+ OptionalFold -> OptionalFold+ Record kts -> Record kts'+ where+ kts' = fmap normalize kts+ RecordLit kvs -> RecordLit kvs'+ where+ kvs' = fmap normalize kvs+ Union kts -> Union kts'+ where+ kts' = fmap normalize kts+ UnionLit k v kvs -> UnionLit k v' kvs'+ where+ v' = normalize v+ kvs' = fmap normalize kvs+ Combine x y ->+ case x of+ RecordLit kvsX ->+ case y of+ RecordLit kvsY ->+ RecordLit (fmap normalize (Data.Map.union kvsX kvsY))+ _ -> Combine x' y'+ _ -> Combine x' y'+ where+ x' = normalize x+ y' = normalize y+ Merge x y t ->+ case x' of+ RecordLit kvsX ->+ case y' of+ UnionLit kY vY _ ->+ case Data.Map.lookup kY kvsX of+ Just vX -> normalize (App vX vY)+ Nothing -> Merge x' y' t'+ _ -> Merge x' y' t'+ _ -> Merge x' y' t'+ where+ x' = normalize x+ y' = normalize y+ t' = normalize t+ Field r x ->+ case normalize r of+ RecordLit kvs ->+ case Data.Map.lookup x kvs of+ Just v -> normalize v+ Nothing -> Field (RecordLit (fmap normalize kvs)) x+ r' -> Field r' x+ Note _ e' -> normalize e'+ Embed a -> Embed a+ where+ -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of+ -- `normalize`. In theory, this might change a failing repro case into+ -- a successful one, but the risk of that is low enough to not warrant+ -- the `Show` constraint. I care more about proving at the type level+ -- that the @a@ and @s@ type parameters are never used+ e'' = bimap (\_ -> ()) (\_ -> ()) e++ text = "normalize (" <> Data.Text.pack (show e'') <> ")"++internalError :: Data.Text.Text -> forall b . b+internalError text = error (Data.Text.unpack [NeatInterpolation.text|+Error: Compiler bug++Explanation: This error message means that there is a bug in the Dhall compiler.+You didn't do anything wrong, but if you would like to see this problem fixed+then you should report the bug at:++https://github.com/Gabriel439/Haskell-Dhall-Library/issues++Please include the following text in your bug report:++```+$text+```+|])++buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a+buildVector f = Data.Vector.reverse (Data.Vector.create (do+ let cons a st = do+ (len, cap, mv) <- st+ if len < cap+ then do+ Data.Vector.Mutable.write mv len a+ return (len + 1, cap, mv)+ else do+ let cap' = 2 * cap+ mv' <- Data.Vector.Mutable.unsafeGrow mv cap'+ Data.Vector.Mutable.write mv' len a+ return (len + 1, cap', mv')+ let nil = do+ mv <- Data.Vector.Mutable.unsafeNew 1+ return (0, 1, mv)+ (len, _, mv) <- f cons nil+ return (Data.Vector.Mutable.slice 0 len mv) ))
+ src/Dhall/Import.hs view
@@ -0,0 +1,486 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# OPTIONS_GHC -Wall #-}++{-| Dhall lets you import external expressions located either in local files or+ hosted on network endpoints.++ To import a local file as an expression, just insert the path to the file,+ prepending a @./@ if the path is relative to the current directory. For+ example, suppose we had the following three local files:++ > -- id+ > \(a : *) -> \(x : a) -> x++ > -- Bool+ > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool++ > -- True+ > \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True++ You could then reference them within a Dhall expression using this syntax:++ > ./id ./Bool ./True++ ... which would embed their expressions directly within the syntax tree:++ > -- ... expands out to:+ > (\(a : *) -> \(x : a) -> x)+ > (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True)+ > (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True)++ ... and which normalizes to:++ > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++ Imported expressions may contain imports of their own, too, which will+ continue to be resolved. However, Dhall will prevent cyclic imports. For+ example, if you had these two files:++ > -- foo+ > ./bar++ > -- bar+ > ./foo++ ... Dhall would throw the following exception if you tried to import @foo@:++ > dhall: + > ⤷ ./foo+ > ⤷ ./bar+ > Cyclic import: ./foo++ You can also import expressions hosted on network endpoints. Just use the+ URL++ > http://host[:port]/path++ The compiler expects the downloaded expressions to be in the same format + as local files, specifically UTF8-encoded source code text.++ For example, if our @id@ expression were hosted at @http://example.com/id@,+ then we would embed the expression within our code using:++ > http://example.com/id++ You can also reuse directory names as expressions. If you provide a path+ to a local or remote directory then the compiler will look for a file named+ @\@@ within that directory and use that file to represent the directory.+-}++module Dhall.Import (+ -- * Import+ load+ , exprFromFile+ , exprFromURL+ , Cycle(..)+ , ReferentiallyOpaque(..)+ , Imported(..)+ ) where++import Control.Exception+ (Exception, IOException, SomeException, catch, onException, throwIO)+import Control.Monad (join)+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Trans.State.Strict (StateT)+import Data.ByteString.Lazy (ByteString)+import Data.Map.Strict (Map)+import Data.Monoid ((<>))+import Data.Text.Buildable (build)+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+#if MIN_VERSION_base(4,8,0)+#else+import Data.Traversable (traverse)+#endif+import Data.Typeable (Typeable)+import Filesystem.Path ((</>), FilePath)+import Lens.Micro (Lens')+import Lens.Micro.Mtl (zoom)+import Dhall.Core (Expr, Path(..))+import Dhall.Parser (Parser(..), ParseError(..), Src)+import Dhall.TypeCheck (X(..))+import Network.HTTP.Client (HttpException(..), Manager)+import Prelude hiding (FilePath)+import Text.Trifecta (Result(..))+import Text.Trifecta.Delta (Delta(..))++import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.ByteString.Lazy+import qualified Data.Foldable as Foldable+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import qualified Data.Text+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Text.Lazy.Encoding+import qualified Dhall.Parser+import qualified Dhall.TypeCheck+import qualified Filesystem.Path.CurrentOS+import qualified NeatInterpolation+import qualified Network.HTTP.Client as HTTP+import qualified Network.HTTP.Client.TLS as HTTP+import qualified Filesystem.Path.CurrentOS as Filesystem+import qualified Text.Parser.Combinators+import qualified Text.Parser.Token+import qualified Text.Trifecta++builderToString :: Builder -> String+builderToString = Text.unpack . Builder.toLazyText++-- | An import failed because of a cycle in the import graph+newtype Cycle = Cycle+ { cyclicImport :: Path -- ^ The offending cyclic import+ }+ deriving (Typeable)++instance Exception Cycle++instance Show Cycle where+ show (Cycle path) = "Cyclic import: " ++ builderToString (build path)++{-| Dhall tries to ensure that all expressions hosted on network endpoints are+ weakly referentially transparent, meaning roughly that any two clients will+ compile the exact same result given the same URL.++ To be precise, a strong interpretaton of referential transparency means that+ if you compiled a URL you could replace the expression hosted at that URL+ with the compiled result. Let's term this \"static linking\". Dhall (very+ intentionally) does not satisfy this stronger interpretation of referential+ transparency since \"statically linking\" an expression (i.e. permanently+ resolving all imports) means that the expression will no longer update if+ its dependencies change.++ In general, either interpretation of referential transparency is not+ enforceable in a networked context since one can easily violate referential+ transparency with a custom DNS, but Dhall can still try to guard against+ common unintentional violations. To do this, Dhall enforces that a+ non-local import may not reference a local import.++ Local imports are defined as:++ * A file++ * A URL with a host of @localhost@ or @127.0.0.1@++ All other imports are defined to be non-local+-}+newtype ReferentiallyOpaque = ReferentiallyOpaque+ { opaqueImport :: Path -- ^ The offending opaque import+ } deriving (Typeable)++instance Exception ReferentiallyOpaque++instance Show ReferentiallyOpaque where+ show (ReferentiallyOpaque path) =+ "Referentially opaque import: " ++ builderToString (build path)++-- | Extend another exception with the current import stack+data Imported e = Imported+ { importStack :: [Path] -- ^ Imports resolved so far, in reverse order+ , nested :: e -- ^ The nested exception+ } deriving (Typeable)++instance Exception e => Exception (Imported e)++instance Show e => Show (Imported e) where+ show (Imported paths e) =+ unlines (map (\(n, path) -> take (2 * n) (repeat ' ') ++ "↳ " ++ builderToString (build path)) paths')+ ++ "\n"+ ++ show e+ where+ -- Canonicalize all paths+ paths' = zip [0..] (drop 1 (reverse (canonicalizeAll paths)))++newtype PrettyHttpException = PrettyHttpException HttpException+ deriving (Typeable)++instance Exception PrettyHttpException++instance Show PrettyHttpException where+ show (PrettyHttpException (FailedConnectionException2 _ _ _ _)) =+ "\ESC[1;31mError\ESC[0m: Connection timed out\n"+ show (PrettyHttpException e) = show e++data Status = Status+ { _stack :: [Path]+ , _cache :: Map Path (Expr Src X)+ , _manager :: Maybe Manager+ }++canonicalizeAll :: [Path] -> [Path]+canonicalizeAll = map canonicalize . List.tails++stack :: Lens' Status [Path]+stack k s = fmap (\x -> s { _stack = x }) (k (_stack s))++cache :: Lens' Status (Map Path (Expr Src X))+cache k s = fmap (\x -> s { _cache = x }) (k (_cache s))++manager :: Lens' Status (Maybe Manager)+manager k s = fmap (\x -> s { _manager = x }) (k (_manager s))++needManager :: StateT Status IO Manager+needManager = do+ x <- zoom manager State.get+ case x of+ Just m -> return m+ Nothing -> do+ let settings = HTTP.tlsManagerSettings+ { HTTP.managerResponseTimeout = Just 1000000 } -- 1 second+ m <- liftIO (HTTP.newManager settings)+ zoom manager (State.put (Just m))+ return m++{-| This function computes the current path by taking the last absolute path+ (either an absolute `FilePath` or `URL`) and combining it with all following+ relative paths++ For example, if the file `./foo/bar` imports `./baz`, that will resolve to+ `./foo/baz`. Relative imports are relative to a file's parent directory.+ This also works for URLs, too.++ This code is full of all sorts of edge cases so it wouldn't surprise me at+ all if you find something broken in here. Most of the ugliness is due to:++ * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only+ if you navigate to any downstream relative paths+ * Removing spurious @.@s and @..@s from the path++ Also, there are way too many `reverse`s in the URL-handling cod For now I+ don't mind, but if were to really do this correctly we'd store the URLs as+ `Text` for O(1) access to the end of the string. The only reason we use+ `String` at all is for consistency with the @http-client@ library.+-}+canonicalize :: [Path] -> Path+canonicalize [] = File "."+canonicalize (File file0:paths0) =+ if Filesystem.relative file0+ then go file0 paths0+ else File (clean file0)+ where+ go currPath [] = File (clean currPath)+ go currPath (URL url0:_ ) = combine prefix suffix+ where+ prefix = parentURL (removeAtFromURL url0)++ suffix = clean currPath++ -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still+ -- need to manually handle @.@/@..@'s at the beginning of the path+ combine url path = case Filesystem.stripPrefix ".." path of+ Just path' -> combine url' path'+ where+ url' = parentURL (removeAtFromURL url)+ Nothing -> case Filesystem.stripPrefix "." path of+ Just path' -> combine url path'+ Nothing -> + -- This `last` is safe because the lexer constrains all+ -- URLs to be non-empty. I couldn't find a simple and safe+ -- equivalent in the `text` API+ case Text.last url of+ '/' -> URL (url <> path')+ _ -> URL (url <> "/" <> path')+ where+ path' = Text.fromStrict (case Filesystem.toText path of+ Left txt -> txt+ Right txt -> txt )+ go currPath (File file:paths) =+ if Filesystem.relative file+ then go file' paths+ else File (clean file')+ where+ file' = Filesystem.parent (removeAtFromFile file) </> currPath+canonicalize (URL path:_) = URL path++parentURL :: Text -> Text+parentURL = Text.dropWhileEnd (/= '/')++removeAtFromURL:: Text -> Text+removeAtFromURL url+ | Text.isSuffixOf "/@" url = Text.dropEnd 2 url+ | Text.isSuffixOf "/" url = Text.dropEnd 1 url+ | otherwise = url++removeAtFromFile :: FilePath -> FilePath+removeAtFromFile file =+ if Filesystem.filename file == "@"+ then Filesystem.parent file+ else file++-- | Remove all @.@'s and @..@'s in the path+clean :: FilePath -> FilePath+clean = strip . Filesystem.collapse+ where+ strip p = case Filesystem.stripPrefix "." p of+ Nothing -> p+ Just p' -> p'++-- | Parse an expression from a `FilePath` containing a Dhall program+exprFromFile :: FilePath -> IO (Expr Src Path)+exprFromFile path = do+ let string = Filesystem.Path.CurrentOS.encodeString path++ -- 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))+ handler e = do+ let string' = Filesystem.Path.CurrentOS.encodeString (path </> "@")++ -- If the fallback fails, reuse the original exception to avoid user+ -- confusion+ Text.Trifecta.parseFromFileEx parser string' `onException` throwIO e++ x <- Text.Trifecta.parseFromFileEx parser string `catch` handler+ case x of+ Failure errInfo -> throwIO (ParseError (Text.Trifecta._errDoc errInfo))+ Success expr -> return expr+ where+ parser = do+ Text.Parser.Token.whiteSpace+ r <- unParser Dhall.Parser.exprA+ Text.Parser.Combinators.eof+ return r++exprFromURL :: Manager -> Text -> IO (Expr Src Path)+exprFromURL m url = do+ request <- HTTP.parseUrlThrow (Text.unpack url)++ let handler :: HTTP.HttpException -> IO (HTTP.Response ByteString)+ handler err@(HTTP.StatusCodeException _ _ _) = do+ let request' = request { HTTP.path = HTTP.path request <> "/@" }+ -- If the fallback fails, reuse the original exception to avoid user+ -- confusion+ HTTP.httpLbs request' m `onException` throwIO (PrettyHttpException err)+ handler err = throwIO (PrettyHttpException err)+ response <- HTTP.httpLbs request m `catch` handler++ let bytes = HTTP.responseBody response++ text <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes of+ Left err -> throwIO err+ Right text -> return text++ 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+ -- 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)++ request' <- HTTP.parseUrlThrow (Text.unpack url)++ let request'' = request' { HTTP.path = HTTP.path request' <> "/@" }+ response' <- HTTP.httpLbs request'' m `onException` throwIO err'++ let bytes' = HTTP.responseBody response'++ text' <- case Data.Text.Lazy.Encoding.decodeUtf8' bytes' of+ Left _ -> throwIO err'+ Right text' -> return text'++ case Text.Trifecta.parseString parser delta (Text.unpack text') of+ Failure _ -> throwIO err'+ Success expr -> return expr+ Success expr -> return expr+ where+ parser = do+ Text.Parser.Token.whiteSpace+ r <- unParser Dhall.Parser.exprA+ Text.Parser.Combinators.eof+ return r++{-| Load a `Path` as a \"dynamic\" expression (without resolving any imports)++ This also returns the true final path (i.e. explicit "/@" at the end for+ directories)+-}+loadDynamic :: Path -> StateT Status IO (Expr Src Path)+loadDynamic p = do+ paths <- zoom stack State.get++ let handler :: SomeException -> IO (Expr Src Path)+ handler e = throwIO (Imported (p:paths) e)+ case canonicalize (p:paths) of+ File file -> do+ liftIO (exprFromFile file `catch` handler)+ URL url -> do+ m <- needManager+ liftIO (exprFromURL m url `catch` handler)++-- | Load a `Path` as a \"static\" expression (with all imports resolved)+loadStatic :: Path -> StateT Status IO (Expr Src X)+loadStatic path = do+ paths <- zoom stack State.get++ let local (URL url) = case HTTP.parseUrlThrow (Text.unpack url) of+ Nothing -> False+ Just request -> case HTTP.host request of+ "127.0.0.1" -> True+ "localhost" -> True+ _ -> False+ local (File _) = True++ let parent = canonicalize paths+ let here = canonicalize (path:paths)++ if local here && not (local parent)+ then liftIO (throwIO (Imported paths (ReferentiallyOpaque path)))+ else return ()++ (expr, cached) <- if here `elem` canonicalizeAll paths+ then liftIO (throwIO (Imported paths (Cycle path)))+ else do+ m <- zoom cache State.get+ case Map.lookup here m of+ Just expr -> return (expr, True)+ Nothing -> do+ expr' <- loadDynamic path+ expr'' <- case traverse (\_ -> Nothing) expr' of+ -- No imports left+ Just expr -> do+ zoom cache (State.put $! Map.insert here expr m)+ return expr+ -- Some imports left, so recurse+ Nothing -> do+ let paths' = path:paths+ zoom stack (State.put paths')+ expr'' <- fmap join (traverse loadStatic expr')+ zoom stack (State.put paths)+ return expr''+ return (expr'', False)++ -- Type-check expressions here for two separate reasons:+ --+ -- * to verify that they are closed+ -- * to catch type errors as early in the import process as possible+ --+ -- There is no need to check expressions that have been cached, since they+ -- have already been checked+ if cached+ then return ()+ else case Dhall.TypeCheck.typeOf expr of+ Left err -> liftIO (throwIO (Imported (path:paths) err))+ Right _ -> return ()++ return expr++{-| Resolve all imports within an expression++ By default the starting path is the current directory, but you can override+ the starting path with a file if you read in the expression from that file+-}+load+ :: Maybe Path+ -- ^ Starting path+ -> Expr Src Path+ -- ^ Expression to resolve+ -> IO (Expr Src X)+load here expr = State.evalStateT (fmap join (traverse loadStatic expr)) status+ where+ status = Status (Foldable.toList here) Map.empty Nothing
+ src/Dhall/Parser.hs view
@@ -0,0 +1,708 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}++module Dhall.Parser (+ -- * Utilities+ exprFromText++ -- * Parsers+ , exprA++ -- * Types+ , Src(..)+ , ParseError(..)+ , Parser(..)+ ) where++import Control.Applicative (Alternative(..), optional)+import Control.Exception (Exception)+import Control.Monad (MonadPlus)+import Data.ByteString (ByteString)+import Data.Map (Map)+import Data.Monoid ((<>))+import Data.Sequence (ViewL(..))+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Typeable (Typeable)+import Data.Vector (Vector)+import Dhall.Core (Const(..), Expr(..), Path(..), Var(..))+import Filesystem.Path (FilePath)+import Prelude hiding (FilePath, const, pi)+import Text.PrettyPrint.ANSI.Leijen (Doc)+import Text.Parser.Combinators (choice, try, (<?>))+import Text.Parser.Expression (Assoc(..), Operator(..))+import Text.Parser.Token (IdentifierStyle(..), TokenParsing(..))+import Text.Parser.Token.Highlight (Highlight(..))+import Text.Parser.Token.Style (CommentStyle(..))+import Text.Trifecta+ (CharParsing, DeltaParsing, MarkParsing, Parsing, Result(..))+import Text.Trifecta.Delta (Delta)++import qualified Data.Char+import qualified Data.HashSet+import qualified Data.Map+import qualified Data.ByteString+import qualified Data.ByteString.Lazy+import qualified Data.List+import qualified Data.Sequence+import qualified Data.Text+import qualified Data.Text.Lazy+import qualified Data.Text.Lazy.Encoding+import qualified Data.Vector+import qualified Dhall.Core+import qualified Filesystem.Path.CurrentOS+import qualified Text.Parser.Char+import qualified Text.Parser.Combinators+import qualified Text.Parser.Expression+import qualified Text.Parser.Token+import qualified Text.Parser.Token.Style+import qualified Text.PrettyPrint.ANSI.Leijen+import qualified Text.Trifecta+import qualified Text.Trifecta.Combinators+import qualified Text.Trifecta.Delta++data Src = Src Delta Delta ByteString deriving (Show)++instance Buildable Src where+ build (Src begin _ bytes) =+ build text <> "\n"+ <> "\n"+ <> build (show (Text.PrettyPrint.ANSI.Leijen.pretty begin))+ <> "\n"+ where+ bytes' = Data.ByteString.Lazy.fromStrict bytes++ text = Data.Text.Lazy.strip (Data.Text.Lazy.Encoding.decodeUtf8 bytes')++newtype Parser a = Parser { unParser :: Text.Trifecta.Parser a }+ deriving+ ( Functor+ , Applicative+ , Monad+ , Alternative+ , MonadPlus+ , Parsing+ , CharParsing+ , DeltaParsing+ , MarkParsing Delta+ )++instance TokenParsing Parser where+ someSpace =+ Text.Parser.Token.Style.buildSomeSpaceParser + (Parser someSpace)+ Text.Parser.Token.Style.haskellCommentStyle++ nesting (Parser m) = Parser (nesting m)++ semi = Parser semi++ highlight h (Parser m) = Parser (highlight h m)++ token parser = do+ r <- parser+ Text.Parser.Token.whiteSpace+ return r++identifierStyle :: IdentifierStyle Parser+identifierStyle = IdentifierStyle+ { _styleName = "dhall"+ , _styleStart =+ Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ "_")+ , _styleLetter =+ Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_/")+ , _styleReserved = Data.HashSet.fromList+ [ "let"+ , "in"+ , "Type"+ , "Kind"+ , "forall"+ , "Bool"+ , "True"+ , "False"+ , "merge"+ , "if"+ , "then"+ , "else"+ , "Natural"+ , "Natural/fold"+ , "Natural/build"+ , "Natural/isZero"+ , "Natural/even"+ , "Natural/odd"+ , "Integer"+ , "Double"+ , "Text"+ , "List"+ , "List/build"+ , "List/fold"+ , "List/length"+ , "List/head"+ , "List/last"+ , "List/indexed"+ , "List/reverse"+ , "Optional"+ , "Optional/fold"+ ]+ , _styleHighlight = Identifier+ , _styleReservedHighlight = ReservedIdentifier+ }++noted :: Parser (Expr Src a) -> Parser (Expr Src a)+noted parser = do+ before <- Text.Trifecta.position+ (expr, bytes) <- Text.Trifecta.slicedWith (,) parser+ after <- Text.Trifecta.position+ return (Note (Src before after bytes) expr)++toMap :: [(Text, a)] -> Parser (Map Text a)+toMap kvs = do+ let adapt (k, v) = (k, pure v)+ let m = Data.Map.fromListWith (<|>) (fmap adapt kvs)+ let action k vs = case Data.Sequence.viewl vs of+ EmptyL -> empty+ v :< vs' ->+ if null vs'+ then pure v+ else+ Text.Parser.Combinators.unexpected+ ("duplicate field: " ++ Data.Text.Lazy.unpack k)+ Data.Map.traverseWithKey action m++reserve :: String -> Parser ()+reserve string = do+ _ <- Text.Parser.Token.reserve identifierStyle string+ return ()++symbol :: String -> Parser ()+symbol string = do+ _ <- Text.Parser.Token.symbol string+ return ()++lambda :: Parser ()+lambda = symbol "\\" <|> symbol "λ"++pi :: Parser ()+pi = reserve "forall" <|> reserve "∀"++arrow :: Parser ()+arrow = symbol "->" <|> symbol "→"++combine :: Parser ()+combine = symbol "/\\" <|> symbol "∧"++label :: Parser Text+label = Text.Parser.Token.ident identifierStyle <?> "label"++exprA :: Parser (Expr Src Path)+exprA = do+ a <- exprB++ let exprA0 = do+ symbol ":"+ b <- exprA+ return (Annot a b)++ let exprA1 = pure a++ exprA0 <|> exprA1++exprB :: Parser (Expr Src Path)+exprB = choice+ [ noted exprB0+ , noted exprB1+ , noted exprB3+ , noted exprB5+ , noted exprB6+ , noted exprB7+ , noted (try exprB2)+ , exprB8+ ]+ where+ exprB0 = do+ lambda+ symbol "("+ a <- label+ symbol ":"+ b <- exprA+ symbol ")"+ arrow+ c <- exprB+ return (Lam a b c)++ exprB1 = do+ reserve "if"+ a <- exprA+ reserve "then"+ b <- exprB+ reserve "else"+ c <- exprC+ return (BoolIf a b c)++ exprB2 = do+ a <- exprC+ arrow+ b <- exprB+ return (Pi "_" a b)++ exprB3 = do+ pi+ symbol "("+ a <- label+ symbol ":"+ b <- exprA+ symbol ")"+ arrow+ c <- exprB+ return (Pi a b c)++ exprB5 = do+ reserve "let"+ a <- label+ b <- optional (do+ symbol ":"+ exprA )+ symbol "="+ c <- exprA+ reserve "in"+ d <- exprB+ return (Let a b c d)++ exprB6 = do+ symbol "["+ a <- elems+ symbol "]"+ symbol ":"+ b <- listLike+ c <- exprE+ return (b c (Data.Vector.fromList a))++ exprB7 = do+ reserve "merge"+ a <- exprE+ b <- exprE+ symbol ":"+ c <- exprD+ return (Merge a b c)++ exprB8 = exprC++listLike :: Parser (Expr Src Path -> Vector (Expr Src Path) -> Expr Src Path)+listLike =+ ( listLike0+ <|> listLike1+ )+ where+ listLike0 = do+ reserve "List"+ return ListLit++ listLike1 = do+ reserve "Optional"+ return OptionalLit++-- TODO: Add `noted` in the right places here+exprC :: Parser (Expr Src Path)+exprC = expressionParser+ where+ expressionParser = Text.Parser.Expression.buildExpressionParser+ [ [ operator BoolAnd (symbol "&&")+ , operator NaturalTimes (symbol "*" )+ , operator Combine combine+ ]+ , [ operator BoolOr (symbol "||")+ , operator TextAppend (symbol "++")+ , operator NaturalPlus (symbol "+" )+ ]+ , [ operator BoolEQ (symbol "==")+ , operator BoolNE (symbol "/=")+ ]+ ]+ exprD++ operator op parser = Infix (do parser; return op) AssocRight++-- We can't use left-recursion to define `exprD` otherwise the parser will+-- loop infinitely. However, I'd still like to use left-recursion in the+-- definition because left recursion greatly simplifies the use of `noted`. The+-- work-around is to parse in two phases:+--+-- * First, parse to count how many arguments the function is applied to+-- * Second, restart the parse using left recursion bounded by the number of+-- arguments+exprD :: Parser (Expr Src Path)+exprD = do+ es <- some (noted exprE)+ let app nL@(Note (Src before _ bytesL) eL) nR@(Note (Src _ after bytesR) eR) =+ Note (Src before after (bytesL <> bytesR)) (App nL nR)+ app _ _ = Dhall.Core.internalError+ ("exprD: foldl1 app (" <> Data.Text.pack (show es) <> ")")+ return (Data.List.foldl1 app es)++exprE :: Parser (Expr Src Path)+exprE = noted (do+ a <- exprF+ b <- many (do+ symbol "."+ label )+ return (Data.List.foldl Field a b) )++exprF :: Parser (Expr Src Path)+exprF = choice+ [ noted exprF01+ , noted exprF03+ , noted exprF04+ , noted exprF05+ , noted exprF06+ , noted exprF07+ , noted exprF12+ , noted exprF13+ , noted exprF14+ , noted exprF15+ , noted exprF16+ , noted exprF17+ , noted exprF18+ , noted exprF20+ , noted exprF19+ , noted exprF21+ , noted exprF22+ , noted (try exprF25)+ , noted exprF23+ , noted (try exprF26)+ , noted exprF24+ , noted exprF27+ , noted (try exprF28)+ , noted exprF29+ , noted (try exprF30)+ , noted exprF31+ , noted exprF32+ , noted exprF02+ , noted exprF08+ , noted exprF09+ , noted exprF10+ , noted exprF11+ , noted exprF00+ , exprF33+ ]+ where+ exprF00 = do+ a <- var+ return (Var a)++ exprF01 = do+ a <- const+ return (Const a)++ exprF02 = do+ reserve "Natural"+ return Natural++ exprF03 = do+ reserve "Natural/fold"+ return NaturalFold++ exprF04 = do+ reserve "Natural/build"+ return NaturalBuild++ exprF05 = do+ reserve "Natural/isZero"+ return NaturalIsZero++ exprF06 = do+ reserve "Natural/even"+ return NaturalEven++ exprF07 = do+ reserve "Natural/odd"+ return NaturalOdd++ exprF08 = do+ reserve "Integer"+ return Integer++ exprF09 = do+ reserve "Double"+ return Double++ exprF10 = do+ reserve "Text"+ return Text++ exprF11 = do+ reserve "List"+ return List++ exprF12 = do+ reserve "List/build"+ return ListBuild++ exprF13 = do+ reserve "List/fold"+ return ListFold++ exprF14 = do+ reserve "List/length"+ return ListLength++ exprF15 = do+ reserve "List/head"+ return ListHead++ exprF16 = do+ reserve "List/last"+ return ListLast++ exprF17 = do+ reserve "List/indexed"+ return ListIndexed++ exprF18 = do+ reserve "List/reverse"+ return ListReverse++ exprF19 = do+ reserve "Optional"+ return Optional++ exprF20 = do+ reserve "Optional/fold"+ return OptionalFold++ exprF21 = do+ reserve "Bool"+ return Bool++ exprF22 = do+ reserve "True"+ return (BoolLit True)++ exprF23 = do+ reserve "False"+ return (BoolLit False)++ exprF24 = do+ a <- Text.Parser.Token.natural+ return (IntegerLit a)++ exprF25 = do+ Text.Parser.Char.char '+'+ a <- Text.Parser.Token.natural+ return (NaturalLit (fromIntegral a))++ exprF26 = do+ a <- Text.Parser.Token.double+ return (DoubleLit a)++ exprF27 = do+ a <- Text.Parser.Token.stringLiteral+ return (TextLit a)++ exprF28 = record++ exprF29 = recordLit++ exprF30 = union++ exprF31 = unionLit++ exprF32 = do+ a <- import_+ return (Embed a)++ exprF33 = do+ symbol "("+ a <- exprA+ symbol ")"+ return a++const :: Parser Const+const = const0+ <|> const1+ where+ const0 = do+ reserve "Type"+ return Type++ const1 = do+ reserve "Kind"+ return Kind++var :: Parser Var+var = do+ a <- label+ m <- optional (do+ symbol "@"+ Text.Parser.Token.natural )+ let b = case m of+ Just b -> b+ Nothing -> 0+ return (V a b)++elems :: Parser [Expr Src Path]+elems = Text.Parser.Combinators.sepBy exprA (symbol ",")++recordLit :: Parser (Expr Src Path)+recordLit =+ recordLit0+ <|> recordLit1+ where+ recordLit0 = do+ symbol "{=}"+ return (RecordLit (Data.Map.fromList []))++ recordLit1 = do+ symbol "{"+ a <- fieldValues+ b <- toMap a+ symbol "}"+ return (RecordLit b)++fieldValues :: Parser [(Text, Expr Src Path)]+fieldValues =+ Text.Parser.Combinators.sepBy1 fieldValue (symbol ",")++fieldValue :: Parser (Text, Expr Src Path)+fieldValue = do+ a <- label+ symbol "="+ b <- exprA+ return (a, b)++record :: Parser (Expr Src Path)+record = do+ symbol "{"+ a <- fieldTypes+ b <- toMap a+ symbol "}"+ return (Record b)++fieldTypes :: Parser [(Text, Expr Src Path)]+fieldTypes =+ Text.Parser.Combinators.sepBy fieldType (symbol ",")++fieldType :: Parser (Text, Expr Src Path)+fieldType = do+ a <- label+ symbol ":"+ b <- exprA+ return (a, b)++union :: Parser (Expr Src Path)+union = do+ symbol "<"+ a <- alternativeTypes+ b <- toMap a+ symbol ">"+ return (Union b)++alternativeTypes :: Parser [(Text, Expr Src Path)]+alternativeTypes =+ Text.Parser.Combinators.sepBy alternativeType (symbol "|")++alternativeType :: Parser (Text, Expr Src Path)+alternativeType = do+ a <- label+ symbol ":"+ b <- exprA+ return (a, b)++unionLit :: Parser (Expr Src Path)+unionLit =+ try unionLit0+ <|> unionLit1+ where+ unionLit0 = do+ symbol "<"+ a <- label+ symbol "="+ b <- exprA+ symbol ">"+ return (UnionLit a b Data.Map.empty)++ unionLit1 = do+ symbol "<"+ a <- label+ symbol "="+ b <- exprA+ symbol "|"+ c <- alternativeTypes+ d <- toMap c+ symbol ">"+ return (UnionLit a b d)++import_ :: Parser Path+import_ = do+ a <- import0 <|> import1+ Text.Parser.Token.whiteSpace+ return a+ where+ import0 = do+ a <- file+ return (File a)++ import1 = do+ a <- url+ return (URL a)++file :: Parser FilePath+file = try (token file0)+ <|> token file1+ <|> token file2+ where+ file0 = do+ a <- Text.Parser.Char.string "/"+ b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+ case b of+ '\\':_ -> empty -- So that "/\" parses as the operator and not a path+ _ -> return ()+ return (Filesystem.Path.CurrentOS.decodeString (a <> b))++ file1 = do+ a <- Text.Parser.Char.string "./"+ b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+ return (Filesystem.Path.CurrentOS.decodeString (a <> b))++ file2 = do+ a <- Text.Parser.Char.string "../"+ b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+ return (Filesystem.Path.CurrentOS.decodeString (a <> b))++url :: Parser Text+url = try url0+ <|> url1+ where+ url0 = do+ a <- Text.Parser.Char.string "https://"+ b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+ return (Data.Text.Lazy.pack (a <> b))++ url1 = do+ a <- Text.Parser.Char.string "http://"+ b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+ return (Data.Text.Lazy.pack (a <> b))++-- | A parsing error+newtype ParseError = ParseError Doc deriving (Typeable)++instance Show ParseError where+ show (ParseError doc) = show doc++instance Exception ParseError++-- | Parse an expression from `Text` containing a Dhall program+exprFromText :: Delta -> Text -> Either ParseError (Expr Src Path)+exprFromText delta text = case result of+ Success r -> Right r+ Failure errInfo -> Left (ParseError (Text.Trifecta._errDoc errInfo))+ where+ string = Data.Text.Lazy.unpack text++ parser = unParser (do+ Text.Parser.Token.whiteSpace+ r <- exprA+ Text.Parser.Combinators.eof+ return r )++ result = Text.Trifecta.parseString parser delta string
+ src/Dhall/TypeCheck.hs view
@@ -0,0 +1,2869 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# OPTIONS_GHC -Wall #-}++module Dhall.TypeCheck (+ -- * Type-checking+ typeWith+ , typeOf++ -- * Types+ , X(..)+ , TypeError(..)+ , DetailedTypeError(..)+ , TypeMessage(..)+ ) where++import Control.Exception (Exception)+import Data.Foldable (forM_)+import Data.Monoid ((<>))+import Data.Set (Set)+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (Builder)+import Data.Typeable (Typeable)+import Dhall.Core (Const(..), Expr(..), Var(..))+import Dhall.Context (Context)++import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Map+import qualified Data.Set+import qualified Data.Text+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Vector+import qualified Dhall.Context+import qualified Dhall.Core+import qualified NeatInterpolation++axiom :: Const -> Either (TypeError s) Const+axiom Type = return Kind+axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped)++rule :: Const -> Const -> Either () Const+rule Type Kind = Left ()+rule Type Type = return Type+rule Kind Kind = return Kind+rule Kind Type = return Type++match :: Var -> Var -> [(Text, Text)] -> Bool+match (V xL nL) (V xR nR) [] =+ xL == xR && nL == nR+match (V xL 0 ) (V xR 0 ) ((xL', xR'):_ )+ | xL == xL' && xR == xR' = True+match (V xL nL) (V xR nR) ((xL', xR'):xs) =+ match (V xL nL') (V xR nR') xs+ where+ nL' = if xL == xL' then nL - 1 else nL+ nR' = if xR == xR' then nR - 1 else nR++propEqual :: Expr s X -> Expr t X -> Bool+propEqual eL0 eR0 =+ State.evalState+ (go (Dhall.Core.normalize eL0) (Dhall.Core.normalize eR0))+ []+ where+ go (Const Type) (Const Type) = return True+ go (Const Kind) (Const Kind) = return True+ go (Var vL) (Var vR) = do+ ctx <- State.get+ return (match vL vR ctx)+ go (Pi xL tL bL) (Pi xR tR bR) = do+ ctx <- State.get+ eq1 <- go tL tR+ if eq1+ then do+ State.put ((xL, xR):ctx)+ eq2 <- go bL bR+ State.put ctx+ return eq2+ else return False+ go (App fL aL) (App fR aR) = do+ b1 <- go fL fR+ if b1 then go aL aR else return False+ go Bool Bool = return True+ go Natural Natural = return True+ go Integer Integer = return True+ go Double Double = return True+ go Text Text = return True+ go List List = return True+ go Optional Optional = return True+ go (Record ktsL0) (Record ktsR0) = do+ let loop ((kL, tL):ktsL) ((kR, tR):ktsR)+ | kL == kR = do+ b <- go tL tR+ if b+ then loop ktsL ktsR+ else return False+ loop [] [] = return True+ loop _ _ = return False+ loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)+ go (Union ktsL0) (Union ktsR0) = do+ let loop ((kL, tL):ktsL) ((kR, tR):ktsR)+ | kL == kR = do+ b <- go tL tR+ if b+ then loop ktsL ktsR+ else return False+ loop [] [] = return True+ loop _ _ = return False+ loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)+ go _ _ = return False++{-| Type-check an expression and return the expression's type if type-checking+ suceeds or an error if type-checking fails++ `typeWith` does not necessarily normalize the type since full normalization+ is not necessary for just type-checking. If you actually care about the+ returned type then you may want to `normalize` it afterwards.+-}+typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X)+typeWith _ (Const c ) = do+ fmap Const (axiom c)+typeWith ctx e@(Var (V x n) ) = do+ case Dhall.Context.lookup x n ctx of+ Nothing -> Left (TypeError ctx e UnboundVariable)+ Just a -> return a+typeWith ctx (Lam x _A b ) = do+ let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx)+ _B <- typeWith ctx' b+ let p = Pi x _A _B+ _t <- typeWith ctx p+ return p+typeWith ctx e@(Pi x _A _B ) = do+ tA <- fmap Dhall.Core.normalize (typeWith ctx _A)+ kA <- case tA of+ Const k -> return k+ _ -> Left (TypeError ctx e (InvalidInputType _A))++ let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx)+ tB <- fmap Dhall.Core.normalize (typeWith ctx' _B)+ kB <- case tB of+ Const k -> return k+ _ -> Left (TypeError ctx' e (InvalidOutputType _B))++ case rule kA kB of+ Left () -> Left (TypeError ctx e (NoDependentTypes _A _B))+ Right k -> Right (Const k)+typeWith ctx e@(App f a ) = do+ tf <- fmap Dhall.Core.normalize (typeWith ctx f)+ (x, _A, _B) <- case tf of+ Pi x _A _B -> return (x, _A, _B)+ _ -> Left (TypeError ctx e (NotAFunction f tf))+ _A' <- typeWith ctx a+ if propEqual _A _A'+ then do+ let a' = Dhall.Core.shift 1 (V x 0) a+ let _B' = Dhall.Core.subst (V x 0) a' _B+ let _B'' = Dhall.Core.shift (-1) (V x 0) _B'+ return _B''+ else do+ let nf_A = Dhall.Core.normalize _A+ let nf_A' = Dhall.Core.normalize _A'+ Left (TypeError ctx e (TypeMismatch f nf_A a nf_A'))+typeWith ctx e@(Let f mt r b ) = do+ tR <- typeWith ctx r+ ttR <- fmap Dhall.Core.normalize (typeWith ctx tR)+ kR <- case ttR of+ Const k -> return k+ -- Don't bother to provide a `let`-specific version of this error+ -- message because this should never happen anyway+ _ -> Left (TypeError ctx e (InvalidInputType tR))++ let ctx' = Dhall.Context.insert f tR ctx+ tB <- typeWith ctx' b+ ttB <- fmap Dhall.Core.normalize (typeWith ctx tB)+ kB <- case ttB of+ Const k -> return k+ -- Don't bother to provide a `let`-specific version of this error+ -- message because this should never happen anyway+ _ -> Left (TypeError ctx e (InvalidOutputType tB))++ case rule kR kB of+ Left () -> Left (TypeError ctx e (NoDependentLet tR tB))+ Right _ -> return ()++ case mt of+ Nothing -> do+ return ()+ Just t -> do+ let nf_t = Dhall.Core.normalize t+ let nf_tR = Dhall.Core.normalize tR+ if propEqual nf_tR nf_t+ then return ()+ else Left (TypeError ctx e (AnnotMismatch r nf_t nf_tR))++ return tB+typeWith ctx e@(Annot x t ) = do+ -- This is mainly just to check that `t` is not `Kind`+ _ <- typeWith ctx t++ t' <- typeWith ctx x+ if propEqual t t'+ then do+ return t+ else do+ let nf_t = Dhall.Core.normalize t+ let nf_t' = Dhall.Core.normalize t'+ Left (TypeError ctx e (AnnotMismatch x nf_t nf_t'))+typeWith _ Bool = do+ return (Const Type)+typeWith _ (BoolLit _ ) = do+ return Bool+typeWith ctx e@(BoolAnd l r ) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantAnd l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantAnd r tr))++ return Bool+typeWith ctx e@(BoolOr l r ) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantOr l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantOr r tr))++ return Bool+typeWith ctx e@(BoolEQ l r ) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantEQ l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantEQ r tr))++ return Bool+typeWith ctx e@(BoolNE l r ) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantNE l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Bool -> return ()+ _ -> Left (TypeError ctx e (CantNE r tr))++ return Bool+typeWith ctx e@(BoolIf x y z ) = do+ tx <- fmap Dhall.Core.normalize (typeWith ctx x)+ case tx of+ Bool -> return ()+ _ -> Left (TypeError ctx e (InvalidPredicate x tx))+ ty <- fmap Dhall.Core.normalize (typeWith ctx y )+ tty <- fmap Dhall.Core.normalize (typeWith ctx ty)+ case tty of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (IfBranchMustBeTerm True y ty tty))++ tz <- fmap Dhall.Core.normalize (typeWith ctx z)+ ttz <- fmap Dhall.Core.normalize (typeWith ctx tz)+ case ttz of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz))++ if propEqual ty tz+ then return ()+ else Left (TypeError ctx e (IfBranchMismatch y z ty tz))+ return ty+typeWith _ Natural = do+ return (Const Type)+typeWith _ (NaturalLit _ ) = do+ return Natural+typeWith _ NaturalFold = do+ return+ (Pi "_" Natural+ (Pi "natural" (Const Type)+ (Pi "succ" (Pi "_" "natural" "natural")+ (Pi "zero" "natural" "natural") ) ) )+typeWith _ NaturalBuild = do+ return+ (Pi "_"+ (Pi "natural" (Const Type)+ (Pi "succ" (Pi "_" "natural" "natural")+ (Pi "zero" "natural" "natural") ) )+ Natural )+typeWith _ NaturalIsZero = do+ return (Pi "_" Natural Bool)+typeWith _ NaturalEven = do+ return (Pi "_" Natural Bool)+typeWith _ NaturalOdd = do+ return (Pi "_" Natural Bool)+typeWith ctx e@(NaturalPlus l r) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Natural -> return ()+ _ -> Left (TypeError ctx e (CantAdd l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Natural -> return ()+ _ -> Left (TypeError ctx e (CantAdd r tr))+ return Natural+typeWith ctx e@(NaturalTimes l r) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Natural -> return ()+ _ -> Left (TypeError ctx e (CantMultiply l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Natural -> return ()+ _ -> Left (TypeError ctx e (CantMultiply r tr))+ return Natural+typeWith _ Integer = do+ return (Const Type)+typeWith _ (IntegerLit _ ) = do+ return Integer+typeWith _ Double = do+ return (Const Type)+typeWith _ (DoubleLit _ ) = do+ return Double+typeWith _ Text = do+ return (Const Type)+typeWith _ (TextLit _ ) = do+ return Text+typeWith ctx e@(TextAppend l r ) = do+ tl <- fmap Dhall.Core.normalize (typeWith ctx l)+ case tl of+ Text -> return ()+ _ -> Left (TypeError ctx e (CantTextAppend l tl))++ tr <- fmap Dhall.Core.normalize (typeWith ctx r)+ case tr of+ Text -> return ()+ _ -> Left (TypeError ctx e (CantTextAppend r tr))+ return Text+typeWith _ List = do+ return (Pi "_" (Const Type) (Const Type))+typeWith ctx e@(ListLit t xs ) = do+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidListType t))+ flip Data.Vector.imapM_ xs (\i x -> do+ t' <- typeWith ctx x+ if propEqual t t'+ then return ()+ else do+ let nf_t = Dhall.Core.normalize t+ let nf_t' = Dhall.Core.normalize t'+ Left (TypeError ctx e (InvalidListElement i nf_t x nf_t')) )+ return (App List t)+typeWith _ ListBuild = do+ return+ (Pi "a" (Const Type)+ (Pi "_"+ (Pi "list" (Const Type)+ (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list"))+ (Pi "nil" "list" "list") ) )+ (App List "a") ) )+typeWith _ ListFold = do+ return+ (Pi "a" (Const Type)+ (Pi "_" (App List "a")+ (Pi "list" (Const Type)+ (Pi "cons" (Pi "_" "a" (Pi "_" "list" "list"))+ (Pi "nil" "list" "list")) ) ) )+typeWith _ ListLength = do+ return (Pi "a" (Const Type) (Pi "_" (App List "a") Natural))+typeWith _ ListHead = do+ return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))+typeWith _ ListLast = do+ return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Optional "a")))+typeWith _ ListIndexed = do+ let kts = [("index", Natural), ("value", "a")]+ return+ (Pi "a" (Const Type)+ (Pi "_" (App List "a")+ (App List (Record (Data.Map.fromList kts))) ) )+typeWith _ ListReverse = do+ return (Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a")))+typeWith _ Optional = do+ return (Pi "_" (Const Type) (Const Type))+typeWith ctx e@(OptionalLit t xs) = do+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidOptionalType t))+ let n = Data.Vector.length xs+ if 2 <= n+ then Left (TypeError ctx e (InvalidOptionalLiteral n))+ else return ()+ forM_ xs (\x -> do+ t' <- typeWith ctx x+ if propEqual t t'+ then return ()+ else do+ let nf_t = Dhall.Core.normalize t+ let nf_t' = Dhall.Core.normalize t'+ Left (TypeError ctx e (InvalidOptionalElement nf_t x nf_t')) )+ return (App Optional t)+typeWith _ OptionalFold = do+ return+ (Pi "a" (Const Type)+ (Pi "_" (App Optional "a")+ (Pi "maybe" (Const Type)+ (Pi "just" (Pi "_" "a" "maybe")+ (Pi "nothing" "maybe" "maybe") ) ) ) )+typeWith ctx e@(Record kts ) = do+ let process (k, t) = do+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidFieldType k t))+ mapM_ process (Data.Map.toList kts)+ return (Const Type)+typeWith ctx e@(RecordLit kvs ) = do+ let process (k, v) = do+ t <- typeWith ctx v+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidField k v))+ return (k, t)+ kts <- mapM process (Data.Map.toAscList kvs)+ return (Record (Data.Map.fromAscList kts))+typeWith ctx e@(Union kts ) = do+ let process (k, t) = do+ s <- fmap Dhall.Core.normalize (typeWith ctx t)+ case s of+ Const Type -> return ()+ _ -> Left (TypeError ctx e (InvalidAlternativeType k t))+ mapM_ process (Data.Map.toList kts)+ return (Const Type)+typeWith ctx e@(UnionLit k v kts) = do+ case Data.Map.lookup k kts of+ Just _ -> Left (TypeError ctx e (DuplicateAlternative k))+ Nothing -> return ()+ t <- typeWith ctx v+ let union = Union (Data.Map.insert k t kts)+ _ <- typeWith ctx union+ return union+typeWith ctx e@(Combine kvsX kvsY) = do+ tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX)+ ktsX <- case tKvsX of+ Record kts -> return kts+ _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))+ let ksX = Data.Map.keysSet ktsX++ tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY)+ ktsY <- case tKvsY of+ Record kts -> return kts+ _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))+ let ksY = Data.Map.keysSet ktsY++ let ks = Data.Set.intersection ksX ksY+ if Data.Set.null ks+ then return ()+ else Left (TypeError ctx e (FieldCollision ks))+ return (Record (Data.Map.union ktsX ktsY))+typeWith ctx e@(Merge kvsX kvsY t) = do+ tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX)+ ktsX <- case tKvsX of+ Record kts -> return kts+ _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))+ let ksX = Data.Map.keysSet ktsX++ tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY)+ ktsY <- case tKvsY of+ Union kts -> return kts+ _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))+ let ksY = Data.Map.keysSet ktsY++ let diffX = Data.Set.difference ksX ksY+ let diffY = Data.Set.difference ksY ksX++ if Data.Set.null diffX+ then return ()+ else Left (TypeError ctx e (UnusedHandler diffX))++ let process (kY, tY) = do+ case Data.Map.lookup kY ktsX of+ Nothing -> Left (TypeError ctx e (MissingHandler diffY))+ Just tX ->+ case tX of+ Pi _ tY' t' -> do+ if propEqual tY tY'+ then return ()+ else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))+ if propEqual t t'+ then return ()+ else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))+ _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))+ mapM_ process (Data.Map.toList ktsY)+ return t+typeWith ctx e@(Field r x ) = do+ t <- fmap Dhall.Core.normalize (typeWith ctx r)+ case t of+ Record kts ->+ case Data.Map.lookup x kts of+ Just t' -> return t'+ Nothing -> Left (TypeError ctx e (MissingField x t))+ _ -> Left (TypeError ctx e (NotARecord x r t))+typeWith ctx (Note s e' ) = case typeWith 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)+ Right r -> Right r+typeWith _ (Embed p ) = do+ absurd p++{-| `typeOf` is the same as `typeWith` with an empty context, meaning that the+ expression must be closed (i.e. no free variables), otherwise type-checking+ will fail.+-}+typeOf :: Expr s X -> Either (TypeError s) (Expr s X)+typeOf = typeWith Dhall.Context.empty++-- | Like `Data.Void.Void`, except with a shorter inferred type+newtype X = X { absurd :: forall a . a }++instance Show X where+ show = absurd++instance Buildable X where+ build = absurd++-- | The specific type error+data TypeMessage s+ = UnboundVariable+ | InvalidInputType (Expr s X)+ | InvalidOutputType (Expr s X)+ | NotAFunction (Expr s X) (Expr s X)+ | TypeMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)+ | AnnotMismatch (Expr s X) (Expr s X) (Expr s X)+ | Untyped+ | InvalidListElement Int (Expr s X) (Expr s X) (Expr s X)+ | InvalidListType (Expr s X)+ | InvalidOptionalElement (Expr s X) (Expr s X) (Expr s X)+ | InvalidOptionalLiteral Int+ | InvalidOptionalType (Expr s X)+ | InvalidPredicate (Expr s X) (Expr s X)+ | IfBranchMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)+ | IfBranchMustBeTerm Bool (Expr s X) (Expr s X) (Expr s X)+ | InvalidField Text (Expr s X)+ | InvalidFieldType Text (Expr s X)+ | InvalidAlternative Text (Expr s X)+ | InvalidAlternativeType Text (Expr s X)+ | DuplicateAlternative Text+ | MustCombineARecord (Expr s X) (Expr s X)+ | FieldCollision (Set Text)+ | MustMergeARecord (Expr s X) (Expr s X)+ | MustMergeUnion (Expr s X) (Expr s X)+ | UnusedHandler (Set Text)+ | MissingHandler (Set Text)+ | HandlerInputTypeMismatch Text (Expr s X) (Expr s X)+ | HandlerOutputTypeMismatch Text (Expr s X) (Expr s X)+ | HandlerNotAFunction Text (Expr s X)+ | NotARecord Text (Expr s X) (Expr s X)+ | MissingField Text (Expr s X)+ | CantAnd (Expr s X) (Expr s X)+ | CantOr (Expr s X) (Expr s X)+ | CantEQ (Expr s X) (Expr s X)+ | CantNE (Expr s X) (Expr s X)+ | CantTextAppend (Expr s X) (Expr s X)+ | CantAdd (Expr s X) (Expr s X)+ | CantMultiply (Expr s X) (Expr s X)+ | NoDependentLet (Expr s X) (Expr s X)+ | NoDependentTypes (Expr s X) (Expr s X)+ deriving (Show)++shortTypeMessage :: TypeMessage s -> Builder+shortTypeMessage msg =+ "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"+ where+ ErrorMessages {..} = prettyTypeMessage msg++longTypeMessage :: TypeMessage s -> Builder+longTypeMessage msg =+ "\ESC[1;31mError\ESC[0m: " <> build short <> "\n"+ <> "\n"+ <> long+ where+ ErrorMessages {..} = prettyTypeMessage msg++data ErrorMessages = ErrorMessages+ { short :: Builder+ -- ^ Default succinct 1-line explanation of what went wrong+ , long :: Builder+ -- ^ Longer and more detailed explanation of the error+ }++instance Buildable ErrorMessages where+ build (ErrorMessages {..}) =+ "Error: " <> build short <> "\n"+ <> "\n"+ <> long++_NOT :: Data.Text.Text+_NOT = "\ESC[1mnot\ESC[0m"++prettyTypeMessage :: TypeMessage s -> ErrorMessages+prettyTypeMessage UnboundVariable = ErrorMessages {..}+ where+ short = "Unbound variable"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Expressions can only reference previously introduced (i.e. "bound")+variables that are still "in scope"++For example, the following valid expressions introduce a "bound" variable named+❰x❱:+++ ┌─────────────────┐+ │ λ(x : Bool) → x │ Anonymous functions introduce "bound" variables+ └─────────────────┘+ ⇧+ This is the bound variable+++ ┌─────────────────┐+ │ let x = 1 in x │ ❰let❱ expressions introduce "bound" variables+ └─────────────────┘+ ⇧+ This is the bound variable+++However, the following expressions are not valid because they all reference a+variable that has not been introduced yet (i.e. an "unbound" variable):+++ ┌─────────────────┐+ │ λ(x : Bool) → y │ The variable ❰y❱ hasn't been introduced yet+ └─────────────────┘+ ⇧+ This is the unbound variable+++ ┌──────────────────────────┐+ │ (let x = True in x) && x │ ❰x❱ is undefined outside the parentheses+ └──────────────────────────┘+ ⇧+ This is the unbound variable+++ ┌────────────────┐+ │ let x = x in x │ The definition for ❰x❱ cannot reference itself+ └────────────────┘+ ⇧+ This is the unbound variable+++Some common reasons why you might get this error:++● You misspell a variable name, like this:+++ ┌────────────────────────────────────────────────────┐+ │ λ(empty : Bool) → if emty then "Empty" else "Full" │+ └────────────────────────────────────────────────────┘+ ⇧+ Typo+++● You misspell a reserved identifier, like this:+++ ┌──────────────────────────┐+ │ foral (a : Type) → a → a │+ └──────────────────────────┘+ ⇧+ Typo+++● You tried to define a recursive value, like this:+++ ┌─────────────────────┐+ │ let x = x + +1 in x │+ └─────────────────────┘+ ⇧+ Recursive definitions are not allowed+++● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱+++ Unbound variable+ ⇩+ ┌─────────────────┐+ │ (x : Bool) → x │+ └─────────────────┘+ ⇧+ A ❰λ❱ here would transform this into a valid anonymous function +++ Unbound variable+ ⇩+ ┌────────────────────┐+ │ (x : Bool) → Bool │+ └────────────────────┘+ ⇧+ A ❰∀❱ or ❰forall❱ here would transform this into a valid function type+|]++prettyTypeMessage (InvalidInputType expr) = ErrorMessages {..}+ where+ short = "Invalid function input"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: A function can accept an input "term" that has a given "type", like+this:+++ This is the input term that the function accepts+ ⇩+ ┌───────────────────────┐+ │ ∀(x : Natural) → Bool │ This is the type of a function that accepts an+ └───────────────────────┘ input term named ❰x❱ that has type ❰Natural❱+ ⇧+ This is the type of the input term+++ ┌────────────────┐+ │ Bool → Integer │ This is the type of a function that accepts an anonymous+ └────────────────┘ input term that has type ❰Bool❱+ ⇧+ This is the type of the input term+++... or a function can accept an input "type" that has a given "kind", like this:+++ This is the input type that the function accepts+ ⇩+ ┌────────────────────┐+ │ ∀(a : Type) → Type │ This is the type of a function that accepts an input+ └────────────────────┘ type named ❰a❱ that has kind ❰Type❱+ ⇧+ This is the kind of the input type+++ ┌──────────────────────┐+ │ (Type → Type) → Type │ This is the type of a function that accepts an+ └──────────────────────┘ anonymous input type that has kind ❰Type → Type❱+ ⇧+ This is the kind of the input type+++Other function inputs are $_NOT valid, like this:+++ ┌──────────────┐+ │ ∀(x : 1) → x │ ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱+ └──────────────┘ cannot have "type" ❰1❱ or "kind" ❰1❱+ ⇧+ This is not a type or kind+++ ┌──────────┐+ │ True → x │ ❰True❱ is a "term" and not a "type" nor a "kind" so the+ └──────────┘ anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱+ ⇧+ This is not a type or kind+++You annotated a function input with the following expression:++↳ $txt++... which is neither a type nor a kind+|]+ where+ txt = Text.toStrict (Dhall.Core.pretty expr)++prettyTypeMessage (InvalidOutputType expr) = ErrorMessages {..}+ where+ short = "Invalid function output"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: A function can return an output "term" that has a given "type",+like this:+++ ┌────────────────────┐+ │ ∀(x : Text) → Bool │ This is the type of a function that returns an+ └────────────────────┘ output term that has type ❰Bool❱+ ⇧+ This is the type of the output term+++ ┌────────────────┐+ │ Bool → Integer │ This is the type of a function that returns an output+ └────────────────┘ term that has type ❰Int❱+ ⇧+ This is the type of the output term+++... or a function can return an output "type" that has a given "kind", like+this:++ ┌────────────────────┐+ │ ∀(a : Type) → Type │ This is the type of a function that returns an+ └────────────────────┘ output type that has kind ❰Type❱+ ⇧+ This is the kind of the output type+++ ┌──────────────────────┐+ │ (Type → Type) → Type │ This is the type of a function that returns an+ └──────────────────────┘ output type that has kind ❰Type❱+ ⇧+ This is the kind of the output type+++Other outputs are $_NOT valid, like this:+++ ┌─────────────────┐+ │ ∀(x : Bool) → x │ ❰x❱ is a "term" and not a "type" nor a "kind" so the+ └─────────────────┘ output cannot have "type" ❰x❱ or "kind" ❰x❱+ ⇧+ This is not a type or kind+++ ┌─────────────┐+ │ Text → True │ ❰True❱ is a "term" and not a "type" nor a "kind" so the+ └─────────────┘ output cannot have "type" ❰True❱ or "kind" ❰True❱+ ⇧+ This is not a type or kind+++You specified that your function outputs a:++↳ $txt++... which is neither a type nor a kind:++Some common reasons why you might get this error:++● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:+++ ┌────────────────┐+ │ ∀(x: Bool) → x │+ └────────────────┘+ ⇧+ Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function+|]+ where+ txt = Text.toStrict (Dhall.Core.pretty expr)++prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..}+ where+ short = "Not a function"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Expressions separated by whitespace denote function application,+like this:+++ ┌─────┐+ │ f x │ This denotes the function ❰f❱ applied to an argument named ❰x❱ + └─────┘+++A function is a term that has type ❰a → b❱ for some ❰a❱ or ❰b❱. For example,+the following expressions are all functions because they have a function type:+++ The function's input type is ❰Bool❱+ ⇩+ ┌───────────────────────────────┐+ │ λ(x : Bool) → x : Bool → Bool │ User-defined anonymous function+ └───────────────────────────────┘+ ⇧+ The function's output type is ❰Bool❱+++ The function's input type is ❰Natural❱+ ⇩+ ┌───────────────────────────────┐+ │ Natural/even : Natural → Bool │ Built-in function+ └───────────────────────────────┘+ ⇧+ The function's output type is ❰Bool❱+++ The function's input kind is ❰Type❱+ ⇩+ ┌───────────────────────────────┐+ │ λ(a : Type) → a : Type → Type │ Type-level functions are still functions+ └───────────────────────────────┘+ ⇧+ The function's output kind is ❰Type❱+++ The function's input kind is ❰Type❱+ ⇩+ ┌────────────────────┐+ │ List : Type → Type │ Built-in type-level function+ └────────────────────┘+ ⇧+ The function's output kind is ❰Type❱+++ Function's input has kind ❰Type❱+ ⇩+ ┌─────────────────────────────────────────────────┐+ │ List/head : ∀(a : Type) → (List a → Optional a) │ A function can return+ └─────────────────────────────────────────────────┘ another function+ ⇧+ Function's output has type ❰List a → Optional a❱+++ The function's input type is ❰List Text❱+ ⇩+ ┌────────────────────────────────────────────┐+ │ List/head Text : List Text → Optional Text │ A function applied to an+ └────────────────────────────────────────────┘ argument can be a function+ ⇧+ The function's output type is ❰Optional Text❱+++An expression is not a function if the expression's type is not of the form+❰a → b❱. For example, these are $_NOT functions:+++ ┌─────────────┐+ │ 1 : Integer │ ❰1❱ is not a function because ❰Integer❱ is not the type of+ └─────────────┘ a function+++ ┌────────────────────────┐+ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ is not a function because+ └────────────────────────┘ ❰Bool❱ is not the type of a function+++ ┌──────────────────┐+ │ List Text : Type │ ❰List Text❱ is not a function because ❰Type❱ is not+ └──────────────────┘ the type of a function+++You tried to use the following expression as a function:++↳ $txt0++... but this expression's type is:++↳ $txt1++... which is not a function type+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}+ where+ short = "Wrong function argument"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every function declares what type or kind of argument to accept++For example:+++ ┌───────────────────────────────┐+ │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts+ └───────────────────────────────┘ arguments that have type ❰Bool❱+ ⇧+ The function's input type+++ ┌───────────────────────────────┐+ │ Natural/even : Natural → Bool │ This built-in function only accepts+ └───────────────────────────────┘ arguments that have type ❰Natural❱+ ⇧+ The function's input type+++ ┌───────────────────────────────┐+ │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts+ └───────────────────────────────┘ arguments that have kind ❰Type❱+ ⇧+ The function's input kind+++ ┌────────────────────┐+ │ List : Type → Type │ This built-in function only accepts arguments that+ └────────────────────┘ have kind ❰Type❱+ ⇧+ The function's input kind+++For example, the following expressions are valid:+++ ┌────────────────────────┐+ │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type+ └────────────────────────┘ of argument that the anonymous function accepts+++ ┌─────────────────┐+ │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of+ └─────────────────┘ argument that the ❰Natural/even❱ function accepts,+++ ┌────────────────────────┐+ │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind+ └────────────────────────┘ of argument that the anonymous function accepts+++ ┌───────────┐+ │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument+ └───────────┘ that that the ❰List❱ function accepts+++However, you can $_NOT apply a function to the wrong type or kind of argument++For example, the following expressions are not valid:+++ ┌───────────────────────┐+ │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function+ └───────────────────────┘ expects an argument that has type ❰Bool❱+++ ┌──────────────────┐+ │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function+ └──────────────────┘ expects an argument that has type ❰Natural❱+++ ┌────────────────────────┐+ │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous+ └────────────────────────┘ function expects an argument of kind ❰Type❱+++ ┌────────┐+ │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an+ └────────┘ argument that has kind ❰Type❱+++You tried to invoke the following function:++↳ $txt0++... which expects an argument of type or kind:++↳ $txt1++... on the following argument:++↳ $txt2++... which has a different type or kind:++↳ $txt3++Some common reasons why you might get this error:++● You omit a function argument by mistake:+++ ┌────────────────────────────────────────┐+ │ List/head ([1, 2, 3] : List Integer) │+ └────────────────────────────────────────┘+ ⇧+ ❰List/head❱ is missing the first argument,+ which should be: ❰Integer❱+++● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱++ ┌────────────────┐+ │ Natural/even 2 │+ └────────────────┘+ ⇧+ This should be ❰+2❱+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)+ txt3 = Text.toStrict (Dhall.Core.pretty expr3)++prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}+ where+ short = "Expression doesn't match annotation"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can annotate an expression with its type or kind using the+❰:❱ symbol, like this:+++ ┌───────┐+ │ x : t │ ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱+ └───────┘++The type checker verifies that the expression's type or kind matches the+provided annotation++For example, all of the following are valid annotations that the type checker+accepts:+++ ┌─────────────┐+ │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type+ └─────────────┘ checker accepts the annotation+++ ┌────────────────────────┐+ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type+ └────────────────────────┘ checker accepts the annotation+++ ┌────────────────────┐+ │ List : Type → Type │ ❰List❱ is an expression that has kind ❰Type → Type❱,+ └────────────────────┘ so the type checker accepts the annotation+++ ┌──────────────────┐+ │ List Text : Type │ ❰List Text❱ is an expression that has kind ❰Type❱, so+ └──────────────────┘ the type checker accepts the annotation+++However, the following annotations are $_NOT valid and the type checker will+reject them:+++ ┌──────────┐+ │ 1 : Text │ The type checker rejects this because ❰1❱ does not have type+ └──────────┘ ❰Text❱+++ ┌─────────────┐+ │ List : Type │ ❰List❱ does not have kind ❰Type❱+ └─────────────┘+++You or the interpreter annotated this expression:++↳ $txt0++... with this type or kind:++↳ $txt1++... but the inferred type or kind of the expression is actually:++↳ $txt2++Some common reasons why you might get this error:++● The Haskell Dhall interpreter implicitly inserts a top-level annotation+ matching the expected type++ For example, if you run the following Haskell code:+++ ┌───────────────────────────────┐+ │ >>> input auto "1" :: IO Text │+ └───────────────────────────────┘+++ ... then the interpreter will actually type check the following annotated+ expression:+++ ┌──────────┐+ │ 1 : Text │+ └──────────┘+++ ... and then type-checking will fail+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage Untyped = ErrorMessages {..}+ where+ short = "❰Kind❱ has no type or kind"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: There are four levels of expressions that form a heirarchy:++● terms+● types+● kinds+● sorts++The following example illustrates this heirarchy:++ ┌────────────────────────────┐+ │ "ABC" : Text : Type : Kind │+ └────────────────────────────┘+ ⇧ ⇧ ⇧ ⇧+ term type kind sort++There is nothing above ❰Kind❱ in this hierarchy, so if you try to type check any+expression containing ❰Kind❱ anywhere in the expression then type checking fails++Some common reasons why you might get this error:++● You supplied a kind where a type was expected++ For example, the following expression will fail to type check:++ ┌────────────────┐+ │ [] : List Type │+ └────────────────┘+ ⇧+ ❰Type❱ is a kind, not a type+|]++prettyTypeMessage (InvalidPredicate expr0 expr1) = ErrorMessages {..}+ where+ short = "Invalid predicate for ❰if❱"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every ❰if❱ expression begins with a predicate which must have type+❰Bool❱++For example, these are valid ❰if❱ expressions:+++ ┌──────────────────────────────┐+ │ if True then "Yes" else "No" │+ └──────────────────────────────┘+ ⇧+ Predicate+++ ┌─────────────────────────────────────────┐+ │ λ(x : Bool) → if x then False else True │+ └─────────────────────────────────────────┘+ ⇧+ Predicate+++... but these are $_NOT valid ❰if❱ expressions:+++ ┌───────────────────────────┐+ │ if 0 then "Yes" else "No" │ ❰0❱ does not have type ❰Bool❱+ └───────────────────────────┘+++ ┌────────────────────────────┐+ │ if "" then False else True │ ❰""❱ does not have type ❰Bool❱+ └────────────────────────────┘+++Your ❰if❱ expression begins with the following predicate:++↳ $txt0++... that has type:++↳ $txt1++... but the predicate must instead have type ❰Bool❱++Some common reasons why you might get this error:++● You might be used to other programming languages that accept predicates other+ than ❰Bool❱++ For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat+ them as equivalent to ❰False❱. However, the Dhall language does not permit+ this+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (IfBranchMustBeTerm b expr0 expr1 expr2) =+ ErrorMessages {..}+ where+ short = "❰if❱ branch is not a term"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which+is an expression:+++ Expression for ❰then❱ branch+ ⇩+ ┌────────────────────────────────┐+ │ if True then "Hello, world!" │+ │ else "Goodbye, world!" │+ └────────────────────────────────┘+ ⇧+ Expression for ❰else❱ branch+++These expressions must be a "term", where a "term" is defined as an expression+that has a type thas has kind ❰Type❱++For example, the following expressions are all valid "terms":+++ ┌────────────────────┐+ │ 1 : Integer : Type │ ❰1❱ is a term with a type (❰Integer❱) of kind ❰Type❱+ └────────────────────┘+ ⇧+ term+++ ┌─────────────────────────────────────┐+ │ Natural/odd : Natural → Bool : Type │ ❰Natural/odd❱ is a term with a type+ └─────────────────────────────────────┘ (❰Natural → Bool❱) of kind ❰Type❱+ ⇧+ term+++However, the following expressions are $_NOT valid terms:+++ ┌────────────────────┐+ │ Text : Type : Kind │ ❰Text❱ has kind (❰Type❱) of sort ❰Kind❱ and is+ └────────────────────┘ therefore not a term+ ⇧+ type+++ ┌───────────────────────────┐+ │ List : Type → Type : Kind │ ❰List❱ has kind (❰Type → Type❱) of sort+ └───────────────────────────┘ ❰Kind❱ and is therefore not a term+ ⇧+ type-level function+++This means that you cannot define an ❰if❱ expression that returns a type. For+example, the following ❰if❱ expression is $_NOT valid:+++ ┌─────────────────────────────┐+ │ if True then Text else Bool │ Invalid ❰if❱ expression+ └─────────────────────────────┘+ ⇧ ⇧+ type type+++Your ❰$txt0❱ branch of your ❰if❱ expression is:++↳ $txt1++... which has kind:++↳ $txt2++... of sort:++↳ $txt3++... and is not a term. Therefore your ❰if❱ expression is not valid+|]+ where+ txt0 = if b then "then" else "else"+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)+ txt2 = Text.toStrict (Dhall.Core.pretty expr1)+ txt3 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =+ ErrorMessages {..}+ where+ short = "❰if❱ branches must have matching types"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which+is an expression:+++ Expression for ❰then❱ branch+ ⇩+ ┌────────────────────────────────┐+ │ if True then "Hello, world!" │+ │ else "Goodbye, world!" │+ └────────────────────────────────┘+ ⇧+ Expression for ❰else❱ branch+++These two expressions must have the same type. For example, the following ❰if❱+expressions are all valid:+++ ┌──────────────────────────────────┐+ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱+ └──────────────────────────────────┘+++ ┌────────────────────────────┐+ │ λ(b : Bool) → │+ │ if b then Natural/even │ Both branches have type ❰Natural → Bool❱+ │ else Natural/odd │+ └────────────────────────────┘+++However, the following expression is $_NOT valid:+++ This branch has type ❰Integer❱+ ⇩+ ┌────────────────────────┐+ │ if True then 0 │+ │ else "ABC" │+ └────────────────────────┘+ ⇧+ This branch has type ❰Text❱+++The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is+always ❰True❱ or ❰False❱++Your ❰if❱ expression has the following ❰then❱ branch:++↳ $txt0++... which has type:++↳ $txt2++... and the following ❰else❱ branch:++↳ $txt1++... which has a different type:++↳ $txt3++Fix your ❰then❱ and ❰else❱ branches to have matching types+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)+ txt3 = Text.toStrict (Dhall.Core.pretty expr3)++prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}+ where+ short = "Invalid type for ❰List❱ elements"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every ❰List❱ documents the type of its elements with a type+annotation, like this:+++ ┌──────────────────────────┐+ │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s+ └──────────────────────────┘+ ⇧+ The type of the ❰List❱'s elements, which are ❰Integer❱s+++ ┌───────────────────┐+ │ [] : List Integer │ An empty ❰List❱+ └───────────────────┘+ ⇧+ You still specify the type even when the ❰List❱ is empty+++The element type must be a type and not something else. For example, the+following element types are $_NOT valid:+++ ┌──────────────┐+ │ ... : List 1 │+ └──────────────┘+ ⇧+ This is an ❰Integer❱ and not a ❰Type❱+++ ┌─────────────────┐+ │ ... : List Type │+ └─────────────────┘+ ⇧+ This is a ❰Kind❱ and not a ❰Type❱+++Even if the ❰List❱ is empty you still must specify a valid type++You declared that the ❰List❱'s elements should have type:++↳ $txt0++... which is not a ❰Type❱+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (InvalidListElement i expr0 expr1 expr2) =+ ErrorMessages {..}+ where+ short = "List element has the wrong type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every element in the list must have a type matching the type+annotation at the end of the list++For example, this is a valid ❰List❱:+++ ┌──────────────────────────┐+ │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱+ └──────────────────────────┘+++.. but this is $_NOT a valid ❰List❱:+++ ┌──────────────────────────────┐+ │ [1, "ABC", 3] : List Integer │ The second element is not an ❰Integer❱+ └──────────────────────────────┘+++Your ❰List❱ elements should have this type:++↳ $txt0++... but the following element at index $txt1:++↳ $txt2++... has this type instead:++↳ $txt3+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty i )+ txt2 = Text.toStrict (Dhall.Core.pretty expr1)+ txt3 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage (InvalidOptionalType expr0) = ErrorMessages {..}+ where+ short = "Invalid type for ❰Optional❱ element"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every optional element ends with a type annotation for the element+that might be present, like this:+++ ┌────────────────────────┐+ │ [1] : Optional Integer │ An optional element that's present+ └────────────────────────┘+ ⇧+ The type of the ❰Optional❱ element, which is an ❰Integer❱+++ ┌────────────────────────┐+ │ [] : Optional Integer │ An optional element that's absent+ └────────────────────────┘+ ⇧+ You still specify the type even when the element is absent+++The element type must be a type and not something else. For example, the+following element types are $_NOT valid:+++ ┌──────────────────┐+ │ ... : Optional 1 │+ └──────────────────┘+ ⇧+ This is an ❰Integer❱ and not a ❰Type❱+++ ┌─────────────────────┐+ │ ... : Optional Type │+ └─────────────────────┘+ ⇧+ This is a ❰Kind❱ and not a ❰Type❱+++Even if the element is absent you still must specify a valid type++You declared that the ❰Optional❱ element should have type:++↳ $txt0++... which is not a ❰Type❱++|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..}+ where+ short = "❰Optional❱ element has the wrong type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: An ❰Optional❱ element must have a type matching the type annotation++For example, this is a valid ❰Optional❱ value:+++ ┌────────────────────────┐+ │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type+ └────────────────────────┘+++... but this is $_NOT a valid ❰Optional❱ value:+++ ┌────────────────────────────┐+ │ ["ABC"] : Optional Integer │ ❰"ABC"❱ is not an ❰Integer❱+ └────────────────────────────┘+++Your ❰Optional❱ element should have this type:++↳ $txt0++... but the element you provided:++↳ $txt1++... has this type instead:++↳ $txt2+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage (InvalidOptionalLiteral n) = ErrorMessages {..}+ where+ short = "Multiple ❰Optional❱ elements not allowed"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s:+++ ┌───────────────────────┐+ │ [] : Optional Integer │ An ❰Optional❱ value which is absent+ └───────────────────────┘+++ ┌───────────────────────┐+ │ [] : List Integer │ An empty (0-element) ❰List❱+ └───────────────────────┘+++ ┌────────────────────────┐+ │ [1] : Optional Integer │ An ❰Optional❱ value which is present+ └────────────────────────┘+++ ┌────────────────────────┐+ │ [1] : List Integer │ A singleton (1-element) ❰List❱+ └────────────────────────┘+++However, an ❰Optional❱ value can $_NOT have more than one element, whereas a+❰List❱ can have multiple elements:+++ ┌───────────────────────────┐+ │ [1, 2] : Optional Integer │ Invalid: multiple elements $_NOT allowed+ └───────────────────────────┘+++ ┌───────────────────────────┐+ │ [1, 2] : List Integer │ Valid: multiple elements allowed+ └───────────────────────────┘+++Your ❰Optional❱ value had this many elements:++↳ $txt0++... when an ❰Optional❱ value can only have at most one element++Some common reasons why you might get this error:++● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this:+++ ┌────────────────────────────────────────────────────┐+ │ List/length Integer ([1, 2, 3] : Optional Integer) │+ └────────────────────────────────────────────────────┘+ ⇧+ This should be ❰List❱ instead+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty n)++prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}+ where+ short = "Invalid field type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every record type documents the type of each field, like this:++ ┌──────────────────────────────────────────────┐+ │ { foo : Integer, bar : Integer, baz : Text } │+ └──────────────────────────────────────────────┘++However, fields cannot be annotated with expressions other than types++For example, these record types are $_NOT valid:+++ ┌────────────────────────────┐+ │ { foo : Integer, bar : 1 } │+ └────────────────────────────┘+ ⇧+ ❰1❱ is an ❰Integer❱ and not a ❰Type❱+++ ┌───────────────────────────────┐+ │ { foo : Integer, bar : Type } │+ └───────────────────────────────┘+ ⇧+ ❰Type❱ is a ❰Kind❱ and not a ❰Type❱+++You provided a record type with a key named:++↳ $txt0++... annotated with the following expression:++↳ $txt1++... which is not a type+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (InvalidField k expr0) = ErrorMessages {..}+ where+ short = "Invalid field"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every record literal is a set of fields assigned to values, like+this:++ ┌────────────────────────────────────────┐+ │ { foo = 100, bar = True, baz = "ABC" } │+ └────────────────────────────────────────┘++However, fields can only be terms and cannot be types or kinds++For example, these record literals are $_NOT valid:+++ ┌───────────────────────────┐+ │ { foo = 100, bar = Text } │+ └───────────────────────────┘+ ⇧+ ❰Text❱ is a type and not a term+++ ┌───────────────────────────┐+ │ { foo = 100, bar = Type } │+ └───────────────────────────┘+ ⇧+ ❰Type❱ is a kind and not a term+++You provided a record literal with a key named:++↳ $txt0++... whose value is:++↳ $txt1++... which is not a term+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (InvalidAlternativeType k expr0) = ErrorMessages {..}+ where+ short = "Invalid alternative"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every union literal begins by selecting one alternative and+specifying the value for that alternative, like this:+++ Select the ❰Left❱ alternative, whose value is ❰True❱+ ⇩+ ┌──────────────────────────────────┐+ │ < Left = True, Right : Natural > │ A union literal with two alternatives+ └──────────────────────────────────┘+++However, this value must be a term and not a type. For example, the following+values are $_NOT valid:+++ ┌──────────────────────────────────┐+ │ < Left = Text, Right : Natural > │ Invalid union literal+ └──────────────────────────────────┘+ ⇧+ This is a type and not a term+++ ┌───────────────────────────────┐+ │ < Left = Type, Right : Type > │ Invalid union type+ └───────────────────────────────┘+ ⇧+ This is a kind and not a term+++You provided a union literal with an alternative named:++↳ $txt0++... whose value is:++↳ $txt1++... which is not a term++Some common reasons why you might get this error:++● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one+ alternative:++ ┌────────────────────┐+ │ < Example = Text > │+ └────────────────────┘+ ⇧+ This could be ❰:❱ instead+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (InvalidAlternative k expr0) = ErrorMessages {..}+ where+ short = "Invalid alternative"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Every union type specifies the type of each alternative, like this:+++ The type of the first alternative is ❰Bool❱+ ⇩+ ┌──────────────────────────────────┐+ │ < Left : Bool, Right : Natural > │ A union type with two alternatives+ └──────────────────────────────────┘+ ⇧+ The type of the second alternative is ❰Natural❱+++However, these alternatives can only be annotated with types. For example, the+following union types are $_NOT valid:+++ ┌────────────────────────────┐+ │ < Left : Bool, Right : 1 > │ Invalid union type+ └────────────────────────────┘+ ⇧+ This is a term and not a type+++ ┌───────────────────────────────┐+ │ < Left : Bool, Right : Type > │ Invalid union type+ └───────────────────────────────┘+ ⇧+ This is a kind and not a type+++You provided a union type with an alternative named:++↳ $txt0++... annotated with the following expression which is not a type:++↳ $txt1++Some common reasons why you might get this error:++● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one+ alternative:++ ┌─────────────────┐+ │ < Example : 1 > │+ └─────────────────┘+ ⇧+ This could be ❰=❱ instead+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (DuplicateAlternative k) = ErrorMessages {..}+ where+ short = "Duplicate union alternative"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: Unions may not have two alternatives that share the same name++For example, the following expressions are $_NOT valid:+++ ┌─────────────────────────────┐+ │ < foo = True | foo : Text > │ Invalid: ❰foo❱ appears twice+ └─────────────────────────────┘+++ ┌───────────────────────────────────────┐+ │ < foo = 1 | bar : Bool | bar : Text > │ Invalid: ❰bar❱ appears twice+ └───────────────────────────────────────┘+++You have more than one alternative named:++↳ $txt0+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k)++prettyTypeMessage (MustCombineARecord expr0 expr1) = ErrorMessages {..}+ where+ short = "You can only combine records"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can combine records using the ❰∧❱ operator, like this:+++ ┌───────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ { baz = True } │+ └───────────────────────────────────────────┘+++ ┌─────────────────────────────────────────────┐+ │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │+ └─────────────────────────────────────────────┘+++... but you cannot combine values that are not records.++For example, the following expressions are $_NOT valid:+++ ┌──────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ 1 │+ └──────────────────────────────┘+ ⇧+ Invalid: Not a record+++ ┌───────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │+ └───────────────────────────────────────────┘+ ⇧+ Invalid: This is a record type and not a record+++ ┌───────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ < baz = True > │+ └───────────────────────────────────────────┘+ ⇧+ Invalid: This is a union and not a record+++You tried to combine the following value:++↳ $txt0++... which is not a record, but is actually a value of type:++↳ $txt1+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (FieldCollision ks) = ErrorMessages {..}+ where+ short = "Field collision"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can combine records if they don't share any fields in common,+like this:+++ ┌───────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ { baz = True } │+ └───────────────────────────────────────────┘+++ ┌────────────────────────────────────────┐+ │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │+ └────────────────────────────────────────┘+++... but you cannot merge two records that share the same field++For example, the following expression is $_NOT valid:+++ ┌───────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ { foo = True } │ Invalid: Colliding ❰foo❱ fields+ └───────────────────────────────────────────┘+++You combined two records that share the following field:++↳ $txt0++... which is not allowed++Some common reasons why you might get this error:++● You tried to use ❰∧❱ to update a field's value, like this:+++ ┌────────────────────────────────────────┐+ │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │+ └────────────────────────────────────────┘+ ⇧+ Invalid attempt to update ❰foo❱'s value to ❰2❱++ Field updates are intentionally not allowed as the Dhall language discourages+ patch-oriented programming+|]+ where+ txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks))++prettyTypeMessage (MustMergeARecord expr0 expr1) = ErrorMessages {..}+ where+ short = "❰merge❱ expects a record of handlers"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... but the first argument to ❰merge❱ must be a record and not some other type.++For example, the following expression is $_NOT valid:+++ ┌─────────────────────────────────────────┐+ │ let handler = λ(x : Bool) → x │+ │ in merge handler < Foo = True > : True │+ └─────────────────────────────────────────┘+ ⇧+ Invalid: ❰handler❱ isn't a record+++You provided the following handler:++↳ $txt0++... which is not a record, but is actually a value of type:++↳ $txt1++Some common reasons why you might get this error:++● You accidentally provide an empty record type instead of an empty record when+ you ❰merge❱ an empty union:+++ ┌──────────────────────────────────────────┐+ │ λ(x : <>) → λ(a : Type) → merge {} x : a │+ └──────────────────────────────────────────┘+ ⇧+ This should be ❰{=}❱ instead+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (MustMergeUnion expr0 expr1) = ErrorMessages {..}+ where+ short = "❰merge❱ expects a union"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... but the second argument to ❰merge❱ must be a union and not some other type.++For example, the following expression is $_NOT valid:+++ ┌──────────────────────────────────────────┐+ │ let handlers = { Foo = λ(x : Bool) → x } │+ │ in merge handlers True : True │+ └──────────────────────────────────────────┘+ ⇧+ Invalid: ❰True❱ isn't a union+++You tried to ❰merge❱ this expression:++↳ $txt0++... which is not a union, but is actually a value of type:++↳ $txt1+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (UnusedHandler ks) = ErrorMessages {..}+ where+ short = "Unused handler"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... but you must provide exactly one handler per alternative in the union. You+cannot supply extra handlers++For example, the following expression is $_NOT valid:+++ ┌───────────────────────────────────────┐+ │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing+ │ in let handlers = │ + │ { Left = Natural/even │+ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used+ │ } │+ │ in merge handlers union : Bool │+ └───────────────────────────────────────┘+++You provided the following handlers:++↳ $txt0++... which had no matching alternatives in the union you tried to ❰merge❱+|]+ where+ txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks))++prettyTypeMessage (MissingHandler ks) = ErrorMessages {..}+ where+ short = "Missing handler"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... but you must provide exactly one handler per alternative in the union. You+cannot omit any handlers++For example, the following expression is $_NOT valid:+++ Invalid: Missing ❰Right❱ handler+ ⇩+ ┌─────────────────────────────────────────────────┐+ │ let handlers = { Left = Natural/even } │+ │ in let union = < Left = +2 | Right : Bool > │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────┘+++Note that you need to provide handlers for other alternatives even if those+alternatives are never used++You need to supply the following handlers:++↳ $txt0+|]+ where+ txt0 = Text.toStrict (Text.intercalate ", " (Data.Set.toList ks))++prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =+ ErrorMessages {..}+ where+ short = "Wrong handler input type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... as long as the input type of each handler function matches the type of the+corresponding alternative:+++ ┌───────────────────────────────────────────────────────────┐+ │ union : < Left : Natural | Right : Bool > │+ └───────────────────────────────────────────────────────────┘+ ⇧ ⇧+ These must match These must match+ ⇩ ⇩+ ┌───────────────────────────────────────────────────────────┐+ │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │+ └───────────────────────────────────────────────────────────┘+++For example, the following expression is $_NOT valid:+++ Invalid: Doesn't match the type of the ❰Right❱ alternative+ ⇩+ ┌──────────────────────────────────────────────────────────────────────┐+ │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │+ │ in let union = < Left = +2 | Right : Bool > │+ │ in merge handlers union : Bool │+ └──────────────────────────────────────────────────────────────────────┘+++Your handler for the following alternative:++↳ $txt0++... needs to accept an input value of type:++↳ $txt1++... but actually accepts an input value of a different type:++↳ $txt2+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage (HandlerOutputTypeMismatch expr0 expr1 expr2) =+ ErrorMessages {..}+ where+ short = "Wrong handler output type"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... as long as the output type of each handler function matches the declared type+of the result:+++ ┌───────────────────────────────────────────────────────────┐+ │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │+ └───────────────────────────────────────────────────────────┘+ ⇧ ⇧+ These output types ...++ ... must match the declared type of the ❰merge❱+ ⇩+ ┌─────────────────────────────┐+ │ merge handlers union : Bool │+ └─────────────────────────────┘+++For example, the following expression is $_NOT valid:+++ ┌──────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Text │+ └──────────────────────────────────────────────────────────────────────┘+ ⇧+ Invalid: Doesn't match output of either handler+++Your handler for the following alternative:++↳ $txt0++... needs to return an output value of type:++↳ $txt1++... but actually returns an output value of a different type:++↳ $txt2+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)+ txt2 = Text.toStrict (Dhall.Core.pretty expr2)++prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..}+ where+ short = "Handler is not a function"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can ❰merge❱ the alternatives of a union using a record with one+handler per alternative, like this:+++ ┌─────────────────────────────────────────────────────────────────────┐+ │ let union = < Left = +2 | Right : Bool > │+ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │+ │ in merge handlers union : Bool │+ └─────────────────────────────────────────────────────────────────────┘+++... as long as each handler is a function++For example, the following expression is $_NOT valid:+++ ┌─────────────────────────────────────────┐+ │ merge { Foo = True } < Foo = 1 > : Bool │+ └─────────────────────────────────────────┘+ ⇧+ Invalid: Not a function+++Your handler for this alternative:++↳ $txt0++... has the following type:++↳ $txt1++... which is not the type of a function+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k)+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (NotARecord k expr0 expr1) = ErrorMessages {..}+ where+ short = "Not a record"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can only access fields on records, like this:+++ ┌─────────────────────────────────┐+ │ { foo = True, bar = "ABC" }.foo │ This is valid ...+ └─────────────────────────────────┘+++ ┌───────────────────────────────────────────┐+ │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this+ └───────────────────────────────────────────┘+++... but you cannot access fields on non-record expressions++For example, the following expression is $_NOT valid:+++ ┌───────┐+ │ 1.foo │+ └───────┘+ ⇧+ Invalid: Not a record+++You tried to access a field named:++↳ $txt0++... on the following expression which is not a record:++↳ $txt1++... but is actually an expression of type:++↳ $txt2++Some common reasons why you might get this error:++● You accidentally try to access a field of a union instead of a record, like+ this:+++ ┌─────────────────┐+ │ < foo : a >.foo │+ └─────────────────┘+ ⇧+ This is a union, not a record+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)+ txt2 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (MissingField k expr0) = ErrorMessages {..}+ where+ short = "Missing record field"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: You can only access fields on records, like this:+++ ┌─────────────────────────────────┐+ │ { foo = True, bar = "ABC" }.foo │ This is valid ...+ └─────────────────────────────────┘+++ ┌───────────────────────────────────────────┐+ │ λ(r : { foo : Bool, bar : Text }) → r.foo │ ... and so is this+ └───────────────────────────────────────────┘+++... but you can only access fields if they are present++For example, the following expression is $_NOT valid:++ ┌─────────────────────────────────┐+ │ { foo = True, bar = "ABC" }.qux │+ └─────────────────────────────────┘+ ⇧+ Invalid: the record has no ❰qux❱ field++You tried to access a field named:++↳ $txt0++... but the field is missing because the record only defines the following fields:++↳ $txt1+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty k )+ txt1 = Text.toStrict (Dhall.Core.pretty expr0)++prettyTypeMessage (CantAnd expr0 expr1) =+ buildBooleanOperator "&&" expr0 expr1++prettyTypeMessage (CantOr expr0 expr1) =+ buildBooleanOperator "||" expr0 expr1++prettyTypeMessage (CantEQ expr0 expr1) =+ buildBooleanOperator "==" expr0 expr1++prettyTypeMessage (CantNE expr0 expr1) =+ buildBooleanOperator "/=" expr0 expr1++prettyTypeMessage (CantTextAppend expr0 expr1) = ErrorMessages {..}+ where+ short = "❰++❱ only works on ❰Text❱"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱++For example, this is a valid use of ❰++❱: +++ ┌────────────────┐+ │ "ABC" ++ "DEF" │+ └────────────────┘+++You provided this argument:++↳ $txt0++... which does not have type ❰Text❱ but instead has type:++↳ $txt1++Some common reasons why you might get this error:++● You might have thought that ❰++❱ was the operator to combine two lists:++ ┌───────────────────────────────────────────────────────────┐+ │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │ Not valid+ └───────────────────────────────────────────────────────────┘++ The Dhall programming language does not provide a built-in operator for+ combining two lists+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (CantAdd expr0 expr1) =+ buildNaturalOperator "+" expr0 expr1++prettyTypeMessage (CantMultiply expr0 expr1) =+ buildNaturalOperator "*" expr0 expr1++prettyTypeMessage (NoDependentTypes expr0 expr1) = ErrorMessages {..}+ where+ short = "No dependent types"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The Dhall programming language does not allow functions from terms+to types. These function types are also known as "dependent function types"+because you have a type whose value "depends" on the value of a term.++For example, this is $_NOT a legal function type:+++ ┌─────────────┐+ │ Bool → Type │+ └─────────────┘+++Similarly, this is $_NOT legal code:+++ ┌────────────────────────────────────────────────────┐+ │ λ(Vector : Natural → Type → Type) → Vector +0 Text │+ └────────────────────────────────────────────────────┘+ ⇧+ Invalid dependent type+++Your function type is invalid because the input has type:++↳ $txt0++... and the output has kind:++↳ $txt1++... which makes this a forbidden dependent function type+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++prettyTypeMessage (NoDependentLet expr0 expr1) = ErrorMessages {..}+ where+ short = "No dependent ❰let❱"++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The Dhall programming language does not allow ❰let❱ expressions+from terms to types. These ❰let❱ expressions are also known as "dependent ❰let❱+expressions" because you have a type whose value depends on the value of a term.++The Dhall language forbids these dependent ❰let❱ expressions in order to+guarantee that ❰let❱ expressions of the form:+++ ┌────────────────────┐+ │ let x : t = r in e │+ └────────────────────┘+++... are always equivalent to:+++ ┌──────────────────┐+ │ (λ(x : t) → e) r │+ └──────────────────┘+++This means that both expressions should normalize to the same result and if one+of the two fails to type check then the other should fail to type check, too.++For this reason, the following is $_NOT legal code:+++ ┌───────────────────┐+ │ let x = 2 in Text │+ └───────────────────┘+++... because the above ❰let❱ expression is equivalent to:+++ ┌─────────────────────────────┐+ │ let x : Integer = 2 in Text │+ └─────────────────────────────┘+++... which in turn must be equivalent to:+++ ┌───────────────────────────┐+ │ (λ(x : Integer) → Text) 2 │+ └───────────────────────────┘+++... which in turn fails to type check because this sub-expression:+++ ┌───────────────────────┐+ │ λ(x : Integer) → Text │+ └───────────────────────┘+++... has type:+++ ┌───────────────────────┐+ │ ∀(x : Integer) → Text │+ └───────────────────────┘+++... which is a forbidden dependent function type (i.e. a function from a term to+a type). Therefore the equivalent ❰let❱ expression is also forbidden.++Your ❰let❱ expression is invalid because the input has type:++↳ $txt0++... and the output has kind:++↳ $txt1++... which makes this a forbidden dependent ❰let❱ expression+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++buildBooleanOperator :: Text -> Expr s X -> Expr s X -> ErrorMessages+buildBooleanOperator operator expr0 expr1 = ErrorMessages {..}+ where+ short =+ Builder.fromText+ (Data.Text.strip+ [NeatInterpolation.text|❰$txt2❱ only works on ❰Bool❱s|] )++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The ❰$txt2❱ operator expects two arguments that have type ❰Bool❱++For example, this is a valid use of ❰$txt2❱: +++ ┌───────────────┐+ │ True $txt2 False │+ └───────────────┘+++You provided this argument:++↳ $txt0++... which does not have type ❰Bool❱ but instead has type:++↳ $txt1+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++ txt2 = Text.toStrict operator++buildNaturalOperator :: Text -> Expr s X -> Expr s X -> ErrorMessages+buildNaturalOperator operator expr0 expr1 = ErrorMessages {..}+ where+ short =+ Builder.fromText+ (Data.Text.strip+ [NeatInterpolation.text|❰$txt2❱ only works on ❰Natural❱s|] )++ long =+ Builder.fromText [NeatInterpolation.text|+Explanation: The ❰$txt2❱ operator expects two arguments that have type ❰Natural❱++For example, this is a valid use of ❰$txt2❱: +++ ┌─────────┐+ │ +3 $txt2 +5 │+ └─────────┘+++You provided this argument:++↳ $txt0++... which does not have type ❰Natural❱ but instead has type:++↳ $txt1++Some common reasons why you might get this error:++● You might have tried to use an ❰Integer❱, which is $_NOT allowed:+++ ┌─────────────────────────────────────────┐+ │ λ(x : Integer) → λ(y : Integer) → x $txt2 y │ Not valid+ └─────────────────────────────────────────┘+++ You can only use ❰Natural❱ numbers+++● You might have mistakenly used an ❰Integer❱ literal, which is $_NOT allowed:+++ ┌───────┐+ │ 2 $txt2 2 │ Not valid+ └───────┘+++ You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱+ literals, like this:+++ ┌─────────┐+ │ +2 $txt2 +2 │ Valid+ └─────────┘+|]+ where+ txt0 = Text.toStrict (Dhall.Core.pretty expr0)+ txt1 = Text.toStrict (Dhall.Core.pretty expr1)++ txt2 = Text.toStrict operator++-- | A structured type error that includes context+data TypeError s = TypeError+ { context :: Context (Expr s X)+ , current :: Expr s X+ , typeMessage :: TypeMessage s+ } deriving (Typeable)++instance Buildable s => Show (TypeError s) where+ show = Text.unpack . Dhall.Core.pretty++instance (Buildable s, Typeable s) => Exception (TypeError s)++instance Buildable s => Buildable (TypeError s) where+ build (TypeError ctx expr msg)+ = ( if Text.null (Builder.toLazyText (buildContext ctx))+ then ""+ else buildContext ctx <> "\n"+ )+ <> shortTypeMessage msg <> "\n"+ <> source+ where+ buildKV (key, val) = build key <> " : " <> build val++ buildContext =+ build+ . Text.unlines+ . map (Builder.toLazyText . buildKV)+ . reverse+ . Dhall.Context.toList++ source = case expr of+ Note s _ -> build s+ _ -> mempty++newtype DetailedTypeError s = DetailedTypeError (TypeError s)+ deriving (Typeable)++instance Buildable s => Show (DetailedTypeError s) where+ show = Text.unpack . Dhall.Core.pretty++instance (Buildable s, Typeable s) => Exception (DetailedTypeError s)++instance Buildable s => Buildable (DetailedTypeError s) where+ build (DetailedTypeError (TypeError ctx expr msg))+ = ( if Text.null (Builder.toLazyText (buildContext ctx))+ then ""+ else buildContext ctx <> "\n"+ )+ <> longTypeMessage msg <> "\n"+ <> "────────────────────────────────────────────────────────────────────────────────\n"+ <> "\n"+ <> source+ where+ buildKV (key, val) = build key <> " : " <> build val++ buildContext =+ build+ . Text.unlines+ . map (Builder.toLazyText . buildKV)+ . reverse+ . Dhall.Context.toList++ source = case expr of+ Note s _ -> build s+ _ -> mempty