1 files changed, 63 insertions, 0 deletions
diff --git a/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt
new file mode 100644
index 0000000..a95b130
--- /dev/null
+++ b/dhall/src/errors/IfBranchMismatch.txt
@@ -0,0 +1,63 @@
+Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which
+is an expression:
+
+
+                   Expression for ❰then❱ branch
+                   ⇩
+    ┌────────────────────────────────┐
+    │ if True then "Hello, world!"   │
+    │         else "Goodbye, world!" │
+    └────────────────────────────────┘
+                   ⇧
+                   Expression for ❰else❱ branch
+
+
+These two expressions must have the same type.  For example, the following ❰if❱
+expressions are all valid:
+
+
+    ┌──────────────────────────────────┐
+    │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱
+    └──────────────────────────────────┘
+
+
+    ┌────────────────────────────┐
+    │ λ(b : Bool) →              │
+    │     if b then Natural/even │ Both branches have type ❰Natural → Bool❱
+    │          else Natural/odd  │
+    └────────────────────────────┘
+
+
+However, the following expression is $_NOT valid:
+
+
+                   This branch has type ❰Integer❱
+                   ⇩
+    ┌────────────────────────┐
+    │ if True then 0         │
+    │         else "ABC"     │
+    └────────────────────────┘
+                   ⇧
+                   This branch has type ❰Text❱
+
+
+The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is
+always ❰True❱ or ❰False❱
+
+Your ❰if❱ expression has the following ❰then❱ branch:
+
+↳ $txt0
+
+... which has type:
+
+↳ $txt2
+
+... and the following ❰else❱ branch:
+
+↳ $txt1
+
+... which has a different type:
+
+↳ $txt3
+
+Fix your ❰then❱ and ❰else❱ branches to have matching types