From 9953043a604556018ba2b1446831aae18f7e7c78 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 16 Apr 2019 20:08:41 +0200
Subject: Typecheck union constructor

---
 dhall/src/typecheck.rs | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'dhall')

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");
-- 
cgit v1.2.3