Typecheck projection by type

2 files changed, 25 insertions, 12 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index 5523ef3..36acc02 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -309,10 +309,6 @@ fn generate_tests() -> std::io::Result<()> {
                 false
                     // Too slow
                     || path == "prelude"
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByType"
-                    || path == "unit/RecordProjectionByTypeEmpty"
-                    || path == "unit/RecordProjectionByTypeJudgmentalEquality"
                     // TODO: record completion
                     || path == "simple/completion"
                     || path == "unit/Completion"
@@ -326,9 +322,6 @@ fn generate_tests() -> std::io::Result<()> {
             variant: "TypeInferenceFailure",
             path_filter: Box::new(|path: &str| {
                 false
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
-                    || path == "unit/RecordProjectionByTypeNotPresent"
                     // TODO: record completion
                     || path == "unit/CompletionMissingRequiredField"
                     || path == "unit/CompletionWithWrongDefaultType"
@@ -346,9 +339,6 @@ fn generate_tests() -> std::io::Result<()> {
             variant: "TypeError",
             path_filter: Box::new(|path: &str| {
                 false
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
-                    || path == "unit/RecordProjectionByTypeNotPresent"
                     // TODO: record completion
                     || path == "unit/CompletionMissingRequiredField"
                     || path == "unit/CompletionWithWrongDefaultType"
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 516ef42..e3ae129 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -726,8 +726,31 @@ fn type_one_layer(
                 record_type.get_type()?,
             )
         }
-        ExprKind::ProjectionByExpr(_, _) => {
-            unimplemented!("selection by expression")
+        ExprKind::ProjectionByExpr(record, selection) => {
+            let record_type = record.get_type()?;
+            let rec_kts = match record_type.kind() {
+                ValueKind::RecordType(kts) => kts,
+                _ => return span_err("ProjectionMustBeRecord"),
+            };
+
+            let selection_val = selection.eval(env.as_nzenv());
+            let sel_kts = match selection_val.kind() {
+                ValueKind::RecordType(kts) => kts,
+                _ => return span_err("ProjectionByExprTakesRecordType"),
+            };
+
+            for (l, sel_ty) in sel_kts {
+                match rec_kts.get(l) {
+                    Some(rec_ty) => {
+                        if rec_ty != sel_ty {
+                            return span_err("ProjectionWrongType");
+                        }
+                    }
+                    None => return span_err("ProjectionMissingEntry"),
+                }
+            }
+
+            selection_val
         }
         ExprKind::Completion(_, _) => unimplemented!("record completion"),
     })