summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/error/text/AnnotMismatch.txt117
-rw-r--r--dhall/src/error/text/CantTextAppend.txt28
-rw-r--r--dhall/src/error/text/DuplicateAlternative.txt18
-rw-r--r--dhall/src/error/text/FieldCollision.txt43
-rw-r--r--dhall/src/error/text/HandlerInputTypeMismatch.txt49
-rw-r--r--dhall/src/error/text/HandlerNotAFunction.txt32
-rw-r--r--dhall/src/error/text/HandlerOutputTypeMismatch.txt51
-rw-r--r--dhall/src/error/text/IfBranchMismatch.txt63
-rw-r--r--dhall/src/error/text/IfBranchMustBeTerm.txt51
-rw-r--r--dhall/src/error/text/InvalidAlterantive.txt48
-rw-r--r--dhall/src/error/text/InvalidAlterantiveType.txt49
-rw-r--r--dhall/src/error/text/InvalidField.txt35
-rw-r--r--dhall/src/error/text/InvalidFieldType.txt34
-rw-r--r--dhall/src/error/text/InvalidInputType.txt61
-rw-r--r--dhall/src/error/text/InvalidListElement.txt30
-rw-r--r--dhall/src/error/text/InvalidListType.txt43
-rw-r--r--dhall/src/error/text/InvalidOptionType.txt44
-rw-r--r--dhall/src/error/text/InvalidOptionalElement.txt29
-rw-r--r--dhall/src/error/text/InvalidOptionalLiteral.txt53
-rw-r--r--dhall/src/error/text/InvalidOutputType.txt68
-rw-r--r--dhall/src/error/text/InvalidPredicate.txt51
-rw-r--r--dhall/src/error/text/MissingField.txt30
-rw-r--r--dhall/src/error/text/MissingHandler.txt32
-rw-r--r--dhall/src/error/text/MustCombineARecord.txt46
-rw-r--r--dhall/src/error/text/MustMergeARecord.txt43
-rw-r--r--dhall/src/error/text/MustMergeUnion.txt31
-rw-r--r--dhall/src/error/text/NoDependentLet.txt76
-rw-r--r--dhall/src/error/text/NoDependentTypes.txt31
-rw-r--r--dhall/src/error/text/NotAFunction.txt68
-rw-r--r--dhall/src/error/text/NotARecord.txt48
-rw-r--r--dhall/src/error/text/TypeMismatch.txt117
-rw-r--r--dhall/src/error/text/UnboundVariable.txt97
-rw-r--r--dhall/src/error/text/Untyped.txt117
-rw-r--r--dhall/src/error/text/UnusedHandler.txt32
34 files changed, 0 insertions, 1765 deletions
diff --git a/dhall/src/error/text/AnnotMismatch.txt b/dhall/src/error/text/AnnotMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/error/text/AnnotMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-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❱
diff --git a/dhall/src/error/text/CantTextAppend.txt b/dhall/src/error/text/CantTextAppend.txt
deleted file mode 100644
index 26b9ceb..0000000
--- a/dhall/src/error/text/CantTextAppend.txt
+++ /dev/null
@@ -1,28 +0,0 @@
-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
diff --git a/dhall/src/error/text/DuplicateAlternative.txt b/dhall/src/error/text/DuplicateAlternative.txt
deleted file mode 100644
index 077f8aa..0000000
--- a/dhall/src/error/text/DuplicateAlternative.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-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
diff --git a/dhall/src/error/text/FieldCollision.txt b/dhall/src/error/text/FieldCollision.txt
deleted file mode 100644
index 2b2d260..0000000
--- a/dhall/src/error/text/FieldCollision.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-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
diff --git a/dhall/src/error/text/HandlerInputTypeMismatch.txt b/dhall/src/error/text/HandlerInputTypeMismatch.txt
deleted file mode 100644
index 7d3525b..0000000
--- a/dhall/src/error/text/HandlerInputTypeMismatch.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-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
diff --git a/dhall/src/error/text/HandlerNotAFunction.txt b/dhall/src/error/text/HandlerNotAFunction.txt
deleted file mode 100644
index ff87443..0000000
--- a/dhall/src/error/text/HandlerNotAFunction.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-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
diff --git a/dhall/src/error/text/HandlerOutputTypeMismatch.txt b/dhall/src/error/text/HandlerOutputTypeMismatch.txt
deleted file mode 100644
index f359459..0000000
--- a/dhall/src/error/text/HandlerOutputTypeMismatch.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-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
diff --git a/dhall/src/error/text/IfBranchMismatch.txt b/dhall/src/error/text/IfBranchMismatch.txt
deleted file mode 100644
index a95b130..0000000
--- a/dhall/src/error/text/IfBranchMismatch.txt
+++ /dev/null
@@ -1,63 +0,0 @@
-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
diff --git a/dhall/src/error/text/IfBranchMustBeTerm.txt b/dhall/src/error/text/IfBranchMustBeTerm.txt
deleted file mode 100644
index 4c15881..0000000
--- a/dhall/src/error/text/IfBranchMustBeTerm.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidAlterantive.txt b/dhall/src/error/text/InvalidAlterantive.txt
deleted file mode 100644
index 391fc3a..0000000
--- a/dhall/src/error/text/InvalidAlterantive.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidAlterantiveType.txt b/dhall/src/error/text/InvalidAlterantiveType.txt
deleted file mode 100644
index f5dadef..0000000
--- a/dhall/src/error/text/InvalidAlterantiveType.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidField.txt b/dhall/src/error/text/InvalidField.txt
deleted file mode 100644
index bfbf106..0000000
--- a/dhall/src/error/text/InvalidField.txt
+++ /dev/null
@@ -1,35 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidFieldType.txt b/dhall/src/error/text/InvalidFieldType.txt
deleted file mode 100644
index 4f76a64..0000000
--- a/dhall/src/error/text/InvalidFieldType.txt
+++ /dev/null
@@ -1,34 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidInputType.txt b/dhall/src/error/text/InvalidInputType.txt
deleted file mode 100644
index eabafa4..0000000
--- a/dhall/src/error/text/InvalidInputType.txt
+++ /dev/null
@@ -1,61 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidListElement.txt b/dhall/src/error/text/InvalidListElement.txt
deleted file mode 100644
index 59db7b7..0000000
--- a/dhall/src/error/text/InvalidListElement.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidListType.txt b/dhall/src/error/text/InvalidListType.txt
deleted file mode 100644
index 676647e..0000000
--- a/dhall/src/error/text/InvalidListType.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-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❱
diff --git a/dhall/src/error/text/InvalidOptionType.txt b/dhall/src/error/text/InvalidOptionType.txt
deleted file mode 100644
index 3bc81de..0000000
--- a/dhall/src/error/text/InvalidOptionType.txt
+++ /dev/null
@@ -1,44 +0,0 @@
-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❱
-
diff --git a/dhall/src/error/text/InvalidOptionalElement.txt b/dhall/src/error/text/InvalidOptionalElement.txt
deleted file mode 100644
index 0254220..0000000
--- a/dhall/src/error/text/InvalidOptionalElement.txt
+++ /dev/null
@@ -1,29 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidOptionalLiteral.txt b/dhall/src/error/text/InvalidOptionalLiteral.txt
deleted file mode 100644
index 41c0fdc..0000000
--- a/dhall/src/error/text/InvalidOptionalLiteral.txt
+++ /dev/null
@@ -1,53 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidOutputType.txt b/dhall/src/error/text/InvalidOutputType.txt
deleted file mode 100644
index dd2695d..0000000
--- a/dhall/src/error/text/InvalidOutputType.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-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
diff --git a/dhall/src/error/text/InvalidPredicate.txt b/dhall/src/error/text/InvalidPredicate.txt
deleted file mode 100644
index 4c15881..0000000
--- a/dhall/src/error/text/InvalidPredicate.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-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
diff --git a/dhall/src/error/text/MissingField.txt b/dhall/src/error/text/MissingField.txt
deleted file mode 100644
index de14a33..0000000
--- a/dhall/src/error/text/MissingField.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-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
diff --git a/dhall/src/error/text/MissingHandler.txt b/dhall/src/error/text/MissingHandler.txt
deleted file mode 100644
index 433445e..0000000
--- a/dhall/src/error/text/MissingHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-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
diff --git a/dhall/src/error/text/MustCombineARecord.txt b/dhall/src/error/text/MustCombineARecord.txt
deleted file mode 100644
index 141b969..0000000
--- a/dhall/src/error/text/MustCombineARecord.txt
+++ /dev/null
@@ -1,46 +0,0 @@
-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:
-
-↳ $txt1
diff --git a/dhall/src/error/text/MustMergeARecord.txt b/dhall/src/error/text/MustMergeARecord.txt
deleted file mode 100644
index 79094bd..0000000
--- a/dhall/src/error/text/MustMergeARecord.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-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
diff --git a/dhall/src/error/text/MustMergeUnion.txt b/dhall/src/error/text/MustMergeUnion.txt
deleted file mode 100644
index 68df70c..0000000
--- a/dhall/src/error/text/MustMergeUnion.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-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
diff --git a/dhall/src/error/text/NoDependentLet.txt b/dhall/src/error/text/NoDependentLet.txt
deleted file mode 100644
index fdc65b4..0000000
--- a/dhall/src/error/text/NoDependentLet.txt
+++ /dev/null
@@ -1,76 +0,0 @@
-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
diff --git a/dhall/src/error/text/NoDependentTypes.txt b/dhall/src/error/text/NoDependentTypes.txt
deleted file mode 100644
index 435bdcb..0000000
--- a/dhall/src/error/text/NoDependentTypes.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-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
diff --git a/dhall/src/error/text/NotAFunction.txt b/dhall/src/error/text/NotAFunction.txt
deleted file mode 100644
index dd2695d..0000000
--- a/dhall/src/error/text/NotAFunction.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-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
diff --git a/dhall/src/error/text/NotARecord.txt b/dhall/src/error/text/NotARecord.txt
deleted file mode 100644
index e0eebc8..0000000
--- a/dhall/src/error/text/NotARecord.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-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
diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/error/text/TypeMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-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❱
diff --git a/dhall/src/error/text/UnboundVariable.txt b/dhall/src/error/text/UnboundVariable.txt
deleted file mode 100644
index bd7d483..0000000
--- a/dhall/src/error/text/UnboundVariable.txt
+++ /dev/null
@@ -1,97 +0,0 @@
-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
diff --git a/dhall/src/error/text/Untyped.txt b/dhall/src/error/text/Untyped.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/error/text/Untyped.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-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❱
diff --git a/dhall/src/error/text/UnusedHandler.txt b/dhall/src/error/text/UnusedHandler.txt
deleted file mode 100644
index 2e46a12..0000000
--- a/dhall/src/error/text/UnusedHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-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❱