diff options
author | Nadrieril | 2019-05-07 18:12:04 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 18:12:04 +0200 |
commit | 3da450aa3fae23214aa982643b9bc4dd0ea4eaa6 (patch) | |
tree | 02e00cd008d2e7dc899b9211379596fe792f41c8 /dhall/src/error/text/TypeMismatch.txt | |
parent | d8a3e831fb67f86269c4baa99f9f0798a73a7247 (diff) | |
parent | 14dfeb8e7d2aa87a361a711a485243449426b144 (diff) |
Merge branch 'reorganize'
Diffstat (limited to 'dhall/src/error/text/TypeMismatch.txt')
-rw-r--r-- | dhall/src/error/text/TypeMismatch.txt | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt new file mode 100644 index 0000000..4904bf8 --- /dev/null +++ b/dhall/src/error/text/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❱ |