summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-23 20:56:03 +0000
committerNadrieril2020-03-05 15:58:31 +0000
commit73af29fb11517f85043d8a866697b150dc7c2191 (patch)
treeaf401099a71c67a647ad5942ae06ff172f4a63c9
parentb7f6c5778c3c980a452abd3da715996fa24d4449 (diff)
Add a bunch of tests
-rw-r--r--dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall1
-rw-r--r--dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall1
-rw-r--r--dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall1
-rw-r--r--dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested1A.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested1B.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested2A.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested2B.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested3A.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextLitNested3B.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextShowEmptyA.dhall1
-rw-r--r--dhall/tests/normalization/success/unit/TextShowEmptyB.dhall1
-rw-r--r--dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall1
-rw-r--r--dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb1
-rw-r--r--dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag1
-rw-r--r--dhall/tests/parser/success/unit/LetAnnotA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/LetAnnotB.dhallbbin0 -> 17 bytes
-rw-r--r--dhall/tests/parser/success/unit/LetAnnotB.diag1
-rw-r--r--dhall/tests/parser/success/unit/LetNoAnnotA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/LetNoAnnotB.dhallbbin0 -> 14 bytes
-rw-r--r--dhall/tests/parser/success/unit/LetNoAnnotB.diag1
-rw-r--r--dhall/tests/parser/success/unit/ToMapA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/ToMapAnnotA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/ToMapAnnotB.dhallbbin0 -> 11 bytes
-rw-r--r--dhall/tests/parser/success/unit/ToMapAnnotB.diag1
-rw-r--r--dhall/tests/parser/success/unit/ToMapB.dhallbbin0 -> 7 bytes
-rw-r--r--dhall/tests/parser/success/unit/ToMapB.diag1
-rw-r--r--dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall1
-rw-r--r--dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallbbin0 -> 6 bytes
-rw-r--r--dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag1
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/LetInSort.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/LetInSort.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/MergeBool.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/MergeBool.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt6
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/TodoA.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/TodoB.dhall1
-rw-r--r--tests_buffer23
50 files changed, 70 insertions, 23 deletions
diff --git a/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall
new file mode 100644
index 0000000..3a69d1e
--- /dev/null
+++ b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgA.dhall
@@ -0,0 +1 @@
+Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True
diff --git a/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall
new file mode 100644
index 0000000..bc59c12
--- /dev/null
+++ b/dhall/tests/normalization/success/regression/NaturalFoldExtraArgB.dhall
@@ -0,0 +1 @@
+False
diff --git a/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall b/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall
new file mode 100644
index 0000000..5d72bbe
--- /dev/null
+++ b/dhall/tests/normalization/success/regression/TrickyBinderIdentityA.dhall
@@ -0,0 +1 @@
+let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0
diff --git a/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall b/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall
new file mode 100644
index 0000000..28233fb
--- /dev/null
+++ b/dhall/tests/normalization/success/regression/TrickyBinderIdentityB.dhall
@@ -0,0 +1 @@
+[ 0, 1 ]
diff --git a/dhall/tests/normalization/success/unit/TextLitNested1A.dhall b/dhall/tests/normalization/success/unit/TextLitNested1A.dhall
new file mode 100644
index 0000000..104dc41
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested1A.dhall
@@ -0,0 +1 @@
+λ(x: Text) → "${""}${x}"
diff --git a/dhall/tests/normalization/success/unit/TextLitNested1B.dhall b/dhall/tests/normalization/success/unit/TextLitNested1B.dhall
new file mode 100644
index 0000000..631a6cf
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested1B.dhall
@@ -0,0 +1 @@
+λ(x : Text) → x
diff --git a/dhall/tests/normalization/success/unit/TextLitNested2A.dhall b/dhall/tests/normalization/success/unit/TextLitNested2A.dhall
new file mode 100644
index 0000000..5b4ae6e
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested2A.dhall
@@ -0,0 +1 @@
+λ(x: Text) → "${"${x}"}"
diff --git a/dhall/tests/normalization/success/unit/TextLitNested2B.dhall b/dhall/tests/normalization/success/unit/TextLitNested2B.dhall
new file mode 100644
index 0000000..631a6cf
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested2B.dhall
@@ -0,0 +1 @@
+λ(x : Text) → x
diff --git a/dhall/tests/normalization/success/unit/TextLitNested3A.dhall b/dhall/tests/normalization/success/unit/TextLitNested3A.dhall
new file mode 100644
index 0000000..d57ac64
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested3A.dhall
@@ -0,0 +1 @@
+λ(x: Text) → "${"${""}"}${x}"
diff --git a/dhall/tests/normalization/success/unit/TextLitNested3B.dhall b/dhall/tests/normalization/success/unit/TextLitNested3B.dhall
new file mode 100644
index 0000000..631a6cf
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextLitNested3B.dhall
@@ -0,0 +1 @@
+λ(x : Text) → x
diff --git a/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall b/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall
new file mode 100644
index 0000000..589f65d
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextShowEmptyA.dhall
@@ -0,0 +1 @@
+Text/show ""
diff --git a/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall b/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall
new file mode 100644
index 0000000..8fbbe76
--- /dev/null
+++ b/dhall/tests/normalization/success/unit/TextShowEmptyB.dhall
@@ -0,0 +1 @@
+"\"\""
diff --git a/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall b/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall
new file mode 100644
index 0000000..6019020
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/AssertNoAnnotation.dhall
@@ -0,0 +1 @@
+assert
diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall b/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall
new file mode 100644
index 0000000..339130f
--- /dev/null
+++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralA.dhall
@@ -0,0 +1 @@
+{=}
diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb
new file mode 100644
index 0000000..58e2e39
--- /dev/null
+++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.dhallb
@@ -0,0 +1 @@
+‚  \ No newline at end of file
diff --git a/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag
new file mode 100644
index 0000000..8ead206
--- /dev/null
+++ b/dhall/tests/parser/success/unit/EmptyRecordLiteralB.diag
@@ -0,0 +1 @@
+[8, {}]
diff --git a/dhall/tests/parser/success/unit/LetAnnotA.dhall b/dhall/tests/parser/success/unit/LetAnnotA.dhall
new file mode 100644
index 0000000..c7d29f8
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetAnnotA.dhall
@@ -0,0 +1 @@
+let x: T = y in e
diff --git a/dhall/tests/parser/success/unit/LetAnnotB.dhallb b/dhall/tests/parser/success/unit/LetAnnotB.dhallb
new file mode 100644
index 0000000..4e3a7e4
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetAnnotB.dhallb
Binary files differ
diff --git a/dhall/tests/parser/success/unit/LetAnnotB.diag b/dhall/tests/parser/success/unit/LetAnnotB.diag
new file mode 100644
index 0000000..36791e0
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetAnnotB.diag
@@ -0,0 +1 @@
+[25, "x", ["T", 0], ["y", 0], ["e", 0]]
diff --git a/dhall/tests/parser/success/unit/LetNoAnnotA.dhall b/dhall/tests/parser/success/unit/LetNoAnnotA.dhall
new file mode 100644
index 0000000..64d30e6
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetNoAnnotA.dhall
@@ -0,0 +1 @@
+let x = y in e
diff --git a/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb b/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb
new file mode 100644
index 0000000..79a2384
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetNoAnnotB.dhallb
Binary files differ
diff --git a/dhall/tests/parser/success/unit/LetNoAnnotB.diag b/dhall/tests/parser/success/unit/LetNoAnnotB.diag
new file mode 100644
index 0000000..a23f605
--- /dev/null
+++ b/dhall/tests/parser/success/unit/LetNoAnnotB.diag
@@ -0,0 +1 @@
+[25, "x", null, ["y", 0], ["e", 0]]
diff --git a/dhall/tests/parser/success/unit/ToMapA.dhall b/dhall/tests/parser/success/unit/ToMapA.dhall
new file mode 100644
index 0000000..ea04391
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapA.dhall
@@ -0,0 +1 @@
+toMap x
diff --git a/dhall/tests/parser/success/unit/ToMapAnnotA.dhall b/dhall/tests/parser/success/unit/ToMapAnnotA.dhall
new file mode 100644
index 0000000..ad65b07
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapAnnotA.dhall
@@ -0,0 +1 @@
+toMap x : T
diff --git a/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb b/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb
new file mode 100644
index 0000000..4b53587
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapAnnotB.dhallb
Binary files differ
diff --git a/dhall/tests/parser/success/unit/ToMapAnnotB.diag b/dhall/tests/parser/success/unit/ToMapAnnotB.diag
new file mode 100644
index 0000000..8e511fb
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapAnnotB.diag
@@ -0,0 +1 @@
+[27, ["x", 0], ["T", 0]]
diff --git a/dhall/tests/parser/success/unit/ToMapB.dhallb b/dhall/tests/parser/success/unit/ToMapB.dhallb
new file mode 100644
index 0000000..25ecd95
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapB.dhallb
Binary files differ
diff --git a/dhall/tests/parser/success/unit/ToMapB.diag b/dhall/tests/parser/success/unit/ToMapB.diag
new file mode 100644
index 0000000..5d25b39
--- /dev/null
+++ b/dhall/tests/parser/success/unit/ToMapB.diag
@@ -0,0 +1 @@
+[27, ["x", 0]]
diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall
new file mode 100644
index 0000000..a1f4d02
--- /dev/null
+++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceA.dhall
@@ -0,0 +1 @@
+` x `
diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb
new file mode 100644
index 0000000..56d9cd9
--- /dev/null
+++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.dhallb
Binary files differ
diff --git a/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag
new file mode 100644
index 0000000..035d650
--- /dev/null
+++ b/dhall/tests/parser/success/unit/VariableQuotedWithSpaceB.diag
@@ -0,0 +1 @@
+[" x ", 0]
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall
new file mode 100644
index 0000000..94b32f9
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall
@@ -0,0 +1 @@
+Bool -> 1
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt
new file mode 100644
index 0000000..bcc44a5
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt
@@ -0,0 +1,7 @@
+Type error: error: Expected a type, found: `1`
+ --> <current file>:1:8
+ |
+1 | Bool -> 1
+ | ^ this has type: `Natural`
+ |
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.dhall b/dhall/tests/type-inference/failure/unit/LetInSort.dhall
new file mode 100644
index 0000000..125ab28
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetInSort.dhall
@@ -0,0 +1 @@
+\(x: let x = 0 in Sort) -> 1
diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.txt b/dhall/tests/type-inference/failure/unit/LetInSort.txt
new file mode 100644
index 0000000..07be298
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetInSort.txt
@@ -0,0 +1,6 @@
+Type error: error: Sort does not have a type
+ --> <current file>:1:18
+ |
+1 | \(x: let x = 0 in Sort) -> 1
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.dhall b/dhall/tests/type-inference/failure/unit/MergeBool.dhall
new file mode 100644
index 0000000..01e7e3f
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeBool.dhall
@@ -0,0 +1 @@
+\(x: { True: Natural, False: Natural }) -> merge x True
diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.txt b/dhall/tests/type-inference/failure/unit/MergeBool.txt
new file mode 100644
index 0000000..209def1
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeBool.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:43
+ |
+1 | \(x: { True: Natural, False: Natural }) -> merge x True
+ | ^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+ |
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall
new file mode 100644
index 0000000..7e5c8ec
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall
@@ -0,0 +1 @@
+(0 : Bool) : Natural
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt
new file mode 100644
index 0000000..b56db54
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: Natural != Bool
+ --> <current file>:1:1
+ |
+1 | (0 : Bool) : Natural
+ | ^ annot mismatch: Natural != Bool
+ |
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall
new file mode 100644
index 0000000..67a1526
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall
@@ -0,0 +1 @@
+(0 : Natural) : Bool
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt
new file mode 100644
index 0000000..2f07b8d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: Natural != Bool
+ --> <current file>:1:1
+ |
+1 | (0 : Natural) : Bool
+ | ^^^^^^^^^^^ annot mismatch: Natural != Bool
+ |
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall
new file mode 100644
index 0000000..72f866f
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall
@@ -0,0 +1 @@
+let T = 0 in λ(T : Type) → λ(x : T) → 1
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall
new file mode 100644
index 0000000..42bfeec
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall
@@ -0,0 +1 @@
+∀(T : Type) → ∀(x : T) → Natural
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall
new file mode 100644
index 0000000..30fd03c
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall
@@ -0,0 +1 @@
+(λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall
new file mode 100644
index 0000000..20aa0d3
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall
@@ -0,0 +1 @@
+∀(T : Type) → ∀(x : T) → T
diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall
new file mode 100644
index 0000000..c7b7fb4
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall
@@ -0,0 +1 @@
+{ x : { a : Bool } } â©“ { x : { b : Bool } } â©“ { x : { c : Bool } }
diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall
new file mode 100644
index 0000000..245bc9d
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall
@@ -0,0 +1 @@
+Type
diff --git a/dhall/tests/type-inference/success/regression/TodoA.dhall b/dhall/tests/type-inference/success/regression/TodoA.dhall
new file mode 100644
index 0000000..9d5ef34
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/TodoA.dhall
@@ -0,0 +1 @@
+λ(todo : ∀(a : Type) → a) → todo
diff --git a/dhall/tests/type-inference/success/regression/TodoB.dhall b/dhall/tests/type-inference/success/regression/TodoB.dhall
new file mode 100644
index 0000000..e0091f2
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/TodoB.dhall
@@ -0,0 +1 @@
+∀(todo : ∀(a : Type) → a) → ∀(a : Type) → a
diff --git a/tests_buffer b/tests_buffer
index c582689..6f6e67e 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -1,26 +1,3 @@
-normalization/success/unit/TextShowEmpty Text/show ""
-normalization/success/unit/TextLitNested1 λ(x: Text) → "${""}${x}"
-normalization/success/unit/TextLitNested2 λ(x: Text) → "${"${x}"}"
-normalization/success/unit/TextLitNested3 λ(x: Text) → "${"${""}"}${x}"
-normalization/success/regression/NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True
-normalization/success/regression/TrickyBinderIdentity let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0
-parser/success/unit/LetNoAnnot let x = y in e
-parser/success/unit/LetAnnot let x: T = y in e
-parser/success/unit/EmptyRecordLiteral {=}
-parser/success/unit/ToMap toMap x
-parser/success/unit/ToMapAnnot toMap x : T
-parser/success/unit/VariableQuotedWithSpace ` x `
-parser/failure/unit/AssertNoAnnotation assert
-type-inference/failure/unit/FunctionTypeOutputTypeNotAType Bool -> 1
-type-inference/failure/unit/NestedAnnotInnerWrong (0 : Bool) : Natural
-type-inference/failure/unit/NestedAnnotOuterWrong (0 : Natural) : Bool
-type-inference/failure/unit/MergeBool merge x True
-type-inference/failure/unit/LetInSort \(x: let x = 0 in Sort) -> 1
-type-inference/success/regression/RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } â©“ { x : { b : Bool } } â©“ { x : { c : Bool } }
-type-inference/success/regression/Todo λ(todo : ∀(a : Type) → a) → todo
-type-inference/success/regression/LambdaInLetScoping1 let T = 0 in λ(T : Type) → λ(x : T) → 1
-type-inference/success/regression/LambdaInLetScoping2 (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
-
parser:
./a%20b
./"a%20b"