summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/value.rs7
-rw-r--r--dhall/src/semantics/phase/mod.rs69
-rw-r--r--dhall/src/semantics/phase/typecheck.rs2
-rw-r--r--dhall/src/semantics/tck/typecheck.rs9
-rw-r--r--dhall/src/tests.rs85
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt2
-rw-r--r--dhall/tests/type-errors/mixedUnions.txt2
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt2
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt2
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/EquivalenceNotTerms.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt7
-rw-r--r--dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt2
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt2
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt22
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt66
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt2
-rw-r--r--dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt2
-rw-r--r--dhall/tests/type-errors/unit/RecordTypeValueMember.txt2
-rw-r--r--dhall/tests/type-errors/unit/TypeAnnotationWrong.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeNotType.txt2
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
30 files changed, 158 insertions, 172 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 3dcbd38..aa819d2 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -9,9 +9,7 @@ use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, builtin_to_value_env, const_to_value,
};
-use crate::semantics::phase::{
- Normalized, NormalizedExpr, ToExprOptions, Typed,
-};
+use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
use crate::semantics::{TyExpr, TyExprKind};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -207,9 +205,6 @@ impl Value {
self.check_type(ty);
self.to_whnf_ignore_type()
}
- pub(crate) fn into_typed(self) -> Typed {
- Typed::from_value(self)
- }
/// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 68c32b2..0f8194c 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -4,6 +4,7 @@ use std::path::Path;
use crate::error::{EncodeError, Error, ImportError, TypeError};
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
+use crate::semantics::tck::tyexpr::TyExpr;
use crate::syntax::binary;
use crate::syntax::{Builtin, Const, Expr};
use resolve::ImportRoot;
@@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(Value);
+pub struct Typed(TyExpr);
/// A normalized expression.
///
@@ -78,11 +79,14 @@ impl Parsed {
}
impl Resolved {
- pub fn typecheck(self) -> Result<Typed, TypeError> {
- Ok(typecheck::typecheck(self.0)?.into_typed())
+ pub fn typecheck(&self) -> Result<Typed, TypeError> {
+ Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?))
}
pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> {
- Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
+ Ok(Typed(crate::semantics::tck::typecheck::typecheck_with(
+ &self.0,
+ ty.to_expr(),
+ )?))
}
/// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> ResolvedExpr {
@@ -97,43 +101,22 @@ impl Resolved {
impl Typed {
/// Reduce an expression to its normal form, performing beta reduction
- pub fn normalize(mut self) -> Normalized {
- self.0.normalize_mut();
- Normalized(self.0)
- }
-
- pub(crate) fn from_value(th: Value) -> Self {
- Typed(th)
+ pub fn normalize(&self) -> Normalized {
+ let mut val = self.0.normalize_whnf_noenv();
+ val.normalize_mut();
+ Normalized(val)
}
/// Converts a value back to the corresponding AST expression.
- pub(crate) fn to_expr(&self) -> ResolvedExpr {
+ fn to_expr(&self) -> ResolvedExpr {
self.0.to_expr(ToExprOptions {
alpha: false,
normalize: false,
})
}
- /// Converts a value back to the corresponding AST expression, beta-normalizing in the process.
- pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr {
- self.0.to_expr(ToExprOptions {
- alpha: false,
- normalize: true,
- })
- }
- /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the
- /// process.
- pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
- self.0.to_expr(ToExprOptions {
- alpha: true,
- normalize: true,
- })
- }
- pub(crate) fn into_value(self) -> Value {
- self.0
- }
- pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
- Ok(self.0.get_type()?.into_typed())
+ pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
+ Ok(Normalized(self.0.get_type()?))
}
}
@@ -142,19 +125,19 @@ impl Normalized {
binary::encode(&self.to_expr())
}
+ /// Converts a value back to the corresponding AST expression.
pub fn to_expr(&self) -> NormalizedExpr {
- // TODO: do it directly
- self.to_typed().normalize_to_expr()
+ self.0.to_expr(ToExprOptions {
+ alpha: false,
+ normalize: false,
+ })
}
+ /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
- // TODO: do it directly
- self.to_typed().normalize_to_expr_alpha()
- }
- pub(crate) fn to_typed(&self) -> Typed {
- Typed(self.0.clone())
- }
- pub(crate) fn into_typed(self) -> Typed {
- Typed(self.0)
+ self.0.to_expr(ToExprOptions {
+ alpha: true,
+ normalize: false,
+ })
}
pub(crate) fn to_value(&self) -> Value {
self.0.clone()
@@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized {
impl Eq for Typed {}
impl PartialEq for Typed {
fn eq(&self, other: &Self) -> bool {
- self.0 == other.0
+ self.normalize() == other.normalize()
}
}
impl Display for Typed {
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index f559323..6de65e8 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -336,7 +336,7 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
// ))
Ok(e)
}
- Embed(p) => Ok(p.clone().into_typed().into_value()),
+ Embed(p) => Ok(p.clone().into_value()),
Var(var) => match ctx.lookup(&var) {
Some(typed) => Ok(typed.clone()),
None => Err(TypeError::new(TypeMessage::UnboundVariable(span))),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a83f175..5880d92 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -677,7 +677,7 @@ pub(crate) fn type_with(
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
ExprKind::Embed(p) => {
- return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+ return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
@@ -692,3 +692,10 @@ pub(crate) fn type_with(
pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
type_with(&TyEnv::new(), e)
}
+
+pub(crate) fn typecheck_with(
+ expr: &Expr<Normalized>,
+ ty: Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+ typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 1c687f6..08feadf 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -158,65 +158,24 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
parse_file_str(&file_path)?.resolve().unwrap_err();
}
TypeInferenceSuccess(expr_file_path, expected_file_path) => {
- // let expr =
- // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
- // let ty = expr.get_type()?.to_expr();
- // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
- // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?;
- // let ty = tyexpr.get_type()?.to_expr();
- //
- let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
- let ty = crate::semantics::tck::typecheck::typecheck(&expr)?
- .get_type()?
- .to_expr(crate::semantics::phase::ToExprOptions {
- alpha: false,
- normalize: true,
- });
+ let expr =
+ parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
+ let ty = expr.get_type()?.to_expr();
let expected = parse_file_str(&expected_file_path)?.to_expr();
assert_eq_display!(ty, expected);
- //
- // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
- // let ty = crate::semantics::tck::typecheck::typecheck(&expr)?
- // .get_type()?;
- // let expected = parse_file_str(&expected_file_path)?.to_expr();
- // let expected = crate::semantics::tck::typecheck::typecheck(&expected)?
- // .normalize_whnf_noenv();
- // // if ty != expected {
- // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions {
- // // alpha: false,
- // // normalize: true,
- // // }), expected.to_expr(crate::semantics::phase::ToExprOptions {
- // // alpha: false,
- // // normalize: true,
- // // }))
- // // }
- // assert_eq_pretty!(ty, expected);
}
TypeInferenceFailure(file_path) => {
- // let mut res =
- // parse_file_str(&file_path)?.skip_resolve()?.typecheck();
- // if let Ok(e) = &res {
- // // If e did typecheck, check that get_type fails
- // res = e.get_type();
- // }
- // res.unwrap_err();
-
- let res = crate::semantics::tck::typecheck::typecheck(
- &parse_file_str(&file_path)?.skip_resolve()?.to_expr(),
- );
+ let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck();
if let Ok(e) = &res {
// If e did typecheck, check that get_type fails
e.get_type().unwrap_err();
- } else {
- res.unwrap_err();
}
}
// Checks the output of the type error against a text file. If the text file doesn't exist,
// we instead write to it the output we got. This makes it easy to update those files: just
// `rm -r dhall/tests/type-errors` and run the tests again.
TypeError(file_path) => {
- let mut res =
- parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+ let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck();
let file_path = PathBuf::from(file_path);
let error_file_path = file_path
.strip_prefix("../dhall-lang/tests/type-inference/failure/")
@@ -224,11 +183,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
let error_file_path =
PathBuf::from("tests/type-errors/").join(error_file_path);
let error_file_path = error_file_path.with_extension("txt");
- if let Ok(e) = &res {
- // If e did typecheck, check that get_type fails
- res = e.get_type();
- }
- let err: Error = res.unwrap_err().into();
+ let err: Error = match res {
+ Ok(e) => {
+ // If e did typecheck, check that get_type fails
+ e.get_type().unwrap_err().into()
+ }
+ Err(e) => e.into(),
+ };
if error_file_path.is_file() {
let expected_msg = std::fs::read_to_string(error_file_path)?;
@@ -241,28 +202,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
}
}
Normalization(expr_file_path, expected_file_path) => {
- // let expr = parse_file_str(&expr_file_path)?
- // .resolve()?
- // .typecheck()?
- // .normalize()
- // .to_expr();
- // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
- // let expr = crate::semantics::nze::nzexpr::typecheck(expr)?
- // .normalize()
- // .to_expr();
- // let expr = parse_file_str(&expr_file_path)?
- // .resolve()?
- // .typecheck()?
- // .to_value()
- // .to_tyexpr_noenv()
- // .normalize_whnf_noenv()
- // .to_expr(crate::semantics::phase::ToExprOptions {
- // alpha: false,
- // normalize: true,
- // });
let expr = parse_file_str(&expr_file_path)?
.resolve()?
- .tck_and_normalize_new_flow()?
+ .typecheck()?
+ .normalize()
.to_expr();
let expected = parse_file_str(&expected_file_path)?.to_expr();
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