s/Value/ValueF/

7 files changed, 343 insertions, 337 deletions

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index cc25749..b1fbde9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use dhall_syntax::{Label, V};
 
 use crate::core::thunk::Thunk;
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 use crate::phase::{Type, Typed};
@@ -44,7 +44,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     let (th, t) = match i {
                         CtxItem::Kept(newvar, t) => {
-                            (Value::Var(newvar).into_thunk(), t)
+                            (ValueF::Var(newvar).into_thunk(), t)
                         }
                         CtxItem::Replaced(th, t) => (th, t),
                     };
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5f96ec8..cf7c097 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -5,7 +5,7 @@ use std::rc::Rc;
 use dhall_syntax::{Const, ExprF};
 
 use crate::core::context::TypecheckContext;
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr};
@@ -24,12 +24,12 @@ use Marker::{NF, WHNF};
 #[derive(Debug)]
 enum ThunkInternal {
     /// Partially normalized value whose subexpressions have been thunked (this is returned from
-    /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
+    /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no
     /// requirement of WHNF here.
     PartialExpr(ExprF<Thunk, Normalized>),
     /// Partially normalized value.
     /// Invariant: if the marker is `NF`, the value must be fully normalized
-    Value(Marker, Value),
+    ValueF(Marker, ValueF),
 }
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
@@ -61,10 +61,10 @@ impl ThunkInternal {
         match self {
             ThunkInternal::PartialExpr(e) => {
                 *self =
-                    ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
+                    ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
             }
             // Already at least in WHNF
-            ThunkInternal::Value(_, _) => {}
+            ThunkInternal::ValueF(_, _) => {}
         }
     }
 
@@ -74,37 +74,37 @@ impl ThunkInternal {
                 self.normalize_whnf();
                 self.normalize_nf();
             }
-            ThunkInternal::Value(m @ WHNF, v) => {
+            ThunkInternal::ValueF(m @ WHNF, v) => {
                 v.normalize_mut();
                 *m = NF;
             }
             // Already in NF
-            ThunkInternal::Value(NF, _) => {}
+            ThunkInternal::ValueF(NF, _) => {}
         }
     }
 
     // Always use normalize_whnf before
-    fn as_whnf(&self) -> &Value {
+    fn as_whnf(&self) -> &ValueF {
         match self {
             ThunkInternal::PartialExpr(_) => unreachable!(),
-            ThunkInternal::Value(_, v) => v,
+            ThunkInternal::ValueF(_, v) => v,
         }
     }
 
     // Always use normalize_nf before
-    fn as_nf(&self) -> &Value {
+    fn as_nf(&self) -> &ValueF {
         match self {
-            ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+            ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
                 unreachable!()
             }
-            ThunkInternal::Value(NF, v) => v,
+            ThunkInternal::ValueF(NF, v) => v,
         }
     }
 }
 
 impl Thunk {
-    pub(crate) fn from_value(v: Value) -> Thunk {
-        ThunkInternal::Value(WHNF, v).into_thunk()
+    pub(crate) fn from_valuef(v: ValueF) -> Thunk {
+        ThunkInternal::ValueF(WHNF, v).into_thunk()
     }
 
     pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
@@ -130,38 +130,38 @@ impl Thunk {
                 self.0.borrow_mut().normalize_whnf();
             }
             // Already at least in WHNF
-            ThunkInternal::Value(_, _) => {}
+            ThunkInternal::ValueF(_, _) => {}
         }
     }
 
     fn do_normalize_nf(&self) {
         let borrow = self.0.borrow();
         match &*borrow {
-            ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+            ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
                 drop(borrow);
                 self.0.borrow_mut().normalize_nf();
             }
             // Already in NF
-            ThunkInternal::Value(NF, _) => {}
+            ThunkInternal::ValueF(NF, _) => {}
         }
     }
 
     // WARNING: avoid normalizing any thunk while holding on to this ref
     // or you could run into BorrowMut panics
-    pub(crate) fn normalize_nf(&self) -> Ref<Value> {
+    pub(crate) fn normalize_nf(&self) -> Ref<ValueF> {
         self.do_normalize_nf();
         Ref::map(self.0.borrow(), ThunkInternal::as_nf)
     }
 
     // WARNING: avoid normalizing any thunk while holding on to this ref
     // or you could run into BorrowMut panics
-    pub(crate) fn as_value(&self) -> Ref<Value> {
+    pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
         self.do_normalize_whnf();
         Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
     }
 
-    pub(crate) fn to_value(&self) -> Value {
-        self.as_value().clone()
+    pub(crate) fn to_valuef(&self) -> ValueF {
+        self.as_valuef().clone()
     }
 
     pub(crate) fn normalize_to_expr_maybe_alpha(
@@ -171,27 +171,27 @@ impl Thunk {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app_val(&self, val: Value) -> Value {
+    pub(crate) fn app_val(&self, val: ValueF) -> ValueF {
         self.app_thunk(val.into_thunk())
     }
 
-    pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
+    pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF {
         apply_any(self.clone(), th)
     }
 }
 
 impl TypedThunk {
-    pub(crate) fn from_value(v: Value) -> TypedThunk {
-        TypedThunk::from_thunk_untyped(Thunk::from_value(v))
+    pub(crate) fn from_valuef(v: ValueF) -> TypedThunk {
+        TypedThunk::from_thunk_untyped(Thunk::from_valuef(v))
     }
 
     pub(crate) fn from_type(t: Type) -> TypedThunk {
         t.into_typethunk()
     }
 
-    pub(crate) fn normalize_nf(&self) -> Value {
+    pub(crate) fn normalize_nf(&self) -> ValueF {
         match self {
-            TypedThunk::Const(c) => Value::Const(*c),
+            TypedThunk::Const(c) => ValueF::Const(*c),
             TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => {
                 thunk.normalize_nf().clone()
             }
@@ -221,27 +221,29 @@ impl TypedThunk {
     pub(crate) fn from_const(c: Const) -> Self {
         TypedThunk::Const(c)
     }
-    pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self {
-        TypedThunk::from_thunk_and_type(Thunk::from_value(v), t)
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
+        TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t)
     }
 
     // TODO: Avoid cloning if possible
-    pub(crate) fn to_value(&self) -> Value {
+    pub(crate) fn to_valuef(&self) -> ValueF {
         match self {
-            TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(),
-            TypedThunk::Const(c) => Value::Const(*c),
+            TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => {
+                th.to_valuef()
+            }
+            TypedThunk::Const(c) => ValueF::Const(*c),
         }
     }
     pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
-        self.to_value().normalize_to_expr()
+        self.to_valuef().normalize_to_expr()
     }
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
-        self.to_value().normalize_to_expr_maybe_alpha(true)
+        self.to_valuef().normalize_to_expr_maybe_alpha(true)
     }
     pub(crate) fn to_thunk(&self) -> Thunk {
         match self {
             TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(),
-            TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)),
+            TypedThunk::Const(c) => Thunk::from_valuef(ValueF::Const(*c)),
         }
     }
     pub(crate) fn to_type(&self) -> Type {
@@ -252,8 +254,8 @@ impl TypedThunk {
     }
     pub(crate) fn as_const(&self) -> Option<Const> {
         // TODO: avoid clone
-        match &self.to_value() {
-            Value::Const(c) => Some(*c),
+        match &self.to_valuef() {
+            ValueF::Const(c) => Some(*c),
             _ => None,
         }
     }
@@ -294,8 +296,8 @@ impl Shift for ThunkInternal {
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
                 )?,
             ),
-            ThunkInternal::Value(m, v) => {
-                ThunkInternal::Value(*m, v.shift(delta, var)?)
+            ThunkInternal::ValueF(m, v) => {
+                ThunkInternal::ValueF(*m, v.shift(delta, var)?)
             }
         })
     }
@@ -336,9 +338,9 @@ impl Subst<Typed> for ThunkInternal {
                     },
                 ),
             ),
-            ThunkInternal::Value(_, v) => {
+            ThunkInternal::ValueF(_, v) => {
                 // The resulting value may not stay in normal form after substitution
-                ThunkInternal::Value(WHNF, v.subst_shift(var, val))
+                ThunkInternal::ValueF(WHNF, v.subst_shift(var, val))
             }
         }
     }
@@ -361,14 +363,14 @@ impl Subst<Typed> for TypedThunk {
 
 impl std::cmp::PartialEq for Thunk {
     fn eq(&self, other: &Self) -> bool {
-        *self.as_value() == *other.as_value()
+        *self.as_valuef() == *other.as_valuef()
     }
 }
 impl std::cmp::Eq for Thunk {}
 
 impl std::cmp::PartialEq for TypedThunk {
     fn eq(&self, other: &Self) -> bool {
-        self.to_value() == other.to_value()
+        self.to_valuef() == other.to_valuef()
     }
 }
 impl std::cmp::Eq for TypedThunk {}
@@ -377,7 +379,7 @@ impl std::fmt::Debug for Thunk {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let b: &ThunkInternal = &self.0.borrow();
         match b {
-            ThunkInternal::Value(m, v) => {
+            ThunkInternal::ValueF(m, v) => {
                 f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish()
             }
             ThunkInternal::PartialExpr(e) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index d3d017d..0f2ef00 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -15,16 +15,16 @@ use crate::phase::{Normalized, Typed};
 /// A semantic value. The invariants ensure this value represents a Weak-Head
 /// Normal Form (WHNF). This means that this first constructor is the first constructor of the
 /// final Normal Form (NF).
-/// This WHNF must be preserved by operations on `Value`s. In particular, `subst_shift` could break
+/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break
 /// the invariants so need to be careful to reevaluate as needed.
 /// Subexpressions are Thunks, which are partially evaluated expressions that are normalized
-/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the
-/// Value is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
+/// on-demand. When all the Thunks in a ValueF are at least in WHNF, and recursively so, then the
+/// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
 /// if we have the first constructor of the NF at all levels, we actually have the NF.
 /// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence
 /// (normalization). Equality will normalize only as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Value {
+pub enum ValueF {
     /// Closures
     Lam(AlphaLabel, TypedThunk, Thunk),
     Pi(AlphaLabel, TypedThunk, TypedThunk),
@@ -55,9 +55,9 @@ pub enum Value {
     PartialExpr(ExprF<Thunk, Normalized>),
 }
 
-impl Value {
+impl ValueF {
     pub(crate) fn into_thunk(self) -> Thunk {
-        Thunk::from_value(self)
+        Thunk::from_valuef(self)
     }
 
     /// Convert the value to a fully normalized syntactic expression
@@ -71,12 +71,12 @@ impl Value {
         alpha: bool,
     ) -> OutputSubExpr {
         match self {
-            Value::Lam(x, t, e) => rc(ExprF::Lam(
+            ValueF::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
                 t.normalize_to_expr_maybe_alpha(alpha),
                 e.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::AppliedBuiltin(b, args) => {
+            ValueF::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(*b));
                 for v in args {
                     e = rc(ExprF::App(
@@ -86,48 +86,48 @@ impl Value {
                 }
                 e
             }
-            Value::Pi(x, t, e) => rc(ExprF::Pi(
+            ValueF::Pi(x, t, e) => rc(ExprF::Pi(
                 x.to_label_maybe_alpha(alpha),
                 t.normalize_to_expr_maybe_alpha(alpha),
                 e.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
-            Value::Const(c) => rc(ExprF::Const(*c)),
-            Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
-            Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
-            Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
-            Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
-            Value::EmptyOptionalLit(n) => rc(ExprF::App(
+            ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
+            ValueF::Const(c) => rc(ExprF::Const(*c)),
+            ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)),
+            ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
+            ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
+            ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
+            ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
                 n.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::NEOptionalLit(n) => {
+            ValueF::NEOptionalLit(n) => {
                 rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
             }
-            Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+            ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::List)),
                 n.normalize_to_expr_maybe_alpha(alpha),
             )))),
-            Value::NEListLit(elts) => rc(ExprF::NEListLit(
+            ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
                 elts.iter()
                     .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
                     .collect(),
             )),
-            Value::RecordLit(kvs) => rc(ExprF::RecordLit(
+            ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.iter()
                     .map(|(k, v)| {
                         (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
                     })
                     .collect(),
             )),
-            Value::RecordType(kts) => rc(ExprF::RecordType(
+            ValueF::RecordType(kts) => rc(ExprF::RecordType(
                 kts.iter()
                     .map(|(k, v)| {
                         (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
                     })
                     .collect(),
             )),
-            Value::UnionType(kts) => rc(ExprF::UnionType(
+            ValueF::UnionType(kts) => rc(ExprF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
                         (
@@ -139,7 +139,7 @@ impl Value {
                     })
                     .collect(),
             )),
-            Value::UnionConstructor(l, kts) => {
+            ValueF::UnionConstructor(l, kts) => {
                 let kts = kts
                     .iter()
                     .map(|(k, v)| {
@@ -153,12 +153,12 @@ impl Value {
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
-            Value::UnionLit(l, v, kts) => rc(ExprF::App(
-                Value::UnionConstructor(l.clone(), kts.clone())
+            ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
+                ValueF::UnionConstructor(l.clone(), kts.clone())
                     .normalize_to_expr_maybe_alpha(alpha),
                 v.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::TextLit(elts) => {
+            ValueF::TextLit(elts) => {
                 use InterpolatedTextContents::{Expr, Text};
                 rc(ExprF::TextLit(
                     elts.iter()
@@ -171,12 +171,12 @@ impl Value {
                         .collect(),
                 ))
             }
-            Value::Equivalence(x, y) => rc(ExprF::BinOp(
+            ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
                 dhall_syntax::BinOp::Equivalence,
                 x.normalize_to_expr_maybe_alpha(alpha),
                 y.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::PartialExpr(e) => {
+            ValueF::PartialExpr(e) => {
                 rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
             }
         }
@@ -184,60 +184,60 @@ impl Value {
 
     pub(crate) fn normalize_mut(&mut self) {
         match self {
-            Value::Var(_)
-            | Value::Const(_)
-            | Value::BoolLit(_)
-            | Value::NaturalLit(_)
-            | Value::IntegerLit(_)
-            | Value::DoubleLit(_) => {}
+            ValueF::Var(_)
+            | ValueF::Const(_)
+            | ValueF::BoolLit(_)
+            | ValueF::NaturalLit(_)
+            | ValueF::IntegerLit(_)
+            | ValueF::DoubleLit(_) => {}
 
-            Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => {
+            ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
                 tth.normalize_mut();
             }
 
-            Value::NEOptionalLit(th) => {
+            ValueF::NEOptionalLit(th) => {
                 th.normalize_mut();
             }
-            Value::Lam(_, t, e) => {
+            ValueF::Lam(_, t, e) => {
                 t.normalize_mut();
                 e.normalize_mut();
             }
-            Value::Pi(_, t, e) => {
+            ValueF::Pi(_, t, e) => {
                 t.normalize_mut();
                 e.normalize_mut();
             }
-            Value::AppliedBuiltin(_, args) => {
+            ValueF::AppliedBuiltin(_, args) => {
                 for x in args.iter_mut() {
                     x.normalize_mut();
                 }
             }
-            Value::NEListLit(elts) => {
+            ValueF::NEListLit(elts) => {
                 for x in elts.iter_mut() {
                     x.normalize_mut();
                 }
             }
-            Value::RecordLit(kvs) => {
+            ValueF::RecordLit(kvs) => {
                 for x in kvs.values_mut() {
                     x.normalize_mut();
                 }
             }
-            Value::RecordType(kvs) => {
+            ValueF::RecordType(kvs) => {
                 for x in kvs.values_mut() {
                     x.normalize_mut();
                 }
             }
-            Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
+            ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.normalize_mut();
                 }
             }
-            Value::UnionLit(_, v, kts) => {
+            ValueF::UnionLit(_, v, kts) => {
                 v.normalize_mut();
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.normalize_mut();
                 }
             }
-            Value::TextLit(elts) => {
+            ValueF::TextLit(elts) => {
                 for x in elts.iter_mut() {
                     use InterpolatedTextContents::{Expr, Text};
                     match x {
@@ -246,11 +246,11 @@ impl Value {
                     }
                 }
             }
-            Value::Equivalence(x, y) => {
+            ValueF::Equivalence(x, y) => {
                 x.normalize_mut();
                 y.normalize_mut();
             }
-            Value::PartialExpr(e) => {
+            ValueF::PartialExpr(e) => {
                 // TODO: need map_mut
                 e.map_ref(|v| {
                     v.normalize_nf();
@@ -260,75 +260,75 @@ impl Value {
     }
 
     /// Apply to a value
-    pub(crate) fn app(self, val: Value) -> Value {
+    pub(crate) fn app(self, val: ValueF) -> ValueF {
         self.app_val(val)
     }
 
     /// Apply to a value
-    pub(crate) fn app_val(self, val: Value) -> Value {
+    pub(crate) fn app_val(self, val: ValueF) -> ValueF {
         self.app_thunk(val.into_thunk())
     }
 
     /// Apply to a thunk
-    pub fn app_thunk(self, th: Thunk) -> Value {
-        Thunk::from_value(self).app_thunk(th)
+    pub fn app_thunk(self, th: Thunk) -> ValueF {
+        Thunk::from_valuef(self).app_thunk(th)
     }
 
-    pub fn from_builtin(b: Builtin) -> Value {
-        Value::AppliedBuiltin(b, vec![])
+    pub fn from_builtin(b: Builtin) -> ValueF {
+        ValueF::AppliedBuiltin(b, vec![])
     }
 }
 
-impl Shift for Value {
+impl Shift for ValueF {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
-            Value::Lam(x, t, e) => Value::Lam(
+            ValueF::Lam(x, t, e) => ValueF::Lam(
                 x.clone(),
                 t.shift(delta, var)?,
                 e.shift(delta, &var.under_binder(x))?,
             ),
-            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+            ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin(
                 *b,
                 args.iter()
                     .map(|v| Ok(v.shift(delta, var)?))
                     .collect::<Result<_, _>>()?,
             ),
-            Value::Pi(x, t, e) => Value::Pi(
+            ValueF::Pi(x, t, e) => ValueF::Pi(
                 x.clone(),
                 t.shift(delta, var)?,
                 e.shift(delta, &var.under_binder(x))?,
             ),
-            Value::Var(v) => Value::Var(v.shift(delta, var)?),
-            Value::Const(c) => Value::Const(*c),
-            Value::BoolLit(b) => Value::BoolLit(*b),
-            Value::NaturalLit(n) => Value::NaturalLit(*n),
-            Value::IntegerLit(n) => Value::IntegerLit(*n),
-            Value::DoubleLit(n) => Value::DoubleLit(*n),
-            Value::EmptyOptionalLit(tth) => {
-                Value::EmptyOptionalLit(tth.shift(delta, var)?)
+            ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?),
+            ValueF::Const(c) => ValueF::Const(*c),
+            ValueF::BoolLit(b) => ValueF::BoolLit(*b),
+            ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
+            ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
+            ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
+            ValueF::EmptyOptionalLit(tth) => {
+                ValueF::EmptyOptionalLit(tth.shift(delta, var)?)
             }
-            Value::NEOptionalLit(th) => {
-                Value::NEOptionalLit(th.shift(delta, var)?)
+            ValueF::NEOptionalLit(th) => {
+                ValueF::NEOptionalLit(th.shift(delta, var)?)
             }
-            Value::EmptyListLit(tth) => {
-                Value::EmptyListLit(tth.shift(delta, var)?)
+            ValueF::EmptyListLit(tth) => {
+                ValueF::EmptyListLit(tth.shift(delta, var)?)
             }
-            Value::NEListLit(elts) => Value::NEListLit(
+            ValueF::NEListLit(elts) => ValueF::NEListLit(
                 elts.iter()
                     .map(|v| Ok(v.shift(delta, var)?))
                     .collect::<Result<_, _>>()?,
             ),
-            Value::RecordLit(kvs) => Value::RecordLit(
+            ValueF::RecordLit(kvs) => ValueF::RecordLit(
                 kvs.iter()
                     .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
                     .collect::<Result<_, _>>()?,
             ),
-            Value::RecordType(kvs) => Value::RecordType(
+            ValueF::RecordType(kvs) => ValueF::RecordType(
                 kvs.iter()
                     .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
                     .collect::<Result<_, _>>()?,
             ),
-            Value::UnionType(kts) => Value::UnionType(
+            ValueF::UnionType(kts) => ValueF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
                         Ok((
@@ -340,7 +340,7 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
-            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+            ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor(
                 x.clone(),
                 kts.iter()
                     .map(|(k, v)| {
@@ -353,7 +353,7 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
-            Value::UnionLit(x, v, kts) => Value::UnionLit(
+            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
                 x.clone(),
                 v.shift(delta, var)?,
                 kts.iter()
@@ -367,7 +367,7 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
-            Value::TextLit(elts) => Value::TextLit(
+            ValueF::TextLit(elts) => ValueF::TextLit(
                 elts.iter()
                     .map(|contents| {
                         use InterpolatedTextContents::{Expr, Text};
@@ -378,10 +378,10 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
-            Value::Equivalence(x, y) => {
-                Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+            ValueF::Equivalence(x, y) => {
+                ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
             }
-            Value::PartialExpr(e) => Value::PartialExpr(
+            ValueF::PartialExpr(e) => ValueF::PartialExpr(
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
@@ -391,16 +391,16 @@ impl Shift for Value {
     }
 }
 
-impl Subst<Typed> for Value {
+impl Subst<Typed> for ValueF {
     fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
             // Retry normalizing since substituting may allow progress
-            Value::AppliedBuiltin(b, args) => apply_builtin(
+            ValueF::AppliedBuiltin(b, args) => apply_builtin(
                 *b,
                 args.iter().map(|v| v.subst_shift(var, val)).collect(),
             ),
             // Retry normalizing since substituting may allow progress
-            Value::PartialExpr(e) => {
+            ValueF::PartialExpr(e) => {
                 normalize_one_layer(e.map_ref_with_special_handling_of_binders(
                     |v| v.subst_shift(var, val),
                     |x, v| {
@@ -412,8 +412,8 @@ impl Subst<Typed> for Value {
                 ))
             }
             // Retry normalizing since substituting may allow progress
-            Value::TextLit(elts) => {
-                Value::TextLit(squash_textlit(elts.iter().map(|contents| {
+            ValueF::TextLit(elts) => {
+                ValueF::TextLit(squash_textlit(elts.iter().map(|contents| {
                     use InterpolatedTextContents::{Expr, Text};
                     match contents {
                         Expr(th) => Expr(th.subst_shift(var, val)),
@@ -421,53 +421,53 @@ impl Subst<Typed> for Value {
                     }
                 })))
             }
-            Value::Lam(x, t, e) => Value::Lam(
+            ValueF::Lam(x, t, e) => ValueF::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
                 e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
             ),
-            Value::Pi(x, t, e) => Value::Pi(
+            ValueF::Pi(x, t, e) => ValueF::Pi(
                 x.clone(),
                 t.subst_shift(var, val),
                 e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
             ),
-            Value::Var(v) if v == var => val.to_value(),
-            Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()),
-            Value::Const(c) => Value::Const(*c),
-            Value::BoolLit(b) => Value::BoolLit(*b),
-            Value::NaturalLit(n) => Value::NaturalLit(*n),
-            Value::IntegerLit(n) => Value::IntegerLit(*n),
-            Value::DoubleLit(n) => Value::DoubleLit(*n),
-            Value::EmptyOptionalLit(tth) => {
-                Value::EmptyOptionalLit(tth.subst_shift(var, val))
+            ValueF::Var(v) if v == var => val.to_valuef(),
+            ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
+            ValueF::Const(c) => ValueF::Const(*c),
+            ValueF::BoolLit(b) => ValueF::BoolLit(*b),
+            ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
+            ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
+            ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
+            ValueF::EmptyOptionalLit(tth) => {
+                ValueF::EmptyOptionalLit(tth.subst_shift(var, val))
             }
-            Value::NEOptionalLit(th) => {
-                Value::NEOptionalLit(th.subst_shift(var, val))
+            ValueF::NEOptionalLit(th) => {
+                ValueF::NEOptionalLit(th.subst_shift(var, val))
             }
-            Value::EmptyListLit(tth) => {
-                Value::EmptyListLit(tth.subst_shift(var, val))
+            ValueF::EmptyListLit(tth) => {
+                ValueF::EmptyListLit(tth.subst_shift(var, val))
             }
-            Value::NEListLit(elts) => Value::NEListLit(
+            ValueF::NEListLit(elts) => ValueF::NEListLit(
                 elts.iter().map(|v| v.subst_shift(var, val)).collect(),
             ),
-            Value::RecordLit(kvs) => Value::RecordLit(
+            ValueF::RecordLit(kvs) => ValueF::RecordLit(
                 kvs.iter()
                     .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
                     .collect(),
             ),
-            Value::RecordType(kvs) => Value::RecordType(
+            ValueF::RecordType(kvs) => ValueF::RecordType(
                 kvs.iter()
                     .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
                     .collect(),
             ),
-            Value::UnionType(kts) => Value::UnionType(
+            ValueF::UnionType(kts) => ValueF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
                         (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
                     })
                     .collect(),
             ),
-            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+            ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor(
                 x.clone(),
                 kts.iter()
                     .map(|(k, v)| {
@@ -475,7 +475,7 @@ impl Subst<Typed> for Value {
                     })
                     .collect(),
             ),
-            Value::UnionLit(x, v, kts) => Value::UnionLit(
+            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
                 x.clone(),
                 v.subst_shift(var, val),
                 kts.iter()
@@ -484,7 +484,7 @@ impl Subst<Typed> for Value {
                     })
                     .collect(),
             ),
-            Value::Equivalence(x, y) => Value::Equivalence(
+            ValueF::Equivalence(x, y) => ValueF::Equivalence(
                 x.subst_shift(var, val),
                 y.subst_shift(var, val),
             ),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index becd653..296e968 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -12,7 +12,7 @@ pub struct AlphaVar {
 }
 
 // Exactly like a Label, but equality returns always true.
-// This is so that Value equality is exactly alpha-equivalence.
+// This is so that ValueF equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct AlphaLabel(Label);
 
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index adf749c..7e74f95 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -5,7 +5,7 @@ use std::path::Path;
 use dhall_syntax::{Const, SubExpr};
 
 use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 
@@ -101,8 +101,8 @@ impl Typed {
     pub(crate) fn from_const(c: Const) -> Self {
         Typed(TypedThunk::from_const(c))
     }
-    pub fn from_value_and_type(v: Value, t: Type) -> Self {
-        Typed(TypedThunk::from_value_and_type(v, t))
+    pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
+        Typed(TypedThunk::from_valuef_and_type(v, t))
     }
     pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
         Typed(th)
@@ -111,8 +111,8 @@ impl Typed {
         Typed::from_const(Const::Type)
     }
 
-    pub(crate) fn to_value(&self) -> Value {
-        self.0.to_value()
+    pub(crate) fn to_valuef(&self) -> ValueF {
+        self.0.to_valuef()
     }
     pub fn to_expr(&self) -> NormalizedSubExpr {
         self.0.to_expr()
@@ -229,7 +229,7 @@ impl std::hash::Hash for Normalized {
 impl Eq for Typed {}
 impl PartialEq for Typed {
     fn eq(&self, other: &Self) -> bool {
-        self.to_value() == other.to_value()
+        self.to_valuef() == other.to_valuef()
     }
 }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 02b705d..da54726 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
 };
 
 use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr, Typed};
 
@@ -20,11 +20,11 @@ macro_rules! make_closure {
             Label::from(stringify!($var)).into(),
             $n
         );
-        Value::Var(var).into_thunk()
+        ValueF::Var(var).into_thunk()
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
     (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        Value::Lam(
+        ValueF::Lam(
             Label::from(stringify!($var)).into(),
             TypedThunk::from_thunk_simple_type(
                 make_closure!($($ty)*),
@@ -32,35 +32,35 @@ macro_rules! make_closure {
             make_closure!($($rest)*),
         ).into_thunk()
     };
-    (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() };
+    (Natural) => { ValueF::from_builtin(Builtin::Natural).into_thunk() };
     (List $($rest:tt)*) => {
-        Value::from_builtin(Builtin::List)
+        ValueF::from_builtin(Builtin::List)
             .app_thunk(make_closure!($($rest)*))
             .into_thunk()
     };
     (Some $($rest:tt)*) => {
-        Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+        ValueF::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
     };
     (1 + $($rest:tt)*) => {
-        Value::PartialExpr(ExprF::BinOp(
+        ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
             make_closure!($($rest)*),
-            Thunk::from_value(Value::NaturalLit(1)),
+            Thunk::from_valuef(ValueF::NaturalLit(1)),
         )).into_thunk()
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {
-        Value::PartialExpr(ExprF::BinOp(
+        ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+            ValueF::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
             make_closure!($($tail)*),
         )).into_thunk()
     };
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
     use dhall_syntax::Builtin::*;
-    use Value::*;
+    use ValueF::*;
 
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
@@ -68,23 +68,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             r,
             EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())),
         )),
-        (NaturalIsZero, [n, r..]) => match &*n.as_value() {
+        (NaturalIsZero, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
             _ => Err(()),
         },
-        (NaturalEven, [n, r..]) => match &*n.as_value() {
+        (NaturalEven, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
             _ => Err(()),
         },
-        (NaturalOdd, [n, r..]) => match &*n.as_value() {
+        (NaturalOdd, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
             _ => Err(()),
         },
-        (NaturalToInteger, [n, r..]) => match &*n.as_value() {
+        (NaturalToInteger, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
             _ => Err(()),
         },
-        (NaturalShow, [n, r..]) => match &*n.as_value() {
+        (NaturalShow, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
@@ -92,7 +92,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             _ => Err(()),
         },
         (NaturalSubtract, [a, b, r..]) => {
-            match (&*a.as_value(), &*b.as_value()) {
+            match (&*a.as_valuef(), &*b.as_valuef()) {
                 (NaturalLit(a), NaturalLit(b)) => {
                     Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
                 }
@@ -102,7 +102,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                 _ => Err(()),
             }
         }
-        (IntegerShow, [n, r..]) => match &*n.as_value() {
+        (IntegerShow, [n, r..]) => match &*n.as_valuef() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
@@ -113,18 +113,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Err(()),
         },
-        (IntegerToDouble, [n, r..]) => match &*n.as_value() {
+        (IntegerToDouble, [n, r..]) => match &*n.as_valuef() {
             IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
             _ => Err(()),
         },
-        (DoubleShow, [n, r..]) => match &*n.as_value() {
+        (DoubleShow, [n, r..]) => match &*n.as_valuef() {
             DoubleLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
             )),
             _ => Err(()),
         },
-        (TextShow, [v, r..]) => match &*v.as_value() {
+        (TextShow, [v, r..]) => match &*v.as_valuef() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -158,41 +158,41 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Err(()),
         },
-        (ListLength, [_, l, r..]) => match &*l.as_value() {
+        (ListLength, [_, l, r..]) => match &*l.as_valuef() {
             EmptyListLit(_) => Ok((r, NaturalLit(0))),
             NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
             _ => Err(()),
         },
-        (ListHead, [_, l, r..]) => match &*l.as_value() {
+        (ListHead, [_, l, r..]) => match &*l.as_valuef() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListLast, [_, l, r..]) => match &*l.as_value() {
+        (ListLast, [_, l, r..]) => match &*l.as_valuef() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListReverse, [_, l, r..]) => match &*l.as_value() {
+        (ListReverse, [_, l, r..]) => match &*l.as_valuef() {
             EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
             }
             _ => Err(()),
         },
-        (ListIndexed, [_, l, r..]) => match &*l.as_value() {
+        (ListIndexed, [_, l, r..]) => match &*l.as_valuef() {
             EmptyListLit(t) => {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypedThunk::from_value(Value::from_builtin(Natural)),
+                    TypedThunk::from_valuef(ValueF::from_builtin(Natural)),
                 );
                 kts.insert("value".into(), t.clone());
-                Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts)))))
+                Ok((r, EmptyListLit(TypedThunk::from_valuef(RecordType(kts)))))
             }
             NEListLit(xs) => {
                 let xs = xs
@@ -201,20 +201,20 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = HashMap::new();
-                        kvs.insert("index".into(), Thunk::from_value(i));
+                        kvs.insert("index".into(), Thunk::from_valuef(i));
                         kvs.insert("value".into(), e.clone());
-                        Thunk::from_value(RecordLit(kvs))
+                        Thunk::from_valuef(RecordLit(kvs))
                     })
                     .collect();
                 Ok((r, NEListLit(xs)))
             }
             _ => Err(()),
         },
-        (ListBuild, [t, f, r..]) => match &*f.as_value() {
+        (ListBuild, [t, f, r..]) => match &*f.as_valuef() {
             // fold/build fusion
-            Value::AppliedBuiltin(ListFold, args) => {
+            ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_value()))
+                    Ok((r, args[1].to_valuef()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -222,7 +222,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Ok((
                 r,
-                f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
+                f.app_val(ValueF::from_builtin(List).app_thunk(t.clone()))
                     .app_thunk({
                         // Move `t` under new `x` variable
                         let t1 = t.under_binder(Label::from("x"));
@@ -237,8 +237,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                     ))),
             )),
         },
-        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
-            EmptyListLit(_) => Ok((r, nil.to_value())),
+        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() {
+            EmptyListLit(_) => Ok((r, nil.to_valuef())),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().rev() {
@@ -248,15 +248,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                         .app_thunk(v)
                         .into_thunk();
                 }
-                Ok((r, v.to_value()))
+                Ok((r, v.to_valuef()))
             }
             _ => Err(()),
         },
-        (OptionalBuild, [t, f, r..]) => match &*f.as_value() {
+        (OptionalBuild, [t, f, r..]) => match &*f.as_valuef() {
             // fold/build fusion
-            Value::AppliedBuiltin(OptionalFold, args) => {
+            ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_value()))
+                    Ok((r, args[1].to_valuef()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -264,23 +264,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Ok((
                 r,
-                f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
+                f.app_val(ValueF::from_builtin(Optional).app_thunk(t.clone()))
                     .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
                     .app_val(EmptyOptionalLit(
                         TypedThunk::from_thunk_simple_type(t.clone()),
                     )),
             )),
         },
-        (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
-            EmptyOptionalLit(_) => Ok((r, nothing.to_value())),
-            NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
-            _ => Err(()),
-        },
-        (NaturalBuild, [f, r..]) => match &*f.as_value() {
+        (OptionalFold, [_, v, _, just, nothing, r..]) => {
+            match &*v.as_valuef() {
+                EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())),
+                NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+                _ => Err(()),
+            }
+        }
+        (NaturalBuild, [f, r..]) => match &*f.as_valuef() {
             // fold/build fusion
-            Value::AppliedBuiltin(NaturalFold, args) => {
+            ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].to_value()))
+                    Ok((r, args[0].to_valuef()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -288,15 +290,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Ok((
                 r,
-                f.app_val(Value::from_builtin(Natural))
+                f.app_val(ValueF::from_builtin(Natural))
                     .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
                     .app_val(NaturalLit(0)),
             )),
         },
-        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() {
-            NaturalLit(0) => Ok((r, zero.to_value())),
+        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() {
+            NaturalLit(0) => Ok((r, zero.to_valuef())),
             NaturalLit(n) => {
-                let fold = Value::from_builtin(NaturalFold)
+                let fold = ValueF::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
                     .app_thunk(t.clone())
                     .app_thunk(succ.clone())
@@ -319,22 +321,22 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
     }
 }
 
-pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value {
-    let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF {
+    let fallback = |f: Thunk, a: Thunk| ValueF::PartialExpr(ExprF::App(f, a));
 
-    let f_borrow = f.as_value();
+    let f_borrow = f.as_valuef();
     match &*f_borrow {
-        Value::Lam(x, _, e) => {
+        ValueF::Lam(x, _, e) => {
             let val = Typed::from_thunk_untyped(a);
-            e.subst_shift(&x.into(), &val).to_value()
+            e.subst_shift(&x.into(), &val).to_valuef()
         }
-        Value::AppliedBuiltin(b, args) => {
+        ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args)
         }
-        Value::UnionConstructor(l, kts) => {
-            Value::UnionLit(l.clone(), a, kts.clone())
+        ValueF::UnionConstructor(l, kts) => {
+            ValueF::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
@@ -358,9 +360,9 @@ pub(crate) fn squash_textlit(
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => {
-                    let e_borrow = e.as_value();
+                    let e_borrow = e.as_valuef();
                     match &*e_borrow {
-                        Value::TextLit(elts2) => {
+                        ValueF::TextLit(elts2) => {
                             inner(elts2.iter().cloned(), crnt_str, ret)
                         }
                         _ => {
@@ -387,7 +389,7 @@ pub(crate) fn squash_textlit(
 
 // Small helper enum to avoid repetition
 enum Ret<'a> {
-    Value(Value),
+    ValueF(ValueF),
     Thunk(Thunk),
     ThunkRef(&'a Thunk),
     Expr(ExprF<Thunk, Normalized>),
@@ -512,67 +514,67 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use Value::{
+    use ValueF::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
     };
-    let x_borrow = x.as_value();
-    let y_borrow = y.as_value();
+    let x_borrow = x.as_valuef();
+    let y_borrow = y.as_valuef();
     Some(match (o, &*x_borrow, &*y_borrow) {
         (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
         (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
-        (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)),
+        (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
+        (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
         (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
-        (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)),
+        (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
+        (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
         (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
         (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
         (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
         (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
         (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)),
+        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)),
+        (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
         (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
         (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)),
+        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
+        (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
 
         (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
         (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
         (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::Value(NaturalLit(x + y))
+            Ret::ValueF(NaturalLit(x + y))
         }
-        (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)),
+        (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
+        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
         (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
         (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
         (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::Value(NaturalLit(x * y))
+            Ret::ValueF(NaturalLit(x * y))
         }
 
         (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
         (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => {
-            Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
-        }
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
+            xs.iter().chain(ys.iter()).cloned().collect(),
+        )),
 
         (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
         (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
-        (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit(
+        (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
             squash_textlit(x.iter().chain(y.iter()).cloned()),
         )),
         (TextAppend, TextLit(x), _) => {
             use std::iter::once;
             let y = InterpolatedTextContents::Expr(y.clone());
-            Ret::Value(TextLit(squash_textlit(
+            Ret::ValueF(TextLit(squash_textlit(
                 x.iter().cloned().chain(once(y)),
             )))
         }
         (TextAppend, _, TextLit(y)) => {
             use std::iter::once;
             let x = InterpolatedTextContents::Expr(x.clone());
-            Ret::Value(TextLit(squash_textlit(
+            Ret::ValueF(TextLit(squash_textlit(
                 once(x).chain(y.iter().cloned()),
             )))
         }
@@ -589,7 +591,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            Ret::Value(RecordLit(kvs))
+            Ret::ValueF(RecordLit(kvs))
         }
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
@@ -606,7 +608,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                     v2.clone(),
                 ))
             });
-            Ret::Value(RecordLit(kvs))
+            Ret::ValueF(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
@@ -625,10 +627,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                     ),
                 ))
             });
-            Ret::Value(RecordType(kvs))
+            Ret::ValueF(RecordType(kvs))
         }
 
-        (Equivalence, _, _) => Ret::Value(Value::Equivalence(
+        (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence(
             TypedThunk::from_thunk_simple_type(x.clone()),
             TypedThunk::from_thunk_simple_type(y.clone()),
         )),
@@ -637,8 +639,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
-    use Value::{
+pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
+    use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
         TextLit, UnionConstructor, UnionLit, UnionType,
@@ -653,9 +655,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         ExprF::Annot(x, _) => Ret::Thunk(x),
         ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
-            Ret::Value(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e))
+            Ret::ValueF(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e))
         }
-        ExprF::Pi(x, t, e) => Ret::Value(Pi(
+        ExprF::Pi(x, t, e) => Ret::ValueF(Pi(
             x.into(),
             TypedThunk::from_thunk_untyped(t),
             TypedThunk::from_thunk_untyped(e),
@@ -664,20 +666,20 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             let v = Typed::from_thunk_untyped(v);
             Ret::Thunk(b.subst_shift(&x.into(), &v))
         }
-        ExprF::App(v, a) => Ret::Value(v.app_thunk(a)),
-        ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)),
-        ExprF::Const(c) => Ret::Value(Value::Const(c)),
-        ExprF::BoolLit(b) => Ret::Value(BoolLit(b)),
-        ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
-        ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
-        ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
-        ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
+        ExprF::App(v, a) => Ret::ValueF(v.app_thunk(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)),
+        ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
+        ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
         ExprF::EmptyListLit(ref t) => {
             // Check if the type is of the form `List x`
-            let t_borrow = t.as_value();
+            let t_borrow = t.as_valuef();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::Value(EmptyListLit(
+                    Ret::ValueF(EmptyListLit(
                         TypedThunk::from_thunk_simple_type(args[0].clone()),
                     ))
                 }
@@ -688,17 +690,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             }
         }
         ExprF::NEListLit(elts) => {
-            Ret::Value(NEListLit(elts.into_iter().collect()))
+            Ret::ValueF(NEListLit(elts.into_iter().collect()))
         }
         ExprF::RecordLit(kvs) => {
-            Ret::Value(RecordLit(kvs.into_iter().collect()))
+            Ret::ValueF(RecordLit(kvs.into_iter().collect()))
         }
-        ExprF::RecordType(kts) => Ret::Value(RecordType(
+        ExprF::RecordType(kts) => Ret::ValueF(RecordType(
             kts.into_iter()
                 .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t)))
                 .collect(),
         )),
-        ExprF::UnionType(kts) => Ret::Value(UnionType(
+        ExprF::UnionType(kts) => Ret::ValueF(UnionType(
             kts.into_iter()
                 .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t))))
                 .collect(),
@@ -710,17 +712,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             if let [Expr(th)] = elts.as_slice() {
                 Ret::Thunk(th.clone())
             } else {
-                Ret::Value(TextLit(elts))
+                Ret::ValueF(TextLit(elts))
             }
         }
         ExprF::BoolIf(ref b, ref e1, ref e2) => {
-            let b_borrow = b.as_value();
+            let b_borrow = b.as_valuef();
             match &*b_borrow {
                 BoolLit(true) => Ret::ThunkRef(e1),
                 BoolLit(false) => Ret::ThunkRef(e2),
                 _ => {
-                    let e1_borrow = e1.as_value();
-                    let e2_borrow = e2.as_value();
+                    let e1_borrow = e1.as_valuef();
+                    let e2_borrow = e2.as_valuef();
                     match (&*e1_borrow, &*e2_borrow) {
                         // Simplify `if b then True else False`
                         (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
@@ -741,12 +743,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         },
 
         ExprF::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::Value(RecordLit(HashMap::new()))
+            Ret::ValueF(RecordLit(HashMap::new()))
         }
         ExprF::Projection(ref v, ref ls) => {
-            let v_borrow = v.as_value();
+            let v_borrow = v.as_valuef();
             match &*v_borrow {
-                RecordLit(kvs) => Ret::Value(RecordLit(
+                RecordLit(kvs) => Ret::ValueF(RecordLit(
                     ls.iter()
                         .filter_map(|l| {
                             kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -760,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             }
         }
         ExprF::Field(ref v, ref l) => {
-            let v_borrow = v.as_value();
+            let v_borrow = v.as_valuef();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
                     Some(r) => Ret::Thunk(r.clone()),
@@ -770,7 +772,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
                     }
                 },
                 UnionType(kts) => {
-                    Ret::Value(UnionConstructor(l.clone(), kts.clone()))
+                    Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
                 }
                 _ => {
                     drop(v_borrow);
@@ -780,8 +782,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         }
 
         ExprF::Merge(ref handlers, ref variant, _) => {
-            let handlers_borrow = handlers.as_value();
-            let variant_borrow = variant.as_value();
+            let handlers_borrow = handlers.as_valuef();
+            let variant_borrow = variant.as_valuef();
             match (&*handlers_borrow, &*variant_borrow) {
                 (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
                     Some(h) => Ret::Thunk(h.clone()),
@@ -792,7 +794,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::Value(h.app_thunk(v.clone())),
+                    Some(h) => Ret::ValueF(h.app_thunk(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -809,9 +811,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
     };
 
     match ret {
-        Ret::Value(v) => v,
-        Ret::Thunk(th) => th.to_value(),
-        Ret::ThunkRef(th) => th.to_value(),
-        Ret::Expr(expr) => Value::PartialExpr(expr),
+        Ret::ValueF(v) => v,
+        Ret::Thunk(th) => th.to_valuef(),
+        Ret::ThunkRef(th) => th.to_valuef(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index dd6da70..8d7a3bc 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
 
 use crate::core::context::TypecheckContext;
 use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::{Normalized, Resolved, Type, Typed};
@@ -43,7 +43,7 @@ fn tck_pi_type(
     let k = function_check(ka, kb);
 
     Ok(Typed::from_thunk_and_type(
-        Value::Pi(
+        ValueF::Pi(
             x.into(),
             TypedThunk::from_type(tx),
             TypedThunk::from_type(te),
@@ -88,7 +88,7 @@ fn tck_record_type(
     let k = k.unwrap_or(dhall_syntax::Const::Type);
 
     Ok(Typed::from_thunk_and_type(
-        Value::RecordType(new_kts).into_thunk(),
+        ValueF::RecordType(new_kts).into_thunk(),
         Type::from_const(k),
     ))
 }
@@ -132,7 +132,7 @@ fn tck_union_type(
     let k = k.unwrap_or(dhall_syntax::Const::Type);
 
     Ok(Typed::from_thunk_and_type(
-        Value::UnionType(new_kts).into_thunk(),
+        ValueF::UnionType(new_kts).into_thunk(),
         Type::from_const(k),
     ))
 }
@@ -335,14 +335,14 @@ fn type_with(
             let tx = mktype(ctx, t.clone())?;
             let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
-            let v = Value::Lam(
+            let v = ValueF::Lam(
                 x.clone().into(),
                 TypedThunk::from_type(tx.clone()),
                 b.to_thunk(),
             );
             let tb = b.get_type()?.into_owned();
             let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type();
-            Typed::from_thunk_and_type(Thunk::from_value(v), t)
+            Typed::from_thunk_and_type(Thunk::from_valuef(v), t)
         }
         Pi(x, ta, tb) => {
             let ta = mktype(ctx, ta.clone())?;
@@ -415,8 +415,10 @@ fn type_last_layer(
         }
         App(f, a) => {
             let tf = f.get_type()?;
-            let (x, tx, tb) = match &tf.to_value() {
-                Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()),
+            let (x, tx, tb) = match &tf.to_valuef() {
+                ValueF::Pi(x, tx, tb) => {
+                    (x.clone(), tx.to_type(), tb.to_type())
+                }
                 _ => return Err(mkerr(NotAFunction(f.clone()))),
             };
             if a.get_type()?.as_ref() != &tx {
@@ -437,9 +439,9 @@ fn type_last_layer(
             Ok(RetTypeOnly(x.get_type()?.into_owned()))
         }
         Assert(t) => {
-            match t.to_value() {
-                Value::Equivalence(ref x, ref y) if x == y => {}
-                Value::Equivalence(x, y) => {
+            match t.to_valuef() {
+                ValueF::Equivalence(ref x, ref y) if x == y => {}
+                ValueF::Equivalence(x, y) => {
                     return Err(mkerr(AssertMismatch(
                         x.to_typed(),
                         y.to_typed(),
@@ -470,8 +472,8 @@ fn type_last_layer(
         }
         EmptyListLit(t) => {
             let t = t.to_type();
-            match &t.to_value() {
-                Value::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+            match &t.to_valuef() {
+                ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args)
                     if args.len() == 1 => {}
                 _ => {
                     return Err(TypeError::new(
@@ -504,8 +506,8 @@ fn type_last_layer(
 
             Ok(RetTypeOnly(
                 Typed::from_thunk_and_type(
-                    Value::from_builtin(dhall_syntax::Builtin::List)
-                        .app(t.to_value())
+                    ValueF::from_builtin(dhall_syntax::Builtin::List)
+                        .app(t.to_valuef())
                         .into_thunk(),
                     Typed::from_const(Type),
                 )
@@ -523,8 +525,8 @@ fn type_last_layer(
 
             Ok(RetTypeOnly(
                 Typed::from_thunk_and_type(
-                    Value::from_builtin(dhall_syntax::Builtin::Optional)
-                        .app(t.to_value())
+                    ValueF::from_builtin(dhall_syntax::Builtin::Optional)
+                        .app(t.to_valuef())
                         .into_thunk(),
                     Typed::from_const(Type).into_type(),
                 )
@@ -549,8 +551,8 @@ fn type_last_layer(
             .into_type(),
         )),
         Field(r, x) => {
-            match &r.get_type()?.to_value() {
-                Value::RecordType(kts) => match kts.get(&x) {
+            match &r.get_type()?.to_valuef() {
+                ValueF::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => {
                         Ok(RetTypeOnly(tth.to_type()))
                     },
@@ -560,8 +562,8 @@ fn type_last_layer(
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
                     let r = r.to_type();
-                    match &r.to_value() {
-                        Value::UnionType(kts) => match kts.get(&x) {
+                    match &r.to_valuef() {
+                        ValueF::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(t)) => {
                                 Ok(RetTypeOnly(
@@ -631,14 +633,14 @@ fn type_last_layer(
             }
 
             // Extract the LHS record type
-            let kts_x = match l_type.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_x = match l_type.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(l.clone()))),
             };
 
             // Extract the RHS record type
-            let kts_y = match r_type.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_y = match r_type.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(r.clone()))),
             };
 
@@ -672,10 +674,10 @@ fn type_last_layer(
                                inner_l: &TypedThunk,
                                inner_r: &TypedThunk|
                  -> Result<Typed, TypeError> {
-                    match (inner_l.to_value(), inner_r.to_value()) {
+                    match (inner_l.to_valuef(), inner_r.to_valuef()) {
                         (
-                            Value::RecordType(inner_l_kvs),
-                            Value::RecordType(inner_r_kvs),
+                            ValueF::RecordType(inner_l_kvs),
+                            ValueF::RecordType(inner_r_kvs),
                         ) => {
                             combine_record_types(ctx, inner_l_kvs, inner_r_kvs)
                         }
@@ -715,14 +717,14 @@ fn type_last_layer(
             }
 
             // Extract the LHS record type
-            let kts_x = match l_type.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_x = match l_type.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(l.clone()))),
             };
 
             // Extract the RHS record type
-            let kts_y = match r_type.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_y = match r_type.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(r.clone()))),
             };
 
@@ -745,10 +747,10 @@ fn type_last_layer(
                                kts_l_inner: &TypedThunk,
                                kts_r_inner: &TypedThunk|
                  -> Result<Typed, TypeError> {
-                    match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
+                    match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) {
                         (
-                            Value::RecordType(kvs_l_inner),
-                            Value::RecordType(kvs_r_inner),
+                            ValueF::RecordType(kvs_l_inner),
+                            ValueF::RecordType(kvs_r_inner),
                         ) => {
                             combine_record_types(ctx, kvs_l_inner, kvs_r_inner)
                         }
@@ -774,8 +776,8 @@ fn type_last_layer(
             };
 
             // Extract the Const of the LHS
-            let k_l = match l.get_type()?.to_value() {
-                Value::Const(k) => k,
+            let k_l = match l.get_type()?.to_valuef() {
+                ValueF::Const(k) => k,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         l.clone(),
@@ -784,8 +786,8 @@ fn type_last_layer(
             };
 
             // Extract the Const of the RHS
-            let k_r = match r.get_type()?.to_value() {
-                Value::Const(k) => k,
+            let k_r = match r.get_type()?.to_valuef() {
+                ValueF::Const(k) => k,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         r.clone(),
@@ -806,8 +808,8 @@ fn type_last_layer(
             };
 
             // Extract the LHS record type
-            let kts_x = match l.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_x = match l.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         l.clone(),
@@ -816,8 +818,8 @@ fn type_last_layer(
             };
 
             // Extract the RHS record type
-            let kts_y = match r.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts_y = match r.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         r.clone(),
@@ -831,8 +833,8 @@ fn type_last_layer(
                 .and(Ok(RetTypeOnly(Typed::from_const(k))))
         }
         BinOp(o @ ListAppend, l, r) => {
-            match l.get_type()?.to_value() {
-                Value::AppliedBuiltin(List, _) => {}
+            match l.get_type()?.to_valuef() {
+                ValueF::AppliedBuiltin(List, _) => {}
                 _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
             }
 
@@ -893,13 +895,13 @@ fn type_last_layer(
             Ok(RetTypeOnly(t))
         }
         Merge(record, union, type_annot) => {
-            let handlers = match record.get_type()?.to_value() {
-                Value::RecordType(kts) => kts,
+            let handlers = match record.get_type()?.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))),
             };
 
-            let variants = match union.get_type()?.to_value() {
-                Value::UnionType(kts) => kts,
+            let variants = match union.get_type()?.to_valuef() {
+                ValueF::UnionType(kts) => kts,
                 _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))),
             };
 
@@ -910,8 +912,8 @@ fn type_last_layer(
                     Some(Some(variant_type)) => {
                         let variant_type = variant_type.to_type();
                         let handler_type = handler.to_type();
-                        let (x, tx, tb) = match &handler_type.to_value() {
-                            Value::Pi(x, tx, tb) => {
+                        let (x, tx, tb) = match &handler_type.to_valuef() {
+                            ValueF::Pi(x, tx, tb) => {
                                 (x.clone(), tx.to_type(), tb.to_type())
                             }
                             _ => return Err(mkerr(NotAFunction(handler_type))),
@@ -973,8 +975,8 @@ fn type_last_layer(
         }
         Projection(record, labels) => {
             let trecord = record.get_type()?;
-            let kts = match trecord.to_value() {
-                Value::RecordType(kts) => kts,
+            let kts = match trecord.to_valuef() {
+                ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(ProjectionMustBeRecord)),
             };
 
@@ -988,7 +990,7 @@ fn type_last_layer(
 
             Ok(RetTypeOnly(
                 Typed::from_thunk_and_type(
-                    Value::RecordType(new_kts).into_thunk(),
+                    ValueF::RecordType(new_kts).into_thunk(),
                     trecord.get_type()?.into_owned(),
                 )
                 .to_type(),