From 04438824db21fb5d9d3a2abdb3fa167875bda892 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 16:39:27 +0200
Subject: Add Value::from_builtin

---
 dhall/src/core/value.rs      |  7 +++++--
 dhall/src/core/valuef.rs     | 10 ----------
 dhall/src/phase/normalize.rs | 44 +++++++++++++++++++-------------------------
 3 files changed, 24 insertions(+), 37 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5367c86..f897f16 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,14 +2,14 @@ use std::borrow::Cow;
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
-use dhall_syntax::Const;
+use dhall_syntax::{Builtin, Const};
 
 use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
-use crate::phase::typecheck::const_to_value;
+use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
@@ -115,6 +115,9 @@ impl Value {
     pub fn const_type() -> Self {
         Value::from_const(Const::Type)
     }
+    pub fn from_builtin(b: Builtin) -> Self {
+        builtin_to_value(b)
+    }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.as_whnf() {
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 0c3058d..da03cbd 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -257,16 +257,6 @@ impl ValueF {
         }
     }
 
-    /// Apply to a valuef
-    pub(crate) fn app(self, val: ValueF) -> ValueF {
-        self.app_valuef(val)
-    }
-
-    /// Apply to a valuef
-    pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
-        self.app_value(val.into_value_untyped())
-    }
-
     /// Apply to a value
     pub fn app_value(self, th: Value) -> ValueF {
         Value::from_valuef_untyped(self).app_value(th)
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a379a4b..f943171 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -31,11 +31,10 @@ macro_rules! make_closure {
         ).into_value_untyped()
     };
     (Natural) => {
-        ValueF::from_builtin(Builtin::Natural)
-            .into_value_simple_type()
+        Value::from_builtin(Builtin::Natural)
     };
     (List $($rest:tt)*) => {
-        ValueF::from_builtin(Builtin::List)
+        Value::from_builtin(Builtin::List)
             .app_value(make_closure!($($rest)*))
             .into_value_simple_type()
     };
@@ -192,10 +191,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
         (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(t) => {
                 let mut kts = HashMap::new();
-                kts.insert(
-                    "index".into(),
-                    Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
-                );
+                kts.insert("index".into(), Value::from_builtin(Natural));
                 kts.insert("value".into(), t.clone());
                 Ok((
                     r,
@@ -232,7 +228,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 }
             }
             _ => {
-                let list_t = ValueF::from_builtin(List)
+                let list_t = Value::from_builtin(List)
                     .app_value(t.clone())
                     .into_value_simple_type();
                 Ok((
@@ -280,7 +276,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 }
             }
             _ => {
-                let optional_t = ValueF::from_builtin(Optional)
+                let optional_t = Value::from_builtin(Optional)
                     .app_value(t.clone())
                     .into_value_simple_type();
                 Ok((
@@ -309,26 +305,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                     unimplemented!()
                 }
             }
-            _ => {
-                let nat_type =
-                    ValueF::from_builtin(Natural).into_value_simple_type();
-                Ok((
-                    r,
-                    f.app_value(nat_type.clone())
-                        .app_value(
-                            make_closure!(λ(x : Natural) -> 1 + var(x, 0)),
-                        )
-                        .app_value(
-                            NaturalLit(0).into_value_with_type(nat_type),
-                        ),
-                ))
-            }
+            _ => Ok((
+                r,
+                f.app_value(Value::from_builtin(Natural))
+                    .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                    .app_value(
+                        NaturalLit(0)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    ),
+            )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
             NaturalLit(0) => Ok((r, zero.to_whnf())),
             NaturalLit(n) => {
-                let fold = ValueF::from_builtin(NaturalFold)
-                    .app(NaturalLit(n - 1))
+                let fold = Value::from_builtin(NaturalFold)
+                    .app_value(
+                        NaturalLit(n - 1)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    )
                     .app_value(t.clone())
                     .app_value(succ.clone())
                     .app_value(zero.clone())
-- 
cgit v1.2.3


From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 17:08:01 +0200
Subject: Naming tweaks

---
 dhall/src/core/value.rs      |  6 ++---
 dhall/src/core/valuef.rs     | 11 +++++-----
 dhall/src/phase/normalize.rs | 52 ++++++++++++++++++++------------------------
 dhall/src/phase/typecheck.rs |  5 ++---
 serde_dhall/src/lib.rs       |  6 ++---
 5 files changed, 35 insertions(+), 45 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index f897f16..5055ac2 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -8,7 +8,7 @@ use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
+use crate::phase::normalize::{apply_any, normalize_whnf};
 use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
@@ -208,11 +208,11 @@ impl Value {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         self.as_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app_value(&self, th: Value) -> ValueF {
+    pub(crate) fn app(&self, th: Value) -> ValueF {
         apply_any(self.clone(), th)
     }
 
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index da03cbd..e9049c7 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,8 +7,7 @@ use dhall_syntax::{
 
 use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::OutputSubExpr;
-use crate::phase::Normalized;
+use crate::phase::{Normalized, NormalizedSubExpr};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
 /// normalized on-demand.
@@ -59,7 +58,7 @@ impl ValueF {
     }
 
     /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
         self.normalize_to_expr_maybe_alpha(false)
     }
     /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -67,7 +66,7 @@ impl ValueF {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         match self {
             ValueF::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
@@ -258,8 +257,8 @@ impl ValueF {
     }
 
     /// Apply to a value
-    pub fn app_value(self, th: Value) -> ValueF {
-        Value::from_valuef_untyped(self).app_value(th)
+    pub fn app(self, th: Value) -> ValueF {
+        Value::from_valuef_untyped(self).app(th)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index f943171..afc2e7f 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -8,9 +8,7 @@ use dhall_syntax::{
 use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
-
-pub(crate) type OutputSubExpr = NormalizedSubExpr;
+use crate::phase::Normalized;
 
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
@@ -35,7 +33,7 @@ macro_rules! make_closure {
     };
     (List $($rest:tt)*) => {
         Value::from_builtin(Builtin::List)
-            .app_value(make_closure!($($rest)*))
+            .app(make_closure!($($rest)*))
             .into_value_simple_type()
     };
     (Some($($rest:tt)*)) => {
@@ -229,12 +227,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => {
                 let list_t = Value::from_builtin(List)
-                    .app_value(t.clone())
+                    .app(t.clone())
                     .into_value_simple_type();
                 Ok((
                     r,
-                    f.app_value(list_t.clone())
-                        .app_value({
+                    f.app(list_t.clone())
+                        .app({
                             // Move `t` under new `x` variable
                             let t1 = t.under_binder(Label::from("x"));
                             make_closure!(
@@ -243,7 +241,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                                 [ var(x, 1) ] # var(xs, 0)
                             )
                         })
-                        .app_value(
+                        .app(
                             EmptyListLit(t.clone())
                                 .into_value_with_type(list_t),
                         ),
@@ -255,11 +253,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().rev() {
-                    v = cons
-                        .clone()
-                        .app_value(x.clone())
-                        .app_value(v)
-                        .into_value_untyped();
+                    v = cons.clone().app(x.clone()).app(v).into_value_untyped();
                 }
                 Ok((r, v.to_whnf()))
             }
@@ -277,13 +271,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => {
                 let optional_t = Value::from_builtin(Optional)
-                    .app_value(t.clone())
+                    .app(t.clone())
                     .into_value_simple_type();
                 Ok((
                     r,
-                    f.app_value(optional_t.clone())
-                        .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
-                        .app_value(
+                    f.app(optional_t.clone())
+                        .app(make_closure!(λ(x: #t) -> Some(var(x, 0))))
+                        .app(
                             EmptyOptionalLit(t.clone())
                                 .into_value_with_type(optional_t),
                         ),
@@ -292,7 +286,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
             EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
-            NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
+            NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
             _ => Err(()),
         },
         (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
@@ -307,9 +301,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => Ok((
                 r,
-                f.app_value(Value::from_builtin(Natural))
-                    .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
-                    .app_value(
+                f.app(Value::from_builtin(Natural))
+                    .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                    .app(
                         NaturalLit(0)
                             .into_value_with_type(Value::from_builtin(Natural)),
                     ),
@@ -319,15 +313,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             NaturalLit(0) => Ok((r, zero.to_whnf())),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
-                    .app_value(
+                    .app(
                         NaturalLit(n - 1)
                             .into_value_with_type(Value::from_builtin(Natural)),
                     )
-                    .app_value(t.clone())
-                    .app_value(succ.clone())
-                    .app_value(zero.clone())
+                    .app(t.clone())
+                    .app(succ.clone())
+                    .app(zero.clone())
                     .into_value_with_type(t.clone());
-                Ok((r, succ.app_value(fold)))
+                Ok((r, succ.app(fold)))
             }
             _ => Err(()),
         },
@@ -337,7 +331,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
         Ok((unconsumed_args, mut v)) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
-                v = v.app_value(x);
+                v = v.app(x);
             }
             v
         }
@@ -621,7 +615,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
         ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
-        ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
+        ExprF::App(v, a) => Ret::ValueF(v.app(a)),
         ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
         ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -743,7 +737,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::ValueF(h.app_value(v.clone())),
+                    Some(h) => Ret::ValueF(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 1ea87d1..440d694 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -457,7 +457,7 @@ fn type_last_layer(
 
             RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app_value(t.into_owned()),
+                    .app(t.into_owned()),
                 Value::from_const(Type),
             ))
         }
@@ -468,8 +468,7 @@ fn type_last_layer(
             }
 
             RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app_value(t),
+                ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t),
                 Value::from_const(Type),
             ))
         }
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index cef11dd..4171fab 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -169,14 +169,12 @@ pub mod value {
         }
         pub(crate) fn make_optional_type(t: Value) -> Self {
             Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::Optional)
-                    .app_value(t.to_value()),
+                DhallValueF::from_builtin(Builtin::Optional).app(t.to_value()),
             )
         }
         pub(crate) fn make_list_type(t: Value) -> Self {
             Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::List)
-                    .app_value(t.to_value()),
+                DhallValueF::from_builtin(Builtin::List).app(t.to_value()),
             )
         }
         // Made public for the StaticType derive macro
-- 
cgit v1.2.3


From 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 18:03:59 +0200
Subject: Introduce a new enum to store either a Value or a ValueF

---
 dhall/src/core/value.rs      |  54 ++++++++++++++++-
 dhall/src/core/valuef.rs     |   9 ++-
 dhall/src/phase/normalize.rs | 141 +++++++++++++++++++++++++------------------
 dhall/src/phase/typecheck.rs |  17 +++---
 serde_dhall/src/lib.rs       |   8 ++-
 5 files changed, 153 insertions(+), 76 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5055ac2..25fcaae 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,6 +44,14 @@ struct ValueInternal {
 #[derive(Clone)]
 pub struct Value(Rc<RefCell<ValueInternal>>);
 
+/// When a function needs to return either a freshly created ValueF or an existing Value, but
+/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
+/// avoid loss of typ information.
+pub enum VoVF {
+    Value(Value),
+    ValueF(ValueF),
+}
+
 impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
@@ -56,7 +64,8 @@ impl ValueInternal {
         take_mut::take(self, |vint| match &vint.form {
             Unevaled => ValueInternal {
                 form: WHNF,
-                value: normalize_whnf(vint.value),
+                // TODO: thunk chaining
+                value: normalize_whnf(vint.value).into_whnf(),
                 ty: vint.ty,
             },
             // Already in WHNF
@@ -166,6 +175,9 @@ impl Value {
     pub(crate) fn into_typed(self) -> Typed {
         Typed::from_value(self)
     }
+    pub(crate) fn into_vovf(self) -> VoVF {
+        VoVF::Value(self)
+    }
 
     /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
     fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
@@ -212,8 +224,8 @@ impl Value {
         self.as_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app(&self, th: Value) -> ValueF {
-        apply_any(self.clone(), th)
+    pub(crate) fn app(&self, v: Value) -> VoVF {
+        apply_any(self.clone(), v)
     }
 
     pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
@@ -221,6 +233,42 @@ impl Value {
     }
 }
 
+impl VoVF {
+    pub fn into_whnf(self) -> ValueF {
+        match self {
+            VoVF::Value(v) => v.to_whnf(),
+            VoVF::ValueF(v) => v,
+        }
+    }
+    pub(crate) fn into_value_untyped(self) -> Value {
+        match self {
+            VoVF::Value(v) => v,
+            VoVF::ValueF(v) => v.into_value_untyped(),
+        }
+    }
+    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+        match self {
+            // TODO: check type with debug_assert ?
+            VoVF::Value(v) => v,
+            VoVF::ValueF(v) => v.into_value_with_type(t),
+        }
+    }
+    pub(crate) fn into_value_simple_type(self) -> Value {
+        match self {
+            // TODO: check type with debug_assert ?
+            VoVF::Value(v) => v,
+            VoVF::ValueF(v) => v.into_value_simple_type(),
+        }
+    }
+
+    pub(crate) fn app(self, x: Value) -> Self {
+        match self {
+            VoVF::Value(v) => v.app(x),
+            VoVF::ValueF(v) => v.into_value_untyped().app(x),
+        }
+    }
+}
+
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index e9049c7..80978a7 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::Value;
+use crate::core::value::{Value, VoVF};
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
 
@@ -56,6 +56,9 @@ impl ValueF {
     pub(crate) fn into_value_simple_type(self) -> Value {
         Value::from_valuef_simple_type(self)
     }
+    pub(crate) fn into_vovf(self) -> VoVF {
+        VoVF::ValueF(self)
+    }
 
     /// Convert the value to a fully normalized syntactic expression
     pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
@@ -257,8 +260,8 @@ impl ValueF {
     }
 
     /// Apply to a value
-    pub fn app(self, th: Value) -> ValueF {
-        Value::from_valuef_untyped(self).app(th)
+    pub fn app(self, v: Value) -> VoVF {
+        self.into_vovf().app(v)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index afc2e7f..e044018 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::value::Value;
+use crate::core::value::{Value, VoVF};
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::phase::Normalized;
@@ -63,44 +63,48 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
+        (OptionalNone, [t, r..]) => {
+            Ok((r, EmptyOptionalLit(t.clone()).into_vovf()))
+        }
         (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
+            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())),
             _ => Err(()),
         },
         (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())),
             _ => Err(()),
         },
         (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())),
             _ => Err(()),
         },
         (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
+            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())),
             _ => Err(()),
         },
         (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
+                TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
+                    .into_vovf(),
             )),
             _ => Err(()),
         },
         (NaturalSubtract, [a, b, r..]) => {
             match (&*a.as_whnf(), &*b.as_whnf()) {
-                (NaturalLit(a), NaturalLit(b)) => {
-                    Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
-                }
-                (NaturalLit(0), b) => Ok((r, b.clone())),
-                (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
-                _ if a == b => Ok((r, NaturalLit(0))),
+                (NaturalLit(a), NaturalLit(b)) => Ok((
+                    r,
+                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf(),
+                )),
+                (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())),
+                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())),
+                _ if a == b => Ok((r, NaturalLit(0).into_vovf())),
                 _ => Err(()),
             }
         }
@@ -111,18 +115,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 } else {
                     format!("+{}", n)
                 };
-                Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)])))
+                Ok((
+                    r,
+                    TextLit(vec![InterpolatedTextContents::Text(s)])
+                        .into_vovf(),
+                ))
             }
             _ => Err(()),
         },
         (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
-            IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
+            IntegerLit(n) => {
+                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf()))
+            }
             _ => Err(()),
         },
         (DoubleShow, [n, r..]) => match &*n.as_whnf() {
             DoubleLit(n) => Ok((
                 r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
+                TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
+                    .into_vovf(),
             )),
             _ => Err(()),
         },
@@ -137,7 +148,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         let s = txt.to_string();
                         Ok((
                             r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)]),
+                            TextLit(vec![InterpolatedTextContents::Text(s)])
+                                .into_vovf(),
                         ))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
@@ -152,7 +164,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         let s = txt.to_string();
                         Ok((
                             r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)]),
+                            TextLit(vec![InterpolatedTextContents::Text(s)])
+                                .into_vovf(),
                         ))
                     }
                     _ => Err(()),
@@ -161,29 +174,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             _ => Err(()),
         },
         (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, NaturalLit(0))),
-            NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
+            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())),
+            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())),
             _ => Err(()),
         },
         (ListHead, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
-            NEListLit(xs) => {
-                Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
-            }
+            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            NEListLit(xs) => Ok((
+                r,
+                NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(),
+            )),
             _ => Err(()),
         },
         (ListLast, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
-            NEListLit(xs) => {
-                Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
-            }
+            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            NEListLit(xs) => Ok((
+                r,
+                NEOptionalLit(xs.iter().rev().next().unwrap().clone())
+                    .into_vovf(),
+            )),
             _ => Err(()),
         },
         (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
-            NEListLit(xs) => {
-                Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
-            }
+            EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())),
+            NEListLit(xs) => Ok((
+                r,
+                NEListLit(xs.iter().rev().cloned().collect()).into_vovf(),
+            )),
             _ => Err(()),
         },
         (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
@@ -193,7 +210,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 kts.insert("value".into(), t.clone());
                 Ok((
                     r,
-                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
+                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts)))
+                        .into_vovf(),
                 ))
             }
             NEListLit(xs) => {
@@ -211,7 +229,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
-                Ok((r, NEListLit(xs)))
+                Ok((r, NEListLit(xs).into_vovf()))
             }
             _ => Err(()),
         },
@@ -219,7 +237,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_whnf()))
+                    Ok((r, args[1].clone().into_vovf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -249,13 +267,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, nil.to_whnf())),
+            EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
             NEListLit(xs) => {
-                let mut v = nil.clone();
-                for x in xs.iter().rev() {
-                    v = cons.clone().app(x.clone()).app(v).into_value_untyped();
+                let mut v = nil.clone().into_vovf();
+                for x in xs.iter().cloned().rev() {
+                    v = cons.app(x).app(v.into_value_untyped());
                 }
-                Ok((r, v.to_whnf()))
+                Ok((r, v))
             }
             _ => Err(()),
         },
@@ -263,7 +281,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             // fold/build fusion
             ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_whnf()))
+                    Ok((r, args[1].clone().into_vovf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -285,7 +303,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
-            EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
+            EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
             NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
             _ => Err(()),
         },
@@ -293,7 +311,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             // fold/build fusion
             ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].to_whnf()))
+                    Ok((r, args[0].clone().into_vovf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -310,7 +328,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
-            NaturalLit(0) => Ok((r, zero.to_whnf())),
+            NaturalLit(0) => Ok((r, zero.clone().into_vovf())),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
                     .app(
@@ -335,23 +353,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             v
         }
-        Err(()) => AppliedBuiltin(b, args),
+        Err(()) => AppliedBuiltin(b, args).into_vovf(),
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
-    let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
+    let fallback =
+        |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf();
 
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(),
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args)
         }
         ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone())
+            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf()
         }
         _ => {
             drop(f_borrow);
@@ -465,6 +484,7 @@ where
 enum Ret<'a> {
     ValueF(ValueF),
     Value(Value),
+    VoVF(VoVF),
     ValueRef(&'a Value),
     Expr(ExprF<Value, Normalized>),
 }
@@ -597,7 +617,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -615,7 +635,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
         ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
-        ExprF::App(v, a) => Ret::ValueF(v.app(a)),
+        ExprF::App(v, a) => Ret::VoVF(v.app(a)),
         ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
         ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -737,7 +757,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::ValueF(h.app(v.clone())),
+                    Some(h) => Ret::VoVF(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -754,22 +774,23 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
     };
 
     match ret {
-        Ret::ValueF(v) => v,
-        Ret::Value(th) => th.as_whnf().clone(),
-        Ret::ValueRef(th) => th.as_whnf().clone(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr),
+        Ret::ValueF(v) => v.into_vovf(),
+        Ret::Value(v) => v.into_vovf(),
+        Ret::VoVF(v) => v,
+        Ret::ValueRef(v) => v.clone().into_vovf(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(),
     }
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+pub(crate) fn normalize_whnf(v: ValueF) -> VoVF {
     match v {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
         ValueF::PartialExpr(e) => normalize_one_layer(e),
         ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter()))
+            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf()
         }
         // All other cases are already in WHNF
-        v => v,
+        v => v.into_vovf(),
     }
 }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 440d694..996c26c 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -455,11 +455,11 @@ fn type_last_layer(
                 return mkerr(InvalidListType(t.into_owned()));
             }
 
-            RetTypeOnly(Value::from_valuef_and_type(
+            RetTypeOnly(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app(t.into_owned()),
-                Value::from_const(Type),
-            ))
+                    .app(t.into_owned())
+                    .into_value_simple_type(),
+            )
         }
         SomeLit(x) => {
             let t = x.get_type()?.into_owned();
@@ -467,10 +467,11 @@ fn type_last_layer(
                 return mkerr(InvalidOptionalType(t));
             }
 
-            RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t),
-                Value::from_const(Type),
-            ))
+            RetTypeOnly(
+                Value::from_builtin(dhall_syntax::Builtin::Optional)
+                    .app(t)
+                    .into_value_simple_type(),
+            )
         }
         RecordType(kts) => RetWhole(tck_record_type(
             ctx,
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 4171fab..e2449de 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -169,12 +169,16 @@ pub mod value {
         }
         pub(crate) fn make_optional_type(t: Value) -> Self {
             Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::Optional).app(t.to_value()),
+                DhallValueF::from_builtin(Builtin::Optional)
+                    .app(t.to_value())
+                    .into_whnf(),
             )
         }
         pub(crate) fn make_list_type(t: Value) -> Self {
             Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::List).app(t.to_value()),
+                DhallValueF::from_builtin(Builtin::List)
+                    .app(t.to_value())
+                    .into_whnf(),
             )
         }
         // Made public for the StaticType derive macro
-- 
cgit v1.2.3


From c157df5e66fb80ff6184cb3934e5b0883f0fdbf0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 18:11:05 +0200
Subject: No need for Cow in return type of get_type

---
 dhall/src/core/value.rs      |  5 ++---
 dhall/src/phase/mod.rs       |  5 ++---
 dhall/src/phase/typecheck.rs | 39 +++++++++++++++++++--------------------
 dhall/src/tests.rs           |  2 +-
 4 files changed, 24 insertions(+), 27 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 25fcaae..64a4842 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,4 +1,3 @@
-use std::borrow::Cow;
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
@@ -228,8 +227,8 @@ impl Value {
         apply_any(self.clone(), v)
     }
 
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
-        Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
+    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+        Ok(self.as_internal().get_type()?.clone())
     }
 }
 
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 1f7e5f0..1f80791 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,4 +1,3 @@
-use std::borrow::Cow;
 use std::fmt::Display;
 use std::path::Path;
 
@@ -121,8 +120,8 @@ impl Typed {
     }
 
     #[allow(dead_code)]
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> {
-        Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed()))
+    pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
+        Ok(self.0.get_type()?.into_typed())
     }
 }
 
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 996c26c..4abc314 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -31,7 +31,7 @@ fn tck_pi_type(
         _ => {
             return Err(TypeError::new(
                 &ctx2,
-                InvalidOutputType(te.get_type()?.into_owned()),
+                InvalidOutputType(te.get_type()?),
             ))
         }
     };
@@ -312,7 +312,7 @@ fn type_with(
             let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
             let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone());
-            let tb = b.get_type()?.into_owned();
+            let tb = b.get_type()?;
             let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
             Value::from_valuef_and_type(v, t)
         }
@@ -389,17 +389,17 @@ fn type_last_layer(
                 ValueF::Pi(x, tx, tb) => (x, tx, tb),
                 _ => return mkerr(NotAFunction(f.clone())),
             };
-            if a.get_type()?.as_ref() != tx {
+            if &a.get_type()? != tx {
                 return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
             }
 
             RetTypeOnly(tb.subst_shift(&x.into(), a))
         }
         Annot(x, t) => {
-            if t != x.get_type()?.as_ref() {
+            if &x.get_type()? != t {
                 return mkerr(AnnotMismatch(x.clone(), t.clone()));
             }
-            RetTypeOnly(x.get_type()?.into_owned())
+            RetTypeOnly(x.get_type()?)
         }
         Assert(t) => {
             match &*t.as_whnf() {
@@ -412,7 +412,7 @@ fn type_last_layer(
             RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
-            if x.get_type()?.as_ref() != &builtin_to_value(Bool) {
+            if &*x.get_type()?.as_whnf() != &ValueF::from_builtin(Bool) {
                 return mkerr(InvalidPredicate(x.clone()));
             }
 
@@ -428,7 +428,7 @@ fn type_last_layer(
                 return mkerr(IfBranchMismatch(y.clone(), z.clone()));
             }
 
-            RetTypeOnly(y.get_type()?.into_owned())
+            RetTypeOnly(y.get_type()?)
         }
         EmptyListLit(t) => {
             match &*t.as_whnf() {
@@ -445,24 +445,24 @@ fn type_last_layer(
                 if x.get_type()? != y.get_type()? {
                     return mkerr(InvalidListElement(
                         i,
-                        x.get_type()?.into_owned(),
+                        x.get_type()?,
                         y.clone(),
                     ));
                 }
             }
             let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidListType(t.into_owned()));
+                return mkerr(InvalidListType(t));
             }
 
             RetTypeOnly(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app(t.into_owned())
+                    .app(t)
                     .into_value_simple_type(),
             )
         }
         SomeLit(x) => {
-            let t = x.get_type()?.into_owned();
+            let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
                 return mkerr(InvalidOptionalType(t));
             }
@@ -483,8 +483,7 @@ fn type_last_layer(
         )?),
         RecordLit(kvs) => RetTypeOnly(tck_record_type(
             ctx,
-            kvs.iter()
-                .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
+            kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
         )?),
         Field(r, x) => {
             match &*r.get_type()?.as_whnf() {
@@ -545,7 +544,7 @@ fn type_last_layer(
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
-                    if x.get_type()?.as_ref() != &text_type {
+                    if x.get_type()? != text_type {
                         return mkerr(InvalidTextInterpolation(x.clone()));
                     }
                 }
@@ -586,8 +585,8 @@ fn type_last_layer(
             ctx,
             ExprF::BinOp(
                 RecursiveRecordTypeMerge,
-                l.get_type()?.into_owned(),
-                r.get_type()?.into_owned(),
+                l.get_type()?,
+                r.get_type()?,
             ),
         )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
@@ -659,7 +658,7 @@ fn type_last_layer(
                 return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
-            RetTypeOnly(l.get_type()?.into_owned())
+            RetTypeOnly(l.get_type()?)
         }
         BinOp(Equivalence, l, r) => {
             if l.get_type()?.get_type()?.as_const() != Some(Type) {
@@ -692,11 +691,11 @@ fn type_last_layer(
                 Equivalence => unreachable!(),
             });
 
-            if l.get_type()?.as_ref() != &t {
+            if l.get_type()? != t {
                 return mkerr(BinOpTypeMismatch(*o, l.clone()));
             }
 
-            if r.get_type()?.as_ref() != &t {
+            if r.get_type()? != t {
                 return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
@@ -800,7 +799,7 @@ fn type_last_layer(
 
             RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::RecordType(new_kts),
-                record_type.get_type()?.into_owned(),
+                record_type.get_type()?,
             ))
         }
     };
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index be4805d..8f16a12 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -185,7 +185,7 @@ pub fn run_test(
                 }
                 TypeInference => {
                     let expr = expr.typecheck()?;
-                    let ty = expr.get_type()?.into_owned().normalize();
+                    let ty = expr.get_type()?.normalize();
                     assert_eq_display!(ty, expected);
                 }
                 Normalization => {
-- 
cgit v1.2.3


From f70e45daef2570259eccd227a0126493c015d7b0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 21:50:47 +0200
Subject: Track evaluation status alongside ValueF in VoVF

---
 dhall/src/core/value.rs      | 44 +++++++++++----------------
 dhall/src/core/valuef.rs     | 32 ++++++++++++++------
 dhall/src/phase/normalize.rs | 72 ++++++++++++++++++++++++--------------------
 3 files changed, 80 insertions(+), 68 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 64a4842..b44dad6 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
-enum Form {
+pub enum Form {
     /// No constraints; expression may not be normalized at all.
     Unevaled,
     /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
@@ -46,9 +46,10 @@ pub struct Value(Rc<RefCell<ValueInternal>>);
 /// When a function needs to return either a freshly created ValueF or an existing Value, but
 /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
 /// avoid loss of typ information.
+#[derive(Debug, Clone)]
 pub enum VoVF {
     Value(Value),
-    ValueF(ValueF),
+    ValueF { val: ValueF, form: Form },
 }
 
 impl ValueInternal {
@@ -98,24 +99,14 @@ impl ValueInternal {
 }
 
 impl Value {
+    pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
+        ValueInternal { form, value, ty }.into_value()
+    }
     pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
-        ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: None,
-        }
-        .into_value()
+        Value::new(v, Unevaled, None)
     }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
-        ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: Some(t),
-        }
-        .into_value()
-    }
-    pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
-        Value::from_valuef_and_type(v, Value::from_const(Const::Type))
+        Value::new(v, Unevaled, Some(t))
     }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
@@ -236,34 +227,35 @@ impl VoVF {
     pub fn into_whnf(self) -> ValueF {
         match self {
             VoVF::Value(v) => v.to_whnf(),
-            VoVF::ValueF(v) => v,
+            VoVF::ValueF {
+                val,
+                form: Unevaled,
+            } => normalize_whnf(val).into_whnf(),
+            // Already at lest in WHNF
+            VoVF::ValueF { val, .. } => val,
         }
     }
     pub(crate) fn into_value_untyped(self) -> Value {
         match self {
             VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_untyped(),
+            VoVF::ValueF { val, form } => Value::new(val, form, None),
         }
     }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         match self {
             // TODO: check type with debug_assert ?
             VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_with_type(t),
+            VoVF::ValueF { val, form } => Value::new(val, form, Some(t)),
         }
     }
     pub(crate) fn into_value_simple_type(self) -> Value {
-        match self {
-            // TODO: check type with debug_assert ?
-            VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_simple_type(),
-        }
+        self.into_value_with_type(Value::from_const(Const::Type))
     }
 
     pub(crate) fn app(self, x: Value) -> Self {
         match self {
             VoVF::Value(v) => v.app(x),
-            VoVF::ValueF(v) => v.into_value_untyped().app(x),
+            VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
         }
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 80978a7..db8a284 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::{Value, VoVF};
+use crate::core::value::{Form, Value, VoVF};
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
 
@@ -19,7 +19,7 @@ pub enum ValueF {
     /// Closures
     Lam(AlphaLabel, Value, Value),
     Pi(AlphaLabel, Value, Value),
-    // Invariant: the evaluation must not be able to progress further.
+    // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
     Var(AlphaVar),
@@ -33,16 +33,16 @@ pub enum ValueF {
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(Value),
     NEListLit(Vec<Value>),
-    RecordLit(HashMap<Label, Value>),
     RecordType(HashMap<Label, Value>),
+    RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
     UnionConstructor(Label, HashMap<Label, Option<Value>>),
     UnionLit(Label, Value, HashMap<Label, Option<Value>>),
-    // Invariant: this must not contain interpolations that are themselves TextLits, and
+    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Value>>),
     Equivalence(Value, Value),
-    // Invariant: this must not contain a value captured by one of the variants above.
+    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Value, Normalized>),
 }
 
@@ -53,11 +53,23 @@ impl ValueF {
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_value_simple_type(self) -> Value {
-        Value::from_valuef_simple_type(self)
+    pub(crate) fn into_vovf_unevaled(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::Unevaled,
+        }
+    }
+    pub(crate) fn into_vovf_whnf(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::WHNF,
+        }
     }
-    pub(crate) fn into_vovf(self) -> VoVF {
-        VoVF::ValueF(self)
+    pub(crate) fn into_vovf_nf(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::NF,
+        }
     }
 
     /// Convert the value to a fully normalized syntactic expression
@@ -261,7 +273,7 @@ impl ValueF {
 
     /// Apply to a value
     pub fn app(self, v: Value) -> VoVF {
-        self.into_vovf().app(v)
+        self.into_vovf_unevaled().app(v)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index e044018..a146ec7 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -70,29 +70,29 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t, r..]) => {
-            Ok((r, EmptyOptionalLit(t.clone()).into_vovf()))
+            Ok((r, EmptyOptionalLit(t.clone()).into_vovf_whnf()))
         }
         (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())),
+            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf(),
+                    .into_vovf_nf(),
             )),
             _ => Err(()),
         },
@@ -100,11 +100,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             match (&*a.as_whnf(), &*b.as_whnf()) {
                 (NaturalLit(a), NaturalLit(b)) => Ok((
                     r,
-                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf(),
+                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(),
                 )),
                 (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())),
-                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())),
-                _ if a == b => Ok((r, NaturalLit(0).into_vovf())),
+                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())),
+                _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())),
                 _ => Err(()),
             }
         }
@@ -118,14 +118,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 Ok((
                     r,
                     TextLit(vec![InterpolatedTextContents::Text(s)])
-                        .into_vovf(),
+                        .into_vovf_nf(),
                 ))
             }
             _ => Err(()),
         },
         (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => {
-                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf()))
+                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf()))
             }
             _ => Err(()),
         },
@@ -133,7 +133,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             DoubleLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf(),
+                    .into_vovf_nf(),
             )),
             _ => Err(()),
         },
@@ -149,7 +149,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Ok((
                             r,
                             TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf(),
+                                .into_vovf_nf(),
                         ))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
@@ -165,7 +165,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Ok((
                             r,
                             TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf(),
+                                .into_vovf_nf(),
                         ))
                     }
                     _ => Err(()),
@@ -174,32 +174,39 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             _ => Err(()),
         },
         (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())),
-            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())),
+            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())),
+            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())),
             _ => Err(()),
         },
         (ListHead, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
-                NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(),
+                NEOptionalLit(xs.iter().next().unwrap().clone())
+                    .into_vovf_whnf(),
             )),
             _ => Err(()),
         },
         (ListLast, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
                 NEOptionalLit(xs.iter().rev().next().unwrap().clone())
-                    .into_vovf(),
+                    .into_vovf_whnf(),
             )),
             _ => Err(()),
         },
         (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyListLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
-                NEListLit(xs.iter().rev().cloned().collect()).into_vovf(),
+                NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(),
             )),
             _ => Err(()),
         },
@@ -211,7 +218,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 Ok((
                     r,
                     EmptyListLit(Value::from_valuef_untyped(RecordType(kts)))
-                        .into_vovf(),
+                        .into_vovf_whnf(),
                 ))
             }
             NEListLit(xs) => {
@@ -229,7 +236,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
-                Ok((r, NEListLit(xs).into_vovf()))
+                Ok((r, NEListLit(xs).into_vovf_whnf()))
             }
             _ => Err(()),
         },
@@ -353,13 +360,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             }
             v
         }
-        Err(()) => AppliedBuiltin(b, args).into_vovf(),
+        Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(),
     }
 }
 
 pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
-    let fallback =
-        |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf();
+    let fallback = |f: Value, a: Value| {
+        ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
+    };
 
     let f_borrow = f.as_whnf();
     match &*f_borrow {
@@ -370,7 +378,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
             apply_builtin(*b, args)
         }
         ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf()
+            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
         }
         _ => {
             drop(f_borrow);
@@ -774,11 +782,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
     };
 
     match ret {
-        Ret::ValueF(v) => v.into_vovf(),
+        Ret::ValueF(v) => v.into_vovf_whnf(),
         Ret::Value(v) => v.into_vovf(),
         Ret::VoVF(v) => v,
         Ret::ValueRef(v) => v.clone().into_vovf(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
     }
 }
 
@@ -788,9 +796,9 @@ pub(crate) fn normalize_whnf(v: ValueF) -> VoVF {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
         ValueF::PartialExpr(e) => normalize_one_layer(e),
         ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf()
+            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
         }
         // All other cases are already in WHNF
-        v => v.into_vovf(),
+        v => v.into_vovf_whnf(),
     }
 }
-- 
cgit v1.2.3


From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 22:20:59 +0200
Subject: Propagate type information in Value::app()

---
 dhall/src/core/value.rs      | 23 +++++++++++++++--------
 dhall/src/phase/normalize.rs | 35 ++++++++++++++++-------------------
 dhall/src/phase/typecheck.rs | 10 ++--------
 tests_buffer                 |  1 +
 4 files changed, 34 insertions(+), 35 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index b44dad6..24e2803 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -214,8 +214,18 @@ impl Value {
         self.as_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app(&self, v: Value) -> VoVF {
-        apply_any(self.clone(), v)
+    pub(crate) fn app(&self, v: Value) -> Value {
+        let vovf = apply_any(self.clone(), v.clone());
+        match self.as_internal().get_type() {
+            Err(_) => vovf.into_value_untyped(),
+            Ok(t) => match &*t.as_whnf() {
+                ValueF::Pi(x, _, e) => {
+                    let t = e.subst_shift(&x.into(), &v);
+                    vovf.into_value_with_type(t)
+                }
+                _ => unreachable!("Internal type error"),
+            },
+        }
     }
 
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
@@ -248,15 +258,12 @@ impl VoVF {
             VoVF::ValueF { val, form } => Value::new(val, form, Some(t)),
         }
     }
-    pub(crate) fn into_value_simple_type(self) -> Value {
-        self.into_value_with_type(Value::from_const(Const::Type))
-    }
 
-    pub(crate) fn app(self, x: Value) -> Self {
-        match self {
+    pub(crate) fn app(self, x: Value) -> VoVF {
+        VoVF::Value(match self {
             VoVF::Value(v) => v.app(x),
             VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
-        }
+        })
     }
 }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a146ec7..e4a0c5b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -34,7 +34,6 @@ macro_rules! make_closure {
     (List $($rest:tt)*) => {
         Value::from_builtin(Builtin::List)
             .app(make_closure!($($rest)*))
-            .into_value_simple_type()
     };
     (Some($($rest:tt)*)) => {
         ValueF::NEOptionalLit(make_closure!($($rest)*))
@@ -251,9 +250,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 }
             }
             _ => {
-                let list_t = Value::from_builtin(List)
-                    .app(t.clone())
-                    .into_value_simple_type();
+                let list_t = Value::from_builtin(List).app(t.clone());
                 Ok((
                     r,
                     f.app(list_t.clone())
@@ -269,18 +266,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         .app(
                             EmptyListLit(t.clone())
                                 .into_value_with_type(list_t),
-                        ),
+                        )
+                        .into_vovf(),
                 ))
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
             EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
             NEListLit(xs) => {
-                let mut v = nil.clone().into_vovf();
+                let mut v = nil.clone();
                 for x in xs.iter().cloned().rev() {
-                    v = cons.app(x).app(v.into_value_untyped());
+                    v = cons.app(x).app(v);
                 }
-                Ok((r, v))
+                Ok((r, v.into_vovf()))
             }
             _ => Err(()),
         },
@@ -295,9 +293,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 }
             }
             _ => {
-                let optional_t = Value::from_builtin(Optional)
-                    .app(t.clone())
-                    .into_value_simple_type();
+                let optional_t = Value::from_builtin(Optional).app(t.clone());
                 Ok((
                     r,
                     f.app(optional_t.clone())
@@ -305,13 +301,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         .app(
                             EmptyOptionalLit(t.clone())
                                 .into_value_with_type(optional_t),
-                        ),
+                        )
+                        .into_vovf(),
                 ))
             }
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
             EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
-            NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
+            NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())),
             _ => Err(()),
         },
         (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
@@ -331,7 +328,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     .app(
                         NaturalLit(0)
                             .into_value_with_type(Value::from_builtin(Natural)),
-                    ),
+                    )
+                    .into_vovf(),
             )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
@@ -344,9 +342,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     )
                     .app(t.clone())
                     .app(succ.clone())
-                    .app(zero.clone())
-                    .into_value_with_type(t.clone());
-                Ok((r, succ.app(fold)))
+                    .app(zero.clone());
+                Ok((r, succ.app(fold).into_vovf()))
             }
             _ => Err(()),
         },
@@ -643,7 +640,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
         ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
         ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
-        ExprF::App(v, a) => Ret::VoVF(v.app(a)),
+        ExprF::App(v, a) => Ret::Value(v.app(a)),
         ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
         ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -765,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::VoVF(h.app(v.clone())),
+                    Some(h) => Ret::Value(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4abc314..abe05a3 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -455,11 +455,7 @@ fn type_last_layer(
                 return mkerr(InvalidListType(t));
             }
 
-            RetTypeOnly(
-                ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app(t)
-                    .into_value_simple_type(),
-            )
+            RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
         }
         SomeLit(x) => {
             let t = x.get_type()?;
@@ -468,9 +464,7 @@ fn type_last_layer(
             }
 
             RetTypeOnly(
-                Value::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app(t)
-                    .into_value_simple_type(),
+                Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
             )
         }
         RecordType(kts) => RetWhole(tck_record_type(
diff --git a/tests_buffer b/tests_buffer
index c6366ba..15dc9c5 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -41,5 +41,6 @@ failure/
     merge {x=...,y=...} <x:T>.x
     MergeBoolIsNotUnion merge x True
     MergeOptionalIsNotUnion merge x (Some 1)
+    SortInLet let x = Sort in 1
 
 equivalence:
-- 
cgit v1.2.3


From 8e68396e9fe3751bcf8bcfd68301ca7fea836787 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 22:35:53 +0200
Subject: Use Ret in apply_builtin

---
 dhall/src/core/valuef.rs     |   6 --
 dhall/src/phase/normalize.rs | 191 +++++++++++++++++++++++--------------------
 2 files changed, 101 insertions(+), 96 deletions(-)

diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index db8a284..316238c 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -65,12 +65,6 @@ impl ValueF {
             form: Form::WHNF,
         }
     }
-    pub(crate) fn into_vovf_nf(self) -> VoVF {
-        VoVF::ValueF {
-            val: self,
-            form: Form::NF,
-        }
-    }
 
     /// Convert the value to a fully normalized syntactic expression
     pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index e4a0c5b..0c4e185 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -10,6 +10,25 @@ use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::phase::Normalized;
 
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+    ValueF(ValueF),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprF<Value, Normalized>),
+}
+
+impl<'a> Ret<'a> {
+    fn into_vovf_whnf(self) -> VoVF {
+        match self {
+            Ret::ValueF(v) => v.into_vovf_whnf(),
+            Ret::Value(v) => v.into_vovf(),
+            Ret::ValueRef(v) => v.clone().into_vovf(),
+            Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
+        }
+    }
+}
+
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
     (#$var:ident) => { $var.clone() };
@@ -69,29 +88,30 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t, r..]) => {
-            Ok((r, EmptyOptionalLit(t.clone()).into_vovf_whnf()))
+            Ok((r, Ret::ValueF(EmptyOptionalLit(t.clone()))))
         }
         (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())),
+            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n == 0)))),
             _ => Err(()),
         },
         (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())),
+            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 == 0)))),
             _ => Err(()),
         },
         (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())),
+            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 != 0)))),
             _ => Err(()),
         },
         (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())),
+            NaturalLit(n) => Ok((r, Ret::ValueF(IntegerLit(*n as isize)))),
             _ => Err(()),
         },
         (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf_nf(),
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+                    n.to_string(),
+                )])),
             )),
             _ => Err(()),
         },
@@ -99,11 +119,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             match (&*a.as_whnf(), &*b.as_whnf()) {
                 (NaturalLit(a), NaturalLit(b)) => Ok((
                     r,
-                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(),
+                    Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })),
                 )),
-                (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())),
-                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())),
-                _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())),
+                (NaturalLit(0), _) => Ok((r, Ret::ValueRef(b))),
+                (_, NaturalLit(0)) => Ok((r, Ret::ValueF(NaturalLit(0)))),
+                _ if a == b => Ok((r, Ret::ValueF(NaturalLit(0)))),
                 _ => Err(()),
             }
         }
@@ -116,23 +136,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 };
                 Ok((
                     r,
-                    TextLit(vec![InterpolatedTextContents::Text(s)])
-                        .into_vovf_nf(),
+                    Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+                        s,
+                    )])),
                 ))
             }
             _ => Err(()),
         },
         (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => {
-                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf()))
+                Ok((r, Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))))
             }
             _ => Err(()),
         },
         (DoubleShow, [n, r..]) => match &*n.as_whnf() {
             DoubleLit(n) => Ok((
                 r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf_nf(),
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+                    n.to_string(),
+                )])),
             )),
             _ => Err(()),
         },
@@ -147,8 +169,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         let s = txt.to_string();
                         Ok((
                             r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf_nf(),
+                            Ret::ValueF(TextLit(vec![
+                                InterpolatedTextContents::Text(s),
+                            ])),
                         ))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
@@ -163,8 +186,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         let s = txt.to_string();
                         Ok((
                             r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf_nf(),
+                            Ret::ValueF(TextLit(vec![
+                                InterpolatedTextContents::Text(s),
+                            ])),
                         ))
                     }
                     _ => Err(()),
@@ -173,39 +197,37 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             _ => Err(()),
         },
         (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())),
-            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())),
+            EmptyListLit(_) => Ok((r, Ret::ValueF(NaturalLit(0)))),
+            NEListLit(xs) => Ok((r, Ret::ValueF(NaturalLit(xs.len())))),
             _ => Err(()),
         },
         (ListHead, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => {
-                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+                Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone()))))
             }
             NEListLit(xs) => Ok((
                 r,
-                NEOptionalLit(xs.iter().next().unwrap().clone())
-                    .into_vovf_whnf(),
+                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())),
             )),
             _ => Err(()),
         },
         (ListLast, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => {
-                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+                Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone()))))
             }
             NEListLit(xs) => Ok((
                 r,
-                NEOptionalLit(xs.iter().rev().next().unwrap().clone())
-                    .into_vovf_whnf(),
+                Ret::ValueF(NEOptionalLit(
+                    xs.iter().rev().next().unwrap().clone(),
+                )),
             )),
             _ => Err(()),
         },
         (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => {
-                Ok((r, EmptyListLit(n.clone()).into_vovf_whnf()))
-            }
+            EmptyListLit(n) => Ok((r, Ret::ValueF(EmptyListLit(n.clone())))),
             NEListLit(xs) => Ok((
                 r,
-                NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(),
+                Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())),
             )),
             _ => Err(()),
         },
@@ -216,8 +238,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 kts.insert("value".into(), t.clone());
                 Ok((
                     r,
-                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts)))
-                        .into_vovf_whnf(),
+                    Ret::ValueF(EmptyListLit(Value::from_valuef_untyped(
+                        RecordType(kts),
+                    ))),
                 ))
             }
             NEListLit(xs) => {
@@ -235,7 +258,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
-                Ok((r, NEListLit(xs).into_vovf_whnf()))
+                Ok((r, Ret::ValueF(NEListLit(xs))))
             }
             _ => Err(()),
         },
@@ -243,7 +266,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].clone().into_vovf()))
+                    Ok((r, Ret::Value(args[1].clone())))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -253,32 +276,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 let list_t = Value::from_builtin(List).app(t.clone());
                 Ok((
                     r,
-                    f.app(list_t.clone())
-                        .app({
-                            // Move `t` under new `x` variable
-                            let t1 = t.under_binder(Label::from("x"));
-                            make_closure!(
-                                λ(x : #t) ->
-                                λ(xs : List #t1) ->
-                                [ var(x, 1) ] # var(xs, 0)
-                            )
-                        })
-                        .app(
-                            EmptyListLit(t.clone())
-                                .into_value_with_type(list_t),
-                        )
-                        .into_vovf(),
+                    Ret::Value(
+                        f.app(list_t.clone())
+                            .app({
+                                // Move `t` under new `x` variable
+                                let t1 = t.under_binder(Label::from("x"));
+                                make_closure!(
+                                    λ(x : #t) ->
+                                    λ(xs : List #t1) ->
+                                    [ var(x, 1) ] # var(xs, 0)
+                                )
+                            })
+                            .app(
+                                EmptyListLit(t.clone())
+                                    .into_value_with_type(list_t),
+                            ),
+                    ),
                 ))
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
+            EmptyListLit(_) => Ok((r, Ret::ValueRef(nil))),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().cloned().rev() {
                     v = cons.app(x).app(v);
                 }
-                Ok((r, v.into_vovf()))
+                Ok((r, Ret::Value(v)))
             }
             _ => Err(()),
         },
@@ -286,7 +310,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             // fold/build fusion
             ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].clone().into_vovf()))
+                    Ok((r, Ret::Value(args[1].clone())))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -296,26 +320,27 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 let optional_t = Value::from_builtin(Optional).app(t.clone());
                 Ok((
                     r,
-                    f.app(optional_t.clone())
-                        .app(make_closure!(λ(x: #t) -> Some(var(x, 0))))
-                        .app(
-                            EmptyOptionalLit(t.clone())
-                                .into_value_with_type(optional_t),
-                        )
-                        .into_vovf(),
+                    Ret::Value(
+                        f.app(optional_t.clone())
+                            .app(make_closure!(λ(x: #t) -> Some(var(x, 0))))
+                            .app(
+                                EmptyOptionalLit(t.clone())
+                                    .into_value_with_type(optional_t),
+                            ),
+                    ),
                 ))
             }
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
-            EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
-            NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())),
+            EmptyOptionalLit(_) => Ok((r, Ret::ValueRef(nothing))),
+            NEOptionalLit(x) => Ok((r, Ret::Value(just.app(x.clone())))),
             _ => Err(()),
         },
         (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].clone().into_vovf()))
+                    Ok((r, Ret::Value(args[0].clone())))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -323,17 +348,17 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             }
             _ => Ok((
                 r,
-                f.app(Value::from_builtin(Natural))
-                    .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
-                    .app(
-                        NaturalLit(0)
-                            .into_value_with_type(Value::from_builtin(Natural)),
-                    )
-                    .into_vovf(),
+                Ret::Value(
+                    f.app(Value::from_builtin(Natural))
+                        .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                        .app(NaturalLit(0).into_value_with_type(
+                            Value::from_builtin(Natural),
+                        )),
+                ),
             )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
-            NaturalLit(0) => Ok((r, zero.clone().into_vovf())),
+            NaturalLit(0) => Ok((r, Ret::ValueRef(zero))),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
                     .app(
@@ -343,14 +368,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     .app(t.clone())
                     .app(succ.clone())
                     .app(zero.clone());
-                Ok((r, succ.app(fold).into_vovf()))
+                Ok((r, Ret::Value(succ.app(fold))))
             }
             _ => Err(()),
         },
         _ => Err(()),
     };
     match ret {
-        Ok((unconsumed_args, mut v)) => {
+        Ok((unconsumed_args, ret)) => {
+            let mut v = ret.into_vovf_whnf();
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
                 v = v.app(x);
@@ -485,15 +511,6 @@ where
     kvs
 }
 
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    ValueF(ValueF),
-    Value(Value),
-    VoVF(VoVF),
-    ValueRef(&'a Value),
-    Expr(ExprF<Value, Normalized>),
-}
-
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -778,13 +795,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
         }
     };
 
-    match ret {
-        Ret::ValueF(v) => v.into_vovf_whnf(),
-        Ret::Value(v) => v.into_vovf(),
-        Ret::VoVF(v) => v,
-        Ret::ValueRef(v) => v.clone().into_vovf(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
-    }
+    ret.into_vovf_whnf()
 }
 
 /// Normalize a ValueF into WHNF
-- 
cgit v1.2.3


From 8c1ffc5b68489be4694fff922ca48afeb0d45fc4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 23:02:56 +0200
Subject: Move type construction fns from serde_dhall to dhall

---
 dhall/src/phase/mod.rs | 35 ++++++++++++++++++++++++++++++++++-
 serde_dhall/src/lib.rs | 32 ++++++--------------------------
 2 files changed, 40 insertions(+), 27 deletions(-)

diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 1f80791..b5b7b64 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,7 +1,7 @@
 use std::fmt::Display;
 use std::path::Path;
 
-use dhall_syntax::{Const, SubExpr};
+use dhall_syntax::{Builtin, Const, SubExpr};
 
 use crate::core::value::Value;
 use crate::core::valuef::ValueF;
@@ -123,6 +123,39 @@ impl Typed {
     pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
         Ok(self.0.get_type()?.into_typed())
     }
+
+    pub fn make_builtin_type(b: Builtin) -> Self {
+        Typed::from_value(Value::from_builtin(b))
+    }
+    pub fn make_optional_type(t: Typed) -> Self {
+        Typed::from_value(
+            Value::from_builtin(Builtin::Optional).app(t.to_value()),
+        )
+    }
+    pub fn make_list_type(t: Typed) -> Self {
+        Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value()))
+    }
+    pub fn make_record_type(
+        kts: impl Iterator<Item = (String, Typed)>,
+    ) -> Self {
+        Typed::from_valuef_and_type(
+            ValueF::RecordType(
+                kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+            ),
+            Typed::const_type(),
+        )
+    }
+    pub fn make_union_type(
+        kts: impl Iterator<Item = (String, Option<Typed>)>,
+    ) -> Self {
+        Typed::from_valuef_and_type(
+            ValueF::UnionType(
+                kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+                    .collect(),
+            ),
+            Typed::const_type(),
+        )
+    }
 }
 
 impl Normalized {
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index e2449de..ce3468f 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -124,8 +124,6 @@ pub use value::Value;
 
 // A Dhall value.
 pub mod value {
-    use dhall::core::value::Value as DhallValue;
-    use dhall::core::valuef::ValueF as DhallValueF;
     use dhall::phase::{NormalizedSubExpr, Parsed, Typed};
     use dhall_syntax::Builtin;
 
@@ -153,50 +151,32 @@ pub mod value {
         pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
             self.0.to_expr()
         }
-        pub(crate) fn to_value(&self) -> DhallValue {
-            self.0.to_value()
-        }
         pub(crate) fn as_typed(&self) -> &Typed {
             &self.0
         }
 
-        /// Assumes that the given value has type `Type`.
-        pub(crate) fn make_simple_type(v: DhallValueF) -> Self {
-            Value(Typed::from_valuef_and_type(v, Typed::const_type()))
-        }
         pub(crate) fn make_builtin_type(b: Builtin) -> Self {
-            Self::make_simple_type(DhallValueF::from_builtin(b))
+            Value(Typed::make_builtin_type(b))
         }
         pub(crate) fn make_optional_type(t: Value) -> Self {
-            Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::Optional)
-                    .app(t.to_value())
-                    .into_whnf(),
-            )
+            Value(Typed::make_optional_type(t.0))
         }
         pub(crate) fn make_list_type(t: Value) -> Self {
-            Self::make_simple_type(
-                DhallValueF::from_builtin(Builtin::List)
-                    .app(t.to_value())
-                    .into_whnf(),
-            )
+            Value(Typed::make_list_type(t.0))
         }
         // Made public for the StaticType derive macro
         #[doc(hidden)]
         pub fn make_record_type(
             kts: impl Iterator<Item = (String, Value)>,
         ) -> Self {
-            Self::make_simple_type(DhallValueF::RecordType(
-                kts.map(|(k, t)| (k.into(), t.to_value())).collect(),
-            ))
+            Value(Typed::make_record_type(kts.map(|(k, t)| (k, t.0))))
         }
         #[doc(hidden)]
         pub fn make_union_type(
             kts: impl Iterator<Item = (String, Option<Value>)>,
         ) -> Self {
-            Self::make_simple_type(DhallValueF::UnionType(
-                kts.map(|(k, t)| (k.into(), t.map(|t| t.to_value())))
-                    .collect(),
+            Value(Typed::make_union_type(
+                kts.map(|(k, t)| (k, t.map(|t| t.0))),
             ))
         }
     }
-- 
cgit v1.2.3


From 6c006e122a050ebbe76c8c566e559bbf9f2301a7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 23:06:14 +0200
Subject: Reduce API surface of dhall crate

---
 dhall/src/core/value.rs  | 13 +++++--------
 dhall/src/core/valuef.rs | 15 ++-------------
 dhall/src/phase/mod.rs   |  6 +++---
 3 files changed, 10 insertions(+), 24 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 24e2803..e1623a8 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
-pub enum Form {
+pub(crate) enum Form {
     /// No constraints; expression may not be normalized at all.
     Unevaled,
     /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
@@ -41,13 +41,13 @@ struct ValueInternal {
 /// sharing computation automatically. Uses a RefCell to share computation.
 /// Can optionally store a type from typechecking to preserve type information.
 #[derive(Clone)]
-pub struct Value(Rc<RefCell<ValueInternal>>);
+pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
 /// When a function needs to return either a freshly created ValueF or an existing Value, but
 /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
 /// avoid loss of typ information.
 #[derive(Debug, Clone)]
-pub enum VoVF {
+pub(crate) enum VoVF {
     Value(Value),
     ValueF { val: ValueF, form: Form },
 }
@@ -111,10 +111,7 @@ impl Value {
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
     }
-    pub fn const_type() -> Self {
-        Value::from_const(Const::Type)
-    }
-    pub fn from_builtin(b: Builtin) -> Self {
+    pub(crate) fn from_builtin(b: Builtin) -> Self {
         builtin_to_value(b)
     }
 
@@ -234,7 +231,7 @@ impl Value {
 }
 
 impl VoVF {
-    pub fn into_whnf(self) -> ValueF {
+    pub(crate) fn into_whnf(self) -> ValueF {
         match self {
             VoVF::Value(v) => v.to_whnf(),
             VoVF::ValueF {
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 316238c..42606a9 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -15,7 +15,7 @@ use crate::phase::{Normalized, NormalizedSubExpr};
 /// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
 /// recursively normalize as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ValueF {
+pub(crate) enum ValueF {
     /// Closures
     Lam(AlphaLabel, Value, Value),
     Pi(AlphaLabel, Value, Value),
@@ -53,12 +53,6 @@ impl ValueF {
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_vovf_unevaled(self) -> VoVF {
-        VoVF::ValueF {
-            val: self,
-            form: Form::Unevaled,
-        }
-    }
     pub(crate) fn into_vovf_whnf(self) -> VoVF {
         VoVF::ValueF {
             val: self,
@@ -265,12 +259,7 @@ impl ValueF {
         }
     }
 
-    /// Apply to a value
-    pub fn app(self, v: Value) -> VoVF {
-        self.into_vovf_unevaled().app(v)
-    }
-
-    pub fn from_builtin(b: Builtin) -> ValueF {
+    pub(crate) fn from_builtin(b: Builtin) -> ValueF {
         ValueF::AppliedBuiltin(b, vec![])
     }
 }
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index b5b7b64..ecf04e9 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -92,13 +92,13 @@ impl Typed {
     pub(crate) fn from_const(c: Const) -> Self {
         Typed(Value::from_const(c))
     }
-    pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
         Typed(Value::from_valuef_and_type(v, t.into_value()))
     }
     pub(crate) fn from_value(th: Value) -> Self {
         Typed(th)
     }
-    pub fn const_type() -> Self {
+    pub(crate) fn const_type() -> Self {
         Typed::from_const(Const::Type)
     }
 
@@ -108,7 +108,7 @@ impl Typed {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.0.to_expr_alpha()
     }
-    pub fn to_value(&self) -> Value {
+    pub(crate) fn to_value(&self) -> Value {
         self.0.clone()
     }
     pub(crate) fn into_value(self) -> Value {
-- 
cgit v1.2.3


From e8a9178ebe4860a8a00a6ec8f77b661fdad84890 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 21 Aug 2019 17:40:56 +0200
Subject: Don't use take_mut::take lightly since normalize_whnf might panic

---
 dhall/src/core/value.rs | 27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index e1623a8..69d372a 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -61,16 +61,25 @@ impl ValueInternal {
     }
 
     fn normalize_whnf(&mut self) {
-        take_mut::take(self, |vint| match &vint.form {
-            Unevaled => ValueInternal {
-                form: WHNF,
-                // TODO: thunk chaining
-                value: normalize_whnf(vint.value).into_whnf(),
-                ty: vint.ty,
+        take_mut::take_or_recover(
+            self,
+            // Dummy value in case the other closure panics
+            || ValueInternal {
+                form: Unevaled,
+                value: ValueF::Const(Const::Type),
+                ty: None,
             },
-            // Already in WHNF
-            WHNF | NF => vint,
-        })
+            |vint| match &vint.form {
+                Unevaled => ValueInternal {
+                    form: WHNF,
+                    // TODO: thunk chaining
+                    value: normalize_whnf(vint.value).into_whnf(),
+                    ty: vint.ty,
+                },
+                // Already in WHNF
+                WHNF | NF => vint,
+            },
+        )
     }
     fn normalize_nf(&mut self) {
         match self.form {
-- 
cgit v1.2.3


From d9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 23 Aug 2019 18:34:43 +0200
Subject: Keep type information after RecursiveRecordTypeMerge

---
 dhall/src/phase/normalize.rs | 75 ++++++++------------------------------------
 dhall/src/phase/typecheck.rs | 37 ++++++----------------
 tests_buffer                 |  4 ++-
 3 files changed, 26 insertions(+), 90 deletions(-)

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 0c4e185..28dc0f6 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -452,53 +452,20 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-/// Performs an intersection of two HashMaps.
-///
-/// # Arguments
-///
-/// * `f` - Will compute the final value from the intersecting
-///         key and the values from both maps.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `f` function.
-///
-/// The final map will contain the shared keys from the
-/// two input maps with the final computed value from `f`.
-pub(crate) fn intersection_with_key<K, T, U, V>(
-    mut f: impl FnMut(&K, &T, &U) -> V,
-    map1: &HashMap<K, T>,
-    map2: &HashMap<K, U>,
-) -> HashMap<K, V>
-where
-    K: std::hash::Hash + Eq + Clone,
-{
-    let mut kvs = HashMap::new();
-
-    for (k, t) in map1 {
-        // Only insert in the final map if the key exists in both
-        if let Some(u) = map2.get(k) {
-            kvs.insert(k.clone(), f(k, t, u));
-        }
-    }
-
-    kvs
-}
-
-pub(crate) fn merge_maps<K, V>(
+pub(crate) fn merge_maps<K, V, F, Err>(
     map1: &HashMap<K, V>,
     map2: &HashMap<K, V>,
-    mut f: impl FnMut(&V, &V) -> V,
-) -> HashMap<K, V>
+    mut f: F,
+) -> Result<HashMap<K, V>, Err>
 where
+    F: FnMut(&V, &V) -> Result<V, Err>,
     K: std::hash::Hash + Eq + Clone,
     V: Clone,
 {
     let mut kvs = HashMap::new();
     for (x, v2) in map2 {
         let newv = if let Some(v1) = map1.get(x) {
-            f(v1, v2)
+            f(v1, v2)?
         } else {
             v2.clone()
         };
@@ -508,7 +475,7 @@ where
         // Insert only if key not already present
         kvs.entry(x.clone()).or_insert_with(|| v1.clone());
     }
-    kvs
+    Ok(kvs)
 }
 
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
@@ -518,8 +485,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         RightBiasedRecordMerge, TextAppend,
     };
     use ValueF::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-        TextLit,
+        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit,
     };
     let x_borrow = x.as_whnf();
     let y_borrow = y.as_whnf();
@@ -604,31 +570,16 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordMerge,
-                    v1.clone(),
-                    v2.clone(),
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| {
+                Ok(Value::from_valuef_untyped(ValueF::PartialExpr(
+                    ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()),
                 )))
-            });
+            })?;
             Ret::ValueF(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordTypeMerge,
-                    v1.clone(),
-                    v2.clone(),
-                )))
-            });
-            Ret::ValueF(RecordType(kvs))
+        (RecursiveRecordTypeMerge, _, _) => {
+            unreachable!("This case should have been handled in typecheck")
         }
 
         (Equivalence, _, _) => {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index abe05a3..363d733 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -567,7 +567,9 @@ fn type_last_layer(
 
             // Union the two records, prefering
             // the values found in the RHS.
-            let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
+            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, r_t| {
+                Ok(r_t.clone())
+            })?;
 
             // Construct the final record type from the union
             RetTypeOnly(tck_record_type(
@@ -584,25 +586,7 @@ fn type_last_layer(
             ),
         )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
-            use crate::phase::normalize::intersection_with_key;
-
-            // Extract the Const of the LHS
-            let k_l = match l.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
-                }
-            };
-
-            // Extract the Const of the RHS
-            let k_r = match r.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
-                }
-            };
-
-            let k = max(k_l, k_r);
+            use crate::phase::normalize::merge_maps;
 
             // Extract the LHS record type
             let borrow_l = l.as_whnf();
@@ -623,9 +607,11 @@ fn type_last_layer(
             };
 
             // Ensure that the records combine without a type error
-            let kts = intersection_with_key(
+            let kts = merge_maps(
+                kts_x,
+                kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |_: &Label, l: &Value, r: &Value| {
+                |l: &Value, r: &Value| {
                     type_last_layer(
                         ctx,
                         ExprF::BinOp(
@@ -635,12 +621,9 @@ fn type_last_layer(
                         ),
                     )
                 },
-                kts_x,
-                kts_y,
-            );
-            tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+            )?;
 
-            RetTypeOnly(Value::from_const(k))
+            RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
diff --git a/tests_buffer b/tests_buffer
index 15dc9c5..511ea49 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -32,7 +32,9 @@ variables across import boundaries
 typecheck:
 something that involves destructuring a recordtype after merge
 add some of the more complicated Prelude tests back, like List/enumerate
-failure on old-style optional literal
+success/
+    regression/
+        RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } }
 failure/
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
-- 
cgit v1.2.3


From d5bdd48d4c34b4e213e3e2431936c160e4320a80 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 23 Aug 2019 18:53:46 +0200
Subject: Clarify which syntax elements are completely handled in the tck phase

---
 dhall/src/phase/normalize.rs | 40 ++++++++++++++++++----------------------
 dhall/src/phase/typecheck.rs |  9 ++++++---
 2 files changed, 24 insertions(+), 25 deletions(-)

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 28dc0f6..c8f5bc2 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -578,39 +578,41 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueF(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, _) => {
+        (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
             unreachable!("This case should have been handled in typecheck")
         }
 
-        (Equivalence, _, _) => {
-            Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
-        }
-
         _ => return None,
     })
 }
 
 pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
     use ValueF::{
-        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
-        NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
-        TextLit, UnionConstructor, UnionLit, UnionType,
+        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+        NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+        UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
         ExprF::Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprF::Embed(_) => unreachable!(),
-        ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => Ret::Value(x),
+        // Those cases have already been completely handled in the typechecking phase (using
+        // `RetWhole`), so they won't appear here.
+        ExprF::Lam(_, _, _)
+        | ExprF::Pi(_, _, _)
+        | ExprF::Let(_, _, _, _)
+        | ExprF::Embed(_)
+        | ExprF::Const(_)
+        | ExprF::Builtin(_)
+        | ExprF::Var(_)
+        | ExprF::Annot(_, _)
+        | ExprF::RecordType(_)
+        | ExprF::UnionType(_) => {
+            unreachable!("This case should have been handled in typecheck")
+        }
         ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
-        ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
-        ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
         ExprF::App(v, a) => Ret::Value(v.app(a)),
-        ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
-        ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
         ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
         ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -635,12 +637,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
         ExprF::RecordLit(kvs) => {
             Ret::ValueF(RecordLit(kvs.into_iter().collect()))
         }
-        ExprF::RecordType(kts) => {
-            Ret::ValueF(RecordType(kts.into_iter().collect()))
-        }
-        ExprF::UnionType(kts) => {
-            Ret::ValueF(UnionType(kts.into_iter().collect()))
-        }
         ExprF::TextLit(elts) => {
             use InterpolatedTextContents::Expr;
             let elts: Vec<_> = squash_textlit(elts.into_iter());
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 363d733..0268b80 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -291,7 +291,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     let ctx = TypecheckContext::new();
     Value::from_valuef_and_type(
-        ValueF::PartialExpr(ExprF::Builtin(b)),
+        ValueF::from_builtin(b),
         type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
     )
 }
@@ -399,7 +399,7 @@ fn type_last_layer(
             if &x.get_type()? != t {
                 return mkerr(AnnotMismatch(x.clone(), t.clone()));
             }
-            RetTypeOnly(x.get_type()?)
+            RetWhole(x.clone())
         }
         Assert(t) => {
             match &*t.as_whnf() {
@@ -649,7 +649,10 @@ fn type_last_layer(
                 return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
             }
 
-            RetTypeOnly(Value::from_const(Type))
+            RetWhole(Value::from_valuef_and_type(
+                ValueF::Equivalence(l.clone(), r.clone()),
+                Value::from_const(Type),
+            ))
         }
         BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
-- 
cgit v1.2.3


From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 16:09:55 +0200
Subject: Keep type information through normalization

---
 dhall/src/core/value.rs      |  39 ++++++---
 dhall/src/phase/normalize.rs | 200 ++++++++++++++++++++++++++++---------------
 dhall/src/phase/typecheck.rs |  21 ++---
 tests_buffer                 |   3 +
 4 files changed, 173 insertions(+), 90 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 69d372a..6f9f78a 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -70,12 +70,25 @@ impl ValueInternal {
                 ty: None,
             },
             |vint| match &vint.form {
-                Unevaled => ValueInternal {
-                    form: WHNF,
-                    // TODO: thunk chaining
-                    value: normalize_whnf(vint.value).into_whnf(),
-                    ty: vint.ty,
-                },
+                Unevaled => {
+                    let (value, ty) = (vint.value, vint.ty);
+                    let vovf = normalize_whnf(value, ty.as_ref());
+                    // let was_value = if let VoVF::Value(_) = &vovf {
+                    //     true
+                    // } else {
+                    //     false
+                    // };
+                    let (new_val, _new_ty) =
+                        vovf.into_whnf_and_type(ty.as_ref());
+                    // if was_value {
+                    //     debug_assert_eq!(ty, new_ty);
+                    // }
+                    ValueInternal {
+                        form: WHNF,
+                        value: new_val,
+                        ty: ty,
+                    }
+                }
                 // Already in WHNF
                 WHNF | NF => vint,
             },
@@ -221,7 +234,8 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let vovf = apply_any(self.clone(), v.clone());
+        let ty = self.get_type().ok();
+        let vovf = apply_any(self.clone(), v.clone(), ty.as_ref());
         match self.as_internal().get_type() {
             Err(_) => vovf.into_value_untyped(),
             Ok(t) => match &*t.as_whnf() {
@@ -240,15 +254,18 @@ impl Value {
 }
 
 impl VoVF {
-    pub(crate) fn into_whnf(self) -> ValueF {
+    pub(crate) fn into_whnf_and_type(
+        self,
+        ty: Option<&Value>,
+    ) -> (ValueF, Option<Value>) {
         match self {
-            VoVF::Value(v) => v.to_whnf(),
             VoVF::ValueF {
                 val,
                 form: Unevaled,
-            } => normalize_whnf(val).into_whnf(),
+            } => normalize_whnf(val, ty).into_whnf_and_type(ty),
             // Already at lest in WHNF
-            VoVF::ValueF { val, .. } => val,
+            VoVF::ValueF { val, .. } => (val, None),
+            VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()),
         }
     }
     pub(crate) fn into_value_untyped(self) -> Value {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index c8f5bc2..5743b0d 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,5 +1,6 @@
 use std::collections::HashMap;
 
+use dhall_syntax::Const::Type;
 use dhall_syntax::{
     BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
     NaiveDouble,
@@ -7,7 +8,7 @@ use dhall_syntax::{
 
 use crate::core::value::{Value, VoVF};
 use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
+use crate::core::var::{AlphaLabel, Shift, Subst};
 use crate::phase::Normalized;
 
 // Small helper enum to avoid repetition
@@ -32,21 +33,24 @@ impl<'a> Ret<'a> {
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
     (#$var:ident) => { $var.clone() };
-    (var($var:ident, $n:expr)) => {{
+    (var($var:ident, $n:expr, $($ty:tt)*)) => {{
         let var = crate::core::var::AlphaVar::from_var_and_alpha(
             Label::from(stringify!($var)).into(),
             $n
         );
-        ValueF::Var(var).into_value_untyped()
+        ValueF::Var(var)
+            .into_value_with_type(make_closure!($($ty)*))
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
-    (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ValueF::Lam(
-            Label::from(stringify!($var)).into(),
-            make_closure!($($ty)*),
-            make_closure!($($rest)*),
-        ).into_value_untyped()
-    };
+    (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+        let var: AlphaLabel = Label::from(stringify!($var)).into();
+        let ty = make_closure!($($ty)*);
+        let body = make_closure!($($body)*);
+        let body_ty = body.get_type().expect("Internal type error");
+        let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+            .into_value_with_type(Value::from_const(Type));
+        ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+    }};
     (Natural) => {
         Value::from_builtin(Builtin::Natural)
     };
@@ -54,10 +58,12 @@ macro_rules! make_closure {
         Value::from_builtin(Builtin::List)
             .app(make_closure!($($rest)*))
     };
-    (Some($($rest:tt)*)) => {
-        ValueF::NEOptionalLit(make_closure!($($rest)*))
-            .into_value_untyped()
-    };
+    (Some($($rest:tt)*)) => {{
+        let v = make_closure!($($rest)*);
+        let v_type = v.get_type().expect("Internal type error");
+        ValueF::NEOptionalLit(v)
+            .into_value_with_type(v_type)
+    }};
     (1 + $($rest:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
@@ -70,18 +76,25 @@ macro_rules! make_closure {
             make_closure!(Natural)
         )
     };
-    ([ $($head:tt)* ] # $($tail:tt)*) => {
+    ([ $($head:tt)* ] # $($tail:tt)*) => {{
+        let head = make_closure!($($head)*);
+        let tail = make_closure!($($tail)*);
+        let list_type = tail.get_type().expect("Internal type error");
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![make_closure!($($head)*)])
-                .into_value_untyped(),
-            make_closure!($($tail)*),
-        )).into_value_untyped()
-    };
+            ValueF::NEListLit(vec![head])
+                .into_value_with_type(list_type.clone()),
+            tail,
+        )).into_value_with_type(list_type)
+    }};
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
+pub(crate) fn apply_builtin(
+    b: Builtin,
+    args: Vec<Value>,
+    _ty: Option<&Value>,
+) -> VoVF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -231,37 +244,60 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             )),
             _ => Err(()),
         },
-        (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(t) => {
-                let mut kts = HashMap::new();
-                kts.insert("index".into(), Value::from_builtin(Natural));
-                kts.insert("value".into(), t.clone());
-                Ok((
-                    r,
-                    Ret::ValueF(EmptyListLit(Value::from_valuef_untyped(
+        (ListIndexed, [_, l, r..]) => {
+            let l_whnf = l.as_whnf();
+            match &*l_whnf {
+                EmptyListLit(_) | NEListLit(_) => {
+                    // Extract the type of the list elements
+                    let t = match &*l_whnf {
+                        EmptyListLit(t) => t.clone(),
+                        NEListLit(xs) => {
+                            xs[0].get_type().expect("Internal type error")
+                        }
+                        _ => unreachable!(),
+                    };
+
+                    // Construct the returned record type: { index: Natural, value: t }
+                    let mut kts = HashMap::new();
+                    kts.insert("index".into(), Value::from_builtin(Natural));
+                    kts.insert("value".into(), t.clone());
+                    let t = Value::from_valuef_and_type(
                         RecordType(kts),
-                    ))),
-                ))
-            }
-            NEListLit(xs) => {
-                let xs = xs
-                    .iter()
-                    .enumerate()
-                    .map(|(i, e)| {
-                        let i = NaturalLit(i);
-                        let mut kvs = HashMap::new();
-                        kvs.insert(
-                            "index".into(),
-                            Value::from_valuef_untyped(i),
-                        );
-                        kvs.insert("value".into(), e.clone());
-                        Value::from_valuef_untyped(RecordLit(kvs))
-                    })
-                    .collect();
-                Ok((r, Ret::ValueF(NEListLit(xs))))
+                        Value::from_const(Type),
+                    );
+
+                    // Construct the new list, with added indices
+                    let list = match &*l_whnf {
+                        EmptyListLit(_) => EmptyListLit(t),
+                        NEListLit(xs) => NEListLit(
+                            xs.iter()
+                                .enumerate()
+                                .map(|(i, e)| {
+                                    let mut kvs = HashMap::new();
+                                    kvs.insert(
+                                        "index".into(),
+                                        Value::from_valuef_and_type(
+                                            NaturalLit(i),
+                                            Value::from_builtin(
+                                                Builtin::Natural,
+                                            ),
+                                        ),
+                                    );
+                                    kvs.insert("value".into(), e.clone());
+                                    Value::from_valuef_and_type(
+                                        RecordLit(kvs),
+                                        t.clone(),
+                                    )
+                                })
+                                .collect(),
+                        ),
+                        _ => unreachable!(),
+                    };
+                    Ok((r, Ret::ValueF(list)))
+                }
+                _ => Err(()),
             }
-            _ => Err(()),
-        },
+        }
         (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
@@ -279,12 +315,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     Ret::Value(
                         f.app(list_t.clone())
                             .app({
-                                // Move `t` under new `x` variable
+                                // Move `t` under new variables
                                 let t1 = t.under_binder(Label::from("x"));
+                                let t2 = t1.under_binder(Label::from("xs"));
                                 make_closure!(
                                     λ(x : #t) ->
                                     λ(xs : List #t1) ->
-                                    [ var(x, 1) ] # var(xs, 0)
+                                    [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
                                 )
                             })
                             .app(
@@ -322,7 +359,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     r,
                     Ret::Value(
                         f.app(optional_t.clone())
-                            .app(make_closure!(λ(x: #t) -> Some(var(x, 0))))
+                            .app({
+                                let t1 = t.under_binder(Label::from("x"));
+                                make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+                            })
                             .app(
                                 EmptyOptionalLit(t.clone())
                                     .into_value_with_type(optional_t),
@@ -350,7 +390,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 r,
                 Ret::Value(
                     f.app(Value::from_builtin(Natural))
-                        .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                        .app(make_closure!(
+                            λ(x : Natural) -> 1 + var(x, 0, Natural)
+                        ))
                         .app(NaturalLit(0).into_value_with_type(
                             Value::from_builtin(Natural),
                         )),
@@ -387,7 +429,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF {
     let fallback = |f: Value, a: Value| {
         ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
     };
@@ -398,7 +440,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
-            apply_builtin(*b, args)
+            apply_builtin(*b, args, ty)
         }
         ValueF::UnionConstructor(l, kts) => {
             ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
@@ -458,14 +500,14 @@ pub(crate) fn merge_maps<K, V, F, Err>(
     mut f: F,
 ) -> Result<HashMap<K, V>, Err>
 where
-    F: FnMut(&V, &V) -> Result<V, Err>,
+    F: FnMut(&K, &V, &V) -> Result<V, Err>,
     K: std::hash::Hash + Eq + Clone,
     V: Clone,
 {
     let mut kvs = HashMap::new();
     for (x, v2) in map2 {
         let newv = if let Some(v1) = map1.get(x) {
-            f(v1, v2)?
+            f(x, v1, v2)?
         } else {
             v2.clone()
         };
@@ -478,14 +520,20 @@ where
     Ok(kvs)
 }
 
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(
+    o: BinOp,
+    x: &'a Value,
+    y: &'a Value,
+    ty: Option<&Value>,
+) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
     use ValueF::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit,
+        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
+        TextLit,
     };
     let x_borrow = x.as_whnf();
     let y_borrow = y.as_whnf();
@@ -570,10 +618,21 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| {
-                Ok(Value::from_valuef_untyped(ValueF::PartialExpr(
-                    ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()),
-                )))
+            let ty = ty.expect("Internal type error");
+            let ty_borrow = ty.as_whnf();
+            let kts = match &*ty_borrow {
+                RecordType(kts) => kts,
+                _ => unreachable!("Internal type error"),
+            };
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+                Ok(Value::from_valuef_and_type(
+                    ValueF::PartialExpr(ExprF::BinOp(
+                        RecursiveRecordMerge,
+                        v1.clone(),
+                        v2.clone(),
+                    )),
+                    kts.get(k).expect("Internal type error").clone(),
+                ))
             })?;
             Ret::ValueF(RecordLit(kvs))
         }
@@ -586,7 +645,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
+pub(crate) fn normalize_one_layer(
+    expr: ExprF<Value, Normalized>,
+    ty: Option<&Value>,
+) -> VoVF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
         NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
@@ -669,7 +731,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
                 }
             }
         }
-        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
+        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
@@ -746,10 +808,10 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF {
     match v {
-        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
-        ValueF::PartialExpr(e) => normalize_one_layer(e),
+        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+        ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
         ValueF::TextLit(elts) => {
             ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
         }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 0268b80..270191a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -307,14 +307,15 @@ fn type_with(
     use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
 
     Ok(match e.as_ref() {
-        Lam(x, t, b) => {
-            let tx = type_with(ctx, t.clone())?;
-            let ctx2 = ctx.insert_type(x, tx.clone());
-            let b = type_with(&ctx2, b.clone())?;
-            let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone());
-            let tb = b.get_type()?;
-            let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
-            Value::from_valuef_and_type(v, t)
+        Lam(var, annot, body) => {
+            let annot = type_with(ctx, annot.clone())?;
+            let ctx2 = ctx.insert_type(var, annot.clone());
+            let body = type_with(&ctx2, body.clone())?;
+            let body_type = body.get_type()?;
+            Value::from_valuef_and_type(
+                ValueF::Lam(var.clone().into(), annot.clone(), body),
+                tck_pi_type(ctx, var.clone(), annot, body_type)?,
+            )
         }
         Pi(x, ta, tb) => {
             let ta = type_with(ctx, ta.clone())?;
@@ -567,7 +568,7 @@ fn type_last_layer(
 
             // Union the two records, prefering
             // the values found in the RHS.
-            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, r_t| {
+            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
                 Ok(r_t.clone())
             })?;
 
@@ -611,7 +612,7 @@ fn type_last_layer(
                 kts_x,
                 kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |l: &Value, r: &Value| {
+                |_, l: &Value, r: &Value| {
                     type_last_layer(
                         ctx,
                         ExprF::BinOp(
diff --git a/tests_buffer b/tests_buffer
index 511ea49..93eb626 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -35,6 +35,9 @@ add some of the more complicated Prelude tests back, like List/enumerate
 success/
     regression/
         RecursiveRecordTypeMergeTripleCollision { x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } }
+        somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type
+        somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases
+        somehow test types added to the Foo/build closures
 failure/
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
-- 
cgit v1.2.3


From 80fb5355ea90377492b9863f632c01a808f8aade Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 16:33:12 +0200
Subject: Check consistency of type information

---
 dhall/src/core/value.rs      | 53 +++++++++++++++++++++++---------------------
 dhall/src/phase/normalize.rs |  4 ++--
 2 files changed, 30 insertions(+), 27 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 6f9f78a..7f98826 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -71,22 +71,13 @@ impl ValueInternal {
             },
             |vint| match &vint.form {
                 Unevaled => {
-                    let (value, ty) = (vint.value, vint.ty);
-                    let vovf = normalize_whnf(value, ty.as_ref());
-                    // let was_value = if let VoVF::Value(_) = &vovf {
-                    //     true
-                    // } else {
-                    //     false
-                    // };
-                    let (new_val, _new_ty) =
-                        vovf.into_whnf_and_type(ty.as_ref());
-                    // if was_value {
-                    //     debug_assert_eq!(ty, new_ty);
-                    // }
+                    let new_value =
+                        normalize_whnf(vint.value, vint.ty.as_ref())
+                            .into_whnf(vint.ty.as_ref());
                     ValueInternal {
                         form: WHNF,
-                        value: new_val,
-                        ty: ty,
+                        value: new_value,
+                        ty: vint.ty,
                     }
                 }
                 // Already in WHNF
@@ -254,18 +245,23 @@ impl Value {
 }
 
 impl VoVF {
-    pub(crate) fn into_whnf_and_type(
-        self,
-        ty: Option<&Value>,
-    ) -> (ValueF, Option<Value>) {
+    pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF {
         match self {
             VoVF::ValueF {
                 val,
                 form: Unevaled,
-            } => normalize_whnf(val, ty).into_whnf_and_type(ty),
+            } => normalize_whnf(val, ty).into_whnf(ty),
             // Already at lest in WHNF
-            VoVF::ValueF { val, .. } => (val, None),
-            VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()),
+            VoVF::ValueF { val, .. } => val,
+            VoVF::Value(v) => {
+                let v_ty = v.get_type().ok();
+                debug_assert_eq!(
+                    ty,
+                    v_ty.as_ref(),
+                    "The type recovered from normalization doesn't match the stored type."
+                );
+                v.to_whnf()
+            }
         }
     }
     pub(crate) fn into_value_untyped(self) -> Value {
@@ -274,11 +270,18 @@ impl VoVF {
             VoVF::ValueF { val, form } => Value::new(val, form, None),
         }
     }
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+    pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
         match self {
-            // TODO: check type with debug_assert ?
-            VoVF::Value(v) => v,
-            VoVF::ValueF { val, form } => Value::new(val, form, Some(t)),
+            VoVF::Value(v) => {
+                let v_ty = v.get_type().ok();
+                debug_assert_eq!(
+                    Some(&ty),
+                    v_ty.as_ref(),
+                    "The type recovered from normalization doesn't match the stored type."
+                );
+                v
+            }
+            VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)),
         }
     }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 5743b0d..fe99696 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -61,8 +61,8 @@ macro_rules! make_closure {
     (Some($($rest:tt)*)) => {{
         let v = make_closure!($($rest)*);
         let v_type = v.get_type().expect("Internal type error");
-        ValueF::NEOptionalLit(v)
-            .into_value_with_type(v_type)
+        let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
+        ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
     }};
     (1 + $($rest:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
-- 
cgit v1.2.3


From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 17:07:59 +0200
Subject: Enforce type information almost everywhere

---
 dhall/src/core/value.rs      | 66 ++++++++++++++++++++++++--------------------
 dhall/src/core/valuef.rs     |  3 --
 dhall/src/error/mod.rs       |  1 -
 dhall/src/phase/normalize.rs | 25 ++++++-----------
 dhall/src/phase/typecheck.rs | 21 ++++++--------
 5 files changed, 53 insertions(+), 63 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 7f98826..4a78b05 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -27,13 +27,14 @@ pub(crate) enum Form {
 }
 use Form::{Unevaled, NF, WHNF};
 
-#[derive(Debug)]
 /// Partially normalized value.
 /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 /// Invariant: if `form` is `NF`, `value` must be fully normalized
+#[derive(Debug)]
 struct ValueInternal {
     form: Form,
     value: ValueF,
+    /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
 }
 
@@ -69,11 +70,15 @@ impl ValueInternal {
                 value: ValueF::Const(Const::Type),
                 ty: None,
             },
-            |vint| match &vint.form {
-                Unevaled => {
+            |vint| match (&vint.form, &vint.ty) {
+                (Unevaled, None) => ValueInternal {
+                    form: NF,
+                    value: ValueF::Const(Const::Sort),
+                    ty: None,
+                },
+                (Unevaled, Some(ty)) => {
                     let new_value =
-                        normalize_whnf(vint.value, vint.ty.as_ref())
-                            .into_whnf(vint.ty.as_ref());
+                        normalize_whnf(vint.value, &ty).into_whnf(&ty);
                     ValueInternal {
                         form: WHNF,
                         value: new_value,
@@ -81,7 +86,7 @@ impl ValueInternal {
                     }
                 }
                 // Already in WHNF
-                WHNF | NF => vint,
+                (WHNF, _) | (NF, _) => vint,
             },
         )
     }
@@ -103,10 +108,9 @@ impl ValueInternal {
     fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
+            None => {
+                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+            }
         }
     }
 }
@@ -115,9 +119,13 @@ impl Value {
     pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
         ValueInternal { form, value, ty }.into_value()
     }
+    // TODO: this is very wrong
     pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
         Value::new(v, Unevaled, None)
     }
+    pub(crate) fn const_sort() -> Value {
+        Value::new(ValueF::Const(Const::Sort), NF, None)
+    }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
         Value::new(v, Unevaled, Some(t))
     }
@@ -225,27 +233,30 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let ty = self.get_type().ok();
-        let vovf = apply_any(self.clone(), v.clone(), ty.as_ref());
-        match self.as_internal().get_type() {
-            Err(_) => vovf.into_value_untyped(),
-            Ok(t) => match &*t.as_whnf() {
-                ValueF::Pi(x, _, e) => {
-                    let t = e.subst_shift(&x.into(), &v);
-                    vovf.into_value_with_type(t)
-                }
-                _ => unreachable!("Internal type error"),
-            },
+        let t = self.get_type_not_sort();
+        let vovf = apply_any(self.clone(), v.clone(), &t);
+        let t_borrow = t.as_whnf();
+        match &*t_borrow {
+            ValueF::Pi(x, _, e) => {
+                let t = e.subst_shift(&x.into(), &v);
+                vovf.into_value_with_type(t)
+            }
+            _ => unreachable!("Internal type error"),
         }
     }
 
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
         Ok(self.as_internal().get_type()?.clone())
     }
+    /// When we know the value isn't `Sort`, this gets the type directly
+    pub(crate) fn get_type_not_sort(&self) -> Value {
+        self.get_type()
+            .expect("Internal type error: value is `Sort` but shouldn't be")
+    }
 }
 
 impl VoVF {
-    pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF {
+    pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
         match self {
             VoVF::ValueF {
                 val,
@@ -256,7 +267,7 @@ impl VoVF {
             VoVF::Value(v) => {
                 let v_ty = v.get_type().ok();
                 debug_assert_eq!(
-                    ty,
+                    Some(ty),
                     v_ty.as_ref(),
                     "The type recovered from normalization doesn't match the stored type."
                 );
@@ -264,12 +275,6 @@ impl VoVF {
             }
         }
     }
-    pub(crate) fn into_value_untyped(self) -> Value {
-        match self {
-            VoVF::Value(v) => v,
-            VoVF::ValueF { val, form } => Value::new(val, form, None),
-        }
-    }
     pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
         match self {
             VoVF::Value(v) => {
@@ -288,7 +293,8 @@ impl VoVF {
     pub(crate) fn app(self, x: Value) -> VoVF {
         VoVF::Value(match self {
             VoVF::Value(v) => v.app(x),
-            VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
+            // TODO: this is very wrong
+            VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x),
         })
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 42606a9..5638078 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -47,9 +47,6 @@ pub(crate) enum ValueF {
 }
 
 impl ValueF {
-    pub(crate) fn into_value_untyped(self) -> Value {
-        Value::from_valuef_untyped(self)
-    }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13a9d7e..2ddaf3d 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -54,7 +54,6 @@ pub(crate) enum TypeMessage {
     NotAFunction(Value),
     TypeMismatch(Value, Value, Value),
     AnnotMismatch(Value, Value),
-    Untyped,
     InvalidListElement(usize, Value, Value),
     InvalidListType(Value),
     InvalidOptionalType(Value),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fe99696..9837a8b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -46,7 +46,7 @@ macro_rules! make_closure {
         let var: AlphaLabel = Label::from(stringify!($var)).into();
         let ty = make_closure!($($ty)*);
         let body = make_closure!($($body)*);
-        let body_ty = body.get_type().expect("Internal type error");
+        let body_ty = body.get_type_not_sort();
         let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
             .into_value_with_type(Value::from_const(Type));
         ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
@@ -60,7 +60,7 @@ macro_rules! make_closure {
     };
     (Some($($rest:tt)*)) => {{
         let v = make_closure!($($rest)*);
-        let v_type = v.get_type().expect("Internal type error");
+        let v_type = v.get_type_not_sort();
         let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
         ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
     }};
@@ -79,7 +79,7 @@ macro_rules! make_closure {
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
         let head = make_closure!($($head)*);
         let tail = make_closure!($($tail)*);
-        let list_type = tail.get_type().expect("Internal type error");
+        let list_type = tail.get_type_not_sort();
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
             ValueF::NEListLit(vec![head])
@@ -90,11 +90,7 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    _ty: Option<&Value>,
-) -> VoVF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -251,9 +247,7 @@ pub(crate) fn apply_builtin(
                     // Extract the type of the list elements
                     let t = match &*l_whnf {
                         EmptyListLit(t) => t.clone(),
-                        NEListLit(xs) => {
-                            xs[0].get_type().expect("Internal type error")
-                        }
+                        NEListLit(xs) => xs[0].get_type_not_sort(),
                         _ => unreachable!(),
                     };
 
@@ -429,7 +423,7 @@ pub(crate) fn apply_builtin(
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
     let fallback = |f: Value, a: Value| {
         ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
     };
@@ -524,7 +518,7 @@ fn apply_binop<'a>(
     o: BinOp,
     x: &'a Value,
     y: &'a Value,
-    ty: Option<&Value>,
+    ty: &Value,
 ) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -618,7 +612,6 @@ fn apply_binop<'a>(
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let ty = ty.expect("Internal type error");
             let ty_borrow = ty.as_whnf();
             let kts = match &*ty_borrow {
                 RecordType(kts) => kts,
@@ -647,7 +640,7 @@ fn apply_binop<'a>(
 
 pub(crate) fn normalize_one_layer(
     expr: ExprF<Value, Normalized>,
-    ty: Option<&Value>,
+    ty: &Value,
 ) -> VoVF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
@@ -808,7 +801,7 @@ pub(crate) fn normalize_one_layer(
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
     match v {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
         ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 270191a..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
-    match c {
-        Const::Type => Ok(const_to_value(Const::Kind)),
-        Const::Kind => Ok(const_to_value(Const::Sort)),
-        Const::Sort => {
-            Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
-        }
-    }
-}
-
 pub(crate) fn const_to_value(c: Const) -> Value {
     let v = ValueF::Const(c);
-    match type_of_const(c) {
-        Ok(t) => Value::from_valuef_and_type(v, t),
-        Err(_) => Value::from_valuef_untyped(v),
+    match c {
+        Const::Type => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+        }
+        Const::Kind => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+        }
+        Const::Sort => Value::const_sort(),
     }
 }
 
-- 
cgit v1.2.3


From bf37fd9da3782134ca4bca9567c34bbee81784b9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 21:16:38 +0200
Subject: Rework apply_builtin to enforce preservation of type information

---
 dhall/src/core/value.rs      |  32 ++--
 dhall/src/phase/normalize.rs | 339 ++++++++++++++++++++-----------------------
 tests_buffer                 |   2 +
 3 files changed, 173 insertions(+), 200 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 4a78b05..2554da1 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -116,18 +116,24 @@ impl ValueInternal {
 }
 
 impl Value {
-    pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
-        ValueInternal { form, value, ty }.into_value()
-    }
-    // TODO: this is very wrong
-    pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
-        Value::new(v, Unevaled, None)
+    fn new(value: ValueF, form: Form, ty: Value) -> Value {
+        ValueInternal {
+            form,
+            value,
+            ty: Some(ty),
+        }
+        .into_value()
     }
     pub(crate) fn const_sort() -> Value {
-        Value::new(ValueF::Const(Const::Sort), NF, None)
+        ValueInternal {
+            form: NF,
+            value: ValueF::Const(Const::Sort),
+            ty: None,
+        }
+        .into_value()
     }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
-        Value::new(v, Unevaled, Some(t))
+        Value::new(v, Unevaled, t)
     }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
@@ -286,17 +292,9 @@ impl VoVF {
                 );
                 v
             }
-            VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)),
+            VoVF::ValueF { val, form } => Value::new(val, form, ty),
         }
     }
-
-    pub(crate) fn app(self, x: Value) -> VoVF {
-        VoVF::Value(match self {
-            VoVF::Value(v) => v.app(x),
-            // TODO: this is very wrong
-            VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x),
-        })
-    }
 }
 
 impl Shift for Value {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 9837a8b..77f5023 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -11,25 +11,6 @@ use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaLabel, Shift, Subst};
 use crate::phase::Normalized;
 
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    ValueF(ValueF),
-    Value(Value),
-    ValueRef(&'a Value),
-    Expr(ExprF<Value, Normalized>),
-}
-
-impl<'a> Ret<'a> {
-    fn into_vovf_whnf(self) -> VoVF {
-        match self {
-            Ret::ValueF(v) => v.into_vovf_whnf(),
-            Ret::Value(v) => v.into_vovf(),
-            Ret::ValueRef(v) => v.clone().into_vovf(),
-            Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
-        }
-    }
-}
-
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
     (#$var:ident) => { $var.clone() };
@@ -94,80 +75,77 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
-    // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
+    // Small helper enum
+    enum Ret<'a> {
+        ValueF(ValueF),
+        Value(Value),
+        // For applications that can return a function, it's important to keep the remaining
+        // arguments to apply them to the resulting function.
+        ValueWithRemainingArgs(&'a [Value], Value),
+        DoneAsIs,
+    }
+
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t, r..]) => {
-            Ok((r, Ret::ValueF(EmptyOptionalLit(t.clone()))))
-        }
-        (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n == 0)))),
-            _ => Err(()),
+        (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+        (NaturalIsZero, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 == 0)))),
-            _ => Err(()),
+        (NaturalEven, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 != 0)))),
-            _ => Err(()),
+        (NaturalOdd, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, Ret::ValueF(IntegerLit(*n as isize)))),
-            _ => Err(()),
+        (NaturalToInteger, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalShow, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((
-                r,
+        (NaturalShow, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => {
                 Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
                     n.to_string(),
-                )])),
-            )),
-            _ => Err(()),
+                )]))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (NaturalSubtract, [a, b, r..]) => {
-            match (&*a.as_whnf(), &*b.as_whnf()) {
-                (NaturalLit(a), NaturalLit(b)) => Ok((
-                    r,
-                    Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })),
-                )),
-                (NaturalLit(0), _) => Ok((r, Ret::ValueRef(b))),
-                (_, NaturalLit(0)) => Ok((r, Ret::ValueF(NaturalLit(0)))),
-                _ if a == b => Ok((r, Ret::ValueF(NaturalLit(0)))),
-                _ => Err(()),
+        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+            (NaturalLit(a), NaturalLit(b)) => {
+                Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
             }
-        }
-        (IntegerShow, [n, r..]) => match &*n.as_whnf() {
+            (NaturalLit(0), _) => Ret::Value(b.clone()),
+            (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+            _ if a == b => Ret::ValueF(NaturalLit(0)),
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerShow, [n]) => match &*n.as_whnf() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
                 } else {
                     format!("+{}", n)
                 };
-                Ok((
-                    r,
-                    Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
-                        s,
-                    )])),
-                ))
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
+        (IntegerToDouble, [n]) => match &*n.as_whnf() {
             IntegerLit(n) => {
-                Ok((r, Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))))
+                Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (DoubleShow, [n, r..]) => match &*n.as_whnf() {
-            DoubleLit(n) => Ok((
-                r,
+        (DoubleShow, [n]) => match &*n.as_whnf() {
+            DoubleLit(n) => {
                 Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
                     n.to_string(),
-                )])),
-            )),
-            _ => Err(()),
+                )]))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (TextShow, [v, r..]) => match &*v.as_whnf() {
+        (TextShow, [v]) => match &*v.as_whnf() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -176,12 +154,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
                         let txt: InterpolatedText<Normalized> =
                             std::iter::empty().collect();
                         let s = txt.to_string();
-                        Ok((
-                            r,
-                            Ret::ValueF(TextLit(vec![
-                                InterpolatedTextContents::Text(s),
-                            ])),
-                        ))
+                        Ret::ValueF(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
                     // interpolations, there is a single Text item) in the literal.
@@ -193,54 +168,42 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
                             ))
                             .collect();
                         let s = txt.to_string();
-                        Ok((
-                            r,
-                            Ret::ValueF(TextLit(vec![
-                                InterpolatedTextContents::Text(s),
-                            ])),
-                        ))
+                        Ret::ValueF(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
                     }
-                    _ => Err(()),
+                    _ => Ret::DoneAsIs,
                 }
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, Ret::ValueF(NaturalLit(0)))),
-            NEListLit(xs) => Ok((r, Ret::ValueF(NaturalLit(xs.len())))),
-            _ => Err(()),
+        (ListLength, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+            NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+            _ => Ret::DoneAsIs,
         },
-        (ListHead, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => {
-                Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone()))))
+        (ListHead, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => {
+                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
-            NEListLit(xs) => Ok((
-                r,
-                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())),
-            )),
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (ListLast, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => {
-                Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone()))))
-            }
-            NEListLit(xs) => Ok((
-                r,
-                Ret::ValueF(NEOptionalLit(
-                    xs.iter().rev().next().unwrap().clone(),
-                )),
+        (ListLast, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+                xs.iter().rev().next().unwrap().clone(),
             )),
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, Ret::ValueF(EmptyListLit(n.clone())))),
-            NEListLit(xs) => Ok((
-                r,
-                Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())),
-            )),
-            _ => Err(()),
+        (ListReverse, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
+            NEListLit(xs) => {
+                Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (ListIndexed, [_, l, r..]) => {
+        (ListIndexed, [_, l]) => {
             let l_whnf = l.as_whnf();
             match &*l_whnf {
                 EmptyListLit(_) | NEListLit(_) => {
@@ -287,16 +250,16 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
                         ),
                         _ => unreachable!(),
                     };
-                    Ok((r, Ret::ValueF(list)))
+                    Ret::ValueF(list)
                 }
-                _ => Err(()),
+                _ => Ret::DoneAsIs,
             }
         }
-        (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
+        (ListBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, Ret::Value(args[1].clone())))
+                    Ret::Value(args[1].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -304,44 +267,41 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
             }
             _ => {
                 let list_t = Value::from_builtin(List).app(t.clone());
-                Ok((
-                    r,
-                    Ret::Value(
-                        f.app(list_t.clone())
-                            .app({
-                                // Move `t` under new variables
-                                let t1 = t.under_binder(Label::from("x"));
-                                let t2 = t1.under_binder(Label::from("xs"));
-                                make_closure!(
-                                    λ(x : #t) ->
-                                    λ(xs : List #t1) ->
-                                    [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
-                                )
-                            })
-                            .app(
-                                EmptyListLit(t.clone())
-                                    .into_value_with_type(list_t),
-                            ),
-                    ),
-                ))
+                Ret::Value(
+                    f.app(list_t.clone())
+                        .app({
+                            // Move `t` under new variables
+                            let t1 = t.under_binder(Label::from("x"));
+                            let t2 = t1.under_binder(Label::from("xs"));
+                            make_closure!(
+                                λ(x : #t) ->
+                                λ(xs : List #t1) ->
+                                [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
+                            )
+                        })
+                        .app(
+                            EmptyListLit(t.clone())
+                                .into_value_with_type(list_t),
+                        ),
+                )
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, Ret::ValueRef(nil))),
+            EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().cloned().rev() {
                     v = cons.app(x).app(v);
                 }
-                Ok((r, Ret::Value(v)))
+                Ret::ValueWithRemainingArgs(r, v)
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
+        (OptionalBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, Ret::Value(args[1].clone())))
+                    Ret::Value(args[1].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -349,52 +309,51 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
             }
             _ => {
                 let optional_t = Value::from_builtin(Optional).app(t.clone());
-                Ok((
-                    r,
-                    Ret::Value(
-                        f.app(optional_t.clone())
-                            .app({
-                                let t1 = t.under_binder(Label::from("x"));
-                                make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
-                            })
-                            .app(
-                                EmptyOptionalLit(t.clone())
-                                    .into_value_with_type(optional_t),
-                            ),
-                    ),
-                ))
+                Ret::Value(
+                    f.app(optional_t.clone())
+                        .app({
+                            let t1 = t.under_binder(Label::from("x"));
+                            make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+                        })
+                        .app(
+                            EmptyOptionalLit(t.clone())
+                                .into_value_with_type(optional_t),
+                        ),
+                )
             }
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
-            EmptyOptionalLit(_) => Ok((r, Ret::ValueRef(nothing))),
-            NEOptionalLit(x) => Ok((r, Ret::Value(just.app(x.clone())))),
-            _ => Err(()),
+            EmptyOptionalLit(_) => {
+                Ret::ValueWithRemainingArgs(r, nothing.clone())
+            }
+            NEOptionalLit(x) => {
+                Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
+        (NaturalBuild, [f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, Ret::Value(args[0].clone())))
+                    Ret::Value(args[0].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
-            _ => Ok((
-                r,
-                Ret::Value(
-                    f.app(Value::from_builtin(Natural))
-                        .app(make_closure!(
-                            λ(x : Natural) -> 1 + var(x, 0, Natural)
-                        ))
-                        .app(NaturalLit(0).into_value_with_type(
-                            Value::from_builtin(Natural),
-                        )),
-                ),
-            )),
+            _ => Ret::Value(
+                f.app(Value::from_builtin(Natural))
+                    .app(make_closure!(
+                        λ(x : Natural) -> 1 + var(x, 0, Natural)
+                    ))
+                    .app(
+                        NaturalLit(0)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    ),
+            ),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
-            NaturalLit(0) => Ok((r, Ret::ValueRef(zero))),
+            NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
                     .app(
@@ -404,22 +363,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
                     .app(t.clone())
                     .app(succ.clone())
                     .app(zero.clone());
-                Ok((r, Ret::Value(succ.app(fold))))
+                Ret::ValueWithRemainingArgs(r, succ.app(fold))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        _ => Err(()),
+        _ => Ret::DoneAsIs,
     };
     match ret {
-        Ok((unconsumed_args, ret)) => {
-            let mut v = ret.into_vovf_whnf();
+        Ret::ValueF(v) => v.into_vovf_whnf(),
+        Ret::Value(v) => v.into_vovf(),
+        Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
                 v = v.app(x);
             }
-            v
+            v.into_vovf()
         }
-        Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(),
+        Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(),
     }
 }
 
@@ -514,6 +474,14 @@ where
     Ok(kvs)
 }
 
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+    ValueF(ValueF),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprF<Value, Normalized>),
+}
+
 fn apply_binop<'a>(
     o: BinOp,
     x: &'a Value,
@@ -797,7 +765,12 @@ pub(crate) fn normalize_one_layer(
         }
     };
 
-    ret.into_vovf_whnf()
+    match ret {
+        Ret::ValueF(v) => v.into_vovf_whnf(),
+        Ret::Value(v) => v.into_vovf(),
+        Ret::ValueRef(v) => v.clone().into_vovf(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
+    }
 }
 
 /// Normalize a ValueF into WHNF
diff --git a/tests_buffer b/tests_buffer
index 93eb626..1ad880e 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -28,6 +28,8 @@ variables across import boundaries
     TextLitNested1 "${""}${x}"
     TextLitNested2 "${"${x}"}"
     TextLitNested3 "${"${""}"}${x}"
+    regression/
+        NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True
 
 typecheck:
 something that involves destructuring a recordtype after merge
-- 
cgit v1.2.3


From 906cbf5fc4c3bee65f24df1604497e33c6a20833 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 21:52:59 +0200
Subject: Remove now unnecessary VoVF enum

---
 dhall/src/core/value.rs      | 95 +++++++++++++-------------------------------
 dhall/src/core/valuef.rs     | 10 +----
 dhall/src/phase/normalize.rs | 46 +++++++++++----------
 3 files changed, 53 insertions(+), 98 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 2554da1..13f8e59 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,15 +44,6 @@ struct ValueInternal {
 #[derive(Clone)]
 pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
-/// When a function needs to return either a freshly created ValueF or an existing Value, but
-/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
-/// avoid loss of typ information.
-#[derive(Debug, Clone)]
-pub(crate) enum VoVF {
-    Value(Value),
-    ValueF { val: ValueF, form: Form },
-}
-
 impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
@@ -76,15 +67,11 @@ impl ValueInternal {
                     value: ValueF::Const(Const::Sort),
                     ty: None,
                 },
-                (Unevaled, Some(ty)) => {
-                    let new_value =
-                        normalize_whnf(vint.value, &ty).into_whnf(&ty);
-                    ValueInternal {
-                        form: WHNF,
-                        value: new_value,
-                        ty: vint.ty,
-                    }
-                }
+                (Unevaled, Some(ty)) => ValueInternal {
+                    form: WHNF,
+                    value: normalize_whnf(vint.value, &ty),
+                    ty: vint.ty,
+                },
                 // Already in WHNF
                 (WHNF, _) | (NF, _) => vint,
             },
@@ -135,6 +122,9 @@ impl Value {
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
         Value::new(v, Unevaled, t)
     }
+    pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+        Value::new(v, WHNF, t)
+    }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
     }
@@ -182,16 +172,22 @@ impl Value {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.as_whnf().normalize_to_expr_maybe_alpha(true)
     }
-    /// TODO: cloning a valuef can often be avoided
-    pub(crate) fn to_whnf(&self) -> ValueF {
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
         self.as_whnf().clone()
     }
+    /// Before discarding type information, check that it matches the expected return type.
+    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+        let self_ty = self.get_type().ok();
+        debug_assert_eq!(
+            Some(ty),
+            self_ty.as_ref(),
+            "The value returned from normalization doesn't have the expected type."
+        );
+        self.to_whnf_ignore_type()
+    }
     pub(crate) fn into_typed(self) -> Typed {
         Typed::from_value(self)
     }
-    pub(crate) fn into_vovf(self) -> VoVF {
-        VoVF::Value(self)
-    }
 
     /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
     fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
@@ -239,16 +235,14 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let t = self.get_type_not_sort();
-        let vovf = apply_any(self.clone(), v.clone(), &t);
-        let t_borrow = t.as_whnf();
-        match &*t_borrow {
-            ValueF::Pi(x, _, e) => {
-                let t = e.subst_shift(&x.into(), &v);
-                vovf.into_value_with_type(t)
-            }
+        let body_t = match &*self.get_type_not_sort().as_whnf() {
+            ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v),
             _ => unreachable!("Internal type error"),
-        }
+        };
+        Value::from_valuef_and_type_whnf(
+            apply_any(self.clone(), v, &body_t),
+            body_t,
+        )
     }
 
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
@@ -261,42 +255,6 @@ impl Value {
     }
 }
 
-impl VoVF {
-    pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
-        match self {
-            VoVF::ValueF {
-                val,
-                form: Unevaled,
-            } => normalize_whnf(val, ty).into_whnf(ty),
-            // Already at lest in WHNF
-            VoVF::ValueF { val, .. } => val,
-            VoVF::Value(v) => {
-                let v_ty = v.get_type().ok();
-                debug_assert_eq!(
-                    Some(ty),
-                    v_ty.as_ref(),
-                    "The type recovered from normalization doesn't match the stored type."
-                );
-                v.to_whnf()
-            }
-        }
-    }
-    pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
-        match self {
-            VoVF::Value(v) => {
-                let v_ty = v.get_type().ok();
-                debug_assert_eq!(
-                    Some(&ty),
-                    v_ty.as_ref(),
-                    "The type recovered from normalization doesn't match the stored type."
-                );
-                v
-            }
-            VoVF::ValueF { val, form } => Value::new(val, form, ty),
-        }
-    }
-}
-
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -324,6 +282,7 @@ impl Subst<Value> for ValueInternal {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
+            // TODO: check type info if self.value if Var(v) and v == var
             value: self.value.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
         }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 5638078..9ea2467 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::{Form, Value, VoVF};
+use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
 
@@ -50,12 +50,6 @@ impl ValueF {
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_vovf_whnf(self) -> VoVF {
-        VoVF::ValueF {
-            val: self,
-            form: Form::WHNF,
-        }
-    }
 
     /// Convert the value to a fully normalized syntactic expression
     pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
@@ -339,7 +333,7 @@ impl Subst<Value> for ValueF {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
             ),
-            ValueF::Var(v) if v == var => val.to_whnf(),
+            ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
             ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
             ValueF::Const(c) => ValueF::Const(*c),
             ValueF::BoolLit(b) => ValueF::BoolLit(*b),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 77f5023..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::value::{Value, VoVF};
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaLabel, Shift, Subst};
 use crate::phase::Normalized;
@@ -71,7 +71,11 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
+pub(crate) fn apply_builtin(
+    b: Builtin,
+    args: Vec<Value>,
+    ty: &Value,
+) -> ValueF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -370,38 +374,36 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
         _ => Ret::DoneAsIs,
     };
     match ret {
-        Ret::ValueF(v) => v.into_vovf_whnf(),
-        Ret::Value(v) => v.into_vovf(),
+        Ret::ValueF(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
         Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
                 v = v.app(x);
             }
-            v.into_vovf()
+            v.to_whnf_check_type(ty)
         }
-        Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(),
+        Ret::DoneAsIs => AppliedBuiltin(b, args),
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
-    let fallback = |f: Value, a: Value| {
-        ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
-    };
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(),
+        ValueF::Lam(x, _, e) => {
+            e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+        }
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args, ty)
         }
         ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
+            ValueF::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
-            fallback(f, a)
+            ValueF::PartialExpr(ExprF::App(f, a))
         }
     }
 }
@@ -609,7 +611,7 @@ fn apply_binop<'a>(
 pub(crate) fn normalize_one_layer(
     expr: ExprF<Value, Normalized>,
     ty: &Value,
-) -> VoVF {
+) -> ValueF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
         NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
@@ -766,22 +768,22 @@ pub(crate) fn normalize_one_layer(
     };
 
     match ret {
-        Ret::ValueF(v) => v.into_vovf_whnf(),
-        Ret::Value(v) => v.into_vovf(),
-        Ret::ValueRef(v) => v.clone().into_vovf(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
+        Ret::ValueF(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
     match v {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
         ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
         ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
+            ValueF::TextLit(squash_textlit(elts.into_iter()))
         }
         // All other cases are already in WHNF
-        v => v.into_vovf_whnf(),
+        v => v,
     }
 }
-- 
cgit v1.2.3


From 829fff5bd3e2115c0a16d40a4dc266747d622b08 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 26 Aug 2019 18:54:29 +0200
Subject: Check correctness of type info in a few more places

---
 dhall/src/core/value.rs | 60 +++++++++++++++++++++++++++++++++++--------------
 1 file changed, 43 insertions(+), 17 deletions(-)

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 13f8e59..21ac288 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -62,16 +62,17 @@ impl ValueInternal {
                 ty: None,
             },
             |vint| match (&vint.form, &vint.ty) {
-                (Unevaled, None) => ValueInternal {
-                    form: NF,
-                    value: ValueF::Const(Const::Sort),
-                    ty: None,
-                },
                 (Unevaled, Some(ty)) => ValueInternal {
                     form: WHNF,
                     value: normalize_whnf(vint.value, &ty),
                     ty: vint.ty,
                 },
+                // `value` is `Sort`
+                (Unevaled, None) => ValueInternal {
+                    form: NF,
+                    value: ValueF::Const(Const::Sort),
+                    ty: None,
+                },
                 // Already in WHNF
                 (WHNF, _) | (NF, _) => vint,
             },
@@ -177,12 +178,7 @@ impl Value {
     }
     /// Before discarding type information, check that it matches the expected return type.
     pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
-        let self_ty = self.get_type().ok();
-        debug_assert_eq!(
-            Some(ty),
-            self_ty.as_ref(),
-            "The value returned from normalization doesn't have the expected type."
-        );
+        self.check_type(ty);
         self.to_whnf_ignore_type()
     }
     pub(crate) fn into_typed(self) -> Typed {
@@ -236,7 +232,10 @@ impl Value {
 
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
-            ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v),
+            ValueF::Pi(x, t, e) => {
+                v.check_type(t);
+                e.subst_shift(&x.into(), &v)
+            }
             _ => unreachable!("Internal type error"),
         };
         Value::from_valuef_and_type_whnf(
@@ -245,6 +244,15 @@ impl Value {
         )
     }
 
+    /// In debug mode, panic if the provided type doesn't match the value's type.
+    /// Otherwise does nothing.
+    pub(crate) fn check_type(&self, ty: &Value) {
+        debug_assert_eq!(
+            Some(ty),
+            self.get_type().ok().as_ref(),
+            "Internal type error"
+        );
+    }
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
         Ok(self.as_internal().get_type()?.clone())
     }
@@ -273,7 +281,17 @@ impl Shift for ValueInternal {
 
 impl Subst<Value> for Value {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        Value(self.0.subst_shift(var, val))
+        match &*self.as_valuef() {
+            // If the var matches, we can just reuse the provided value instead of copying it.
+            // We also check that the types match, if in debug mode.
+            ValueF::Var(v) if v == var => {
+                if let Ok(self_ty) = self.get_type() {
+                    val.check_type(&self_ty.subst_shift(var, val));
+                }
+                val.clone()
+            }
+            _ => Value(self.0.subst_shift(var, val)),
+        }
     }
 }
 
@@ -282,7 +300,6 @@ impl Subst<Value> for ValueInternal {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
-            // TODO: check type info if self.value if Var(v) and v == var
             value: self.value.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
         }
@@ -300,8 +317,17 @@ impl std::cmp::Eq for Value {}
 impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
-        fmt.debug_tuple(&format!("Value@{:?}", &vint.form))
-            .field(&vint.value)
-            .finish()
+        if let ValueF::Const(c) = &vint.value {
+            write!(fmt, "{:?}", c)
+        } else {
+            let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
+            x.field("value", &vint.value);
+            if let Some(ty) = vint.ty.as_ref() {
+                x.field("type", &ty);
+            } else {
+                x.field("type", &None::<()>);
+            }
+            x.finish()
+        }
     }
 }
-- 
cgit v1.2.3