spec: allow unions with mixed kinds

11 files changed, 6 insertions, 58 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 23997c5..9ac4b21 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 #### [Unreleased]
 
+- Allow unions with mixed kinds
 - Adjust precedence of `===` and `with`
 - Fix running tests on Windows. Developing on this lib should now be possible on Windows.
 
diff --git a/dhall-lang b/dhall-lang
-Subproject b788d6dd2150eec49b6bdd0cc7de50e403fad88
+Subproject 5973964062be2e7ea6ff7300a46616086dd9143
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
-  |
diff --git a/tests_buffer b/tests_buffer
index e01d7a7..80fa833 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -35,6 +35,5 @@ failure/
     merge { x = True, y = 1 } < x | y >.x
     merge {x=...,y=...} <x>.x
     merge {x=...,y=...} <x:T>.x
-fix unit_RightBiasedRecordMergeMixedKinds3 & 2 & unit_RecordMixedKinds3
 
 equivalence: