Merge pull request #131 from Nadrieril/hir

Decouple main expression types

21 files changed, 79 insertions, 29 deletions

diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
index 2a754fc..a39a0fb 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+Type error: error: annot mismatch: { x : Natural } != { y : Natural }
  --> <current file>:1:0
   |
 1 | { x = 1 } : { y : Natural }
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+  | ^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural }
   |
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
index e67edb8..9ecc2a4 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+Type error: error: annot mismatch: { x : Natural } != { x : Text }
  --> <current file>:1:0
   |
 1 | { x = 1 } : { x : Text }
-  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+  | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
index d0a9a01..7a4a12c 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
  --> <current file>:1:4
   |
 ...
 6 | in  Example::{=}
-  |     ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+  |     ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
index d4639e9..9235ed4 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
  --> <current file>:1:4
   |
 ...
 6 | in  Example::{=}
-  |     ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+  |     ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
index 0839742..6a6cd1e 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
  --> <current file>:1:4
   |
 ...
 6 | in  Example::{ nam = "John Doe" }
-  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
index 7edef95..b4fe726 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
  --> <current file>:1:4
   |
 ...
 6 | in  Example::{ name = True }
-  |     ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+  |     ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
index e84eb15..ca5bbcd 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `1`
  --> <current file>:1:6
   |
 1 | λ(_ : 1) → _
   |       ^ this has type: `Natural`
   |
-  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+  = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
index 4aa0f4f..168ebb9 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `2`
  --> <current file>:1:0
   |
 1 | 2 → _
   | ^ this has type: `Natural`
   |
-  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+  = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
index 5b88ff7..6f26607 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+  |
+1 | Kind → Sort
+  |        ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
index 5b88ff7..169014b 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+  |
+1 | Type → Sort
+  |        ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
index 5ba4b35..51279f2 100644
--- a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (True : Bool) : Natural
- --> <current file>:1:8
+Type error: error: annot mismatch: Bool != Natural
+ --> <current file>:1:18
   |
 1 | let x : Natural = True in True
-  |         ^^^^^^^ annot mismatch: (True : Bool) : Natural
+  |                   ^^^^ annot mismatch: Bool != Natural
   |
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
index 5332fcb..0cc4bba 100644
--- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ([1] : List Natural) : Optional Natural
+Type error: error: annot mismatch: List Natural != Optional Natural
  --> <current file>:1:0
   |
 1 | [ 1 ] : Optional Natural
-  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ([1] : List Natural) : Optional Natural
+  | ^^^^^ annot mismatch: List Natural != Optional Natural
   |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index 5b88ff7..146018f 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+  |
+1 | { x = Type, y = Kind }
+  | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
index f74e839..02cf64f 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | True ∧ {=}
+  | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
index f74e839..202a3e5 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | { x = True } ∧ { x = False }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
index f74e839..a0b4676 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | {=} ∧ True
+  | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
index f74e839..769712b 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -1 +1,6 @@
 Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+  |
+1 | { x : Bool } ⩓ { x : Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index 5b88ff7..521ae05 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:15
+  |
+1 | { x = Bool } ⫽ { x = Kind }
+  |                ^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index 5b88ff7..3abf62c 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:14
+  |
+1 | { x = {=} } ⫽ { x = Kind }
+  |               ^^^^^^^^^^^^ InvalidFieldType
+  |
diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt
index 5b88ff7..e402127 100644
--- a/dhall/tests/type-inference/failure/unit/Sort.txt
+++ b/dhall/tests/type-inference/failure/unit/Sort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:0
+  |
+1 | Sort
+  | ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
index 7360e68..dffadb1 100644
--- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (1 : Natural) : Bool
+Type error: error: annot mismatch: Natural != Bool
  --> <current file>:1:0
   |
 1 | 1 : Bool
-  | ^^^^^^^^ annot mismatch: (1 : Natural) : Bool
+  | ^ annot mismatch: Natural != Bool
   |