8 files changed, 927 insertions, 925 deletions

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index b1fbde9..e1a23a9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,8 +3,8 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::thunk::Thunk;
-use crate::core::value::ValueF;
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 use crate::phase::{Type, Typed};
@@ -12,7 +12,7 @@ use crate::phase::{Type, Typed};
 #[derive(Debug, Clone)]
 enum CtxItem {
     Kept(AlphaVar, Type),
-    Replaced(Thunk, Type),
+    Replaced(Value, Type),
 }
 
 #[derive(Debug, Clone)]
@@ -31,7 +31,7 @@ impl TypecheckContext {
         let mut vec = self.0.as_ref().clone();
         vec.push((
             x.clone(),
-            CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()),
+            CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
         ));
         Ok(TypecheckContext(Rc::new(vec)))
     }
@@ -44,11 +44,11 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     let (th, t) = match i {
                         CtxItem::Kept(newvar, t) => {
-                            (ValueF::Var(newvar).into_thunk(), t)
+                            (ValueF::Var(newvar).into_value(), t)
                         }
                         CtxItem::Replaced(th, t) => (th, t),
                     };
-                    return Some(Typed::from_thunk_and_type(th, t));
+                    return Some(Typed::from_value_and_type(th, t));
                 }
                 Some(newvar) => var = newvar,
             };
@@ -133,7 +133,7 @@ impl Subst<Typed> for CtxItem {
             ),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
                 None => {
-                    CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val))
+                    CtxItem::Replaced(val.to_value(), t.subst_shift(var, val))
                 }
                 Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
             },
diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs
index 0667df8..08213f7 100644
--- a/dhall/src/core/mod.rs
+++ b/dhall/src/core/mod.rs
@@ -1,4 +1,4 @@
 pub mod context;
-pub mod thunk;
 pub mod value;
+pub mod valuef;
 pub mod var;
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
deleted file mode 100644
index 325a410..0000000
--- a/dhall/src/core/thunk.rs
+++ /dev/null
@@ -1,406 +0,0 @@
-use std::borrow::Cow;
-use std::cell::{Ref, RefCell, RefMut};
-use std::rc::Rc;
-
-use dhall_syntax::{Const, ExprF};
-
-use crate::core::context::TypecheckContext;
-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};
-use crate::phase::typecheck::type_of_const;
-use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
-
-#[derive(Debug, Clone, Copy)]
-enum Marker {
-    /// Weak Head Normal Form, i.e. subexpressions may not be normalized
-    WHNF,
-    /// Normal form, i.e. completely normalized
-    NF,
-}
-use Marker::{NF, WHNF};
-
-#[derive(Debug, Clone)]
-enum ThunkInternal {
-    /// Partially normalized value whose subexpressions have been thunked (this is returned from
-    /// 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
-    ValueF(Marker, ValueF),
-}
-
-#[derive(Debug)]
-struct TypedThunkInternal {
-    internal: ThunkInternal,
-    typ: Option<Type>,
-}
-
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
-/// sharing computation automatically. Uses a RefCell to share computation.
-/// Can optionally store a Type from the typechecking phase to preserve type information through
-/// the normalization phase.
-#[derive(Clone)]
-pub struct Thunk(Rc<RefCell<TypedThunkInternal>>);
-
-#[derive(Debug, Clone)]
-pub struct TypedThunk(Thunk);
-
-impl ThunkInternal {
-    fn into_thunk(self, t: Option<Type>) -> Thunk {
-        TypedThunkInternal {
-            internal: self,
-            typ: t,
-        }
-        .into_thunk()
-    }
-
-    fn normalize_whnf(&mut self) {
-        match self {
-            ThunkInternal::PartialExpr(e) => {
-                *self =
-                    ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
-            }
-            // Already at least in WHNF
-            ThunkInternal::ValueF(_, _) => {}
-        }
-    }
-
-    fn normalize_nf(&mut self) {
-        match self {
-            ThunkInternal::PartialExpr(_) => {
-                self.normalize_whnf();
-                self.normalize_nf();
-            }
-            ThunkInternal::ValueF(m @ WHNF, v) => {
-                v.normalize_mut();
-                *m = NF;
-            }
-            // Already in NF
-            ThunkInternal::ValueF(NF, _) => {}
-        }
-    }
-
-    // Always use normalize_whnf before
-    fn as_whnf(&self) -> &ValueF {
-        match self {
-            ThunkInternal::PartialExpr(_) => unreachable!(),
-            ThunkInternal::ValueF(_, v) => v,
-        }
-    }
-
-    // Always use normalize_nf before
-    fn as_nf(&self) -> &ValueF {
-        match self {
-            ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
-                unreachable!()
-            }
-            ThunkInternal::ValueF(NF, v) => v,
-        }
-    }
-}
-
-impl TypedThunkInternal {
-    fn into_thunk(self) -> Thunk {
-        Thunk(Rc::new(RefCell::new(self)))
-    }
-    fn as_internal(&self) -> &ThunkInternal {
-        &self.internal
-    }
-    fn as_internal_mut(&mut self) -> &mut ThunkInternal {
-        &mut self.internal
-    }
-
-    fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.typ {
-            Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
-        }
-    }
-}
-
-impl Thunk {
-    pub(crate) fn from_valuef(v: ValueF) -> Thunk {
-        ThunkInternal::ValueF(WHNF, v).into_thunk(None)
-    }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk {
-        ThunkInternal::ValueF(WHNF, v).into_thunk(Some(t))
-    }
-    pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
-        ThunkInternal::PartialExpr(e).into_thunk(None)
-    }
-    pub(crate) fn with_type(self, t: Type) -> Thunk {
-        self.as_internal().clone().into_thunk(Some(t))
-    }
-
-    /// Mutates the contents. If no one else shares this thunk,
-    /// mutates directly, thus avoiding a RefCell lock.
-    fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedThunkInternal)) {
-        match Rc::get_mut(&mut self.0) {
-            // Mutate directly if sole owner
-            Some(refcell) => f(RefCell::get_mut(refcell)),
-            // Otherwise mutate through the refcell
-            None => f(&mut self.as_tinternal_mut()),
-        }
-    }
-
-    /// Normalizes contents to normal form; faster than `normalize_nf` if
-    /// no one else shares this thunk
-    pub(crate) fn normalize_mut(&mut self) {
-        self.mutate_internal(|i| i.as_internal_mut().normalize_nf())
-    }
-
-    fn as_tinternal(&self) -> Ref<TypedThunkInternal> {
-        self.0.borrow()
-    }
-    fn as_tinternal_mut(&mut self) -> RefMut<TypedThunkInternal> {
-        self.0.borrow_mut()
-    }
-    fn as_internal(&self) -> Ref<ThunkInternal> {
-        Ref::map(self.as_tinternal(), TypedThunkInternal::as_internal)
-    }
-    fn as_internal_mut(&self) -> RefMut<ThunkInternal> {
-        RefMut::map(self.0.borrow_mut(), TypedThunkInternal::as_internal_mut)
-    }
-
-    fn do_normalize_whnf(&self) {
-        let borrow = self.as_internal();
-        match &*borrow {
-            ThunkInternal::PartialExpr(_) => {
-                drop(borrow);
-                self.as_internal_mut().normalize_whnf();
-            }
-            // Already at least in WHNF
-            ThunkInternal::ValueF(_, _) => {}
-        }
-    }
-
-    fn do_normalize_nf(&self) {
-        let borrow = self.as_internal();
-        match &*borrow {
-            ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
-                drop(borrow);
-                self.as_internal_mut().normalize_nf();
-            }
-            // Already in 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<ValueF> {
-        self.do_normalize_nf();
-        Ref::map(self.as_internal(), 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_valuef(&self) -> Ref<ValueF> {
-        self.do_normalize_whnf();
-        Ref::map(self.as_internal(), ThunkInternal::as_whnf)
-    }
-
-    pub(crate) fn to_valuef(&self) -> ValueF {
-        self.as_valuef().clone()
-    }
-
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
-    }
-
-    pub(crate) fn app_val(&self, val: ValueF) -> ValueF {
-        self.app_thunk(val.into_thunk())
-    }
-
-    pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF {
-        apply_any(self.clone(), th)
-    }
-
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
-        Ok(Cow::Owned(self.as_tinternal().get_type()?))
-    }
-}
-
-impl TypedThunk {
-    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) -> ValueF {
-        self.0.normalize_nf().clone()
-    }
-
-    pub(crate) fn to_typed(&self) -> Typed {
-        self.clone().into_typed()
-    }
-
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
-    }
-
-    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
-        TypedThunk(th.with_type(t))
-    }
-    pub fn from_thunk_simple_type(th: Thunk) -> Self {
-        TypedThunk::from_thunk_and_type(th, Type::const_type())
-    }
-    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
-        TypedThunk(th)
-    }
-    pub(crate) fn from_const(c: Const) -> Self {
-        match type_of_const(c) {
-            Ok(t) => TypedThunk::from_valuef_and_type(ValueF::Const(c), t),
-            Err(_) => TypedThunk::from_valuef(ValueF::Const(c)),
-        }
-    }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
-        TypedThunk(Thunk::from_valuef_and_type(v, t))
-    }
-
-    pub(crate) fn to_valuef(&self) -> ValueF {
-        self.0.to_valuef()
-    }
-    pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
-        self.to_valuef().normalize_to_expr()
-    }
-    pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
-        self.to_valuef().normalize_to_expr_maybe_alpha(true)
-    }
-    pub(crate) fn to_thunk(&self) -> Thunk {
-        self.0.clone()
-    }
-    pub(crate) fn to_type(&self) -> Type {
-        self.clone().into_typed().into_type()
-    }
-    pub(crate) fn into_typed(self) -> Typed {
-        Typed::from_typethunk(self)
-    }
-    pub(crate) fn as_const(&self) -> Option<Const> {
-        // TODO: avoid clone
-        match &self.to_valuef() {
-            ValueF::Const(c) => Some(*c),
-            _ => None,
-        }
-    }
-
-    pub(crate) fn normalize_mut(&mut self) {
-        self.0.normalize_mut()
-    }
-
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
-        self.0.get_type()
-    }
-}
-
-impl Shift for Thunk {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Thunk(self.0.shift(delta, var)?))
-    }
-}
-
-impl Shift for ThunkInternal {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(match self {
-            ThunkInternal::PartialExpr(e) => {
-                ThunkInternal::PartialExpr(e.shift(delta, var)?)
-            }
-            ThunkInternal::ValueF(m, v) => {
-                ThunkInternal::ValueF(*m, v.shift(delta, var)?)
-            }
-        })
-    }
-}
-
-impl Shift for TypedThunk {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(TypedThunk(self.0.shift(delta, var)?))
-    }
-}
-
-impl Shift for TypedThunkInternal {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(TypedThunkInternal {
-            internal: self.internal.shift(delta, var)?,
-            typ: self.typ.shift(delta, var)?,
-        })
-    }
-}
-
-impl Subst<Typed> for Thunk {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        Thunk(self.0.subst_shift(var, val))
-    }
-}
-
-impl Subst<Typed> for ThunkInternal {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        match self {
-            ThunkInternal::PartialExpr(e) => {
-                ThunkInternal::PartialExpr(e.subst_shift(var, val))
-            }
-            ThunkInternal::ValueF(_, v) => {
-                // The resulting value may not stay in normal form after substitution
-                ThunkInternal::ValueF(WHNF, v.subst_shift(var, val))
-            }
-        }
-    }
-}
-
-impl Subst<Typed> for TypedThunkInternal {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        TypedThunkInternal {
-            internal: self.internal.subst_shift(var, val),
-            typ: self.typ.subst_shift(var, val),
-        }
-    }
-}
-
-impl Subst<Typed> for TypedThunk {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        TypedThunk(self.0.subst_shift(var, val))
-    }
-}
-
-impl std::cmp::PartialEq for Thunk {
-    fn eq(&self, other: &Self) -> bool {
-        *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_valuef() == other.to_valuef()
-    }
-}
-impl std::cmp::Eq for TypedThunk {}
-
-impl std::fmt::Debug for Thunk {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let b: &ThunkInternal = &self.as_internal();
-        match b {
-            ThunkInternal::ValueF(m, v) => {
-                f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish()
-            }
-            ThunkInternal::PartialExpr(e) => {
-                f.debug_tuple("Thunk@PartialExpr").field(e).finish()
-            }
-        }
-    }
-}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index da70118..5c29bf0 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,405 +1,406 @@
-use std::collections::HashMap;
-
-use dhall_syntax::{
-    rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural,
-};
-
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::{
-    apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
-};
-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 `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 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 ValueF {
-    /// Closures
-    Lam(AlphaLabel, TypedThunk, Thunk),
-    Pi(AlphaLabel, TypedThunk, TypedThunk),
-    // Invariant: the evaluation must not be able to progress further.
-    AppliedBuiltin(Builtin, Vec<Thunk>),
-
-    Var(AlphaVar),
-    Const(Const),
-    BoolLit(bool),
-    NaturalLit(Natural),
-    IntegerLit(Integer),
-    DoubleLit(NaiveDouble),
-    EmptyOptionalLit(TypedThunk),
-    NEOptionalLit(Thunk),
-    // EmptyListLit(t) means `[] : List t`, not `[] : t`
-    EmptyListLit(TypedThunk),
-    NEListLit(Vec<Thunk>),
-    RecordLit(HashMap<Label, Thunk>),
-    RecordType(HashMap<Label, TypedThunk>),
-    UnionType(HashMap<Label, Option<TypedThunk>>),
-    UnionConstructor(Label, HashMap<Label, Option<TypedThunk>>),
-    UnionLit(Label, Thunk, HashMap<Label, Option<TypedThunk>>),
-    // Invariant: this must not contain interpolations that are themselves TextLits, and
-    // contiguous text values must be merged.
-    TextLit(Vec<InterpolatedTextContents<Thunk>>),
-    Equivalence(TypedThunk, TypedThunk),
-    // Invariant: this must not contain a value captured by one of the variants above.
-    PartialExpr(ExprF<Thunk, Normalized>),
+use std::borrow::Cow;
+use std::cell::{Ref, RefCell, RefMut};
+use std::rc::Rc;
+
+use dhall_syntax::{Const, ExprF};
+
+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_one_layer, OutputSubExpr};
+use crate::phase::typecheck::type_of_const;
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
+
+#[derive(Debug, Clone, Copy)]
+enum Marker {
+    /// Weak Head Normal Form, i.e. subexpressions may not be normalized
+    WHNF,
+    /// Normal form, i.e. completely normalized
+    NF,
 }
+use Marker::{NF, WHNF};
 
-impl ValueF {
-    pub(crate) fn into_thunk(self) -> Thunk {
-        Thunk::from_valuef(self)
-    }
+#[derive(Debug, Clone)]
+enum ValueInternal {
+    /// Partially normalized value whose subexpressions have been thunked (this is returned from
+    /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no
+    /// requirement of WHNF here.
+    PartialExpr(ExprF<Value, Normalized>),
+    /// Partially normalized value.
+    /// Invariant: if the marker is `NF`, the value must be fully normalized
+    ValueF(Marker, ValueF),
+}
 
-    /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
-        self.normalize_to_expr_maybe_alpha(false)
+#[derive(Debug)]
+struct TypedValueInternal {
+    internal: ValueInternal,
+    typ: Option<Type>,
+}
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
+/// sharing computation automatically. Uses a RefCell to share computation.
+/// Can optionally store a Type from typechecking to preserve type information through
+/// normalization.
+#[derive(Clone)]
+pub struct Value(Rc<RefCell<TypedValueInternal>>);
+
+#[derive(Debug, Clone)]
+pub struct TypedValue(Value);
+
+impl ValueInternal {
+    fn into_value(self, t: Option<Type>) -> Value {
+        TypedValueInternal {
+            internal: self,
+            typ: t,
+        }
+        .into_value()
     }
-    /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
-    /// if alpha is `true`
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> OutputSubExpr {
+
+    fn normalize_whnf(&mut self) {
         match self {
-            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),
-            )),
-            ValueF::AppliedBuiltin(b, args) => {
-                let mut e = rc(ExprF::Builtin(*b));
-                for v in args {
-                    e = rc(ExprF::App(
-                        e,
-                        v.normalize_to_expr_maybe_alpha(alpha),
-                    ));
-                }
-                e
+            ValueInternal::PartialExpr(e) => {
+                *self =
+                    ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
             }
-            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),
-            )),
-            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),
-            )),
-            ValueF::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
+            // Already at least in WHNF
+            ValueInternal::ValueF(_, _) => {}
+        }
+    }
+
+    fn normalize_nf(&mut self) {
+        match self {
+            ValueInternal::PartialExpr(_) => {
+                self.normalize_whnf();
+                self.normalize_nf();
             }
-            ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
-                rc(ExprF::Builtin(Builtin::List)),
-                n.normalize_to_expr_maybe_alpha(alpha),
-            )))),
-            ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.iter()
-                    .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
-                    .collect(),
-            )),
-            ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
-                    })
-                    .collect(),
-            )),
-            ValueF::RecordType(kts) => rc(ExprF::RecordType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
-                    })
-                    .collect(),
-            )),
-            ValueF::UnionType(kts) => rc(ExprF::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref().map(|v| {
-                                v.normalize_to_expr_maybe_alpha(alpha)
-                            }),
-                        )
-                    })
-                    .collect(),
-            )),
-            ValueF::UnionConstructor(l, kts) => {
-                let kts = kts
-                    .iter()
-                    .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref().map(|v| {
-                                v.normalize_to_expr_maybe_alpha(alpha)
-                            }),
-                        )
-                    })
-                    .collect();
-                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
+            ValueInternal::ValueF(m @ WHNF, v) => {
+                v.normalize_mut();
+                *m = NF;
             }
-            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),
-            )),
-            ValueF::TextLit(elts) => {
-                use InterpolatedTextContents::{Expr, Text};
-                rc(ExprF::TextLit(
-                    elts.iter()
-                        .map(|contents| match contents {
-                            Expr(e) => {
-                                Expr(e.normalize_to_expr_maybe_alpha(alpha))
-                            }
-                            Text(s) => Text(s.clone()),
-                        })
-                        .collect(),
-                ))
+            // Already in NF
+            ValueInternal::ValueF(NF, _) => {}
+        }
+    }
+
+    // Always use normalize_whnf before
+    fn as_whnf(&self) -> &ValueF {
+        match self {
+            ValueInternal::PartialExpr(_) => unreachable!(),
+            ValueInternal::ValueF(_, v) => v,
+        }
+    }
+
+    // Always use normalize_nf before
+    fn as_nf(&self) -> &ValueF {
+        match self {
+            ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => {
+                unreachable!()
             }
-            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),
+            ValueInternal::ValueF(NF, v) => v,
+        }
+    }
+}
+
+impl TypedValueInternal {
+    fn into_value(self) -> Value {
+        Value(Rc::new(RefCell::new(self)))
+    }
+    fn as_internal(&self) -> &ValueInternal {
+        &self.internal
+    }
+    fn as_internal_mut(&mut self) -> &mut ValueInternal {
+        &mut self.internal
+    }
+
+    fn get_type(&self) -> Result<Type, TypeError> {
+        match &self.typ {
+            Some(t) => Ok(t.clone()),
+            None => Err(TypeError::new(
+                &TypecheckContext::new(),
+                TypeMessage::Untyped,
             )),
-            ValueF::PartialExpr(e) => {
-                rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
-            }
         }
     }
+}
 
+impl Value {
+    pub(crate) fn from_valuef(v: ValueF) -> Value {
+        ValueInternal::ValueF(WHNF, v).into_value(None)
+    }
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value {
+        ValueInternal::ValueF(WHNF, v).into_value(Some(t))
+    }
+    pub(crate) fn from_partial_expr(e: ExprF<Value, Normalized>) -> Value {
+        ValueInternal::PartialExpr(e).into_value(None)
+    }
+    pub(crate) fn with_type(self, t: Type) -> Value {
+        self.as_internal().clone().into_value(Some(t))
+    }
+
+    /// Mutates the contents. If no one else shares this thunk,
+    /// mutates directly, thus avoiding a RefCell lock.
+    fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) {
+        match Rc::get_mut(&mut self.0) {
+            // Mutate directly if sole owner
+            Some(refcell) => f(RefCell::get_mut(refcell)),
+            // Otherwise mutate through the refcell
+            None => f(&mut self.as_tinternal_mut()),
+        }
+    }
+
+    /// Normalizes contents to normal form; faster than `normalize_nf` if
+    /// no one else shares this thunk
     pub(crate) fn normalize_mut(&mut self) {
-        match self {
-            ValueF::Var(_)
-            | ValueF::Const(_)
-            | ValueF::BoolLit(_)
-            | ValueF::NaturalLit(_)
-            | ValueF::IntegerLit(_)
-            | ValueF::DoubleLit(_) => {}
-
-            ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
-                tth.normalize_mut();
-            }
+        self.mutate_internal(|i| i.as_internal_mut().normalize_nf())
+    }
 
-            ValueF::NEOptionalLit(th) => {
-                th.normalize_mut();
-            }
-            ValueF::Lam(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
-            ValueF::Pi(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
-            ValueF::AppliedBuiltin(_, args) => {
-                for x in args.iter_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::NEListLit(elts) => {
-                for x in elts.iter_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::RecordLit(kvs) => {
-                for x in kvs.values_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::RecordType(kvs) => {
-                for x in kvs.values_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::UnionLit(_, v, kts) => {
-                v.normalize_mut();
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::TextLit(elts) => {
-                for x in elts.iter_mut() {
-                    use InterpolatedTextContents::{Expr, Text};
-                    match x {
-                        Expr(n) => n.normalize_mut(),
-                        Text(_) => {}
-                    }
-                }
-            }
-            ValueF::Equivalence(x, y) => {
-                x.normalize_mut();
-                y.normalize_mut();
-            }
-            ValueF::PartialExpr(e) => {
-                // TODO: need map_mut
-                e.map_ref(|v| {
-                    v.normalize_nf();
-                });
-            }
+    fn as_tinternal(&self) -> Ref<TypedValueInternal> {
+        self.0.borrow()
+    }
+    fn as_tinternal_mut(&mut self) -> RefMut<TypedValueInternal> {
+        self.0.borrow_mut()
+    }
+    fn as_internal(&self) -> Ref<ValueInternal> {
+        Ref::map(self.as_tinternal(), TypedValueInternal::as_internal)
+    }
+    fn as_internal_mut(&self) -> RefMut<ValueInternal> {
+        RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut)
+    }
+
+    fn do_normalize_whnf(&self) {
+        let borrow = self.as_internal();
+        match &*borrow {
+            ValueInternal::PartialExpr(_) => {
+                drop(borrow);
+                self.as_internal_mut().normalize_whnf();
+            }
+            // Already at least in WHNF
+            ValueInternal::ValueF(_, _) => {}
         }
     }
 
-    /// Apply to a value
-    pub(crate) fn app(self, val: ValueF) -> ValueF {
-        self.app_val(val)
+    fn do_normalize_nf(&self) {
+        let borrow = self.as_internal();
+        match &*borrow {
+            ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => {
+                drop(borrow);
+                self.as_internal_mut().normalize_nf();
+            }
+            // Already in NF
+            ValueInternal::ValueF(NF, _) => {}
+        }
     }
 
-    /// Apply to a value
-    pub(crate) fn app_val(self, val: ValueF) -> ValueF {
-        self.app_thunk(val.into_thunk())
+    // 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<ValueF> {
+        self.do_normalize_nf();
+        Ref::map(self.as_internal(), ValueInternal::as_nf)
     }
 
-    /// Apply to a thunk
-    pub fn app_thunk(self, th: Thunk) -> ValueF {
-        Thunk::from_valuef(self).app_thunk(th)
+    // WARNING: avoid normalizing any thunk while holding on to this ref
+    // or you could run into BorrowMut panics
+    pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
+        self.do_normalize_whnf();
+        Ref::map(self.as_internal(), ValueInternal::as_whnf)
     }
 
-    pub fn from_builtin(b: Builtin) -> ValueF {
-        ValueF::AppliedBuiltin(b, vec![])
+    pub(crate) fn to_valuef(&self) -> ValueF {
+        self.as_valuef().clone()
+    }
+
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
+    }
+
+    pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF {
+        self.app_value(val.into_value())
+    }
+
+    pub(crate) fn app_value(&self, th: Value) -> ValueF {
+        apply_any(self.clone(), th)
+    }
+
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
+        Ok(Cow::Owned(self.as_tinternal().get_type()?))
     }
 }
 
-impl Shift for ValueF {
+impl TypedValue {
+    pub(crate) fn from_valuef(v: ValueF) -> TypedValue {
+        TypedValue::from_value_untyped(Value::from_valuef(v))
+    }
+
+    pub(crate) fn from_type(t: Type) -> TypedValue {
+        t.into_typedvalue()
+    }
+
+    pub(crate) fn normalize_nf(&self) -> ValueF {
+        self.0.normalize_nf().clone()
+    }
+
+    pub(crate) fn to_typed(&self) -> Typed {
+        self.clone().into_typed()
+    }
+
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
+    }
+
+    pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self {
+        TypedValue(th.with_type(t))
+    }
+    pub fn from_value_simple_type(th: Value) -> Self {
+        TypedValue::from_value_and_type(th, Type::const_type())
+    }
+    pub(crate) fn from_value_untyped(th: Value) -> Self {
+        TypedValue(th)
+    }
+    pub(crate) fn from_const(c: Const) -> Self {
+        match type_of_const(c) {
+            Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t),
+            Err(_) => TypedValue::from_valuef(ValueF::Const(c)),
+        }
+    }
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
+        TypedValue(Value::from_valuef_and_type(v, t))
+    }
+
+    pub(crate) fn to_valuef(&self) -> ValueF {
+        self.0.to_valuef()
+    }
+    pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
+        self.to_valuef().normalize_to_expr()
+    }
+    pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
+        self.to_valuef().normalize_to_expr_maybe_alpha(true)
+    }
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.clone()
+    }
+    pub(crate) fn to_type(&self) -> Type {
+        self.clone().into_typed().into_type()
+    }
+    pub(crate) fn into_typed(self) -> Typed {
+        Typed::from_typedvalue(self)
+    }
+    pub(crate) fn as_const(&self) -> Option<Const> {
+        // TODO: avoid clone
+        match &self.to_valuef() {
+            ValueF::Const(c) => Some(*c),
+            _ => None,
+        }
+    }
+
+    pub(crate) fn normalize_mut(&mut self) {
+        self.0.normalize_mut()
+    }
+
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
+        self.0.get_type()
+    }
+}
+
+impl Shift for Value {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(Value(self.0.shift(delta, var)?))
+    }
+}
+
+impl Shift for ValueInternal {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
-            ValueF::Lam(x, t, e) => ValueF::Lam(
-                x.clone(),
-                t.shift(delta, var)?,
-                e.shift(delta, &var.under_binder(x))?,
-            ),
-            ValueF::AppliedBuiltin(b, args) => {
-                ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
-            }
-            ValueF::Pi(x, t, e) => ValueF::Pi(
-                x.clone(),
-                t.shift(delta, var)?,
-                e.shift(delta, &var.under_binder(x))?,
-            ),
-            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)?)
-            }
-            ValueF::NEOptionalLit(th) => {
-                ValueF::NEOptionalLit(th.shift(delta, var)?)
+            ValueInternal::PartialExpr(e) => {
+                ValueInternal::PartialExpr(e.shift(delta, var)?)
             }
-            ValueF::EmptyListLit(tth) => {
-                ValueF::EmptyListLit(tth.shift(delta, var)?)
+            ValueInternal::ValueF(m, v) => {
+                ValueInternal::ValueF(*m, v.shift(delta, var)?)
             }
-            ValueF::NEListLit(elts) => {
-                ValueF::NEListLit(elts.shift(delta, var)?)
-            }
-            ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
-            ValueF::RecordType(kvs) => {
-                ValueF::RecordType(kvs.shift(delta, var)?)
-            }
-            ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
-            ValueF::UnionConstructor(x, kts) => {
-                ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
-            }
-            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
-                x.clone(),
-                v.shift(delta, var)?,
-                kts.shift(delta, var)?,
-            ),
-            ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
-            ValueF::Equivalence(x, y) => {
-                ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
-            }
-            ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
         })
     }
 }
 
-impl Subst<Typed> for ValueF {
+impl Shift for TypedValue {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(TypedValue(self.0.shift(delta, var)?))
+    }
+}
+
+impl Shift for TypedValueInternal {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(TypedValueInternal {
+            internal: self.internal.shift(delta, var)?,
+            typ: self.typ.shift(delta, var)?,
+        })
+    }
+}
+
+impl Subst<Typed> for Value {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        Value(self.0.subst_shift(var, val))
+    }
+}
+
+impl Subst<Typed> for ValueInternal {
     fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
-            // Retry normalizing since substituting may allow progress
-            ValueF::AppliedBuiltin(b, args) => {
-                apply_builtin(*b, args.subst_shift(var, val))
-            }
-            // Retry normalizing since substituting may allow progress
-            ValueF::PartialExpr(e) => {
-                normalize_one_layer(e.subst_shift(var, val))
-            }
-            // Retry normalizing since substituting may allow progress
-            ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit(
-                elts.iter().map(|contents| contents.subst_shift(var, val)),
-            )),
-            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)),
-            ),
-            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)),
-            ),
-            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))
-            }
-            ValueF::NEOptionalLit(th) => {
-                ValueF::NEOptionalLit(th.subst_shift(var, val))
-            }
-            ValueF::EmptyListLit(tth) => {
-                ValueF::EmptyListLit(tth.subst_shift(var, val))
+            ValueInternal::PartialExpr(e) => {
+                ValueInternal::PartialExpr(e.subst_shift(var, val))
             }
-            ValueF::NEListLit(elts) => {
-                ValueF::NEListLit(elts.subst_shift(var, val))
+            ValueInternal::ValueF(_, v) => {
+                // The resulting value may not stay in normal form after substitution
+                ValueInternal::ValueF(WHNF, v.subst_shift(var, val))
             }
-            ValueF::RecordLit(kvs) => {
-                ValueF::RecordLit(kvs.subst_shift(var, val))
-            }
-            ValueF::RecordType(kvs) => {
-                ValueF::RecordType(kvs.subst_shift(var, val))
-            }
-            ValueF::UnionType(kts) => {
-                ValueF::UnionType(kts.subst_shift(var, val))
+        }
+    }
+}
+
+impl Subst<Typed> for TypedValueInternal {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        TypedValueInternal {
+            internal: self.internal.subst_shift(var, val),
+            typ: self.typ.subst_shift(var, val),
+        }
+    }
+}
+
+impl Subst<Typed> for TypedValue {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        TypedValue(self.0.subst_shift(var, val))
+    }
+}
+
+impl std::cmp::PartialEq for Value {
+    fn eq(&self, other: &Self) -> bool {
+        *self.as_valuef() == *other.as_valuef()
+    }
+}
+impl std::cmp::Eq for Value {}
+
+impl std::cmp::PartialEq for TypedValue {
+    fn eq(&self, other: &Self) -> bool {
+        self.to_valuef() == other.to_valuef()
+    }
+}
+impl std::cmp::Eq for TypedValue {}
+
+impl std::fmt::Debug for Value {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let b: &ValueInternal = &self.as_internal();
+        match b {
+            ValueInternal::ValueF(m, v) => {
+                f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish()
             }
-            ValueF::UnionConstructor(x, kts) => {
-                ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
+            ValueInternal::PartialExpr(e) => {
+                f.debug_tuple("Value@PartialExpr").field(e).finish()
             }
-            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
-                x.clone(),
-                v.subst_shift(var, val),
-                kts.subst_shift(var, val),
-            ),
-            ValueF::Equivalence(x, y) => ValueF::Equivalence(
-                x.subst_shift(var, val),
-                y.subst_shift(var, val),
-            ),
         }
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
new file mode 100644
index 0000000..bea2e2e
--- /dev/null
+++ b/dhall/src/core/valuef.rs
@@ -0,0 +1,405 @@
+use std::collections::HashMap;
+
+use dhall_syntax::{
+    rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+    NaiveDouble, Natural,
+};
+
+use crate::core::value::{TypedValue, Value};
+use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::phase::normalize::{
+    apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
+};
+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 `ValueF`s. In particular, `subst_shift` could break
+/// the invariants so need to be careful to reevaluate as needed.
+/// Subexpressions are Values, which are partially evaluated expressions that are normalized
+/// on-demand. When all the Values 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 ValueF {
+    /// Closures
+    Lam(AlphaLabel, TypedValue, Value),
+    Pi(AlphaLabel, TypedValue, TypedValue),
+    // Invariant: the evaluation must not be able to progress further.
+    AppliedBuiltin(Builtin, Vec<Value>),
+
+    Var(AlphaVar),
+    Const(Const),
+    BoolLit(bool),
+    NaturalLit(Natural),
+    IntegerLit(Integer),
+    DoubleLit(NaiveDouble),
+    EmptyOptionalLit(TypedValue),
+    NEOptionalLit(Value),
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
+    EmptyListLit(TypedValue),
+    NEListLit(Vec<Value>),
+    RecordLit(HashMap<Label, Value>),
+    RecordType(HashMap<Label, TypedValue>),
+    UnionType(HashMap<Label, Option<TypedValue>>),
+    UnionConstructor(Label, HashMap<Label, Option<TypedValue>>),
+    UnionLit(Label, Value, HashMap<Label, Option<TypedValue>>),
+    // Invariant: this must not contain interpolations that are themselves TextLits, and
+    // contiguous text values must be merged.
+    TextLit(Vec<InterpolatedTextContents<Value>>),
+    Equivalence(TypedValue, TypedValue),
+    // Invariant: this must not contain a value captured by one of the variants above.
+    PartialExpr(ExprF<Value, Normalized>),
+}
+
+impl ValueF {
+    pub(crate) fn into_value(self) -> Value {
+        Value::from_valuef(self)
+    }
+
+    /// Convert the value to a fully normalized syntactic expression
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+        self.normalize_to_expr_maybe_alpha(false)
+    }
+    /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
+    /// if alpha is `true`
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
+        match self {
+            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),
+            )),
+            ValueF::AppliedBuiltin(b, args) => {
+                let mut e = rc(ExprF::Builtin(*b));
+                for v in args {
+                    e = rc(ExprF::App(
+                        e,
+                        v.normalize_to_expr_maybe_alpha(alpha),
+                    ));
+                }
+                e
+            }
+            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),
+            )),
+            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),
+            )),
+            ValueF::NEOptionalLit(n) => {
+                rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
+            }
+            ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+                rc(ExprF::Builtin(Builtin::List)),
+                n.normalize_to_expr_maybe_alpha(alpha),
+            )))),
+            ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
+                elts.iter()
+                    .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
+                    .collect(),
+            )),
+            ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+                    })
+                    .collect(),
+            )),
+            ValueF::RecordType(kts) => rc(ExprF::RecordType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+                    })
+                    .collect(),
+            )),
+            ValueF::UnionType(kts) => rc(ExprF::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (
+                            k.clone(),
+                            v.as_ref().map(|v| {
+                                v.normalize_to_expr_maybe_alpha(alpha)
+                            }),
+                        )
+                    })
+                    .collect(),
+            )),
+            ValueF::UnionConstructor(l, kts) => {
+                let kts = kts
+                    .iter()
+                    .map(|(k, v)| {
+                        (
+                            k.clone(),
+                            v.as_ref().map(|v| {
+                                v.normalize_to_expr_maybe_alpha(alpha)
+                            }),
+                        )
+                    })
+                    .collect();
+                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.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),
+            )),
+            ValueF::TextLit(elts) => {
+                use InterpolatedTextContents::{Expr, Text};
+                rc(ExprF::TextLit(
+                    elts.iter()
+                        .map(|contents| match contents {
+                            Expr(e) => {
+                                Expr(e.normalize_to_expr_maybe_alpha(alpha))
+                            }
+                            Text(s) => Text(s.clone()),
+                        })
+                        .collect(),
+                ))
+            }
+            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),
+            )),
+            ValueF::PartialExpr(e) => {
+                rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
+            }
+        }
+    }
+
+    pub(crate) fn normalize_mut(&mut self) {
+        match self {
+            ValueF::Var(_)
+            | ValueF::Const(_)
+            | ValueF::BoolLit(_)
+            | ValueF::NaturalLit(_)
+            | ValueF::IntegerLit(_)
+            | ValueF::DoubleLit(_) => {}
+
+            ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
+                tth.normalize_mut();
+            }
+
+            ValueF::NEOptionalLit(th) => {
+                th.normalize_mut();
+            }
+            ValueF::Lam(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueF::Pi(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueF::AppliedBuiltin(_, args) => {
+                for x in args.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::NEListLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::RecordType(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::UnionLit(_, v, kts) => {
+                v.normalize_mut();
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueF::TextLit(elts) => {
+                for x in elts.iter_mut() {
+                    use InterpolatedTextContents::{Expr, Text};
+                    match x {
+                        Expr(n) => n.normalize_mut(),
+                        Text(_) => {}
+                    }
+                }
+            }
+            ValueF::Equivalence(x, y) => {
+                x.normalize_mut();
+                y.normalize_mut();
+            }
+            ValueF::PartialExpr(e) => {
+                // TODO: need map_mut
+                e.map_ref(|v| {
+                    v.normalize_nf();
+                });
+            }
+        }
+    }
+
+    /// Apply to a value
+    pub(crate) fn app(self, val: ValueF) -> ValueF {
+        self.app_valuef(val)
+    }
+
+    /// Apply to a value
+    pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
+        self.app_value(val.into_value())
+    }
+
+    /// Apply to a thunk
+    pub fn app_value(self, th: Value) -> ValueF {
+        Value::from_valuef(self).app_value(th)
+    }
+
+    pub fn from_builtin(b: Builtin) -> ValueF {
+        ValueF::AppliedBuiltin(b, vec![])
+    }
+}
+
+impl Shift for ValueF {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(match self {
+            ValueF::Lam(x, t, e) => ValueF::Lam(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            ValueF::AppliedBuiltin(b, args) => {
+                ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
+            }
+            ValueF::Pi(x, t, e) => ValueF::Pi(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            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)?)
+            }
+            ValueF::NEOptionalLit(th) => {
+                ValueF::NEOptionalLit(th.shift(delta, var)?)
+            }
+            ValueF::EmptyListLit(tth) => {
+                ValueF::EmptyListLit(tth.shift(delta, var)?)
+            }
+            ValueF::NEListLit(elts) => {
+                ValueF::NEListLit(elts.shift(delta, var)?)
+            }
+            ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
+            ValueF::RecordType(kvs) => {
+                ValueF::RecordType(kvs.shift(delta, var)?)
+            }
+            ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
+            ValueF::UnionConstructor(x, kts) => {
+                ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+            }
+            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
+                x.clone(),
+                v.shift(delta, var)?,
+                kts.shift(delta, var)?,
+            ),
+            ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
+            ValueF::Equivalence(x, y) => {
+                ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+            }
+            ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
+        })
+    }
+}
+
+impl Subst<Typed> for ValueF {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        match self {
+            // Retry normalizing since substituting may allow progress
+            ValueF::AppliedBuiltin(b, args) => {
+                apply_builtin(*b, args.subst_shift(var, val))
+            }
+            // Retry normalizing since substituting may allow progress
+            ValueF::PartialExpr(e) => {
+                normalize_one_layer(e.subst_shift(var, val))
+            }
+            // Retry normalizing since substituting may allow progress
+            ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit(
+                elts.iter().map(|contents| contents.subst_shift(var, val)),
+            )),
+            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)),
+            ),
+            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)),
+            ),
+            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))
+            }
+            ValueF::NEOptionalLit(th) => {
+                ValueF::NEOptionalLit(th.subst_shift(var, val))
+            }
+            ValueF::EmptyListLit(tth) => {
+                ValueF::EmptyListLit(tth.subst_shift(var, val))
+            }
+            ValueF::NEListLit(elts) => {
+                ValueF::NEListLit(elts.subst_shift(var, val))
+            }
+            ValueF::RecordLit(kvs) => {
+                ValueF::RecordLit(kvs.subst_shift(var, val))
+            }
+            ValueF::RecordType(kvs) => {
+                ValueF::RecordType(kvs.subst_shift(var, val))
+            }
+            ValueF::UnionType(kts) => {
+                ValueF::UnionType(kts.subst_shift(var, val))
+            }
+            ValueF::UnionConstructor(x, kts) => {
+                ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
+            }
+            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
+                x.clone(),
+                v.subst_shift(var, val),
+                kts.subst_shift(var, val),
+            ),
+            ValueF::Equivalence(x, y) => ValueF::Equivalence(
+                x.subst_shift(var, val),
+                y.subst_shift(var, val),
+            ),
+        }
+    }
+}
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 7e74f95..c18f976 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,8 +4,8 @@ use std::path::Path;
 
 use dhall_syntax::{Const, SubExpr};
 
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 
@@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed(TypedThunk);
+pub struct Typed(TypedValue);
 
 /// A normalized expression.
 ///
@@ -92,19 +92,19 @@ impl Typed {
         Normalized(self)
     }
 
-    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
-        Typed(TypedThunk::from_thunk_and_type(th, t))
+    pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self {
+        Typed(TypedValue::from_value_and_type(th, t))
     }
-    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
-        Typed(TypedThunk::from_thunk_untyped(th))
+    pub(crate) fn from_value_untyped(th: Value) -> Self {
+        Typed(TypedValue::from_value_untyped(th))
     }
     pub(crate) fn from_const(c: Const) -> Self {
-        Typed(TypedThunk::from_const(c))
+        Typed(TypedValue::from_const(c))
     }
     pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
-        Typed(TypedThunk::from_valuef_and_type(v, t))
+        Typed(TypedValue::from_valuef_and_type(v, t))
     }
-    pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
+    pub(crate) fn from_typedvalue(th: TypedValue) -> Self {
         Typed(th)
     }
     pub fn const_type() -> Self {
@@ -120,8 +120,8 @@ impl Typed {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.0.to_expr_alpha()
     }
-    pub fn to_thunk(&self) -> Thunk {
-        self.0.to_thunk()
+    pub fn to_value(&self) -> Value {
+        self.0.to_value()
     }
     // Deprecated
     pub fn to_type(&self) -> Type {
@@ -131,7 +131,7 @@ impl Typed {
     pub(crate) fn into_type(self) -> Type {
         self
     }
-    pub(crate) fn into_typethunk(self) -> TypedThunk {
+    pub(crate) fn into_typedvalue(self) -> TypedValue {
         self.0
     }
     pub(crate) fn to_normalized(&self) -> Normalized {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index da54726..93f2528 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,8 +5,8 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr, Typed};
 
@@ -20,45 +20,45 @@ macro_rules! make_closure {
             Label::from(stringify!($var)).into(),
             $n
         );
-        ValueF::Var(var).into_thunk()
+        ValueF::Var(var).into_value()
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
     (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
         ValueF::Lam(
             Label::from(stringify!($var)).into(),
-            TypedThunk::from_thunk_simple_type(
+            TypedValue::from_value_simple_type(
                 make_closure!($($ty)*),
             ),
             make_closure!($($rest)*),
-        ).into_thunk()
+        ).into_value()
     };
-    (Natural) => { ValueF::from_builtin(Builtin::Natural).into_thunk() };
+    (Natural) => { ValueF::from_builtin(Builtin::Natural).into_value() };
     (List $($rest:tt)*) => {
         ValueF::from_builtin(Builtin::List)
-            .app_thunk(make_closure!($($rest)*))
-            .into_thunk()
+            .app_value(make_closure!($($rest)*))
+            .into_value()
     };
     (Some $($rest:tt)*) => {
-        ValueF::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+        ValueF::NEOptionalLit(make_closure!($($rest)*)).into_value()
     };
     (1 + $($rest:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
             make_closure!($($rest)*),
-            Thunk::from_valuef(ValueF::NaturalLit(1)),
-        )).into_thunk()
+            Value::from_valuef(ValueF::NaturalLit(1)),
+        )).into_value()
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+            ValueF::NEListLit(vec![make_closure!($($head)*)]).into_value(),
             make_closure!($($tail)*),
-        )).into_thunk()
+        )).into_value()
     };
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -66,7 +66,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t, r..]) => Ok((
             r,
-            EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())),
+            EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())),
         )),
         (NaturalIsZero, [n, r..]) => match &*n.as_valuef() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
@@ -189,10 +189,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypedThunk::from_valuef(ValueF::from_builtin(Natural)),
+                    TypedValue::from_valuef(ValueF::from_builtin(Natural)),
                 );
                 kts.insert("value".into(), t.clone());
-                Ok((r, EmptyListLit(TypedThunk::from_valuef(RecordType(kts)))))
+                Ok((r, EmptyListLit(TypedValue::from_valuef(RecordType(kts)))))
             }
             NEListLit(xs) => {
                 let xs = xs
@@ -201,9 +201,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = HashMap::new();
-                        kvs.insert("index".into(), Thunk::from_valuef(i));
+                        kvs.insert("index".into(), Value::from_valuef(i));
                         kvs.insert("value".into(), e.clone());
-                        Thunk::from_valuef(RecordLit(kvs))
+                        Value::from_valuef(RecordLit(kvs))
                     })
                     .collect();
                 Ok((r, NEListLit(xs)))
@@ -222,8 +222,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
             }
             _ => Ok((
                 r,
-                f.app_val(ValueF::from_builtin(List).app_thunk(t.clone()))
-                    .app_thunk({
+                f.app_valuef(ValueF::from_builtin(List).app_value(t.clone()))
+                    .app_value({
                         // Move `t` under new `x` variable
                         let t1 = t.under_binder(Label::from("x"));
                         make_closure!(
@@ -232,9 +232,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
                             [ var(x, 1) ] # var(xs, 0)
                         )
                     })
-                    .app_val(EmptyListLit(TypedThunk::from_thunk_simple_type(
-                        t.clone(),
-                    ))),
+                    .app_valuef(EmptyListLit(
+                        TypedValue::from_value_simple_type(t.clone()),
+                    )),
             )),
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() {
@@ -244,9 +244,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
                 for x in xs.iter().rev() {
                     v = cons
                         .clone()
-                        .app_thunk(x.clone())
-                        .app_thunk(v)
-                        .into_thunk();
+                        .app_value(x.clone())
+                        .app_value(v)
+                        .into_value();
                 }
                 Ok((r, v.to_valuef()))
             }
@@ -264,17 +264,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
             }
             _ => Ok((
                 r,
-                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()),
-                    )),
+                f.app_valuef(
+                    ValueF::from_builtin(Optional).app_value(t.clone()),
+                )
+                .app_value(make_closure!(λ(x: #t) -> Some var(x, 0)))
+                .app_valuef(EmptyOptionalLit(
+                    TypedValue::from_value_simple_type(t.clone()),
+                )),
             )),
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => {
             match &*v.as_valuef() {
                 EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())),
-                NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+                NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
                 _ => Err(()),
             }
         }
@@ -290,9 +292,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
             }
             _ => Ok((
                 r,
-                f.app_val(ValueF::from_builtin(Natural))
-                    .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
-                    .app_val(NaturalLit(0)),
+                f.app_valuef(ValueF::from_builtin(Natural))
+                    .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                    .app_valuef(NaturalLit(0)),
             )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() {
@@ -300,10 +302,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
             NaturalLit(n) => {
                 let fold = ValueF::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
-                    .app_thunk(t.clone())
-                    .app_thunk(succ.clone())
-                    .app_thunk(zero.clone());
-                Ok((r, succ.app_val(fold)))
+                    .app_value(t.clone())
+                    .app_value(succ.clone())
+                    .app_value(zero.clone());
+                Ok((r, succ.app_valuef(fold)))
             }
             _ => Err(()),
         },
@@ -313,7 +315,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> 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_thunk(x);
+                v = v.app_value(x);
             }
             v
         }
@@ -321,13 +323,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
     }
 }
 
-pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF {
-    let fallback = |f: Thunk, a: Thunk| ValueF::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
+    let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
 
     let f_borrow = f.as_valuef();
     match &*f_borrow {
         ValueF::Lam(x, _, e) => {
-            let val = Typed::from_thunk_untyped(a);
+            let val = Typed::from_value_untyped(a);
             e.subst_shift(&x.into(), &val).to_valuef()
         }
         ValueF::AppliedBuiltin(b, args) => {
@@ -346,15 +348,15 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF {
 }
 
 pub(crate) fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
-) -> Vec<InterpolatedTextContents<Thunk>> {
+    elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
     use std::mem::replace;
     use InterpolatedTextContents::{Expr, Text};
 
     fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
         crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Thunk>>,
+        ret: &mut Vec<InterpolatedTextContents<Value>>,
     ) {
         for contents in elts {
             match contents {
@@ -390,9 +392,9 @@ pub(crate) fn squash_textlit(
 // Small helper enum to avoid repetition
 enum Ret<'a> {
     ValueF(ValueF),
-    Thunk(Thunk),
-    ThunkRef(&'a Thunk),
-    Expr(ExprF<Thunk, Normalized>),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprF<Value, Normalized>),
 }
 
 /// Performs an intersection of two HashMaps.
@@ -508,7 +510,7 @@ where
     kvs
 }
 
-fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -521,46 +523,46 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     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(true), _) => Ret::ValueRef(y),
+        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
         (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
         (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
-        (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
+        (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
         (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),
+        (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
+        (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+        (BoolOr, _, _) if x == y => Ret::ValueRef(x),
+        (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
+        (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
         (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(false), _) => Ret::ValueRef(y),
+        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
         (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(0), _) => Ret::ValueRef(y),
+        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
         (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
             Ret::ValueF(NaturalLit(x + y))
         }
         (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(1), _) => Ret::ValueRef(y),
+        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
         (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
             Ret::ValueF(NaturalLit(x * y))
         }
 
-        (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
+        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
         (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), _) if x.is_empty() => Ret::ValueRef(y),
+        (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x),
         (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
             squash_textlit(x.iter().chain(y.iter()).cloned()),
         )),
@@ -580,10 +582,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
 
         (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let mut kvs = kvs2.clone();
@@ -595,14 +597,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Thunk::from_partial_expr(ExprF::BinOp(
+                Value::from_partial_expr(ExprF::BinOp(
                     RecursiveRecordMerge,
                     v1.clone(),
                     v2.clone(),
@@ -612,18 +614,18 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
 
         (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                TypedThunk::from_thunk_untyped(Thunk::from_partial_expr(
+                TypedValue::from_value_untyped(Value::from_partial_expr(
                     ExprF::BinOp(
                         RecursiveRecordTypeMerge,
-                        v1.to_thunk(),
-                        v2.to_thunk(),
+                        v1.to_value(),
+                        v2.to_value(),
                     ),
                 ))
             });
@@ -631,15 +633,15 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
 
         (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence(
-            TypedThunk::from_thunk_simple_type(x.clone()),
-            TypedThunk::from_thunk_simple_type(y.clone()),
+            TypedValue::from_value_simple_type(x.clone()),
+            TypedValue::from_value_simple_type(y.clone()),
         )),
 
         _ => return None,
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -652,21 +654,21 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
         ),
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => Ret::Thunk(x),
+        ExprF::Annot(x, _) => Ret::Value(x),
         ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
-            Ret::ValueF(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e))
+            Ret::ValueF(Lam(x.into(), TypedValue::from_value_untyped(t), e))
         }
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(
             x.into(),
-            TypedThunk::from_thunk_untyped(t),
-            TypedThunk::from_thunk_untyped(e),
+            TypedValue::from_value_untyped(t),
+            TypedValue::from_value_untyped(e),
         )),
         ExprF::Let(x, _, v, b) => {
-            let v = Typed::from_thunk_untyped(v);
-            Ret::Thunk(b.subst_shift(&x.into(), &v))
+            let v = Typed::from_value_untyped(v);
+            Ret::Value(b.subst_shift(&x.into(), &v))
         }
-        ExprF::App(v, a) => Ret::ValueF(v.app_thunk(a)),
+        ExprF::App(v, a) => Ret::ValueF(v.app_value(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)),
@@ -680,7 +682,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
                     Ret::ValueF(EmptyListLit(
-                        TypedThunk::from_thunk_simple_type(args[0].clone()),
+                        TypedValue::from_value_simple_type(args[0].clone()),
                     ))
                 }
                 _ => {
@@ -697,12 +699,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
         }
         ExprF::RecordType(kts) => Ret::ValueF(RecordType(
             kts.into_iter()
-                .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t)))
+                .map(|(k, t)| (k, TypedValue::from_value_untyped(t)))
                 .collect(),
         )),
         ExprF::UnionType(kts) => Ret::ValueF(UnionType(
             kts.into_iter()
-                .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t))))
+                .map(|(k, t)| (k, t.map(|t| TypedValue::from_value_untyped(t))))
                 .collect(),
         )),
         ExprF::TextLit(elts) => {
@@ -710,7 +712,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
             let elts: Vec<_> = squash_textlit(elts.into_iter());
             // Simplify bare interpolation
             if let [Expr(th)] = elts.as_slice() {
-                Ret::Thunk(th.clone())
+                Ret::Value(th.clone())
             } else {
                 Ret::ValueF(TextLit(elts))
             }
@@ -718,15 +720,15 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
         ExprF::BoolIf(ref b, ref e1, ref e2) => {
             let b_borrow = b.as_valuef();
             match &*b_borrow {
-                BoolLit(true) => Ret::ThunkRef(e1),
-                BoolLit(false) => Ret::ThunkRef(e2),
+                BoolLit(true) => Ret::ValueRef(e1),
+                BoolLit(false) => Ret::ValueRef(e2),
                 _ => {
                     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),
-                        _ if e1 == e2 => Ret::ThunkRef(e1),
+                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+                        _ if e1 == e2 => Ret::ValueRef(e1),
                         _ => {
                             drop(b_borrow);
                             drop(e1_borrow);
@@ -765,7 +767,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
             let v_borrow = v.as_valuef();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
-                    Some(r) => Ret::Thunk(r.clone()),
+                    Some(r) => Ret::Value(r.clone()),
                     None => {
                         drop(v_borrow);
                         Ret::Expr(expr)
@@ -786,7 +788,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> 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()),
+                    Some(h) => Ret::Value(h.clone()),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -794,7 +796,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::ValueF(h.app_thunk(v.clone())),
+                    Some(h) => Ret::ValueF(h.app_value(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -812,8 +814,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
 
     match ret {
         Ret::ValueF(v) => v,
-        Ret::Thunk(th) => th.to_valuef(),
-        Ret::ThunkRef(th) => th.to_valuef(),
+        Ret::Value(th) => th.to_valuef(),
+        Ret::ValueRef(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 8d7a3bc..4154afe 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -5,8 +5,8 @@ use dhall_syntax::{
 };
 
 use crate::core::context::TypecheckContext;
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::{Normalized, Resolved, Type, Typed};
@@ -42,13 +42,13 @@ fn tck_pi_type(
 
     let k = function_check(ka, kb);
 
-    Ok(Typed::from_thunk_and_type(
+    Ok(Typed::from_value_and_type(
         ValueF::Pi(
             x.into(),
-            TypedThunk::from_type(tx),
-            TypedThunk::from_type(te),
+            TypedValue::from_type(tx),
+            TypedValue::from_type(te),
         )
-        .into_thunk(),
+        .into_value(),
         Type::from_const(k),
     ))
 }
@@ -80,15 +80,15 @@ fn tck_record_type(
                 return Err(TypeError::new(ctx, RecordTypeDuplicateField))
             }
             Entry::Vacant(_) => {
-                entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
+                entry.or_insert_with(|| TypedValue::from_type(t.clone()))
             }
         };
     }
     // An empty record type has type Type
     let k = k.unwrap_or(dhall_syntax::Const::Type);
 
-    Ok(Typed::from_thunk_and_type(
-        ValueF::RecordType(new_kts).into_thunk(),
+    Ok(Typed::from_value_and_type(
+        ValueF::RecordType(new_kts).into_value(),
         Type::from_const(k),
     ))
 }
@@ -122,7 +122,7 @@ fn tck_union_type(
                 return Err(TypeError::new(ctx, UnionTypeDuplicateField))
             }
             Entry::Vacant(_) => entry.or_insert_with(|| {
-                t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
+                t.as_ref().map(|t| TypedValue::from_type(t.clone()))
             }),
         };
     }
@@ -131,8 +131,8 @@ fn tck_union_type(
     // an union type with only unary variants also has type Type
     let k = k.unwrap_or(dhall_syntax::Const::Type);
 
-    Ok(Typed::from_thunk_and_type(
-        ValueF::UnionType(new_kts).into_thunk(),
+    Ok(Typed::from_value_and_type(
+        ValueF::UnionType(new_kts).into_value(),
         Type::from_const(k),
     ))
 }
@@ -337,12 +337,12 @@ fn type_with(
             let b = type_with(&ctx2, b.clone())?;
             let v = ValueF::Lam(
                 x.clone().into(),
-                TypedThunk::from_type(tx.clone()),
-                b.to_thunk(),
+                TypedValue::from_type(tx.clone()),
+                b.to_value(),
             );
             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_valuef(v), t)
+            Typed::from_value_and_type(Value::from_valuef(v), t)
         }
         Pi(x, ta, tb) => {
             let ta = mktype(ctx, ta.clone())?;
@@ -380,9 +380,9 @@ fn type_with(
             let ret = type_last_layer(ctx, &expr)?;
             match ret {
                 RetTypeOnly(typ) => {
-                    let expr = expr.map_ref(|typed| typed.to_thunk());
-                    Typed::from_thunk_and_type(
-                        Thunk::from_partial_expr(expr),
+                    let expr = expr.map_ref(|typed| typed.to_value());
+                    Typed::from_value_and_type(
+                        Value::from_partial_expr(expr),
                         typ,
                     )
                 }
@@ -505,10 +505,10 @@ fn type_last_layer(
             }
 
             Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
+                Typed::from_value_and_type(
                     ValueF::from_builtin(dhall_syntax::Builtin::List)
                         .app(t.to_valuef())
-                        .into_thunk(),
+                        .into_value(),
                     Typed::from_const(Type),
                 )
                 .to_type(),
@@ -524,10 +524,10 @@ fn type_last_layer(
             }
 
             Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
+                Typed::from_value_and_type(
                     ValueF::from_builtin(dhall_syntax::Builtin::Optional)
                         .app(t.to_valuef())
-                        .into_thunk(),
+                        .into_value(),
                     Typed::from_const(Type).into_type(),
                 )
                 .to_type(),
@@ -662,8 +662,8 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypedThunk>,
-                kts_r: HashMap<Label, TypedThunk>,
+                kts_l: HashMap<Label, TypedValue>,
+                kts_r: HashMap<Label, TypedValue>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::outer_join;
 
@@ -671,8 +671,8 @@ fn type_last_layer(
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
                 let combine = |k: &Label,
-                               inner_l: &TypedThunk,
-                               inner_r: &TypedThunk|
+                               inner_l: &TypedValue,
+                               inner_r: &TypedValue|
                  -> Result<Typed, TypeError> {
                     match (inner_l.to_valuef(), inner_r.to_valuef()) {
                         (
@@ -690,7 +690,7 @@ fn type_last_layer(
                 let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
                     |l| Ok(l.to_type()),
                     |r| Ok(r.to_type()),
-                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+                    |k: &Label, l: &TypedValue, r: &TypedValue| {
                         combine(k, l, r)
                     },
                     &kts_l,
@@ -735,8 +735,8 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypedThunk>,
-                kts_r: HashMap<Label, TypedThunk>,
+                kts_l: HashMap<Label, TypedValue>,
+                kts_r: HashMap<Label, TypedValue>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::intersection_with_key;
 
@@ -744,8 +744,8 @@ fn type_last_layer(
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
                 let combine = |k: &Label,
-                               kts_l_inner: &TypedThunk,
-                               kts_r_inner: &TypedThunk|
+                               kts_l_inner: &TypedValue,
+                               kts_r_inner: &TypedValue|
                  -> Result<Typed, TypeError> {
                     match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) {
                         (
@@ -761,7 +761,7 @@ fn type_last_layer(
                 };
 
                 let kts = intersection_with_key(
-                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+                    |k: &Label, l: &TypedValue, r: &TypedValue| {
                         combine(k, l, r)
                     },
                     &kts_l,
@@ -989,8 +989,8 @@ fn type_last_layer(
             }
 
             Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
-                    ValueF::RecordType(new_kts).into_thunk(),
+                Typed::from_value_and_type(
+                    ValueF::RecordType(new_kts).into_value(),
                     trecord.get_type()?.into_owned(),
                 )
                 .to_type(),