1 files changed, 76 insertions, 0 deletions
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