summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs21
1 files changed, 15 insertions, 6 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 3cc67f2..c41e34c 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -644,13 +644,22 @@ fn type_last_layer(
kts.insert(x, t);
Ok(RetExpr(UnionType(kts)))
}
- Field(r, x) => ensure_matches!(r.get_type()?,
- RecordType(kts) => match kts.get(&x) {
- Some(e) => Ok(RetExpr(e.unroll().absurd_rec())),
+ Field(r, x) => match r.as_expr().as_ref() {
+ UnionType(kts) => match kts.get(&x) {
+ // Constructor has type T -> < x: T, ... >
+ Some(t) => {
+ Ok(RetExpr(Pi(x.clone(), t.clone(), r.normalize().embed())))
+ }
None => Err(mkerr(MissingField(x, r))),
},
- mkerr(NotARecord(x, r))
- ),
+ _ => match r.get_type()?.unroll_ref()?.as_ref() {
+ RecordType(kts) => match kts.get(&x) {
+ Some(t) => Ok(RetExpr(t.unroll().absurd_rec())),
+ None => Err(mkerr(MissingField(x, r))),
+ },
+ _ => Err(mkerr(NotARecord(x, r))),
+ },
+ },
Const(c) => Ok(RetType(type_of_const(c))),
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
BoolLit(_) => Ok(RetType(simple_type_from_builtin(Bool))),
@@ -1096,7 +1105,7 @@ mod spec_tests {
ti_success!(ti_success_unit_True, "unit/True");
ti_success!(ti_success_unit_Type, "unit/Type");
ti_success!(ti_success_unit_TypeAnnotation, "unit/TypeAnnotation");
- // ti_success!(ti_success_unit_UnionConstructorField, "unit/UnionConstructorField");
+ ti_success!(ti_success_unit_UnionConstructorField, "unit/UnionConstructorField");
ti_success!(ti_success_unit_UnionOne, "unit/UnionOne");
ti_success!(ti_success_unit_UnionTypeEmpty, "unit/UnionTypeEmpty");
ti_success!(ti_success_unit_UnionTypeKind, "unit/UnionTypeKind");