From e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 1 Mar 2019 17:28:19 +0100 Subject: Split abnf_to_pest and dhall into their own crates --- dhall/src/errors/Untyped.txt | 117 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 117 insertions(+) create mode 100644 dhall/src/errors/Untyped.txt (limited to 'dhall/src/errors/Untyped.txt') 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❱ -- cgit v1.2.3