Move ui outputs to a sensible place

105 files changed, 600 insertions, 0 deletions

diff --git a/dhall/tests/type-inference/failure/SortInLet.txt b/dhall/tests/type-inference/failure/SortInLet.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/SortInLet.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt
new file mode 100644
index 0000000..6b99615
--- /dev/null
+++ b/dhall/tests/type-inference/failure/hurkensParadox.txt
@@ -0,0 +1,15 @@
+Type error: error: wrong type of function argument
+  --> <current file>:6:23
+   |
+ 1 |     let bottom : Type = ∀(any : Type) → any
+ 2 | 
+ 3 | in  let not : Type → Type = λ(p : Type) → p → bottom
+ 4 | 
+...
+10 |         : pow (pow U) → U
+11 |         =   λ(t : pow (pow U))
+   |                        ^^^ this expects an argument of type: Kind
+   |                            ^ but this has type: Sort
+   |
+   = note: expected type `Kind`
+              found type `Sort`
diff --git a/dhall/tests/type-inference/failure/mixedUnions.txt b/dhall/tests/type-inference/failure/mixedUnions.txt
new file mode 100644
index 0000000..8e0026d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/mixedUnions.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | < Left : Natural | Right : Type >
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
new file mode 100644
index 0000000..2a754fc
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+ --> <current file>:1:0
+  |
+1 | { x = 1 } : { y : Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
new file mode 100644
index 0000000..e67edb8
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+ --> <current file>:1:0
+  |
+1 | { x = 1 } : { x : Text }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/AssertAlphaTrap.txt b/dhall/tests/type-inference/failure/unit/AssertAlphaTrap.txt
new file mode 100644
index 0000000..7e27d00
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AssertAlphaTrap.txt
@@ -0,0 +1,6 @@
+Type error: error: unbound variable ``_``
+ --> <current file>:1:46
+  |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+  |                                               ^ not found in this scope
+  |
diff --git a/dhall/tests/type-inference/failure/unit/AssertDoubleZeros.txt b/dhall/tests/type-inference/failure/unit/AssertDoubleZeros.txt
new file mode 100644
index 0000000..12231a0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AssertDoubleZeros.txt
@@ -0,0 +1,6 @@
+Type error: error: AssertMismatch
+ --> <current file>:1:0
+  |
+1 | assert : -0.0 ≡ +0.0
+  | ^^^^^^^^^^^^^^^^^^^^ AssertMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/AssertNotEquivalence.txt b/dhall/tests/type-inference/failure/unit/AssertNotEquivalence.txt
new file mode 100644
index 0000000..5973d19
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AssertNotEquivalence.txt
@@ -0,0 +1,6 @@
+Type error: error: AssertMustTakeEquivalence
+ --> <current file>:1:0
+  |
+1 | assert : Bool
+  | ^^^^^^^^^^^^^ AssertMustTakeEquivalence
+  |
diff --git a/dhall/tests/type-inference/failure/unit/AssertTriviallyFalse.txt b/dhall/tests/type-inference/failure/unit/AssertTriviallyFalse.txt
new file mode 100644
index 0000000..5742022
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/AssertTriviallyFalse.txt
@@ -0,0 +1,6 @@
+Type error: error: AssertMismatch
+ --> <current file>:1:0
+  |
+1 | assert : 1 === 2
+  | ^^^^^^^^^^^^^^^^ AssertMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
new file mode 100644
index 0000000..d0a9a01
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
@@ -0,0 +1,7 @@
+Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+ --> <current file>:1:4
+  |
+...
+6 | in  Example::{=}
+  |     ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
new file mode 100644
index 0000000..d4639e9
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
@@ -0,0 +1,7 @@
+Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ --> <current file>:1:4
+  |
+...
+6 | in  Example::{=}
+  |     ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
new file mode 100644
index 0000000..0839742
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
@@ -0,0 +1,7 @@
+Type error: error: annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+ --> <current file>:1:4
+  |
+...
+6 | in  Example::{ nam = "John Doe" }
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
new file mode 100644
index 0000000..7edef95
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
@@ -0,0 +1,7 @@
+Type error: error: annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ --> <current file>:1:4
+  |
+...
+6 | in  Example::{ name = True }
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+  |
diff --git a/dhall/tests/type-inference/failure/unit/EmptyToMap.txt b/dhall/tests/type-inference/failure/unit/EmptyToMap.txt
new file mode 100644
index 0000000..000fac7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/EmptyToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` applied to an empty record requires a type annotation
+ --> <current file>:1:0
+  |
+1 | toMap {=}
+  | ^^^^^^^^^ `toMap` applied to an empty record requires a type annotation
+  |
diff --git a/dhall/tests/type-inference/failure/unit/EquivalenceNotSameType.txt b/dhall/tests/type-inference/failure/unit/EquivalenceNotSameType.txt
new file mode 100644
index 0000000..12e21e4
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/EquivalenceNotSameType.txt
@@ -0,0 +1,6 @@
+Type error: error: EquivalenceTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 === False
+  | ^^^^^^^^^^^ EquivalenceTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/EquivalenceNotTerms.txt b/dhall/tests/type-inference/failure/unit/EquivalenceNotTerms.txt
new file mode 100644
index 0000000..0183c60
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/EquivalenceNotTerms.txt
@@ -0,0 +1,6 @@
+Type error: error: EquivalenceArgumentsMustBeTerms
+ --> <current file>:1:0
+  |
+1 | Bool === Bool
+  | ^^^^^^^^^^^^^ EquivalenceArgumentsMustBeTerms
+  |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-inference/failure/unit/FunctionApplicationArgumentNotMatch.txt
new file mode 100644
index 0000000..07278b8
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionApplicationArgumentNotMatch.txt
@@ -0,0 +1,9 @@
+Type error: error: wrong type of function argument
+ --> <current file>:1:1
+  |
+1 | (λ(_ : Natural) → _) True
+  |  ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+  |                      ^^^^ but this has type: Bool
+  |
+  = note: expected type `Natural`
+             found type `Bool`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-inference/failure/unit/FunctionApplicationIsNotFunction.txt
new file mode 100644
index 0000000..e46904a
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionApplicationIsNotFunction.txt
@@ -0,0 +1,6 @@
+Type error: error: expected function, found `Bool`
+ --> <current file>:1:0
+  |
+1 | True True
+  | ^^^^ function application requires a function
+  |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
new file mode 100644
index 0000000..e84eb15
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -0,0 +1,7 @@
+Type error: error: Invalid input type: `Natural`
+ --> <current file>:1:6
+  |
+1 | λ(_ : 1) → _
+  |       ^ this has type: `Natural`
+  |
+  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
new file mode 100644
index 0000000..4aa0f4f
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -0,0 +1,7 @@
+Type error: error: Invalid input type: `Natural`
+ --> <current file>:1:0
+  |
+1 | 2 → _
+  | ^ this has type: `Natural`
+  |
+  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/HeterogenousToMap.txt b/dhall/tests/type-inference/failure/unit/HeterogenousToMap.txt
new file mode 100644
index 0000000..2f8abf2
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/HeterogenousToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: Every field of the record must have the same type
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= "Bar" }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Every field of the record must have the same type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/IfBranchesNotMatch.txt b/dhall/tests/type-inference/failure/unit/IfBranchesNotMatch.txt
new file mode 100644
index 0000000..d58af95
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/IfBranchesNotMatch.txt
@@ -0,0 +1,6 @@
+Type error: error: IfBranchMismatch
+ --> <current file>:1:0
+  |
+1 | if True then 1 else ""
+  | ^^^^^^^^^^^^^^^^^^^^^^ IfBranchMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/IfBranchesNotType.txt b/dhall/tests/type-inference/failure/unit/IfBranchesNotType.txt
new file mode 100644
index 0000000..b70ac5f
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/IfBranchesNotType.txt
@@ -0,0 +1,6 @@
+Type error: error: IfBranchMustBeTerm
+ --> <current file>:1:0
+  |
+1 | if True then Type else Type
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ IfBranchMustBeTerm
+  |
diff --git a/dhall/tests/type-inference/failure/unit/IfNotBool.txt b/dhall/tests/type-inference/failure/unit/IfNotBool.txt
new file mode 100644
index 0000000..eb5ff42
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/IfNotBool.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidPredicate
+ --> <current file>:1:0
+  |
+1 | if 1 then 1 else 1
+  | ^^^^^^^^^^^^^^^^^^ InvalidPredicate
+  |
diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
new file mode 100644
index 0000000..5ba4b35
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: (True : Bool) : Natural
+ --> <current file>:1:8
+  |
+1 | let x : Natural = True in True
+  |         ^^^^^^^ annot mismatch: (True : Bool) : Natural
+  |
diff --git a/dhall/tests/type-inference/failure/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-inference/failure/unit/ListLiteralEmptyNotType.txt
new file mode 100644
index 0000000..2ca5819
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/ListLiteralEmptyNotType.txt
@@ -0,0 +1,9 @@
+Type error: error: wrong type of function argument
+ --> <current file>:1:5
+  |
+1 | [] : List Type
+  |      ^^^^ this expects an argument of type: Type
+  |           ^^^^ but this has type: Kind
+  |
+  = note: expected type `Type`
+             found type `Kind`
diff --git a/dhall/tests/type-inference/failure/unit/ListLiteralNotType.txt b/dhall/tests/type-inference/failure/unit/ListLiteralNotType.txt
new file mode 100644
index 0000000..62d69e5
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/ListLiteralNotType.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidListType
+ --> <current file>:1:0
+  |
+1 | [ Bool ]
+  | ^^^^^^^^ InvalidListType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-inference/failure/unit/ListLiteralTypesNotMatch.txt
new file mode 100644
index 0000000..33e007d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/ListLiteralTypesNotMatch.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidListElement
+ --> <current file>:1:0
+  |
+1 | [ True, 1 ]
+  | ^^^^^^^^^^^ InvalidListElement
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-inference/failure/unit/MergeAlternativeHasNoHandler.txt
new file mode 100644
index 0000000..a4a967a
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeAlternativeHasNoHandler.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeVariantMissingHandler
+ --> <current file>:1:0
+  |
+1 | merge {=} (< x : Bool >.x True)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ MergeVariantMissingHandler
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-inference/failure/unit/MergeAnnotationMismatch.txt
new file mode 100644
index 0000000..9175f33
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeAnnotationMismatch.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeAnnotMismatch
+ --> <current file>:1:0
+  |
+1 | merge { x = 0 } < x >.x : Bool
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ MergeAnnotMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeAnnotationNotType.txt b/dhall/tests/type-inference/failure/unit/MergeAnnotationNotType.txt
new file mode 100644
index 0000000..1173f0c
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeAnnotationNotType.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:0
+  |
+1 | merge {=} <> : Type
+  | ^^^^^^^^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation1.txt
new file mode 100644
index 0000000..94442e0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation1.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeEmptyNeedsAnnotation
+ --> <current file>:1:13
+  |
+1 | \(x: <>) -> (merge {=} x) : Bool
+  |              ^^^^^^^^^^^ MergeEmptyNeedsAnnotation
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation2.txt
new file mode 100644
index 0000000..5dcffdf
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeEmptyNeedsDirectAnnotation2.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeEmptyNeedsAnnotation
+ --> <current file>:1:26
+  |
+1 | \(x: <>) -> let y: Bool = merge {=} x in 1
+  |                           ^^^^^^^^^^^ MergeEmptyNeedsAnnotation
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-inference/failure/unit/MergeEmptyWithoutAnnotation.txt
new file mode 100644
index 0000000..bf45123
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeEmptyWithoutAnnotation.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:0
+  |
+1 | merge {=} <>
+  | ^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-inference/failure/unit/MergeHandlerNotFunction.txt
new file mode 100644
index 0000000..8528f90
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeHandlerNotFunction.txt
@@ -0,0 +1,9 @@
+Type error: error: merge handler is not a function
+ --> <current file>:1:0
+  |
+1 | merge { x = True } (< x : Bool >.x True)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+  |       ^^^^^^^^^^^^ the handler for `x` has type: `Bool`
+  |                     ------------------- help: the corresponding variant has type: `Bool`
+  |
+  = help: a handler for this variant must be a function that takes an input of type: `Bool`
diff --git a/dhall/tests/type-inference/failure/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-inference/failure/unit/MergeHandlerNotInUnion.txt
new file mode 100644
index 0000000..3159340
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeHandlerNotInUnion.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:0
+  |
+1 | merge { x = λ(_ : Bool) → _ } <> : Bool
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-inference/failure/unit/MergeHandlerNotMatchAlternativeType.txt
new file mode 100644
index 0000000..c2229bd
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -0,0 +1,8 @@
+Type error: error: Wrong handler input type
+ --> <current file>:1:0
+  |
+1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+  |       ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `x` expects a value of type: `Bool`
+  |                                ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural`
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-inference/failure/unit/MergeHandlersWithDifferentType.txt
new file mode 100644
index 0000000..47f3de7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeHandlersWithDifferentType.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeHandlerTypeMismatch
+ --> <current file>:1:0
+  |
+1 | merge { x = λ(_ : Bool) → _, y = λ(_ : Natural) → _ } (< x : Bool | y : Natural >.x True)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ MergeHandlerTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/MergeLhsNotRecord.txt
new file mode 100644
index 0000000..f27dddd
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeLhsNotRecord.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge1ArgMustBeRecord
+ --> <current file>:1:0
+  |
+1 | merge True < x >.x
+  | ^^^^^^^^^^^^^^^^^^ Merge1ArgMustBeRecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeMissingHandler1.txt b/dhall/tests/type-inference/failure/unit/MergeMissingHandler1.txt
new file mode 100644
index 0000000..af58d05
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeMissingHandler1.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeVariantMissingHandler
+ --> <current file>:1:0
+  |
+1 | merge {=} <x>.x
+  | ^^^^^^^^^^^^^^^ MergeVariantMissingHandler
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeMissingHandler2.txt b/dhall/tests/type-inference/failure/unit/MergeMissingHandler2.txt
new file mode 100644
index 0000000..49484df
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeMissingHandler2.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeVariantMissingHandler
+ --> <current file>:1:0
+  |
+1 | merge { x = 0 } <x | y>.x
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^ MergeVariantMissingHandler
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeRhsNotUnion.txt b/dhall/tests/type-inference/failure/unit/MergeRhsNotUnion.txt
new file mode 100644
index 0000000..0108725
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeRhsNotUnion.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:0
+  |
+1 | merge {=} True
+  | ^^^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MergeUnusedHandler.txt b/dhall/tests/type-inference/failure/unit/MergeUnusedHandler.txt
new file mode 100644
index 0000000..2afe376
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeUnusedHandler.txt
@@ -0,0 +1,6 @@
+Type error: error: MergeHandlerMissingVariant
+ --> <current file>:1:0
+  |
+1 | merge { x = 1, y = 2 } < x >.x
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ MergeHandlerMissingVariant
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MistypedToMap1.txt b/dhall/tests/type-inference/failure/unit/MistypedToMap1.txt
new file mode 100644
index 0000000..14d9791
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MistypedToMap1.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : Natural
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MistypedToMap2.txt b/dhall/tests/type-inference/failure/unit/MistypedToMap2.txt
new file mode 100644
index 0000000..88e303e
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MistypedToMap2.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List Natural
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MistypedToMap3.txt b/dhall/tests/type-inference/failure/unit/MistypedToMap3.txt
new file mode 100644
index 0000000..6b3772d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MistypedToMap3.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Natural, mapValue : Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/MistypedToMap4.txt b/dhall/tests/type-inference/failure/unit/MistypedToMap4.txt
new file mode 100644
index 0000000..e0cf651
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MistypedToMap4.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Text, mapValue : Text }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-inference/failure/unit/NaturalSubtractNotNatural.txt
new file mode 100644
index 0000000..ac336a6
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NaturalSubtractNotNatural.txt
@@ -0,0 +1,9 @@
+Type error: error: wrong type of function argument
+ --> <current file>:1:0
+  |
+1 | Natural/subtract True True
+  | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+  |                  ^^^^ but this has type: Bool
+  |
+  = note: expected type `Natural`
+             found type `Bool`
diff --git a/dhall/tests/type-inference/failure/unit/NonRecordToMap.txt b/dhall/tests/type-inference/failure/unit/NonRecordToMap.txt
new file mode 100644
index 0000000..8e83002
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NonRecordToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: The argument to `toMap` must be a record
+ --> <current file>:1:0
+  |
+1 | toMap "text"
+  | ^^^^^^^^^^^^ The argument to `toMap` must be a record
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorAndNotBool.txt b/dhall/tests/type-inference/failure/unit/OperatorAndNotBool.txt
new file mode 100644
index 0000000..f6ea50b
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorAndNotBool.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 && 1
+  | ^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorEqualNotBool.txt b/dhall/tests/type-inference/failure/unit/OperatorEqualNotBool.txt
new file mode 100644
index 0000000..8662c16
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorEqualNotBool.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 == 1
+  | ^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateLhsNotList.txt
new file mode 100644
index 0000000..8075b99
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateLhsNotList.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 # [ True ]
+  | ^^^^^^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateListsNotMatch.txt
new file mode 100644
index 0000000..9e404f8
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateListsNotMatch.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | [ True ] # [ 1 ]
+  | ^^^^^^^^^^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateNotListsButMatch.txt
new file mode 100644
index 0000000..fffc898
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateNotListsButMatch.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 # 2
+  | ^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateRhsNotList.txt
new file mode 100644
index 0000000..2ba0b91
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorListConcatenateRhsNotList.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | [ True ] # 1
+  | ^^^^^^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-inference/failure/unit/OperatorNotEqualNotBool.txt
new file mode 100644
index 0000000..ac04fd4
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorNotEqualNotBool.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 != 1
+  | ^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorOrNotBool.txt b/dhall/tests/type-inference/failure/unit/OperatorOrNotBool.txt
new file mode 100644
index 0000000..9e1c4fb
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorOrNotBool.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 || 1
+  | ^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-inference/failure/unit/OperatorPlusNotNatural.txt
new file mode 100644
index 0000000..97e0df4
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorPlusNotNatural.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | True + True
+  | ^^^^^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateLhsNotText.txt
new file mode 100644
index 0000000..679d991
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateLhsNotText.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | 1 ++ ""
+  | ^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateRhsNotText.txt
new file mode 100644
index 0000000..85611f7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorTextConcatenateRhsNotText.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | "" ++ 1
+  | ^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-inference/failure/unit/OperatorTimesNotNatural.txt
new file mode 100644
index 0000000..d688ed6
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OperatorTimesNotNatural.txt
@@ -0,0 +1,6 @@
+Type error: error: BinOpTypeMismatch
+ --> <current file>:1:0
+  |
+1 | True * True
+  | ^^^^^^^^^^^ BinOpTypeMismatch
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxAbsent.txt
new file mode 100644
index 0000000..bfb36ae
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxAbsent.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidListType
+ --> <current file>:1:0
+  |
+1 | [] : Optional Bool
+  | ^^^^^^^^^^^^^^^^^^ InvalidListType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
new file mode 100644
index 0000000..5332fcb
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: ([1] : List Natural) : Optional Natural
+ --> <current file>:1:0
+  |
+1 | [ 1 ] : Optional Natural
+  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ([1] : List Natural) : Optional Natural
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFields.txt
new file mode 100644
index 0000000..608c6a0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFields.txt
@@ -0,0 +1,6 @@
+Type error: error: RecordTypeDuplicateField
+ --> <current file>:1:0
+  |
+1 | { x = 0, x = 0 }
+  | ^^^^^^^^^^^^^^^^ RecordTypeDuplicateField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeFieldTypeMismatch.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeFieldTypeMismatch.txt
new file mode 100644
index 0000000..d624075
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeFieldTypeMismatch.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionWrongType
+ --> <current file>:1:0
+  |
+1 | { y = {=} }.( {y : Natural} )
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ProjectionWrongType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeNotPresent.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeNotPresent.txt
new file mode 100644
index 0000000..c22c2c4
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionByTypeNotPresent.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionMissingEntry
+ --> <current file>:1:0
+  |
+1 | { y = {=} }.( {x : Natural} )
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ProjectionMissingEntry
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt
new file mode 100644
index 0000000..5c6520b
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionDuplicateField
+ --> <current file>:1:0
+  |
+1 | { x = 1 }.{ x, x }
+  | ^^^^^^^^^^^^^^^^^^ ProjectionDuplicateField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionEmpty.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionEmpty.txt
new file mode 100644
index 0000000..39f263b
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionEmpty.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionMissingEntry
+ --> <current file>:1:0
+  |
+1 | {=}.{ x }
+  | ^^^^^^^^^ ProjectionMissingEntry
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionNotPresent.txt
new file mode 100644
index 0000000..032f7a0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionNotPresent.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionMissingEntry
+ --> <current file>:1:0
+  |
+1 | { y = {=} }.{ x }
+  | ^^^^^^^^^^^^^^^^^ ProjectionMissingEntry
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionNotRecord.txt
new file mode 100644
index 0000000..5ed6ffd
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionNotRecord.txt
@@ -0,0 +1,6 @@
+Type error: error: ProjectionMustBeRecord
+ --> <current file>:1:0
+  |
+1 | True.{ x }
+  | ^^^^^^^^^^ ProjectionMustBeRecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordSelectionEmpty.txt b/dhall/tests/type-inference/failure/unit/RecordSelectionEmpty.txt
new file mode 100644
index 0000000..5b3b7f8
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordSelectionEmpty.txt
@@ -0,0 +1,6 @@
+Type error: error: MissingRecordField
+ --> <current file>:1:0
+  |
+1 | {=}.x
+  | ^^^^^ MissingRecordField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-inference/failure/unit/RecordSelectionNotPresent.txt
new file mode 100644
index 0000000..d435ca0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordSelectionNotPresent.txt
@@ -0,0 +1,6 @@
+Type error: error: MissingRecordField
+ --> <current file>:1:0
+  |
+1 | { y = {=} }.x
+  | ^^^^^^^^^^^^^ MissingRecordField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecordSelectionNotRecord.txt
new file mode 100644
index 0000000..3f9b7ed
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordSelectionNotRecord.txt
@@ -0,0 +1,6 @@
+Type error: error: NotARecord
+ --> <current file>:1:0
+  |
+1 | True.x
+  | ^^^^^^ NotARecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-inference/failure/unit/RecordSelectionTypeNotUnionType.txt
new file mode 100644
index 0000000..cca28b8
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordSelectionTypeNotUnionType.txt
@@ -0,0 +1,6 @@
+Type error: error: NotARecord
+ --> <current file>:1:0
+  |
+1 | Bool.x
+  | ^^^^^^ NotARecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt
new file mode 100644
index 0000000..145a59b
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt
@@ -0,0 +1,6 @@
+Type error: error: RecordTypeDuplicateField
+ --> <current file>:1:0
+  |
+1 | { x: Natural, x: Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeDuplicateField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt
new file mode 100644
index 0000000..04488ad
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | { x : True }
+  | ^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..f74e839
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
new file mode 100644
index 0000000..f74e839
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..f74e839
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
new file mode 100644
index 0000000..b35e64b
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
@@ -0,0 +1,6 @@
+Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | Bool ⩓ {}
+  | ^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
new file mode 100644
index 0000000..f74e839
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
new file mode 100644
index 0000000..0200f97
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
@@ -0,0 +1,6 @@
+Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | {} ⩓ Bool
+  | ^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..3b158ce
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeLhsNotRecord.txt
@@ -0,0 +1,6 @@
+Type error: error: MustCombineRecord
+ --> <current file>:1:0
+  |
+1 | True ⫽ {=}
+  | ^^^^^^^^^^ MustCombineRecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..4f9cb0d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeRhsNotRecord.txt
@@ -0,0 +1,6 @@
+Type error: error: MustCombineRecord
+ --> <current file>:1:0
+  |
+1 | {=} ⫽ True
+  | ^^^^^^^^^^ MustCombineRecord
+  |
diff --git a/dhall/tests/type-inference/failure/unit/SomeNotType.txt b/dhall/tests/type-inference/failure/unit/SomeNotType.txt
new file mode 100644
index 0000000..3584768
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/SomeNotType.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidOptionalType
+ --> <current file>:1:0
+  |
+1 | Some Bool
+  | ^^^^^^^^^ InvalidOptionalType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/Sort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-inference/failure/unit/TextLiteralInterpolateNotText.txt
new file mode 100644
index 0000000..0132a30
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/TextLiteralInterpolateNotText.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidTextInterpolation
+ --> <current file>:1:0
+  |
+1 | "${1}"
+  | ^^^^^^ InvalidTextInterpolation
+  |
diff --git a/dhall/tests/type-inference/failure/unit/ToMapEmptyInvalidAnnotation.txt b/dhall/tests/type-inference/failure/unit/ToMapEmptyInvalidAnnotation.txt
new file mode 100644
index 0000000..c28073e
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/ToMapEmptyInvalidAnnotation.txt
@@ -0,0 +1,7 @@
+Type error: error: The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+ --> <current file>:2:0
+  |
+1 | -- The mapKey must be Text
+2 | toMap {=} : List { mapKey : Bool, mapValue : Text }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+  |
diff --git a/dhall/tests/type-inference/failure/unit/ToMapWrongKind.txt b/dhall/tests/type-inference/failure/unit/ToMapWrongKind.txt
new file mode 100644
index 0000000..8158c08
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/ToMapWrongKind.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` only accepts records of type `Type`
+ --> <current file>:1:0
+  |
+1 | toMap { x = Bool }
+  | ^^^^^^^^^^^^^^^^^^ `toMap` only accepts records of type `Type`
+  |
diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
new file mode 100644
index 0000000..7360e68
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: (1 : Natural) : Bool
+ --> <current file>:1:0
+  |
+1 | 1 : Bool
+  | ^^^^^^^^ annot mismatch: (1 : Natural) : Bool
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-inference/failure/unit/UnionConstructorFieldNotPresent.txt
new file mode 100644
index 0000000..41d283d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionConstructorFieldNotPresent.txt
@@ -0,0 +1,6 @@
+Type error: error: MissingUnionField
+ --> <current file>:1:0
+  |
+1 | < x : Bool >.y
+  | ^^^^^^^^^^^^^^ MissingUnionField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-inference/failure/unit/UnionDeprecatedConstructorsKeyword.txt
new file mode 100644
index 0000000..91fb96d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -0,0 +1,6 @@
+Type error: error: unbound variable `constructors`
+ --> <current file>:1:0
+  |
+1 | constructors < Left : Natural | Right : Bool >
+  | ^^^^^^^^^^^^ not found in this scope
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt
new file mode 100644
index 0000000..7372641
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt
@@ -0,0 +1,6 @@
+Type error: error: UnionTypeDuplicateField
+ --> <current file>:1:0
+  |
+1 | <x | x>
+  | ^^^^^^^ UnionTypeDuplicateField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt
new file mode 100644
index 0000000..07042c2
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt
@@ -0,0 +1,6 @@
+Type error: error: UnionTypeDuplicateField
+ --> <current file>:1:0
+  |
+1 | <x | x: Natural>
+  | ^^^^^^^^^^^^^^^^ UnionTypeDuplicateField
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
new file mode 100644
index 0000000..00e24b3
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | < x : Bool | y : Type >
+  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
new file mode 100644
index 0000000..924b1e1
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | < x : Kind | y : Type >
+  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
new file mode 100644
index 0000000..1113a0d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | < x : Kind | y : Bool >
+  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt
new file mode 100644
index 0000000..b2c06e0
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt
@@ -0,0 +1,6 @@
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | < x : True >
+  | ^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/VariableFree.txt b/dhall/tests/type-inference/failure/unit/VariableFree.txt
new file mode 100644
index 0000000..db78e15
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/VariableFree.txt
@@ -0,0 +1,6 @@
+Type error: error: unbound variable `x`
+ --> <current file>:1:0
+  |
+1 | x
+  | ^ not found in this scope
+  |