summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs20
-rw-r--r--dhall/tests/type-inference/failure/mixedUnions.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt6
8 files changed, 5 insertions, 57 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 361e1b4..d21c7ce 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -137,30 +137,20 @@ fn type_one_layer(
Type::from_const(k)
}
ExprKind::UnionType(kts) => {
- // Check that all types are the same const
- let mut k = None;
+ // An empty union type has type Type;
+ // an union type with only unary variants also has type Type
+ let mut k = Const::Type;
for t in kts.values() {
if let Some(t) = t {
- let c = match t.ty().as_const() {
- Some(c) => c,
+ match t.ty().as_const() {
+ Some(c) => k = max(k, c),
None => {
return mk_span_err(t.span(), "InvalidVariantType")
}
- };
- match k {
- None => k = Some(c),
- Some(k) if k == c => {}
- _ => {
- return mk_span_err(t.span(), "InvalidVariantType")
- }
}
}
}
- // An empty union type has type Type;
- // an union type with only unary variants also has type Type
- let k = k.unwrap_or(Const::Type);
-
Type::from_const(k)
}
ExprKind::Op(op) => typecheck_operation(env, span, op)?,
diff --git a/dhall/tests/type-inference/failure/mixedUnions.txt b/dhall/tests/type-inference/failure/mixedUnions.txt
deleted file mode 100644
index 2b307d0..0000000
--- a/dhall/tests/type-inference/failure/mixedUnions.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:28
- |
-1 | < Left : Natural | Right : Type >
- | ^^^^ InvalidVariantType
- |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
deleted file mode 100644
index a83bb4f..0000000
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:17
- |
-1 | { x = Type, y = Kind }
- | ^^^^ InvalidFieldType
- |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
deleted file mode 100644
index 6a6da80..0000000
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:22
- |
-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
deleted file mode 100644
index 322e7f4..0000000
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:21
- |
-1 | { x = {=} } ⫽ { x = Kind }
- | ^^^^ InvalidFieldType
- |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
deleted file mode 100644
index ae6c845..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
- |
-1 | < x : Bool | y : Type >
- | ^^^^ InvalidVariantType
- |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
deleted file mode 100644
index faf81a9..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
- |
-1 | < x : Kind | y : Type >
- | ^^^^ InvalidVariantType
- |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
deleted file mode 100644
index bbfb1f3..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
- |
-1 | < x : Kind | y : Bool >
- | ^^^^ InvalidVariantType
- |