summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/errors/AnnotMismatch.txt117
-rw-r--r--src/errors/CantTextAppend.txt28
-rw-r--r--src/errors/DuplicateAlternative.txt18
-rw-r--r--src/errors/FieldCollision.txt43
-rw-r--r--src/errors/HandlerInputTypeMismatch.txt49
-rw-r--r--src/errors/HandlerNotAFunction.txt32
-rw-r--r--src/errors/HandlerOutputTypeMismatch.txt51
-rw-r--r--src/errors/IfBranchMismatch.txt63
-rw-r--r--src/errors/IfBranchMustBeTerm.txt51
-rw-r--r--src/errors/InvalidAlterantive.txt48
-rw-r--r--src/errors/InvalidAlterantiveType.txt49
-rw-r--r--src/errors/InvalidField.txt35
-rw-r--r--src/errors/InvalidFieldType.txt34
-rw-r--r--src/errors/InvalidInputType.txt61
-rw-r--r--src/errors/InvalidListElement.txt30
-rw-r--r--src/errors/InvalidListType.txt43
-rw-r--r--src/errors/InvalidOptionType.txt44
-rw-r--r--src/errors/InvalidOptionalElement.txt29
-rw-r--r--src/errors/InvalidOptionalLiteral.txt53
-rw-r--r--src/errors/InvalidOutputType.txt68
-rw-r--r--src/errors/InvalidPredicate.txt51
-rw-r--r--src/errors/MissingField.txt30
-rw-r--r--src/errors/MissingHandler.txt32
-rw-r--r--src/errors/MustCombineARecord.txt46
-rw-r--r--src/errors/MustMergeARecord.txt43
-rw-r--r--src/errors/MustMergeUnion.txt31
-rw-r--r--src/errors/NoDependentLet.txt76
-rw-r--r--src/errors/NoDependentTypes.txt31
-rw-r--r--src/errors/NotAFunction.txt68
-rw-r--r--src/errors/NotARecord.txt48
-rw-r--r--src/errors/TypeMismatch.txt117
-rw-r--r--src/errors/UnboundVariable.txt97
-rw-r--r--src/errors/Untyped.txt117
-rw-r--r--src/errors/UnusedHandler.txt32
-rw-r--r--src/main.rs51
-rw-r--r--src/typecheck.rs38
36 files changed, 1828 insertions, 26 deletions
diff --git a/src/errors/AnnotMismatch.txt b/src/errors/AnnotMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/AnnotMismatch.txt
@@ -0,0 +1,117 @@
+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/src/errors/CantTextAppend.txt b/src/errors/CantTextAppend.txt
new file mode 100644
index 0000000..26b9ceb
--- /dev/null
+++ b/src/errors/CantTextAppend.txt
@@ -0,0 +1,28 @@
+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/src/errors/DuplicateAlternative.txt b/src/errors/DuplicateAlternative.txt
new file mode 100644
index 0000000..077f8aa
--- /dev/null
+++ b/src/errors/DuplicateAlternative.txt
@@ -0,0 +1,18 @@
+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/src/errors/FieldCollision.txt b/src/errors/FieldCollision.txt
new file mode 100644
index 0000000..2b2d260
--- /dev/null
+++ b/src/errors/FieldCollision.txt
@@ -0,0 +1,43 @@
+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/src/errors/HandlerInputTypeMismatch.txt b/src/errors/HandlerInputTypeMismatch.txt
new file mode 100644
index 0000000..7d3525b
--- /dev/null
+++ b/src/errors/HandlerInputTypeMismatch.txt
@@ -0,0 +1,49 @@
+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/src/errors/HandlerNotAFunction.txt b/src/errors/HandlerNotAFunction.txt
new file mode 100644
index 0000000..ff87443
--- /dev/null
+++ b/src/errors/HandlerNotAFunction.txt
@@ -0,0 +1,32 @@
+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/src/errors/HandlerOutputTypeMismatch.txt b/src/errors/HandlerOutputTypeMismatch.txt
new file mode 100644
index 0000000..f359459
--- /dev/null
+++ b/src/errors/HandlerOutputTypeMismatch.txt
@@ -0,0 +1,51 @@
+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/src/errors/IfBranchMismatch.txt b/src/errors/IfBranchMismatch.txt
new file mode 100644
index 0000000..a95b130
--- /dev/null
+++ b/src/errors/IfBranchMismatch.txt
@@ -0,0 +1,63 @@
+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/src/errors/IfBranchMustBeTerm.txt b/src/errors/IfBranchMustBeTerm.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/src/errors/IfBranchMustBeTerm.txt
@@ -0,0 +1,51 @@
+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/src/errors/InvalidAlterantive.txt b/src/errors/InvalidAlterantive.txt
new file mode 100644
index 0000000..391fc3a
--- /dev/null
+++ b/src/errors/InvalidAlterantive.txt
@@ -0,0 +1,48 @@
+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/src/errors/InvalidAlterantiveType.txt b/src/errors/InvalidAlterantiveType.txt
new file mode 100644
index 0000000..f5dadef
--- /dev/null
+++ b/src/errors/InvalidAlterantiveType.txt
@@ -0,0 +1,49 @@
+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/src/errors/InvalidField.txt b/src/errors/InvalidField.txt
new file mode 100644
index 0000000..bfbf106
--- /dev/null
+++ b/src/errors/InvalidField.txt
@@ -0,0 +1,35 @@
+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/src/errors/InvalidFieldType.txt b/src/errors/InvalidFieldType.txt
new file mode 100644
index 0000000..4f76a64
--- /dev/null
+++ b/src/errors/InvalidFieldType.txt
@@ -0,0 +1,34 @@
+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/src/errors/InvalidInputType.txt b/src/errors/InvalidInputType.txt
new file mode 100644
index 0000000..eabafa4
--- /dev/null
+++ b/src/errors/InvalidInputType.txt
@@ -0,0 +1,61 @@
+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/src/errors/InvalidListElement.txt b/src/errors/InvalidListElement.txt
new file mode 100644
index 0000000..59db7b7
--- /dev/null
+++ b/src/errors/InvalidListElement.txt
@@ -0,0 +1,30 @@
+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/src/errors/InvalidListType.txt b/src/errors/InvalidListType.txt
new file mode 100644
index 0000000..676647e
--- /dev/null
+++ b/src/errors/InvalidListType.txt
@@ -0,0 +1,43 @@
+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/src/errors/InvalidOptionType.txt b/src/errors/InvalidOptionType.txt
new file mode 100644
index 0000000..3bc81de
--- /dev/null
+++ b/src/errors/InvalidOptionType.txt
@@ -0,0 +1,44 @@
+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/src/errors/InvalidOptionalElement.txt b/src/errors/InvalidOptionalElement.txt
new file mode 100644
index 0000000..0254220
--- /dev/null
+++ b/src/errors/InvalidOptionalElement.txt
@@ -0,0 +1,29 @@
+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/src/errors/InvalidOptionalLiteral.txt b/src/errors/InvalidOptionalLiteral.txt
new file mode 100644
index 0000000..41c0fdc
--- /dev/null
+++ b/src/errors/InvalidOptionalLiteral.txt
@@ -0,0 +1,53 @@
+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/src/errors/InvalidOutputType.txt b/src/errors/InvalidOutputType.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/src/errors/InvalidOutputType.txt
@@ -0,0 +1,68 @@
+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/src/errors/InvalidPredicate.txt b/src/errors/InvalidPredicate.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/src/errors/InvalidPredicate.txt
@@ -0,0 +1,51 @@
+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/src/errors/MissingField.txt b/src/errors/MissingField.txt
new file mode 100644
index 0000000..de14a33
--- /dev/null
+++ b/src/errors/MissingField.txt
@@ -0,0 +1,30 @@
+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/src/errors/MissingHandler.txt b/src/errors/MissingHandler.txt
new file mode 100644
index 0000000..433445e
--- /dev/null
+++ b/src/errors/MissingHandler.txt
@@ -0,0 +1,32 @@
+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/src/errors/MustCombineARecord.txt b/src/errors/MustCombineARecord.txt
new file mode 100644
index 0000000..141b969
--- /dev/null
+++ b/src/errors/MustCombineARecord.txt
@@ -0,0 +1,46 @@
+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/src/errors/MustMergeARecord.txt b/src/errors/MustMergeARecord.txt
new file mode 100644
index 0000000..79094bd
--- /dev/null
+++ b/src/errors/MustMergeARecord.txt
@@ -0,0 +1,43 @@
+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/src/errors/MustMergeUnion.txt b/src/errors/MustMergeUnion.txt
new file mode 100644
index 0000000..68df70c
--- /dev/null
+++ b/src/errors/MustMergeUnion.txt
@@ -0,0 +1,31 @@
+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/src/errors/NoDependentLet.txt b/src/errors/NoDependentLet.txt
new file mode 100644
index 0000000..fdc65b4
--- /dev/null
+++ b/src/errors/NoDependentLet.txt
@@ -0,0 +1,76 @@
+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/src/errors/NoDependentTypes.txt b/src/errors/NoDependentTypes.txt
new file mode 100644
index 0000000..435bdcb
--- /dev/null
+++ b/src/errors/NoDependentTypes.txt
@@ -0,0 +1,31 @@
+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/src/errors/NotAFunction.txt b/src/errors/NotAFunction.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/src/errors/NotAFunction.txt
@@ -0,0 +1,68 @@
+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/src/errors/NotARecord.txt b/src/errors/NotARecord.txt
new file mode 100644
index 0000000..e0eebc8
--- /dev/null
+++ b/src/errors/NotARecord.txt
@@ -0,0 +1,48 @@
+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/src/errors/TypeMismatch.txt b/src/errors/TypeMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/TypeMismatch.txt
@@ -0,0 +1,117 @@
+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/src/errors/UnboundVariable.txt b/src/errors/UnboundVariable.txt
new file mode 100644
index 0000000..bd7d483
--- /dev/null
+++ b/src/errors/UnboundVariable.txt
@@ -0,0 +1,97 @@
+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/src/errors/Untyped.txt b/src/errors/Untyped.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/Untyped.txt
@@ -0,0 +1,117 @@
+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/src/errors/UnusedHandler.txt b/src/errors/UnusedHandler.txt
new file mode 100644
index 0000000..2e46a12
--- /dev/null
+++ b/src/errors/UnusedHandler.txt
@@ -0,0 +1,32 @@
+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❱
diff --git a/src/main.rs b/src/main.rs
index 6349ed7..d4b541b 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,6 +16,12 @@ pub mod parser;
pub mod typecheck;
use std::io::{self, Read};
+use std::error::Error;
+
+use term_painter::ToStyle;
+
+const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
+const BOLD: term_painter::Attr = term_painter::Attr::Bold;
fn print_error(message: &str, source: &str, start: usize, end: usize) {
let line_number = bytecount::count(source[..start].as_bytes(), '\n' as u8);
@@ -28,34 +34,30 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
let line_number_str = line_number.to_string();
let line_number_width = line_number_str.len();
- use term_painter::ToStyle;
- let err_style = term_painter::Color::Red;
- let bold = term_painter::Attr::Bold;
-
- bold.with(|| {
- err_style.with(|| {
+ BOLD.with(|| {
+ ERROR_STYLE.with(|| {
print!("error: ");
});
println!("{}", message);
});
- bold.with(|| {
+ BOLD.with(|| {
print!(" -->");
});
println!(" {}:{}:0", "(stdin)", line_number);
- bold.with(|| {
+ BOLD.with(|| {
println!("{:w$} |", "", w = line_number_width);
print!("{} |", line_number_str);
});
print!(" {}", context_prefix);
- bold.with(|| {
- err_style.with(|| {
+ BOLD.with(|| {
+ ERROR_STYLE.with(|| {
print!("{}", context_highlighted);
});
});
println!("{}", context_suffix);
- bold.with(|| {
+ BOLD.with(|| {
print!("{:w$} |", "", w = line_number_width);
- err_style.with(|| {
+ ERROR_STYLE.with(|| {
println!(" {:so$}{:^>ew$}", "", "",
so = source[line_start..start].chars().count(),
ew = ::std::cmp::max(1, source[start..end].chars().count()));
@@ -85,28 +87,31 @@ fn main() {
}
};
- println!("{:?}", expr);
-
/*
expr' <- load expr
*/
let type_expr = match typecheck::type_of(&expr) {
Err(e) => {
- println!("{:?}", e);
+ let explain = ::std::env::args().find(|s| s == "--explain").is_some();
+ if !explain {
+ term_painter::Color::BrightBlack.with(|| {
+ println!("Use \"dhall --explain\" for detailed errors");
+ });
+ }
+ ERROR_STYLE.with(|| print!("Error: "));
+ println!("{}", e.type_message.description());
+ if explain {
+ println!("{}", e.type_message);
+ }
+ println!("{}", e.current);
+ // FIXME Print source position
return;
}
Ok(type_expr) => type_expr,
};
+
println!("{}", type_expr);
println!("");
println!("{}", normalize::<_, X, _>(&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')) )
- */
}
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 12555b1..8abc64c 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -1,6 +1,7 @@
#![allow(non_snake_case)]
use std::collections::BTreeMap;
use std::collections::HashSet;
+use std::fmt;
use context::Context;
use core;
@@ -566,9 +567,9 @@ pub enum TypeMessage<'i, S> {
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<'i, S> {
- context: Context<'i, Expr<'i, S, X>>,
- current: Expr<'i, S, X>,
- type_message: TypeMessage<'i, S>,
+ pub context: Context<'i, Expr<'i, S, X>>,
+ pub current: Expr<'i, S, X>,
+ pub type_message: TypeMessage<'i, S>,
}
impl<'i, S: Clone> TypeError<'i, S> {
@@ -583,3 +584,34 @@ impl<'i, S: Clone> TypeError<'i, S> {
}
}
}
+
+impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
+ fn description(&self) -> &str {
+ match self {
+ &UnboundVariable => "Unbound variable",
+ &InvalidInputType(_) => "Invalid function input",
+ &InvalidOutputType(_) => "Invalid function output",
+ &NotAFunction(_, _) => "Not a function",
+ &TypeMismatch(_, _, _, _) => "Wrong type of function argument",
+ _ => "Unhandled error",
+ }
+ }
+}
+
+impl<'i, S> fmt::Display for TypeMessage<'i, S> {
+ fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+ match self {
+ &UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")),
+ &TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
+ let template = include_str!("errors/TypeMismatch.txt");
+ let s = template
+ .replace("$txt0", &format!("{}", e0))
+ .replace("$txt1", &format!("{}", e1))
+ .replace("$txt2", &format!("{}", e2))
+ .replace("$txt3", &format!("{}", e3));
+ f.write_str(&s)
+ }
+ _ => f.write_str("Unhandled error message"),
+ }
+ }
+}