summaryrefslogtreecommitdiff
path: root/dhall/src/errors/InvalidOutputType.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/errors/InvalidOutputType.txt')
-rw-r--r--dhall/src/errors/InvalidOutputType.txt68
1 files changed, 68 insertions, 0 deletions
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