Prepare for https://github.com/dhall-lang/dhall-lang/pull/630

4 files changed, 71 insertions, 45 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index bc8fa34..f47f1b2 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,6 +47,7 @@ pub enum Value {
     DoubleLit(NaiveDouble),
     EmptyOptionalLit(TypeThunk),
     NEOptionalLit(Thunk),
+    // EmptyListLit(t) means `[] : List t`
     EmptyListLit(TypeThunk),
     NEListLit(Vec<Thunk>),
     RecordLit(HashMap<Label, Thunk>),
@@ -128,9 +129,10 @@ impl Value {
             Value::NEOptionalLit(n) => {
                 rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
             }
-            Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
-            }
+            Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+                rc(ExprF::Builtin(Builtin::List)),
+                n.normalize_to_expr_maybe_alpha(alpha),
+            )))),
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
                 elts.iter()
                     .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index bab3fd8..66b235f 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -106,7 +106,7 @@ fn cbor_value_to_dhall(
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                EmptyListLit(t)
+                EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t)))
             }
             [U64(4), Null, rest..] => {
                 let rest = rest
@@ -413,6 +413,7 @@ where
     S: serde::ser::Serializer,
 {
     use cbor::Value::{String, I64, U64};
+    use dhall_syntax::Builtin;
     use dhall_syntax::ExprF::*;
     use std::iter::once;
 
@@ -471,7 +472,13 @@ where
         }
         Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
         SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
-        EmptyListLit(x) => ser_seq!(ser; tag(4), expr(x)),
+        EmptyListLit(x) => match x.as_ref() {
+            App(f, a) => match f.as_ref() {
+                ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)),
+                _ => unreachable!(),
+            },
+            _ => unreachable!(),
+        },
         NEListLit(xs) => ser.collect_seq(
             once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)),
         ),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 4bc0f04..2e9f258 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -622,9 +622,9 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
 
 pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
     use Value::{
-        BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit,
-        NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit,
-        UnionConstructor, UnionLit, UnionType,
+        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
+        NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
+        TextLit, UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
@@ -651,8 +651,20 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
         ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
         ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
-        ExprF::EmptyListLit(t) => {
-            Ret::Value(EmptyListLit(TypeThunk::from_thunk(t)))
+        ExprF::EmptyListLit(ref t) => {
+            // Check if the type is of the form `List x`
+            let t_borrow = t.as_value();
+            match &*t_borrow {
+                AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
+                    Ret::Value(EmptyListLit(TypeThunk::from_thunk(
+                        args[0].clone(),
+                    )))
+                }
+                _ => {
+                    drop(t_borrow);
+                    Ret::Expr(expr)
+                }
+            }
         }
         ExprF::NEListLit(elts) => {
             Ret::Value(NEListLit(elts.into_iter().collect()))
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index fc6c1da..35bf3a9 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -164,37 +164,6 @@ fn tck_union_type(
     ))
 }
 
-fn tck_list_type(ctx: &TypecheckContext, t: Type) -> Result<Typed, TypeError> {
-    use crate::error::TypeMessage::*;
-    ensure_simple_type!(
-        t,
-        TypeError::new(ctx, InvalidListType(t.to_normalized())),
-    );
-    Ok(Typed::from_thunk_and_type(
-        Value::from_builtin(Builtin::List)
-            .app(t.to_value())
-            .into_thunk(),
-        Type::from_const(Const::Type),
-    ))
-}
-
-fn tck_optional_type(
-    ctx: &TypecheckContext,
-    t: Type,
-) -> Result<Typed, TypeError> {
-    use crate::error::TypeMessage::*;
-    ensure_simple_type!(
-        t,
-        TypeError::new(ctx, InvalidOptionalType(t.to_normalized())),
-    );
-    Ok(Typed::from_thunk_and_type(
-        Value::from_builtin(Builtin::Optional)
-            .app(t.to_value())
-            .into_thunk(),
-        Type::from_const(Const::Type),
-    ))
-}
-
 fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_syntax::Const::*;
     match (a, b) {
@@ -460,7 +429,17 @@ fn type_last_layer(
         }
         EmptyListLit(t) => {
             let t = t.to_type();
-            Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
+            match &t.to_value() {
+                Value::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+                    if args.len() == 1 => {}
+                _ => {
+                    return Err(TypeError::new(
+                        ctx,
+                        InvalidListType(t.to_normalized()),
+                    ))
+                }
+            }
+            Ok(RetTypeOnly(t))
         }
         NEListLit(xs) => {
             let mut iter = xs.iter().enumerate();
@@ -476,12 +455,38 @@ fn type_last_layer(
                     ))
                 );
             }
-            let t = x.get_type()?.into_owned();
-            Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
+            let t = x.get_type()?;
+            ensure_simple_type!(
+                t,
+                TypeError::new(ctx, InvalidListType(t.to_normalized())),
+            );
+
+            Ok(RetTypeOnly(
+                Typed::from_thunk_and_type(
+                    Value::from_builtin(dhall_syntax::Builtin::List)
+                        .app(t.to_value())
+                        .into_thunk(),
+                    Type::from_const(dhall_syntax::Const::Type),
+                )
+                .to_type(),
+            ))
         }
         SomeLit(x) => {
             let t = x.get_type()?.into_owned();
-            Ok(RetTypeOnly(tck_optional_type(ctx, t)?.to_type()))
+            ensure_simple_type!(
+                t,
+                TypeError::new(ctx, InvalidOptionalType(t.to_normalized())),
+            );
+
+            Ok(RetTypeOnly(
+                Typed::from_thunk_and_type(
+                    Value::from_builtin(dhall_syntax::Builtin::Optional)
+                        .app(t.to_value())
+                        .into_thunk(),
+                    Type::from_const(dhall_syntax::Const::Type),
+                )
+                .to_type(),
+            ))
         }
         RecordType(kts) => Ok(RetWhole(tck_record_type(
             ctx,