diff options
Diffstat (limited to '')
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 |