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())