From 37acac4b972b38e8dbe2d174dae1031e5a8eda67 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 16:09:35 +0000
Subject: Tweak: handle empty lists in typeck

---
 dhall/src/semantics/phase/normalize.rs | 20 ++++----------------
 dhall/src/semantics/phase/typecheck.rs | 14 ++++++++++----
 2 files changed, 14 insertions(+), 20 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 615b2ff..8f9a58a 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -590,9 +590,9 @@ pub(crate) fn normalize_one_layer(
     ty: &Value,
 ) -> ValueKind<Value> {
     use ValueKind::{
-        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit,
-        IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
-        UnionConstructor, UnionLit, UnionType,
+        BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
+        NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor,
+        UnionLit, UnionType,
     };
 
     let ret = match expr {
@@ -609,6 +609,7 @@ pub(crate) fn normalize_one_layer(
         | ExprKind::Builtin(_)
         | ExprKind::Var(_)
         | ExprKind::Annot(_, _)
+        | ExprKind::EmptyListLit(_)
         | ExprKind::RecordType(_)
         | ExprKind::UnionType(_) => {
             unreachable!("This case should have been handled in typecheck")
@@ -620,19 +621,6 @@ pub(crate) fn normalize_one_layer(
         ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
         ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
-        ExprKind::EmptyListLit(ref t) => {
-            // Check if the type is of the form `List x`
-            let t_borrow = t.as_whnf();
-            match &*t_borrow {
-                AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::ValueKind(EmptyListLit(args[0].clone()))
-                }
-                _ => {
-                    drop(t_borrow);
-                    Ret::Expr(expr)
-                }
-            }
-        }
         ExprKind::NEListLit(elts) => {
             Ret::ValueKind(NEListLit(elts.into_iter().collect()))
         }
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c77d9c4..852f41b 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -433,12 +433,18 @@ fn type_last_layer(
             RetTypeOnly(y.get_type()?)
         }
         EmptyListLit(t) => {
-            match &*t.as_whnf() {
+            let arg = match &*t.as_whnf() {
                 ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
-                    if args.len() == 1 => {}
+                    if args.len() == 1 =>
+                {
+                    args[0].clone()
+                }
                 _ => return mkerr(InvalidListType(t.clone())),
-            }
-            RetTypeOnly(t.clone())
+            };
+            RetWhole(Value::from_kind_and_type(
+                ValueKind::EmptyListLit(arg),
+                t.clone(),
+            ))
         }
         NEListLit(xs) => {
             let mut iter = xs.iter().enumerate();
-- 
cgit v1.2.3