diff options
| -rw-r--r-- | dhall/src/typecheck.rs | 54 |
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"); |