summaryrefslogtreecommitdiff
path: root/dhall/src/error/text/TypeMismatch.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/error/text/TypeMismatch.txt')
-rw-r--r--dhall/src/error/text/TypeMismatch.txt117
1 files changed, 0 insertions, 117 deletions
diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/error/text/TypeMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
- ┌───────────────────────────────┐
- │ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have type ❰Bool❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ Natural/even : Natural → Bool │ This built-in function only accepts
- └───────────────────────────────┘ arguments that have type ❰Natural❱
- ⇧
- The function's input type
-
-
- ┌───────────────────────────────┐
- │ λ(a : Type) → a : Type → Type │ This anonymous function only accepts
- └───────────────────────────────┘ arguments that have kind ❰Type❱
- ⇧
- The function's input kind
-
-
- ┌────────────────────┐
- │ List : Type → Type │ This built-in function only accepts arguments that
- └────────────────────┘ have kind ❰Type❱
- ⇧
- The function's input kind
-
-
-For example, the following expressions are valid:
-
-
- ┌────────────────────────┐
- │ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌─────────────────┐
- │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
- └─────────────────┘ argument that the ❰Natural/even❱ function accepts,
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
- └────────────────────────┘ of argument that the anonymous function accepts
-
-
- ┌───────────┐
- │ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
- └───────────┘ that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
- ┌───────────────────────┐
- │ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function
- └───────────────────────┘ expects an argument that has type ❰Bool❱
-
-
- ┌──────────────────┐
- │ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
- └──────────────────┘ expects an argument that has type ❰Natural❱
-
-
- ┌────────────────────────┐
- │ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
- └────────────────────────┘ function expects an argument of kind ❰Type❱
-
-
- ┌────────┐
- │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
- └────────┘ argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
- ┌────────────────────────────────────────┐
- │ List/head ([1, 2, 3] : List Integer) │
- └────────────────────────────────────────┘
- ⇧
- ❰List/head❱ is missing the first argument,
- which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
- ┌────────────────┐
- │ Natural/even 2 │
- └────────────────┘
- ⇧
- This should be ❰+2❱