From 92bbea48f9a0380a614f2687c73d55a67ff9294e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 15:02:23 +0000 Subject: More nice errors plus some refactor --- dhall/tests/type-errors/hurkensParadox.txt | 4 ++-- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 ++++++- .../type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 4 ++-- dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt | 8 +++++++- dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt | 8 +++++++- dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 4 ++-- dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 4 ++-- .../tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt | 7 ++++++- dhall/tests/type-errors/unit/VariableFree.txt | 7 ++++++- 9 files changed, 40 insertions(+), 13 deletions(-) (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 10bb9a4..e06c4b2 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1,4 +1,4 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> :6:23 | 1 | let bottom : Type = ∀(any : Type) → any @@ -8,7 +8,7 @@ Type error: Unhandled error: error: function annot mismatch ... 10 | : pow (pow U) → U 11 | = λ(t : pow (pow U)) - | ^^^^^ function annot mismatch + | ^^^^^ Wrong type of function argument | --- help: this expects an argument of type: Kind | - help: but this has type: Sort | diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index 87cf48e..e4584f5 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable ``_`` + --> :1:46 + | +1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _) + | ^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 7aa2281..776b14e 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> :1:1 | 1 | (λ(_ : Natural) → _) True - | ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument | ------------------ help: this expects an argument of type: Natural | ---- help: but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index a13fb3a..3fc1652 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> :1:6 + | +1 | λ(_ : 1) → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index a13fb3a..948c6c7 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> :1:0 + | +1 | 2 → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 3673338..125cc87 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> :1:5 | 1 | [] : List Type - | ^^^^^^^^^ function annot mismatch + | ^^^^^^^^^ Wrong type of function argument | ---- help: this expects an argument of type: Type | ---- help: but this has type: Kind | diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 795c97c..5ee2a11 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> :1:0 | 1 | Natural/subtract True True - | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument | ---------------- help: this expects an argument of type: Natural | ---- help: but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index 87cf48e..a234f9f 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `constructors` + --> :1:0 + | +1 | constructors < Left : Natural | Right : Bool > + | ^^^^^^^^^^^^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index 87cf48e..52baa7f 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `x` + --> :1:0 + | +1 | x + | ^ not found in this scope + | -- cgit v1.2.3