Use TyExpr in Typed

25 files changed, 108 insertions, 50 deletions

diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 9342fd8..4dfdcf5 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt
index 30fcdf8..fd4de70 100644
--- a/dhall/tests/type-errors/mixedUnions.txt
+++ b/dhall/tests/type-errors/mixedUnions.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("Right"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
index 045eb98..946b296 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
index 045eb98..89817db 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
index 2969c18..87cf48e 100644
--- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -1,6 +1 @@
- --> 1:47
-  |
-1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊
-  |                                               ^
-  |
-  = Type error: Unbound variable
+Type error: Unhandled error: unbound variable
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
index 7c48d6f..de11e28 100644
--- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -1 +1 @@
-Type error: Unhandled error: EquivalenceArgumentMustBeTerm
+Type error: Unhandled error: EquivalenceArgumentsMustBeTerms
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 9342fd8..8d101c3 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index f1cdf92..13b0819 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1 @@
-Type error: Unhandled error: NotAFunction
+Type error: Unhandled error: apply to not Pi: AppliedBuiltin(Bool, [], [], NzEnv { items: [] })
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
index 9e43c33..a13fb3a 100644
--- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -1,6 +1 @@
- --> 1:7
-  |
-1 | λ(_ : 1) → _␊
-  |       ^
-  |
-  = Type error: Invalid function input
+[unknown location] Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
index dd2e758..a13fb3a 100644
--- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,6 +1 @@
- --> 1:1
-  |
-1 | 2 → _␊
-  | ^
-  |
-  = Type error: Invalid function input
+[unknown location] Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
index 045eb98..cae4fea 100644
--- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 9342fd8..070e461 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
deleted file mode 100644
index de9e256..0000000
--- a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
+++ /dev/null
@@ -1 +0,0 @@
-Type error: Unhandled error: MergeHandlerReturnTypeMustNotBeDependent
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 9342fd8..77fed39 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1 +1,21 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
+    value: AppliedBuiltin(
+        Natural,
+        [],
+        [],
+        NzEnv {
+            items: [],
+        },
+    ),
+    type: Type,
+} != Value@WHNF {
+    value: AppliedBuiltin(
+        Bool,
+        [],
+        [],
+        NzEnv {
+            items: [],
+        },
+    ),
+    type: Type,
+}
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
index 8b729a4..02d2970 100644
--- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -1 +1,65 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch
+Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
+    value: AppliedBuiltin(
+        Bool,
+        [],
+        [],
+        NzEnv {
+            items: [
+                Replaced(
+                    Value@Unevaled {
+                        value: Var(
+                            AlphaVar(0),
+                            Fresh(
+                                119,
+                            ),
+                        ),
+                        type: Value@WHNF {
+                            value: AppliedBuiltin(
+                                Bool,
+                                [],
+                                [],
+                                NzEnv {
+                                    items: [],
+                                },
+                            ),
+                            type: Type,
+                        },
+                    },
+                ),
+            ],
+        },
+    ),
+    type: Type,
+} != Value@WHNF {
+    value: AppliedBuiltin(
+        Natural,
+        [],
+        [],
+        NzEnv {
+            items: [
+                Replaced(
+                    Value@Unevaled {
+                        value: Var(
+                            AlphaVar(0),
+                            Fresh(
+                                120,
+                            ),
+                        ),
+                        type: Value@WHNF {
+                            value: AppliedBuiltin(
+                                Natural,
+                                [],
+                                [],
+                                NzEnv {
+                                    items: [],
+                                },
+                            ),
+                            type: Type,
+                        },
+                    },
+                ),
+            ],
+        },
+    ),
+    type: Type,
+}
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 9342fd8..8d101c3 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
index 045eb98..91d7fb0 100644
--- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ([1] : List Natural) : Optional Natural
diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
index ed3fd6a..fd4de70 100644
--- a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
+++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
index 045eb98..52fc94d 100644
--- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: (1 : Natural) : Bool
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
index 9cc0c19..87cf48e 100644
--- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -1,6 +1 @@
- --> 1:1
-  |
-1 | constructors < Left : Natural | Right : Bool >␊
-  | ^----------^
-  |
-  = Type error: Unbound variable
+Type error: Unhandled error: unbound variable
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
index 07604ba..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
index 07604ba..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
index ded0e5c..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
index ed3fd6a..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeNotType.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
index a46aac0..87cf48e 100644
--- a/dhall/tests/type-errors/unit/VariableFree.txt
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -1,6 +1 @@
- --> 1:1
-  |
-1 | x␊
-  | ^
-  |
-  = Type error: Unbound variable
+Type error: Unhandled error: unbound variable