summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs54
1 files changed, 33 insertions, 21 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index c8929fe..8e36d11 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -220,6 +220,10 @@ fn const_to_normalized<'a>(c: Const) -> Normalized<'a> {
)
}
+fn const_to_type<'a>(c: Const) -> Type<'a> {
+ Type(TypeInternal::Const(c))
+}
+
pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> {
match c {
Const::Type => Type::const_kind(),
@@ -601,22 +605,31 @@ fn type_last_layer(
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
- for (k, t) in kts {
- ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)));
+ // Check that all types are the same const
+ let mut k = None;
+ for (x, t) in kts {
+ let k2 = ensure_is_const!(
+ t.get_type()?,
+ mkerr(InvalidFieldType(x, t))
+ );
+ match k {
+ None => k = Some(k2),
+ Some(k1) if k1 != k2 => {
+ return Err(mkerr(InvalidFieldType(x, t)))
+ }
+ Some(_) => {}
+ }
}
- Ok(RetType(crate::expr::Type::const_type()))
+ // An empty record type has type Type
+ let k = k.unwrap_or(dhall_core::Const::Type);
+ Ok(RetType(const_to_type(k)))
}
RecordLit(kvs) => {
let kts = kvs
.into_iter()
- .map(|(k, v)| {
- ensure_simple_type!(
- v.get_type()?,
- mkerr(InvalidField(k, v)),
- );
- let t = v.get_type_move()?;
- let t = t.embed()?;
- Ok((k, t))
+ .map(|(x, v)| {
+ let t = v.get_type_move()?.embed()?;
+ Ok((x, t))
})
.collect::<Result<_, _>>()?;
Ok(RetExpr(RecordType(kts)))
@@ -705,7 +718,6 @@ pub(crate) enum TypeMessage<'a> {
InvalidPredicate(Typed<'a>),
IfBranchMismatch(Typed<'a>, Typed<'a>),
IfBranchMustBeTerm(bool, Typed<'a>),
- InvalidField(Label, Typed<'a>),
InvalidFieldType(Label, Typed<'a>),
NotARecord(Label, Typed<'a>),
MissingField(Label, Typed<'a>),
@@ -944,7 +956,7 @@ mod spec_tests {
// tc_success!(tc_success_prelude_Text_concatSep_0, "prelude/Text/concatSep/0");
// tc_success!(tc_success_prelude_Text_concatSep_1, "prelude/Text/concatSep/1");
// tc_success!(tc_success_recordOfRecordOfTypes, "recordOfRecordOfTypes");
- // tc_success!(tc_success_recordOfTypes, "recordOfTypes");
+ tc_success!(tc_success_recordOfTypes, "recordOfTypes");
// tc_success!(tc_success_simple_access_0, "simple/access/0");
// tc_success!(tc_success_simple_access_1, "simple/access/1");
// tc_success!(tc_success_simple_alternativesAreTypes, "simple/alternativesAreTypes");
@@ -969,9 +981,9 @@ mod spec_tests {
ti_success!(ti_success_unit_Function, "unit/Function");
ti_success!(ti_success_unit_FunctionApplication, "unit/FunctionApplication");
ti_success!(ti_success_unit_FunctionNamedArg, "unit/FunctionNamedArg");
- // ti_success!(ti_success_unit_FunctionTypeKindKind, "unit/FunctionTypeKindKind");
- // ti_success!(ti_success_unit_FunctionTypeKindTerm, "unit/FunctionTypeKindTerm");
- // ti_success!(ti_success_unit_FunctionTypeKindType, "unit/FunctionTypeKindType");
+ ti_success!(ti_success_unit_FunctionTypeKindKind, "unit/FunctionTypeKindKind");
+ ti_success!(ti_success_unit_FunctionTypeKindTerm, "unit/FunctionTypeKindTerm");
+ ti_success!(ti_success_unit_FunctionTypeKindType, "unit/FunctionTypeKindType");
ti_success!(ti_success_unit_FunctionTypeTermTerm, "unit/FunctionTypeTermTerm");
ti_success!(ti_success_unit_FunctionTypeTypeTerm, "unit/FunctionTypeTypeTerm");
ti_success!(ti_success_unit_FunctionTypeTypeType, "unit/FunctionTypeTypeType");
@@ -982,7 +994,7 @@ mod spec_tests {
ti_success!(ti_success_unit_IntegerLiteral, "unit/IntegerLiteral");
// ti_success!(ti_success_unit_IntegerShow, "unit/IntegerShow");
// ti_success!(ti_success_unit_IntegerToDouble, "unit/IntegerToDouble");
- // ti_success!(ti_success_unit_Kind, "unit/Kind");
+ ti_success!(ti_success_unit_Kind, "unit/Kind");
ti_success!(ti_success_unit_Let, "unit/Let");
ti_success!(ti_success_unit_LetNestedTypeSynonym, "unit/LetNestedTypeSynonym");
ti_success!(ti_success_unit_LetTypeSynonym, "unit/LetTypeSynonym");
@@ -1033,8 +1045,8 @@ mod spec_tests {
// ti_success!(ti_success_unit_OptionalBuild, "unit/OptionalBuild");
ti_success!(ti_success_unit_OptionalFold, "unit/OptionalFold");
ti_success!(ti_success_unit_RecordEmpty, "unit/RecordEmpty");
- // ti_success!(ti_success_unit_RecordOneKind, "unit/RecordOneKind");
- // ti_success!(ti_success_unit_RecordOneType, "unit/RecordOneType");
+ ti_success!(ti_success_unit_RecordOneKind, "unit/RecordOneKind");
+ ti_success!(ti_success_unit_RecordOneType, "unit/RecordOneType");
ti_success!(ti_success_unit_RecordOneValue, "unit/RecordOneValue");
// ti_success!(ti_success_unit_RecordProjectionEmpty, "unit/RecordProjectionEmpty");
// ti_success!(ti_success_unit_RecordProjectionKind, "unit/RecordProjectionKind");
@@ -1045,8 +1057,8 @@ mod spec_tests {
ti_success!(ti_success_unit_RecordSelectionValue, "unit/RecordSelectionValue");
ti_success!(ti_success_unit_RecordType, "unit/RecordType");
ti_success!(ti_success_unit_RecordTypeEmpty, "unit/RecordTypeEmpty");
- // ti_success!(ti_success_unit_RecordTypeKind, "unit/RecordTypeKind");
- // ti_success!(ti_success_unit_RecordTypeType, "unit/RecordTypeType");
+ ti_success!(ti_success_unit_RecordTypeKind, "unit/RecordTypeKind");
+ ti_success!(ti_success_unit_RecordTypeType, "unit/RecordTypeType");
// ti_success!(ti_success_unit_RecursiveRecordMergeLhsEmpty, "unit/RecursiveRecordMergeLhsEmpty");
// ti_success!(ti_success_unit_RecursiveRecordMergeRecursively, "unit/RecursiveRecordMergeRecursively");
// ti_success!(ti_success_unit_RecursiveRecordMergeRecursivelyTypes, "unit/RecursiveRecordMergeRecursivelyTypes");