From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/tests/type-errors/hurkensParadox.txt | 2 +- dhall/tests/type-errors/mixedUnions.txt | 2 +- .../unit/AnnotationRecordWrongFieldName.txt | 2 +- .../unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 +-- .../tests/type-errors/unit/EquivalenceNotTerms.txt | 2 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 2 +- .../unit/FunctionApplicationIsNotFunction.txt | 2 +- .../unit/FunctionArgumentTypeNotAType.txt | 7 +-- .../unit/FunctionTypeArgumentTypeNotAType.txt | 7 +-- .../type-errors/unit/LetWithWrongAnnotation.txt | 2 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 2 +- .../tests/type-errors/unit/MergeHandlerFreeVar.txt | 1 - .../unit/MergeHandlerNotMatchAlternativeType.txt | 22 +++++++- .../unit/MergeHandlersWithDifferentType.txt | 66 +++++++++++++++++++++- .../type-errors/unit/NaturalSubtractNotNatural.txt | 2 +- .../unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- .../type-errors/unit/RecordTypeValueMember.txt | 2 +- .../tests/type-errors/unit/TypeAnnotationWrong.txt | 2 +- .../unit/UnionDeprecatedConstructorsKeyword.txt | 7 +-- .../tests/type-errors/unit/UnionTypeMixedKinds.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds2.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeNotType.txt | 2 +- dhall/tests/type-errors/unit/VariableFree.txt | 7 +-- 25 files changed, 108 insertions(+), 50 deletions(-) delete mode 100644 dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt (limited to 'dhall/tests') 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 -- cgit v1.2.3