From b12c312dcdc067982708193cedf43073483e5043 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 16 Apr 2019 20:57:15 +0200
Subject: Fix union constructor typechecking

---
 dhall/src/typecheck.rs | 41 ++++++++++++++++++++++++-----------------
 dhall_core/src/core.rs |  6 ++++++
 2 files changed, 30 insertions(+), 17 deletions(-)

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index c41e34c..0e1a10e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -644,21 +644,27 @@ fn type_last_layer(
             kts.insert(x, t);
             Ok(RetExpr(UnionType(kts)))
         }
-        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))),
-            },
-            _ => 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))),
+        Field(r, x) => 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(MissingRecordField(x, r))),
             },
+            _ => {
+                let r = r.normalize();
+                match r.as_expr().as_ref() {
+                    UnionType(kts) => match kts.get(&x) {
+                        // Constructor has type T -> < x: T, ... >
+                        // TODO: use "_" instead of x
+                        Some(t) => Ok(RetExpr(Pi(
+                            x.clone(),
+                            t.embed_absurd(),
+                            r.embed(),
+                        ))),
+                        None => Err(mkerr(MissingUnionField(x, r))),
+                    },
+                    _ => Err(mkerr(NotARecord(x, r))),
+                }
+            }
         },
         Const(c) => Ok(RetType(type_of_const(c))),
         Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
@@ -738,8 +744,9 @@ pub(crate) enum TypeMessage<'a> {
     IfBranchMismatch(Typed<'a>, Typed<'a>),
     IfBranchMustBeTerm(bool, Typed<'a>),
     InvalidFieldType(Label, Typed<'a>),
-    NotARecord(Label, Typed<'a>),
-    MissingField(Label, Typed<'a>),
+    NotARecord(Label, Normalized<'a>),
+    MissingRecordField(Label, Typed<'a>),
+    MissingUnionField(Label, Normalized<'a>),
     BinOpTypeMismatch(BinOp, Typed<'a>),
     NoDependentTypes(Normalized<'a>, Normalized<'a>),
     Unimplemented,
@@ -974,7 +981,7 @@ mod spec_tests {
     // tc_success!(tc_success_prelude_Text_concatMapSep_1, "prelude/Text/concatMapSep/1");
     // 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_recordOfRecordOfTypes, "recordOfRecordOfTypes");
     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");
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 16c64c7..6100981 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -447,6 +447,12 @@ impl<N: Clone> Expr<N, X> {
     }
 }
 
+impl<N: Clone> SubExpr<N, X> {
+    pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
+        rc(self.as_ref().embed_absurd())
+    }
+}
+
 impl<N, E> Clone for SubExpr<N, E> {
     fn clone(&self) -> Self {
         SubExpr(Rc::clone(&self.0))
-- 
cgit v1.2.3