summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
m---------dhall-lang0
-rw-r--r--dhall/src/error/mod.rs2
-rw-r--r--dhall/src/phase/typecheck.rs68
3 files changed, 17 insertions, 53 deletions
diff --git a/dhall-lang b/dhall-lang
-Subproject 235d2c0b11a539003d2de6110f8666e93ae1ccd
+Subproject 3d66b4cd56627a39b6c615882beab97fbdf9d13
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 3445768..13a9d7e 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -79,10 +79,8 @@ pub(crate) enum TypeMessage {
ProjectionMustBeRecord,
ProjectionMissingEntry,
Sort,
- RecordMismatch(Value, Value),
RecordTypeDuplicateField,
RecordTypeMergeRequiresRecordType(Value),
- RecordTypeMismatch(Value, Value, Value, Value),
UnionTypeDuplicateField,
EquivalenceArgumentMustBeTerm(bool, Value),
EquivalenceTypeMismatch(Value, Value),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 77ef689..8a3b43a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,3 +1,4 @@
+use std::cmp::max;
use std::collections::HashMap;
use dhall_syntax::{
@@ -50,15 +51,16 @@ fn tck_record_type(
use crate::error::TypeMessage::*;
use std::collections::hash_map::Entry;
let mut new_kts = HashMap::new();
- // Check that all types are the same const
- let mut k = None;
+ // An empty record type has type Type
+ let mut k = Const::Type;
for e in kts {
let (x, t) = e?;
- match (k, t.get_type()?.as_const()) {
- (None, Some(k2)) => k = Some(k2),
- (Some(k1), Some(k2)) if k1 == k2 => {}
- _ => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
+ // Construct the union of the contained `Const`s
+ match t.get_type()?.as_const() {
+ Some(k2) => k = max(k, k2),
+ None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
}
+ // Check for duplicated entries
let entry = new_kts.entry(x);
match &entry {
Entry::Occupied(_) => {
@@ -67,8 +69,6 @@ fn tck_record_type(
Entry::Vacant(_) => entry.or_insert_with(|| t),
};
}
- // An empty record type has type Type
- let k = k.unwrap_or(Const::Type);
Ok(Value::from_valuef_and_type(
ValueF::RecordType(new_kts),
@@ -122,7 +122,6 @@ where
}
fn function_check(a: Const, b: Const) -> Const {
- use std::cmp::max;
if b == Const::Type {
Const::Type
} else {
@@ -546,16 +545,7 @@ fn type_last_layer(
use crate::phase::normalize::merge_maps;
let l_type = l.get_type()?;
- let l_kind = l_type.get_type()?;
let r_type = r.get_type()?;
- let r_kind = r_type.get_type()?;
-
- // Check the equality of kinds.
- // This is to disallow expression such as:
- // "{ x = Text } // { y = 1 }"
- if l_kind != r_kind {
- return mkerr(RecordMismatch(l.clone(), r.clone()));
- }
// Extract the LHS record type
let l_type_borrow = l_type.as_whnf();
@@ -581,28 +571,14 @@ fn type_last_layer(
kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
)?)
}
- BinOp(RecursiveRecordMerge, l, r) => {
- let l_type = l.get_type()?;
- let l_kind = l_type.get_type()?;
- let r_type = r.get_type()?;
- let r_kind = r_type.get_type()?;
-
- // Check the equality of kinds.
- // This is to disallow expression such as:
- // "{ x = Text } // { y = 1 }"
- if l_kind != r_kind {
- return mkerr(RecordMismatch(l.clone(), r.clone()));
- }
-
- RetTypeOnly(type_last_layer(
- ctx,
- ExprF::BinOp(
- RecursiveRecordTypeMerge,
- l_type.into_owned(),
- r_type.into_owned(),
- ),
- )?)
- }
+ BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+ ctx,
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ l.get_type()?.into_owned(),
+ r.get_type()?.into_owned(),
+ ),
+ )?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
use crate::phase::normalize::intersection_with_key;
@@ -622,17 +598,7 @@ fn type_last_layer(
}
};
- // Const values must match for the Records
- let k = if k_l == k_r {
- k_l
- } else {
- return mkerr(RecordTypeMismatch(
- Value::from_const(k_l),
- Value::from_const(k_r),
- l.clone(),
- r.clone(),
- ));
- };
+ let k = max(k_l, k_r);
// Extract the LHS record type
let borrow_l = l.as_whnf();