diff options
Diffstat (limited to 'dhall/src/errors')
34 files changed, 1765 insertions, 0 deletions
diff --git a/dhall/src/errors/AnnotMismatch.txt b/dhall/src/errors/AnnotMismatch.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/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/dhall/src/errors/CantTextAppend.txt b/dhall/src/errors/CantTextAppend.txt new file mode 100644 index 0000000..26b9ceb --- /dev/null +++ b/dhall/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/dhall/src/errors/DuplicateAlternative.txt b/dhall/src/errors/DuplicateAlternative.txt new file mode 100644 index 0000000..077f8aa --- /dev/null +++ b/dhall/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/dhall/src/errors/FieldCollision.txt b/dhall/src/errors/FieldCollision.txt new file mode 100644 index 0000000..2b2d260 --- /dev/null +++ b/dhall/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/dhall/src/errors/HandlerInputTypeMismatch.txt b/dhall/src/errors/HandlerInputTypeMismatch.txt new file mode 100644 index 0000000..7d3525b --- /dev/null +++ b/dhall/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/dhall/src/errors/HandlerNotAFunction.txt b/dhall/src/errors/HandlerNotAFunction.txt new file mode 100644 index 0000000..ff87443 --- /dev/null +++ b/dhall/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/dhall/src/errors/HandlerOutputTypeMismatch.txt b/dhall/src/errors/HandlerOutputTypeMismatch.txt new file mode 100644 index 0000000..f359459 --- /dev/null +++ b/dhall/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/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt new file mode 100644 index 0000000..a95b130 --- /dev/null +++ b/dhall/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/dhall/src/errors/IfBranchMustBeTerm.txt b/dhall/src/errors/IfBranchMustBeTerm.txt new file mode 100644 index 0000000..4c15881 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidAlterantive.txt b/dhall/src/errors/InvalidAlterantive.txt new file mode 100644 index 0000000..391fc3a --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidAlterantiveType.txt b/dhall/src/errors/InvalidAlterantiveType.txt new file mode 100644 index 0000000..f5dadef --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidField.txt b/dhall/src/errors/InvalidField.txt new file mode 100644 index 0000000..bfbf106 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidFieldType.txt b/dhall/src/errors/InvalidFieldType.txt new file mode 100644 index 0000000..4f76a64 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidInputType.txt b/dhall/src/errors/InvalidInputType.txt new file mode 100644 index 0000000..eabafa4 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidListElement.txt b/dhall/src/errors/InvalidListElement.txt new file mode 100644 index 0000000..59db7b7 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidListType.txt b/dhall/src/errors/InvalidListType.txt new file mode 100644 index 0000000..676647e --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidOptionType.txt b/dhall/src/errors/InvalidOptionType.txt new file mode 100644 index 0000000..3bc81de --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidOptionalElement.txt b/dhall/src/errors/InvalidOptionalElement.txt new file mode 100644 index 0000000..0254220 --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidOptionalLiteral.txt b/dhall/src/errors/InvalidOptionalLiteral.txt new file mode 100644 index 0000000..41c0fdc --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidOutputType.txt b/dhall/src/errors/InvalidOutputType.txt new file mode 100644 index 0000000..dd2695d --- /dev/null +++ b/dhall/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/dhall/src/errors/InvalidPredicate.txt b/dhall/src/errors/InvalidPredicate.txt new file mode 100644 index 0000000..4c15881 --- /dev/null +++ b/dhall/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/dhall/src/errors/MissingField.txt b/dhall/src/errors/MissingField.txt new file mode 100644 index 0000000..de14a33 --- /dev/null +++ b/dhall/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/dhall/src/errors/MissingHandler.txt b/dhall/src/errors/MissingHandler.txt new file mode 100644 index 0000000..433445e --- /dev/null +++ b/dhall/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/dhall/src/errors/MustCombineARecord.txt b/dhall/src/errors/MustCombineARecord.txt new file mode 100644 index 0000000..141b969 --- /dev/null +++ b/dhall/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/dhall/src/errors/MustMergeARecord.txt b/dhall/src/errors/MustMergeARecord.txt new file mode 100644 index 0000000..79094bd --- /dev/null +++ b/dhall/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/dhall/src/errors/MustMergeUnion.txt b/dhall/src/errors/MustMergeUnion.txt new file mode 100644 index 0000000..68df70c --- /dev/null +++ b/dhall/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/dhall/src/errors/NoDependentLet.txt b/dhall/src/errors/NoDependentLet.txt new file mode 100644 index 0000000..fdc65b4 --- /dev/null +++ b/dhall/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/dhall/src/errors/NoDependentTypes.txt b/dhall/src/errors/NoDependentTypes.txt new file mode 100644 index 0000000..435bdcb --- /dev/null +++ b/dhall/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/dhall/src/errors/NotAFunction.txt b/dhall/src/errors/NotAFunction.txt new file mode 100644 index 0000000..dd2695d --- /dev/null +++ b/dhall/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/dhall/src/errors/NotARecord.txt b/dhall/src/errors/NotARecord.txt new file mode 100644 index 0000000..e0eebc8 --- /dev/null +++ b/dhall/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/dhall/src/errors/TypeMismatch.txt b/dhall/src/errors/TypeMismatch.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/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/dhall/src/errors/UnboundVariable.txt b/dhall/src/errors/UnboundVariable.txt new file mode 100644 index 0000000..bd7d483 --- /dev/null +++ b/dhall/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/dhall/src/errors/Untyped.txt b/dhall/src/errors/Untyped.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/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/dhall/src/errors/UnusedHandler.txt b/dhall/src/errors/UnusedHandler.txt new file mode 100644 index 0000000..2e46a12 --- /dev/null +++ b/dhall/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❱ |