Merge pull request #118 from Nadrieril/clarify-types

Clarify naming and file organization

29 files changed, 1003 insertions, 1048 deletions

diff --git a/dhall/src/semantics/error/mod.rs b/dhall/src/error/mod.rs
index 1288c12..1288c12 100644
--- a/dhall/src/semantics/error/mod.rs
+++ b/dhall/src/error/mod.rs
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 0991375..12660b4 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -12,5 +12,6 @@
 
 mod tests;
 
+pub mod error;
 pub mod semantics;
 pub mod syntax;
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index d150e56..f755f72 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,10 +1,10 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
+use crate::error::TypeError;
 use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
-use crate::semantics::error::TypeError;
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -39,7 +39,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            Value::from_valuef_and_type(ValueF::Var(newvar), t)
+                            Value::from_kind_and_type(ValueKind::Var(newvar), t)
                         }
                         CtxItem::Replaced(v) => v,
                     });
diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs
index 08213f7..90d74ea 100644
--- a/dhall/src/semantics/core/mod.rs
+++ b/dhall/src/semantics/core/mod.rs
@@ -1,4 +1,3 @@
 pub mod context;
 pub mod value;
-pub mod valuef;
 pub mod var;
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6e6739f..ca7c4bc 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -1,125 +1,93 @@
 use std::cell::{Ref, RefCell, RefMut};
+use std::collections::HashMap;
 use std::rc::Rc;
 
+use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TypecheckContext;
-use crate::semantics::core::valuef::ValueF;
-use crate::semantics::core::var::{AlphaVar, Shift, Subst};
-use crate::semantics::error::{TypeError, TypeMessage};
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::semantics::phase::{NormalizedExpr, Typed};
-use crate::syntax::{Builtin, Const, Span};
+use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
+use crate::semantics::to_expr;
+use crate::syntax::{
+    Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+    NaiveDouble, Natural, Span,
+};
 
-#[derive(Debug, Clone, Copy)]
-pub(crate) enum Form {
-    /// No constraints; expression may not be normalized at all.
-    Unevaled,
-    /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
-    /// not be normalized. This means that the first constructor of the contained ValueF is the first
-    /// constructor of the final Normal Form (NF).
-    WHNF,
-    /// Normal Form, i.e. completely normalized.
-    /// 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.
-    NF,
-}
-use Form::{Unevaled, NF, WHNF};
+use self::Form::{Unevaled, NF, WHNF};
+
+/// 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.
+/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+#[derive(Clone)]
+pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
-/// Partially normalized value.
 /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 /// Invariant: if `form` is `NF`, `value` must be fully normalized
 #[derive(Debug)]
 struct ValueInternal {
     form: Form,
-    value: ValueF,
+    kind: ValueKind,
     /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
     span: Span,
 }
 
-/// 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.
-#[derive(Clone)]
-pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
-
-#[derive(Copy, Clone)]
-/// Controls conversion from `Value` to `Expr`
-pub(crate) struct ToExprOptions {
-    /// Whether to convert all variables to `_`
-    pub(crate) alpha: bool,
-    /// Whether to normalize before converting
-    pub(crate) normalize: bool,
+#[derive(Debug, Clone, Copy)]
+pub(crate) enum Form {
+    /// No constraints; expression may not be normalized at all.
+    Unevaled,
+    /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
+    /// not be normalized. This means that the first constructor of the contained ValueKind is the first
+    /// constructor of the final Normal Form (NF).
+    WHNF,
+    /// Normal Form, i.e. completely normalized.
+    /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the
+    /// ValueKind 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.
+    NF,
 }
 
-impl ValueInternal {
-    fn into_value(self) -> Value {
-        Value(Rc::new(RefCell::new(self)))
-    }
-    fn as_valuef(&self) -> &ValueF {
-        &self.value
-    }
-
-    fn normalize_whnf(&mut self) {
-        take_mut::take_or_recover(
-            self,
-            // Dummy value in case the other closure panics
-            || ValueInternal {
-                form: Unevaled,
-                value: ValueF::Const(Const::Type),
-                ty: None,
-                span: Span::Artificial,
-            },
-            |vint| match (&vint.form, &vint.ty) {
-                (Unevaled, Some(ty)) => ValueInternal {
-                    form: WHNF,
-                    value: normalize_whnf(vint.value, &ty),
-                    ty: vint.ty,
-                    span: vint.span,
-                },
-                // `value` is `Sort`
-                (Unevaled, None) => ValueInternal {
-                    form: NF,
-                    value: ValueF::Const(Const::Sort),
-                    ty: None,
-                    span: vint.span,
-                },
-                // Already in WHNF
-                (WHNF, _) | (NF, _) => vint,
-            },
-        )
-    }
-    fn normalize_nf(&mut self) {
-        match self.form {
-            Unevaled => {
-                self.normalize_whnf();
-                self.normalize_nf();
-            }
-            WHNF => {
-                self.value.normalize_mut();
-                self.form = NF;
-            }
-            // Already in NF
-            NF => {}
-        }
-    }
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind {
+    /// Closures
+    Lam(AlphaLabel, Value, Value),
+    Pi(AlphaLabel, Value, Value),
+    // Invariant: in whnf, the evaluation must not be able to progress further.
+    AppliedBuiltin(Builtin, Vec<Value>),
 
-    fn get_type(&self) -> Result<&Value, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t),
-            None => {
-                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
-            }
-        }
-    }
+    Var(AlphaVar),
+    Const(Const),
+    BoolLit(bool),
+    NaturalLit(Natural),
+    IntegerLit(Integer),
+    DoubleLit(NaiveDouble),
+    EmptyOptionalLit(Value),
+    NEOptionalLit(Value),
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
+    EmptyListLit(Value),
+    NEListLit(Vec<Value>),
+    RecordType(HashMap<Label, Value>),
+    RecordLit(HashMap<Label, Value>),
+    UnionType(HashMap<Label, Option<Value>>),
+    UnionConstructor(Label, HashMap<Label, Option<Value>>),
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
+    // contiguous text values must be merged.
+    TextLit(Vec<InterpolatedTextContents<Value>>),
+    Equivalence(Value, Value),
+    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+    PartialExpr(ExprKind<Value, Normalized>),
 }
 
 impl Value {
-    fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
+    fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
         ValueInternal {
             form,
-            value,
+            kind,
             ty: Some(ty),
             span,
         }
@@ -128,23 +96,23 @@ impl Value {
     pub(crate) fn const_sort() -> Value {
         ValueInternal {
             form: NF,
-            value: ValueF::Const(Const::Sort),
+            kind: ValueKind::Const(Const::Sort),
             ty: None,
             span: Span::Artificial,
         }
         .into_value()
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
         Value::new(v, Unevaled, t, Span::Artificial)
     }
-    pub(crate) fn from_valuef_and_type_and_span(
-        v: ValueF,
+    pub(crate) fn from_kind_and_type_and_span(
+        v: ValueKind,
         t: Value,
         span: Span,
     ) -> Value {
         Value::new(v, Unevaled, t, span)
     }
-    pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+    pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
         Value::new(v, WHNF, t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
@@ -160,7 +128,7 @@ impl Value {
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.as_whnf() {
-            ValueF::Const(c) => Some(*c),
+            ValueKind::Const(c) => Some(*c),
             _ => None,
         }
     }
@@ -174,30 +142,31 @@ impl Value {
     fn as_internal_mut(&self) -> RefMut<ValueInternal> {
         self.0.borrow_mut()
     }
-    /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an
+    /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an
     /// unevaled PartialExpr. You probably want to use `as_whnf`.
-    fn as_valuef(&self) -> Ref<ValueF> {
-        Ref::map(self.as_internal(), ValueInternal::as_valuef)
+    pub(crate) fn as_kind(&self) -> Ref<ValueKind> {
+        Ref::map(self.as_internal(), ValueInternal::as_kind)
     }
     /// This is what you want if you want to pattern-match on the value.
     /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
     /// panics.
-    pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
+    pub(crate) fn as_whnf(&self) -> Ref<ValueKind> {
         self.normalize_whnf();
-        self.as_valuef()
+        self.as_kind()
     }
 
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        if opts.normalize {
-            self.normalize_whnf();
-        }
-        self.as_valuef().to_expr(opts)
-    }
-    pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(
+        &self,
+        opts: to_expr::ToExprOptions,
+    ) -> NormalizedExpr {
+        to_expr::value_to_expr(self, opts)
+    }
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
         self.as_whnf().clone()
     }
     /// Before discarding type information, check that it matches the expected return type.
-    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
         self.check_type(ty);
         self.to_whnf_ignore_type()
     }
@@ -234,13 +203,13 @@ impl Value {
 
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
-            ValueF::Pi(x, t, e) => {
+            ValueKind::Pi(x, t, e) => {
                 v.check_type(t);
                 e.subst_shift(&x.into(), &v)
             }
             _ => unreachable!("Internal type error"),
         };
-        Value::from_valuef_and_type_whnf(
+        Value::from_kind_and_type_whnf(
             apply_any(self.clone(), v, &body_t),
             body_t,
         )
@@ -265,6 +234,156 @@ impl Value {
     }
 }
 
+impl ValueInternal {
+    fn into_value(self) -> Value {
+        Value(Rc::new(RefCell::new(self)))
+    }
+    fn as_kind(&self) -> &ValueKind {
+        &self.kind
+    }
+
+    fn normalize_whnf(&mut self) {
+        take_mut::take_or_recover(
+            self,
+            // Dummy value in case the other closure panics
+            || ValueInternal {
+                form: Unevaled,
+                kind: ValueKind::Const(Const::Type),
+                ty: None,
+                span: Span::Artificial,
+            },
+            |vint| match (&vint.form, &vint.ty) {
+                (Unevaled, Some(ty)) => ValueInternal {
+                    form: WHNF,
+                    kind: normalize_whnf(vint.kind, &ty),
+                    ty: vint.ty,
+                    span: vint.span,
+                },
+                // `value` is `Sort`
+                (Unevaled, None) => ValueInternal {
+                    form: NF,
+                    kind: ValueKind::Const(Const::Sort),
+                    ty: None,
+                    span: vint.span,
+                },
+                // Already in WHNF
+                (WHNF, _) | (NF, _) => vint,
+            },
+        )
+    }
+    fn normalize_nf(&mut self) {
+        match self.form {
+            Unevaled => {
+                self.normalize_whnf();
+                self.normalize_nf();
+            }
+            WHNF => {
+                self.kind.normalize_mut();
+                self.form = NF;
+            }
+            // Already in NF
+            NF => {}
+        }
+    }
+
+    fn get_type(&self) -> Result<&Value, TypeError> {
+        match &self.ty {
+            Some(t) => Ok(t),
+            None => {
+                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+            }
+        }
+    }
+}
+
+impl ValueKind {
+    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+        Value::from_kind_and_type(self, t)
+    }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(
+        &self,
+        opts: to_expr::ToExprOptions,
+    ) -> NormalizedExpr {
+        to_expr::kind_to_expr(self, opts)
+    }
+
+    pub(crate) fn normalize_mut(&mut self) {
+        match self {
+            ValueKind::Var(_)
+            | ValueKind::Const(_)
+            | ValueKind::BoolLit(_)
+            | ValueKind::NaturalLit(_)
+            | ValueKind::IntegerLit(_)
+            | ValueKind::DoubleLit(_) => {}
+
+            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+                tth.normalize_mut();
+            }
+
+            ValueKind::NEOptionalLit(th) => {
+                th.normalize_mut();
+            }
+            ValueKind::Lam(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueKind::Pi(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueKind::AppliedBuiltin(_, args) => {
+                for x in args.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::NEListLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::RecordType(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::UnionLit(_, v, kts) => {
+                v.normalize_mut();
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::TextLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.map_mut(Value::normalize_mut);
+                }
+            }
+            ValueKind::Equivalence(x, y) => {
+                x.normalize_mut();
+                y.normalize_mut();
+            }
+            ValueKind::PartialExpr(e) => {
+                e.map_mut(Value::normalize_mut);
+            }
+        }
+    }
+
+    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+        ValueKind::AppliedBuiltin(b, vec![])
+    }
+}
+
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -275,19 +394,84 @@ impl Shift for ValueInternal {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(ValueInternal {
             form: self.form,
-            value: self.value.shift(delta, var)?,
+            kind: self.kind.shift(delta, var)?,
             ty: self.ty.shift(delta, var)?,
             span: self.span.clone(),
         })
     }
 }
 
+impl Shift for ValueKind {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(match self {
+            ValueKind::Lam(x, t, e) => ValueKind::Lam(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            ValueKind::AppliedBuiltin(b, args) => {
+                ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?)
+            }
+            ValueKind::Pi(x, t, e) => ValueKind::Pi(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+            ValueKind::Const(c) => ValueKind::Const(*c),
+            ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+            ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+            ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+            ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+            ValueKind::EmptyOptionalLit(tth) => {
+                ValueKind::EmptyOptionalLit(tth.shift(delta, var)?)
+            }
+            ValueKind::NEOptionalLit(th) => {
+                ValueKind::NEOptionalLit(th.shift(delta, var)?)
+            }
+            ValueKind::EmptyListLit(tth) => {
+                ValueKind::EmptyListLit(tth.shift(delta, var)?)
+            }
+            ValueKind::NEListLit(elts) => {
+                ValueKind::NEListLit(elts.shift(delta, var)?)
+            }
+            ValueKind::RecordLit(kvs) => {
+                ValueKind::RecordLit(kvs.shift(delta, var)?)
+            }
+            ValueKind::RecordType(kvs) => {
+                ValueKind::RecordType(kvs.shift(delta, var)?)
+            }
+            ValueKind::UnionType(kts) => {
+                ValueKind::UnionType(kts.shift(delta, var)?)
+            }
+            ValueKind::UnionConstructor(x, kts) => {
+                ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+            }
+            ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+                x.clone(),
+                v.shift(delta, var)?,
+                kts.shift(delta, var)?,
+            ),
+            ValueKind::TextLit(elts) => {
+                ValueKind::TextLit(elts.shift(delta, var)?)
+            }
+            ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+                x.shift(delta, var)?,
+                y.shift(delta, var)?,
+            ),
+            ValueKind::PartialExpr(e) => {
+                ValueKind::PartialExpr(e.shift(delta, var)?)
+            }
+        })
+    }
+}
+
 impl Subst<Value> for Value {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match &*self.as_valuef() {
+        match &*self.as_kind() {
             // If the var matches, we can just reuse the provided value instead of copying it.
             // We also check that the types match, if in debug mode.
-            ValueF::Var(v) if v == var => {
+            ValueKind::Var(v) if v == var => {
                 if let Ok(self_ty) = self.get_type() {
                     val.check_type(&self_ty.subst_shift(var, val));
                 }
@@ -303,13 +487,80 @@ impl Subst<Value> for ValueInternal {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
-            value: self.value.subst_shift(var, val),
+            kind: self.kind.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
             span: self.span.clone(),
         }
     }
 }
 
+impl Subst<Value> for ValueKind {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+        match self {
+            ValueKind::AppliedBuiltin(b, args) => {
+                ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val))
+            }
+            ValueKind::PartialExpr(e) => {
+                ValueKind::PartialExpr(e.subst_shift(var, val))
+            }
+            ValueKind::TextLit(elts) => {
+                ValueKind::TextLit(elts.subst_shift(var, val))
+            }
+            ValueKind::Lam(x, t, e) => ValueKind::Lam(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+            ),
+            ValueKind::Pi(x, t, e) => ValueKind::Pi(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+            ),
+            ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
+            ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+            ValueKind::Const(c) => ValueKind::Const(*c),
+            ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+            ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+            ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+            ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+            ValueKind::EmptyOptionalLit(tth) => {
+                ValueKind::EmptyOptionalLit(tth.subst_shift(var, val))
+            }
+            ValueKind::NEOptionalLit(th) => {
+                ValueKind::NEOptionalLit(th.subst_shift(var, val))
+            }
+            ValueKind::EmptyListLit(tth) => {
+                ValueKind::EmptyListLit(tth.subst_shift(var, val))
+            }
+            ValueKind::NEListLit(elts) => {
+                ValueKind::NEListLit(elts.subst_shift(var, val))
+            }
+            ValueKind::RecordLit(kvs) => {
+                ValueKind::RecordLit(kvs.subst_shift(var, val))
+            }
+            ValueKind::RecordType(kvs) => {
+                ValueKind::RecordType(kvs.subst_shift(var, val))
+            }
+            ValueKind::UnionType(kts) => {
+                ValueKind::UnionType(kts.subst_shift(var, val))
+            }
+            ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor(
+                x.clone(),
+                kts.subst_shift(var, val),
+            ),
+            ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+                x.clone(),
+                v.subst_shift(var, val),
+                kts.subst_shift(var, val),
+            ),
+            ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+                x.subst_shift(var, val),
+                y.subst_shift(var, val),
+            ),
+        }
+    }
+}
+
 // TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
@@ -321,11 +572,11 @@ impl std::cmp::Eq for Value {}
 impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
-        if let ValueF::Const(c) = &vint.value {
+        if let ValueKind::Const(c) = &vint.kind {
             write!(fmt, "{:?}", c)
         } else {
             let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
-            x.field("value", &vint.value);
+            x.field("value", &vint.kind);
             if let Some(ty) = vint.ty.as_ref() {
                 x.field("type", &ty);
             } else {
diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs
deleted file mode 100644
index 73c715a..0000000
--- a/dhall/src/semantics/core/valuef.rs
+++ /dev/null
@@ -1,323 +0,0 @@
-use std::collections::HashMap;
-
-use crate::semantics::core::value::{ToExprOptions, Value};
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::{Normalized, NormalizedExpr};
-use crate::syntax;
-use crate::syntax::{
-    Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural,
-};
-
-/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
-/// normalized on-demand.
-/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
-/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
-/// recursively normalize as needed.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueF {
-    /// Closures
-    Lam(AlphaLabel, Value, Value),
-    Pi(AlphaLabel, Value, Value),
-    // Invariant: in whnf, 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(Value),
-    NEOptionalLit(Value),
-    // EmptyListLit(t) means `[] : List t`, not `[] : t`
-    EmptyListLit(Value),
-    NEListLit(Vec<Value>),
-    RecordType(HashMap<Label, Value>),
-    RecordLit(HashMap<Label, Value>),
-    UnionType(HashMap<Label, Option<Value>>),
-    UnionConstructor(Label, HashMap<Label, Option<Value>>),
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
-    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
-    // contiguous text values must be merged.
-    TextLit(Vec<InterpolatedTextContents<Value>>),
-    Equivalence(Value, Value),
-    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
-    PartialExpr(ExprF<Value, Normalized>),
-}
-
-impl ValueF {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_valuef_and_type(self, t)
-    }
-
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        match self {
-            ValueF::Lam(x, t, e) => rc(ExprF::Lam(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueF::AppliedBuiltin(b, args) => args
-                .iter()
-                .map(|v| v.to_expr(opts))
-                .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
-            ValueF::Pi(x, t, e) => rc(ExprF::Pi(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.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.to_expr(opts),
-            )),
-            ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
-            ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
-                rc(ExprF::Builtin(Builtin::List)),
-                n.to_expr(opts),
-            )))),
-            ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.iter().map(|n| n.to_expr(opts)).collect(),
-            )),
-            ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::RecordType(kts) => rc(ExprF::RecordType(
-                kts.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::UnionType(kts) => rc(ExprF::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
-                    })
-                    .collect(),
-            )),
-            ValueF::UnionConstructor(l, kts) => rc(ExprF::Field(
-                ValueF::UnionType(kts.clone()).to_expr(opts),
-                l.clone(),
-            )),
-            ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
-                ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
-                v.to_expr(opts),
-            )),
-            ValueF::TextLit(elts) => rc(ExprF::TextLit(
-                elts.iter()
-                    .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
-                syntax::BinOp::Equivalence,
-                x.to_expr(opts),
-                y.to_expr(opts),
-            )),
-            ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
-        }
-    }
-
-    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() {
-                    x.map_mut(Value::normalize_mut);
-                }
-            }
-            ValueF::Equivalence(x, y) => {
-                x.normalize_mut();
-                y.normalize_mut();
-            }
-            ValueF::PartialExpr(e) => {
-                e.map_mut(Value::normalize_mut);
-            }
-        }
-    }
-
-    pub(crate) 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<Value> for ValueF {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match self {
-            ValueF::AppliedBuiltin(b, args) => {
-                ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
-            }
-            ValueF::PartialExpr(e) => {
-                ValueF::PartialExpr(e.subst_shift(var, val))
-            }
-            ValueF::TextLit(elts) => {
-                ValueF::TextLit(elts.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_whnf_ignore_type(),
-            ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
-            ValueF::Const(c) => ValueF::Const(*c),
-            ValueF::BoolLit(b) => ValueF::BoolLit(*b),
-            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/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 184a372..1548713 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,6 +1,6 @@
 use std::collections::HashMap;
 
-use crate::syntax::{ExprF, InterpolatedTextContents, Label, V};
+use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V};
 
 /// Stores a pair of variables: a normal one and one
 /// that corresponds to the alpha-normalized version of the first one.
@@ -12,7 +12,7 @@ pub struct AlphaVar {
 }
 
 // Exactly like a Label, but equality returns always true.
-// This is so that ValueF equality is exactly alpha-equivalence.
+// This is so that ValueKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct AlphaLabel(Label);
 
@@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> {
     }
 }
 
-impl<T: Shift, E: Clone> Shift for ExprF<T, E> {
+impl<T: Shift, E: Clone> Shift for ExprKind<T, E> {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(self.traverse_ref_with_special_handling_of_binders(
             |v| Ok(v.shift(delta, var)?),
@@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
     }
 }
 
-impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> {
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> {
     fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
         self.map_ref_with_special_handling_of_binders(
             |v| v.subst_shift(var, val),
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 9d2e462..1eeef86 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,3 +1,3 @@
 pub mod core;
-pub mod error;
 pub mod phase;
+pub mod to_expr;
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 752c257..b22120d 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -1,10 +1,11 @@
 use std::fmt::Display;
 use std::path::Path;
 
-use crate::semantics::core::value::{ToExprOptions, Value};
-use crate::semantics::core::valuef::ValueF;
+use crate::error::{EncodeError, Error, ImportError, TypeError};
+use crate::semantics::core::value::Value;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
-use crate::semantics::error::{EncodeError, Error, ImportError, TypeError};
+use crate::semantics::to_expr::ToExprOptions;
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Const, Expr};
 use resolve::ImportRoot;
@@ -76,13 +77,6 @@ impl Resolved {
 
 impl Typed {
     /// Reduce an expression to its normal form, performing beta reduction
-    ///
-    /// `normalize` does not type-check the expression.  You may want to type-check
-    /// expressions before normalizing them since normalization can convert an
-    /// ill-typed expression into a well-typed expression.
-    ///
-    /// However, `normalize` will not fail if the expression is ill-typed and will
-    /// leave ill-typed sub-expressions unevaluated.
     pub fn normalize(mut self) -> Normalized {
         self.normalize_mut();
         Normalized(self)
@@ -91,8 +85,8 @@ impl Typed {
     pub(crate) fn from_const(c: Const) -> Self {
         Typed(Value::from_const(c))
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
-        Typed(Value::from_valuef_and_type(v, t.into_value()))
+    pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self {
+        Typed(Value::from_kind_and_type(v, t.into_value()))
     }
     pub(crate) fn from_value(th: Value) -> Self {
         Typed(th)
@@ -101,18 +95,22 @@ impl Typed {
         Typed::from_const(Const::Type)
     }
 
+    /// Converts a value back to the corresponding AST expression.
     pub(crate) fn to_expr(&self) -> NormalizedExpr {
         self.0.to_expr(ToExprOptions {
             alpha: false,
             normalize: false,
         })
     }
+    /// Converts a value back to the corresponding AST expression, beta-normalizing in the process.
     pub fn normalize_to_expr(&self) -> NormalizedExpr {
         self.0.to_expr(ToExprOptions {
             alpha: false,
             normalize: true,
         })
     }
+    /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the
+    /// process.
     pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
         self.0.to_expr(ToExprOptions {
             alpha: true,
@@ -148,8 +146,8 @@ impl Typed {
     pub fn make_record_type(
         kts: impl Iterator<Item = (String, Typed)>,
     ) -> Self {
-        Typed::from_valuef_and_type(
-            ValueF::RecordType(
+        Typed::from_kind_and_type(
+            ValueKind::RecordType(
                 kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
             ),
             Typed::const_type(),
@@ -158,8 +156,8 @@ impl Typed {
     pub fn make_union_type(
         kts: impl Iterator<Item = (String, Option<Typed>)>,
     ) -> Self {
-        Typed::from_valuef_and_type(
-            ValueF::UnionType(
+        Typed::from_kind_and_type(
+            ValueKind::UnionType(
                 kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
                     .collect(),
             ),
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 81c3ce1..d81a910 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,14 +1,14 @@
 use std::collections::HashMap;
 
 use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::semantics::phase::Normalized;
 use crate::syntax;
 use crate::syntax::Const::Type;
 use crate::syntax::{
-    BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
-    NaiveDouble,
+    BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents,
+    Label, NaiveDouble,
 };
 
 // Ad-hoc macro to help construct closures
@@ -19,7 +19,7 @@ macro_rules! make_closure {
             Label::from(stringify!($var)).into(),
             $n
         );
-        ValueF::Var(var)
+        ValueKind::Var(var)
             .into_value_with_type(make_closure!($($ty)*))
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
@@ -28,9 +28,9 @@ macro_rules! make_closure {
         let ty = make_closure!($($ty)*);
         let body = make_closure!($($body)*);
         let body_ty = body.get_type_not_sort();
-        let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+        let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty)
             .into_value_with_type(Value::from_const(Type));
-        ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+        ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty)
     }};
     (Natural) => {
         Value::from_builtin(Builtin::Natural)
@@ -43,14 +43,14 @@ macro_rules! make_closure {
         let v = make_closure!($($rest)*);
         let v_type = v.get_type_not_sort();
         let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
-        ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+        ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type)
     }};
     (1 + $($rest:tt)*) => {
-        ValueF::PartialExpr(ExprF::BinOp(
+        ValueKind::PartialExpr(ExprKind::BinOp(
             syntax::BinOp::NaturalPlus,
             make_closure!($($rest)*),
-            Value::from_valuef_and_type(
-                ValueF::NaturalLit(1),
+            Value::from_kind_and_type(
+                ValueKind::NaturalLit(1),
                 make_closure!(Natural)
             ),
         )).into_value_with_type(
@@ -61,9 +61,9 @@ macro_rules! make_closure {
         let head = make_closure!($($head)*);
         let tail = make_closure!($($tail)*);
         let list_type = tail.get_type_not_sort();
-        ValueF::PartialExpr(ExprF::BinOp(
+        ValueKind::PartialExpr(ExprKind::BinOp(
             syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![head])
+            ValueKind::NEListLit(vec![head])
                 .into_value_with_type(list_type.clone()),
             tail,
         )).into_value_with_type(list_type)
@@ -75,13 +75,13 @@ pub(crate) fn apply_builtin(
     b: Builtin,
     args: Vec<Value>,
     ty: &Value,
-) -> ValueF {
+) -> ValueKind {
     use syntax::Builtin::*;
-    use ValueF::*;
+    use ValueKind::*;
 
     // Small helper enum
     enum Ret<'a> {
-        ValueF(ValueF),
+        ValueKind(ValueKind),
         Value(Value),
         // For applications that can return a function, it's important to keep the remaining
         // arguments to apply them to the resulting function.
@@ -90,38 +90,38 @@ pub(crate) fn apply_builtin(
     }
 
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+        (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
         (NaturalIsZero, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
             _ => Ret::DoneAsIs,
         },
         (NaturalEven, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
             _ => Ret::DoneAsIs,
         },
         (NaturalOdd, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
             _ => Ret::DoneAsIs,
         },
         (NaturalToInteger, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+            NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalShow, [n]) => match &*n.as_whnf() {
-            NaturalLit(n) => {
-                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
-                    n.to_string(),
-                )]))
+        (NaturalShow, [n]) => {
+            match &*n.as_whnf() {
+                NaturalLit(n) => Ret::ValueKind(TextLit(vec![
+                    InterpolatedTextContents::Text(n.to_string()),
+                ])),
+                _ => Ret::DoneAsIs,
             }
-            _ => Ret::DoneAsIs,
-        },
+        }
         (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
             (NaturalLit(a), NaturalLit(b)) => {
-                Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
+                Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
             }
             (NaturalLit(0), _) => Ret::Value(b.clone()),
-            (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
-            _ if a == b => Ret::ValueF(NaturalLit(0)),
+            (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+            _ if a == b => Ret::ValueKind(NaturalLit(0)),
             _ => Ret::DoneAsIs,
         },
         (IntegerShow, [n]) => match &*n.as_whnf() {
@@ -131,24 +131,24 @@ pub(crate) fn apply_builtin(
                 } else {
                     format!("+{}", n)
                 };
-                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
+                Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)]))
             }
             _ => Ret::DoneAsIs,
         },
         (IntegerToDouble, [n]) => match &*n.as_whnf() {
             IntegerLit(n) => {
-                Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+                Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
             }
             _ => Ret::DoneAsIs,
         },
-        (DoubleShow, [n]) => match &*n.as_whnf() {
-            DoubleLit(n) => {
-                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
-                    n.to_string(),
-                )]))
+        (DoubleShow, [n]) => {
+            match &*n.as_whnf() {
+                DoubleLit(n) => Ret::ValueKind(TextLit(vec![
+                    InterpolatedTextContents::Text(n.to_string()),
+                ])),
+                _ => Ret::DoneAsIs,
             }
-            _ => Ret::DoneAsIs,
-        },
+        }
         (TextShow, [v]) => match &*v.as_whnf() {
             TextLit(elts) => {
                 match elts.as_slice() {
@@ -158,7 +158,7 @@ pub(crate) fn apply_builtin(
                         let txt: InterpolatedText<Normalized> =
                             std::iter::empty().collect();
                         let s = txt.to_string();
-                        Ret::ValueF(TextLit(vec![
+                        Ret::ValueKind(TextLit(vec![
                             InterpolatedTextContents::Text(s),
                         ]))
                     }
@@ -172,7 +172,7 @@ pub(crate) fn apply_builtin(
                             ))
                             .collect();
                         let s = txt.to_string();
-                        Ret::ValueF(TextLit(vec![
+                        Ret::ValueKind(TextLit(vec![
                             InterpolatedTextContents::Text(s),
                         ]))
                     }
@@ -182,28 +182,28 @@ pub(crate) fn apply_builtin(
             _ => Ret::DoneAsIs,
         },
         (ListLength, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
-            NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+            EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
+            NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
             _ => Ret::DoneAsIs,
         },
         (ListHead, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => {
-                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
+                Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
             _ => Ret::DoneAsIs,
         },
         (ListLast, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
                 xs.iter().rev().next().unwrap().clone(),
             )),
             _ => Ret::DoneAsIs,
         },
         (ListReverse, [_, l]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
+            EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
             NEListLit(xs) => {
-                Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+                Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
             }
             _ => Ret::DoneAsIs,
         },
@@ -222,7 +222,7 @@ pub(crate) fn apply_builtin(
                     let mut kts = HashMap::new();
                     kts.insert("index".into(), Value::from_builtin(Natural));
                     kts.insert("value".into(), t.clone());
-                    let t = Value::from_valuef_and_type(
+                    let t = Value::from_kind_and_type(
                         RecordType(kts),
                         Value::from_const(Type),
                     );
@@ -237,7 +237,7 @@ pub(crate) fn apply_builtin(
                                     let mut kvs = HashMap::new();
                                     kvs.insert(
                                         "index".into(),
-                                        Value::from_valuef_and_type(
+                                        Value::from_kind_and_type(
                                             NaturalLit(i),
                                             Value::from_builtin(
                                                 Builtin::Natural,
@@ -245,7 +245,7 @@ pub(crate) fn apply_builtin(
                                         ),
                                     );
                                     kvs.insert("value".into(), e.clone());
-                                    Value::from_valuef_and_type(
+                                    Value::from_kind_and_type(
                                         RecordLit(kvs),
                                         t.clone(),
                                     )
@@ -254,14 +254,14 @@ pub(crate) fn apply_builtin(
                         ),
                         _ => unreachable!(),
                     };
-                    Ret::ValueF(list)
+                    Ret::ValueKind(list)
                 }
                 _ => Ret::DoneAsIs,
             }
         }
         (ListBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
-            ValueF::AppliedBuiltin(ListFold, args) => {
+            ValueKind::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
                     Ret::Value(args[1].clone())
                 } else {
@@ -303,7 +303,7 @@ pub(crate) fn apply_builtin(
         },
         (OptionalBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
-            ValueF::AppliedBuiltin(OptionalFold, args) => {
+            ValueKind::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
                     Ret::Value(args[1].clone())
                 } else {
@@ -338,7 +338,7 @@ pub(crate) fn apply_builtin(
         },
         (NaturalBuild, [f]) => match &*f.as_whnf() {
             // fold/build fusion
-            ValueF::AppliedBuiltin(NaturalFold, args) => {
+            ValueKind::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
                     Ret::Value(args[0].clone())
                 } else {
@@ -375,7 +375,7 @@ pub(crate) fn apply_builtin(
         _ => Ret::DoneAsIs,
     };
     match ret {
-        Ret::ValueF(v) => v,
+        Ret::ValueKind(v) => v,
         Ret::Value(v) => v.to_whnf_check_type(ty),
         Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
@@ -388,23 +388,23 @@ pub(crate) fn apply_builtin(
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => {
+        ValueKind::Lam(x, _, e) => {
             e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
         }
-        ValueF::AppliedBuiltin(b, args) => {
+        ValueKind::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args, ty)
         }
-        ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone())
+        ValueKind::UnionConstructor(l, kts) => {
+            ValueKind::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
-            ValueF::PartialExpr(ExprF::App(f, a))
+            ValueKind::PartialExpr(ExprKind::App(f, a))
         }
     }
 }
@@ -426,7 +426,7 @@ pub(crate) fn squash_textlit(
                 Expr(e) => {
                     let e_borrow = e.as_whnf();
                     match &*e_borrow {
-                        ValueF::TextLit(elts2) => {
+                        ValueKind::TextLit(elts2) => {
                             inner(elts2.iter().cloned(), crnt_str, ret)
                         }
                         _ => {
@@ -479,10 +479,10 @@ where
 
 // Small helper enum to avoid repetition
 enum Ret<'a> {
-    ValueF(ValueF),
+    ValueKind(ValueKind),
     Value(Value),
     ValueRef(&'a Value),
-    Expr(ExprF<Value, Normalized>),
+    Expr(ExprKind<Value, Normalized>),
 }
 
 fn apply_binop<'a>(
@@ -496,7 +496,7 @@ fn apply_binop<'a>(
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use ValueF::{
+    use ValueKind::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
     };
@@ -505,58 +505,58 @@ fn apply_binop<'a>(
     Some(match (o, &*x_borrow, &*y_borrow) {
         (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, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
+        (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
         (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
-        (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
+        (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
+        (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
         (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)),
+        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
+        (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
         (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)),
+        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
+        (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
 
         (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
         (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
         (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueF(NaturalLit(x + y))
+            Ret::ValueKind(NaturalLit(x + y))
         }
-        (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+        (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
+        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
         (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
         (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
         (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueF(NaturalLit(x * y))
+            Ret::ValueKind(NaturalLit(x * y))
         }
 
         (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(),
-        )),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
+            NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
+        ),
 
         (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(
+        (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit(
             squash_textlit(x.iter().chain(y.iter()).cloned()),
         )),
         (TextAppend, TextLit(x), _) => {
             use std::iter::once;
             let y = InterpolatedTextContents::Expr(y.clone());
-            Ret::ValueF(TextLit(squash_textlit(
+            Ret::ValueKind(TextLit(squash_textlit(
                 x.iter().cloned().chain(once(y)),
             )))
         }
         (TextAppend, _, TextLit(y)) => {
             use std::iter::once;
             let x = InterpolatedTextContents::Expr(x.clone());
-            Ret::ValueF(TextLit(squash_textlit(
+            Ret::ValueKind(TextLit(squash_textlit(
                 once(x).chain(y.iter().cloned()),
             )))
         }
@@ -573,7 +573,7 @@ fn apply_binop<'a>(
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            Ret::ValueF(RecordLit(kvs))
+            Ret::ValueKind(RecordLit(kvs))
         }
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
@@ -589,8 +589,8 @@ fn apply_binop<'a>(
                 _ => unreachable!("Internal type error"),
             };
             let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_valuef_and_type(
-                    ValueF::PartialExpr(ExprF::BinOp(
+                Ok(Value::from_kind_and_type(
+                    ValueKind::PartialExpr(ExprKind::BinOp(
                         RecursiveRecordMerge,
                         v1.clone(),
                         v2.clone(),
@@ -598,7 +598,7 @@ fn apply_binop<'a>(
                     kts.get(k).expect("Internal type error").clone(),
                 ))
             })?;
-            Ret::ValueF(RecordLit(kvs))
+            Ret::ValueKind(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
@@ -610,46 +610,46 @@ fn apply_binop<'a>(
 }
 
 pub(crate) fn normalize_one_layer(
-    expr: ExprF<Value, Normalized>,
+    expr: ExprKind<Value, Normalized>,
     ty: &Value,
-) -> ValueF {
-    use ValueF::{
+) -> ValueKind {
+    use ValueKind::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
         NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
         UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
-        ExprF::Import(_) => unreachable!(
+        ExprKind::Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
         // Those cases have already been completely handled in the typechecking phase (using
         // `RetWhole`), so they won't appear here.
-        ExprF::Lam(_, _, _)
-        | ExprF::Pi(_, _, _)
-        | ExprF::Let(_, _, _, _)
-        | ExprF::Embed(_)
-        | ExprF::Const(_)
-        | ExprF::Builtin(_)
-        | ExprF::Var(_)
-        | ExprF::Annot(_, _)
-        | ExprF::RecordType(_)
-        | ExprF::UnionType(_) => {
+        ExprKind::Lam(_, _, _)
+        | ExprKind::Pi(_, _, _)
+        | ExprKind::Let(_, _, _, _)
+        | ExprKind::Embed(_)
+        | ExprKind::Const(_)
+        | ExprKind::Builtin(_)
+        | ExprKind::Var(_)
+        | ExprKind::Annot(_, _)
+        | ExprKind::RecordType(_)
+        | ExprKind::UnionType(_) => {
             unreachable!("This case should have been handled in typecheck")
         }
-        ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::App(v, a) => Ret::Value(v.app(a)),
-        ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
-        ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
-        ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
-        ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
-        ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
-        ExprF::EmptyListLit(ref t) => {
+        ExprKind::Assert(_) => Ret::Expr(expr),
+        ExprKind::App(v, a) => Ret::Value(v.app(a)),
+        ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
+        ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
+        ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
+        ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+        ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+        ExprKind::EmptyListLit(ref t) => {
             // Check if the type is of the form `List x`
             let t_borrow = t.as_whnf();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::ValueF(EmptyListLit(args[0].clone()))
+                    Ret::ValueKind(EmptyListLit(args[0].clone()))
                 }
                 _ => {
                     drop(t_borrow);
@@ -657,23 +657,23 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprF::NEListLit(elts) => {
-            Ret::ValueF(NEListLit(elts.into_iter().collect()))
+        ExprKind::NEListLit(elts) => {
+            Ret::ValueKind(NEListLit(elts.into_iter().collect()))
         }
-        ExprF::RecordLit(kvs) => {
-            Ret::ValueF(RecordLit(kvs.into_iter().collect()))
+        ExprKind::RecordLit(kvs) => {
+            Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
         }
-        ExprF::TextLit(elts) => {
+        ExprKind::TextLit(elts) => {
             use InterpolatedTextContents::Expr;
             let elts: Vec<_> = squash_textlit(elts.into_iter());
             // Simplify bare interpolation
             if let [Expr(th)] = elts.as_slice() {
                 Ret::Value(th.clone())
             } else {
-                Ret::ValueF(TextLit(elts))
+                Ret::ValueKind(TextLit(elts))
             }
         }
-        ExprF::BoolIf(ref b, ref e1, ref e2) => {
+        ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             let b_borrow = b.as_whnf();
             match &*b_borrow {
                 BoolLit(true) => Ret::ValueRef(e1),
@@ -695,18 +695,18 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
 
-        ExprF::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::ValueF(RecordLit(HashMap::new()))
+        ExprKind::Projection(_, ref ls) if ls.is_empty() => {
+            Ret::ValueKind(RecordLit(HashMap::new()))
         }
-        ExprF::Projection(ref v, ref ls) => {
+        ExprKind::Projection(ref v, ref ls) => {
             let v_borrow = v.as_whnf();
             match &*v_borrow {
-                RecordLit(kvs) => Ret::ValueF(RecordLit(
+                RecordLit(kvs) => Ret::ValueKind(RecordLit(
                     ls.iter()
                         .filter_map(|l| {
                             kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -719,7 +719,7 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprF::Field(ref v, ref l) => {
+        ExprKind::Field(ref v, ref l) => {
             let v_borrow = v.as_whnf();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
@@ -730,7 +730,7 @@ pub(crate) fn normalize_one_layer(
                     }
                 },
                 UnionType(kts) => {
-                    Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
+                    Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
                 }
                 _ => {
                     drop(v_borrow);
@@ -738,11 +738,11 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprF::ProjectionByExpr(_, _) => {
+        ExprKind::ProjectionByExpr(_, _) => {
             unimplemented!("selection by expression")
         }
 
-        ExprF::Merge(ref handlers, ref variant, _) => {
+        ExprKind::Merge(ref handlers, ref variant, _) => {
             let handlers_borrow = handlers.as_whnf();
             let variant_borrow = variant.as_whnf();
             match (&*handlers_borrow, &*variant_borrow) {
@@ -769,24 +769,24 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprF::ToMap(_, _) => unimplemented!("toMap"),
+        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
     };
 
     match ret {
-        Ret::ValueF(v) => v,
+        Ret::ValueKind(v) => v,
         Ret::Value(v) => v.to_whnf_check_type(ty),
         Ret::ValueRef(v) => v.to_whnf_check_type(ty),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr),
+        Ret::Expr(expr) => ValueKind::PartialExpr(expr),
     }
 }
 
-/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
+/// Normalize a ValueKind into WHNF
+pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
     match v {
-        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
-        ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
-        ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter()))
+        ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+        ValueKind::PartialExpr(e) => normalize_one_layer(e, ty),
+        ValueKind::TextLit(elts) => {
+            ValueKind::TextLit(squash_textlit(elts.into_iter()))
         }
         // All other cases are already in WHNF
         v => v,
diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs
index 4c8ad7b..00db422 100644
--- a/dhall/src/semantics/phase/parse.rs
+++ b/dhall/src/semantics/phase/parse.rs
@@ -2,7 +2,7 @@ use std::fs::File;
 use std::io::Read;
 use std::path::Path;
 
-use crate::semantics::error::Error;
+use crate::error::Error;
 use crate::semantics::phase::resolve::ImportRoot;
 use crate::semantics::phase::Parsed;
 use crate::syntax::binary;
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index 86dc7ae..cc4a024 100644
--- a/dhall/src/semantics/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 use std::path::{Path, PathBuf};
 
-use crate::semantics::error::{Error, ImportError};
+use crate::error::{Error, ImportError};
 use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
 use crate::syntax;
 use crate::syntax::{FilePath, ImportLocation, URL};
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 59380a3..c439f74 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,16 +1,17 @@
 use std::cmp::max;
 use std::collections::HashMap;
 
+use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TypecheckContext;
 use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{Shift, Subst};
-use crate::semantics::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
 use crate::syntax;
 use crate::syntax::{
-    Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
+    Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
+    UnspannedExpr,
 };
 
 fn tck_pi_type(
@@ -39,8 +40,8 @@ fn tck_pi_type(
 
     let k = function_check(ka, kb);
 
-    Ok(Value::from_valuef_and_type(
-        ValueF::Pi(x.into(), tx, te),
+    Ok(Value::from_kind_and_type(
+        ValueKind::Pi(x.into(), tx, te),
         Value::from_const(k),
     ))
 }
@@ -71,8 +72,8 @@ fn tck_record_type(
         };
     }
 
-    Ok(Value::from_valuef_and_type(
-        ValueF::RecordType(new_kts),
+    Ok(Value::from_kind_and_type(
+        ValueKind::RecordType(new_kts),
         Value::from_const(k),
     ))
 }
@@ -116,8 +117,8 @@ where
     // an union type with only unary variants also has type Type
     let k = k.unwrap_or(Const::Type);
 
-    Ok(Value::from_valuef_and_type(
-        ValueF::UnionType(new_kts),
+    Ok(Value::from_kind_and_type(
+        ValueKind::UnionType(new_kts),
         Value::from_const(k),
     ))
 }
@@ -131,42 +132,42 @@ fn function_check(a: Const, b: Const) -> Const {
 }
 
 pub(crate) fn const_to_value(c: Const) -> Value {
-    let v = ValueF::Const(c);
+    let v = ValueKind::Const(c);
     match c {
         Const::Type => {
-            Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+            Value::from_kind_and_type(v, const_to_value(Const::Kind))
         }
         Const::Kind => {
-            Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+            Value::from_kind_and_type(v, const_to_value(Const::Sort))
         }
         Const::Sort => Value::const_sort(),
     }
 }
 
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
     Expr::new(x, Span::Artificial)
 }
 
 // Ad-hoc macro to help construct the types of builtins
 macro_rules! make_type {
-    (Type) => { ExprF::Const(Const::Type) };
-    (Bool) => { ExprF::Builtin(Builtin::Bool) };
-    (Natural) => { ExprF::Builtin(Builtin::Natural) };
-    (Integer) => { ExprF::Builtin(Builtin::Integer) };
-    (Double) => { ExprF::Builtin(Builtin::Double) };
-    (Text) => { ExprF::Builtin(Builtin::Text) };
+    (Type) => { ExprKind::Const(Const::Type) };
+    (Bool) => { ExprKind::Builtin(Builtin::Bool) };
+    (Natural) => { ExprKind::Builtin(Builtin::Natural) };
+    (Integer) => { ExprKind::Builtin(Builtin::Integer) };
+    (Double) => { ExprKind::Builtin(Builtin::Double) };
+    (Text) => { ExprKind::Builtin(Builtin::Text) };
     ($var:ident) => {
-        ExprF::Var(syntax::V(stringify!($var).into(), 0))
+        ExprKind::Var(syntax::V(stringify!($var).into(), 0))
     };
     (Optional $ty:ident) => {
-        ExprF::App(
-            rc(ExprF::Builtin(Builtin::Optional)),
+        ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::Optional)),
             rc(make_type!($ty))
         )
     };
     (List $($rest:tt)*) => {
-        ExprF::App(
-            rc(ExprF::Builtin(Builtin::List)),
+        ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::List)),
             rc(make_type!($($rest)*))
         )
     };
@@ -178,24 +179,24 @@ macro_rules! make_type {
                 rc(make_type!($ty)),
             );
         )*
-        ExprF::RecordType(kts)
+        ExprKind::RecordType(kts)
     }};
     ($ty:ident -> $($rest:tt)*) => {
-        ExprF::Pi(
+        ExprKind::Pi(
             "_".into(),
             rc(make_type!($ty)),
             rc(make_type!($($rest)*))
         )
     };
     (($($arg:tt)*) -> $($rest:tt)*) => {
-        ExprF::Pi(
+        ExprKind::Pi(
             "_".into(),
             rc(make_type!($($arg)*)),
             rc(make_type!($($rest)*))
         )
     };
     (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ExprF::Pi(
+        ExprKind::Pi(
             stringify!($var).into(),
             rc(make_type!($($ty)*)),
             rc(make_type!($($rest)*))
@@ -290,8 +291,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     let ctx = TypecheckContext::new();
-    Value::from_valuef_and_type(
-        ValueF::from_builtin(b),
+    Value::from_kind_and_type(
+        ValueKind::from_builtin(b),
         type_with(&ctx, type_of_builtin(b)).unwrap(),
     )
 }
@@ -304,7 +305,7 @@ fn type_with(
     ctx: &TypecheckContext,
     e: Expr<Normalized>,
 ) -> Result<Value, TypeError> {
-    use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+    use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
     let span = e.span();
 
     Ok(match e.as_ref() {
@@ -313,8 +314,8 @@ fn type_with(
             let ctx2 = ctx.insert_type(var, annot.clone());
             let body = type_with(&ctx2, body.clone())?;
             let body_type = body.get_type()?;
-            Value::from_valuef_and_type(
-                ValueF::Lam(var.clone().into(), annot.clone(), body),
+            Value::from_kind_and_type(
+                ValueKind::Lam(var.clone().into(), annot.clone(), body),
                 tck_pi_type(ctx, var.clone(), annot, body_type)?,
             )
         }
@@ -359,13 +360,13 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: ExprF<Value, Normalized>,
+    e: ExprKind<Value, Normalized>,
     span: Span,
 ) -> Result<Value, TypeError> {
     use syntax::BinOp::*;
     use syntax::Builtin::*;
     use syntax::Const::Type;
-    use syntax::ExprF::*;
+    use syntax::ExprKind::*;
     use TypeMessage::*;
     let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
 
@@ -389,7 +390,7 @@ fn type_last_layer(
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
             let (x, tx, tb) = match &*tf_borrow {
-                ValueF::Pi(x, tx, tb) => (x, tx, tb),
+                ValueKind::Pi(x, tx, tb) => (x, tx, tb),
                 _ => return mkerr(NotAFunction(f.clone())),
             };
             if &a.get_type()? != tx {
@@ -406,8 +407,8 @@ fn type_last_layer(
         }
         Assert(t) => {
             match &*t.as_whnf() {
-                ValueF::Equivalence(x, y) if x == y => {}
-                ValueF::Equivalence(x, y) => {
+                ValueKind::Equivalence(x, y) if x == y => {}
+                ValueKind::Equivalence(x, y) => {
                     return mkerr(AssertMismatch(x.clone(), y.clone()))
                 }
                 _ => return mkerr(AssertMustTakeEquivalence),
@@ -415,7 +416,7 @@ fn type_last_layer(
             RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
-            if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) {
+            if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
                 return mkerr(InvalidPredicate(x.clone()));
             }
 
@@ -435,7 +436,7 @@ fn type_last_layer(
         }
         EmptyListLit(t) => {
             match &*t.as_whnf() {
-                ValueF::AppliedBuiltin(syntax::Builtin::List, args)
+                ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
                     if args.len() == 1 => {}
                 _ => return mkerr(InvalidListType(t.clone())),
             }
@@ -482,7 +483,7 @@ fn type_last_layer(
         )?),
         Field(r, x) => {
             match &*r.get_type()?.as_whnf() {
-                ValueF::RecordType(kts) => match kts.get(&x) {
+                ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => {
                         RetTypeOnly(tth.clone())
                     },
@@ -492,7 +493,7 @@ fn type_last_layer(
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
                     match &*r.as_whnf() {
-                        ValueF::UnionType(kts) => match kts.get(&x) {
+                        ValueKind::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(t)) => {
                                 RetTypeOnly(
@@ -553,14 +554,14 @@ fn type_last_layer(
             // Extract the LHS record type
             let l_type_borrow = l_type.as_whnf();
             let kts_x = match &*l_type_borrow {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr(MustCombineRecord(l.clone())),
             };
 
             // Extract the RHS record type
             let r_type_borrow = r_type.as_whnf();
             let kts_y = match &*r_type_borrow {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr(MustCombineRecord(r.clone())),
             };
 
@@ -578,7 +579,7 @@ fn type_last_layer(
         }
         BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
             ctx,
-            ExprF::BinOp(
+            ExprKind::BinOp(
                 RecursiveRecordTypeMerge,
                 l.get_type()?,
                 r.get_type()?,
@@ -589,7 +590,7 @@ fn type_last_layer(
             // Extract the LHS record type
             let borrow_l = l.as_whnf();
             let kts_x = match &*borrow_l {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => {
                     return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
                 }
@@ -598,7 +599,7 @@ fn type_last_layer(
             // Extract the RHS record type
             let borrow_r = r.as_whnf();
             let kts_y = match &*borrow_r {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => {
                     return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
                 }
@@ -612,7 +613,7 @@ fn type_last_layer(
                 |_, l: &Value, r: &Value| {
                     type_last_layer(
                         ctx,
-                        ExprF::BinOp(
+                        ExprKind::BinOp(
                             RecursiveRecordTypeMerge,
                             l.clone(),
                             r.clone(),
@@ -626,7 +627,7 @@ fn type_last_layer(
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
-                ValueF::AppliedBuiltin(List, _) => {}
+                ValueKind::AppliedBuiltin(List, _) => {}
                 _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
             }
 
@@ -648,8 +649,8 @@ fn type_last_layer(
                 return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
             }
 
-            RetWhole(Value::from_valuef_and_type(
-                ValueF::Equivalence(l.clone(), r.clone()),
+            RetWhole(Value::from_kind_and_type(
+                ValueKind::Equivalence(l.clone(), r.clone()),
                 Value::from_const(Type),
             ))
         }
@@ -684,14 +685,14 @@ fn type_last_layer(
             let record_type = record.get_type()?;
             let record_borrow = record_type.as_whnf();
             let handlers = match &*record_borrow {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
             };
 
             let union_type = union.get_type()?;
             let union_borrow = union_type.as_whnf();
             let variants = match &*union_borrow {
-                ValueF::UnionType(kts) => kts,
+                ValueKind::UnionType(kts) => kts,
                 _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
             };
 
@@ -703,7 +704,7 @@ fn type_last_layer(
                         Some(Some(variant_type)) => {
                             let handler_type_borrow = handler_type.as_whnf();
                             let (x, tx, tb) = match &*handler_type_borrow {
-                                ValueF::Pi(x, tx, tb) => (x, tx, tb),
+                                ValueKind::Pi(x, tx, tb) => (x, tx, tb),
                                 _ => {
                                     return mkerr(NotAFunction(
                                         handler_type.clone(),
@@ -765,7 +766,7 @@ fn type_last_layer(
             let record_type = record.get_type()?;
             let record_type_borrow = record_type.as_whnf();
             let kts = match &*record_type_borrow {
-                ValueF::RecordType(kts) => kts,
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr(ProjectionMustBeRecord),
             };
 
@@ -777,8 +778,8 @@ fn type_last_layer(
                 };
             }
 
-            RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::RecordType(new_kts),
+            RetTypeOnly(Value::from_kind_and_type(
+                ValueKind::RecordType(new_kts),
                 record_type.get_type()?,
             ))
         }
@@ -786,8 +787,8 @@ fn type_last_layer(
     };
 
     Ok(match ret {
-        RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
-            ValueF::PartialExpr(e),
+        RetTypeOnly(typ) => Value::from_kind_and_type_and_span(
+            ValueKind::PartialExpr(e),
             typ,
             span,
         ),
@@ -806,5 +807,5 @@ pub(crate) fn typecheck_with(
     expr: Expr<Normalized>,
     ty: Expr<Normalized>,
 ) -> Result<Value, TypeError> {
-    typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
+    typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
 }
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
new file mode 100644
index 0000000..b21fb29
--- /dev/null
+++ b/dhall/src/semantics/to_expr.rs
@@ -0,0 +1,105 @@
+use crate::semantics::core::value::Value;
+use crate::semantics::core::value::ValueKind;
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::NormalizedExpr;
+use crate::syntax;
+use crate::syntax::{Builtin, ExprKind};
+
+#[derive(Copy, Clone)]
+/// Controls conversion from `Value` to `Expr`
+pub(crate) struct ToExprOptions {
+    /// Whether to convert all variables to `_`
+    pub(crate) alpha: bool,
+    /// Whether to normalize before converting
+    pub(crate) normalize: bool,
+}
+
+/// Converts a value back to the corresponding AST expression.
+pub(crate) fn value_to_expr(
+    val: &Value,
+    opts: ToExprOptions,
+) -> NormalizedExpr {
+    if opts.normalize {
+        val.normalize_whnf();
+    }
+    val.as_kind().to_expr(opts)
+}
+
+/// Converts a value back to the corresponding AST expression.
+pub(crate) fn kind_to_expr(
+    kind: &ValueKind,
+    opts: ToExprOptions,
+) -> NormalizedExpr {
+    match kind {
+        ValueKind::Lam(x, t, e) => rc(ExprKind::Lam(
+            x.to_label_maybe_alpha(opts.alpha),
+            t.to_expr(opts),
+            e.to_expr(opts),
+        )),
+        ValueKind::AppliedBuiltin(b, args) => args
+            .iter()
+            .map(|v| v.to_expr(opts))
+            .fold(rc(ExprKind::Builtin(*b)), |acc, v| {
+                rc(ExprKind::App(acc, v))
+            }),
+        ValueKind::Pi(x, t, e) => rc(ExprKind::Pi(
+            x.to_label_maybe_alpha(opts.alpha),
+            t.to_expr(opts),
+            e.to_expr(opts),
+        )),
+        ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))),
+        ValueKind::Const(c) => rc(ExprKind::Const(*c)),
+        ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)),
+        ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)),
+        ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)),
+        ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)),
+        ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App(
+            rc(ExprKind::Builtin(Builtin::OptionalNone)),
+            n.to_expr(opts),
+        )),
+        ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))),
+        ValueKind::EmptyListLit(n) => {
+            rc(ExprKind::EmptyListLit(rc(ExprKind::App(
+                rc(ExprKind::Builtin(Builtin::List)),
+                n.to_expr(opts),
+            ))))
+        }
+        ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(
+            elts.iter().map(|n| n.to_expr(opts)).collect(),
+        )),
+        ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit(
+            kvs.iter()
+                .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+                .collect(),
+        )),
+        ValueKind::RecordType(kts) => rc(ExprKind::RecordType(
+            kts.iter()
+                .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+                .collect(),
+        )),
+        ValueKind::UnionType(kts) => rc(ExprKind::UnionType(
+            kts.iter()
+                .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts))))
+                .collect(),
+        )),
+        ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field(
+            ValueKind::UnionType(kts.clone()).to_expr(opts),
+            l.clone(),
+        )),
+        ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App(
+            ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
+            v.to_expr(opts),
+        )),
+        ValueKind::TextLit(elts) => rc(ExprKind::TextLit(
+            elts.iter()
+                .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
+                .collect(),
+        )),
+        ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp(
+            syntax::BinOp::Equivalence,
+            x.to_expr(opts),
+            y.to_expr(opts),
+        )),
+        ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
+    }
+}
diff --git a/dhall/src/syntax/core/expr.rs b/dhall/src/syntax/ast/expr.rs
index 5b9f401..48c48d8 100644
--- a/dhall/src/syntax/core/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,51 +1,15 @@
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
-use crate::syntax::visitor::{self, ExprFMutVisitor, ExprFVisitor};
+use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
 use crate::syntax::*;
 
 pub type Integer = isize;
 pub type Natural = usize;
 pub type Double = NaiveDouble;
 
-pub fn trivial_result<T>(x: Result<T, !>) -> T {
-    match x {
-        Ok(x) => x,
-        Err(e) => e,
-    }
-}
-
 /// Double with bitwise equality
 #[derive(Debug, Copy, Clone)]
 pub struct NaiveDouble(f64);
 
-impl PartialEq for NaiveDouble {
-    fn eq(&self, other: &Self) -> bool {
-        self.0.to_bits() == other.0.to_bits()
-    }
-}
-
-impl Eq for NaiveDouble {}
-
-impl std::hash::Hash for NaiveDouble {
-    fn hash<H>(&self, state: &mut H)
-    where
-        H: std::hash::Hasher,
-    {
-        self.0.to_bits().hash(state)
-    }
-}
-
-impl From<f64> for NaiveDouble {
-    fn from(x: f64) -> Self {
-        NaiveDouble(x)
-    }
-}
-
-impl From<NaiveDouble> for f64 {
-    fn from(x: NaiveDouble) -> f64 {
-        x.0
-    }
-}
-
 /// Constants for a pure type system
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Const {
@@ -62,18 +26,6 @@ pub enum Const {
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct V<Label>(pub Label, pub usize);
 
-// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
-    fn from(x: Label) -> V<Label> {
-        V(x, 0)
-    }
-}
-impl<'a> From<&'a Label> for V<Label> {
-    fn from(x: &'a Label) -> V<Label> {
-        V(x.clone(), 0)
-    }
-}
-
 // Definition order must match precedence order for
 // pretty-printing to work correctly
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -142,33 +94,19 @@ pub enum Builtin {
 
 // Each node carries an annotation.
 #[derive(Debug, Clone)]
-pub struct Expr<Embed>(Box<(RawExpr<Embed>, Span)>);
-
-pub type RawExpr<Embed> = ExprF<Expr<Embed>, Embed>;
-
-impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> {
-    fn eq(&self, other: &Self) -> bool {
-        self.0.as_ref().0 == other.0.as_ref().0
-    }
+pub struct Expr<Embed> {
+    kind: Box<ExprKind<Expr<Embed>, Embed>>,
+    span: Span,
 }
 
-impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {}
-
-impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> {
-    fn hash<H>(&self, state: &mut H)
-    where
-        H: std::hash::Hasher,
-    {
-        (self.0).0.hash(state)
-    }
-}
+pub type UnspannedExpr<Embed> = ExprKind<Expr<Embed>, Embed>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum ExprF<SubExpr, Embed> {
+pub enum ExprKind<SubExpr, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
@@ -231,12 +169,12 @@ pub enum ExprF<SubExpr, Embed> {
     Embed(Embed),
 }
 
-impl<SE, E> ExprF<SE, E> {
+impl<SE, E> ExprKind<SE, E> {
     pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>(
         &'a self,
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         visit_under_binder: impl FnOnce(&'a Label, &'a SE) -> Result<SE2, Err>,
-    ) -> Result<ExprF<SE2, E>, Err>
+    ) -> Result<ExprKind<SE2, E>, Err>
     where
         E: Clone,
     {
@@ -250,7 +188,7 @@ impl<SE, E> ExprF<SE, E> {
     fn traverse_ref<'a, SE2, Err>(
         &'a self,
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
-    ) -> Result<ExprF<SE2, E>, Err>
+    ) -> Result<ExprKind<SE2, E>, Err>
     where
         E: Clone,
     {
@@ -268,7 +206,7 @@ impl<SE, E> ExprF<SE, E> {
         &'a self,
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         mut map_under_binder: impl FnMut(&'a Label, &'a SE) -> SE2,
-    ) -> ExprF<SE2, E>
+    ) -> ExprKind<SE2, E>
     where
         E: Clone,
     {
@@ -281,7 +219,7 @@ impl<SE, E> ExprF<SE, E> {
     pub fn map_ref<'a, SE2>(
         &'a self,
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
-    ) -> ExprF<SE2, E>
+    ) -> ExprKind<SE2, E>
     where
         E: Clone,
     {
@@ -294,22 +232,25 @@ impl<SE, E> ExprF<SE, E> {
 }
 
 impl<E> Expr<E> {
-    pub fn as_ref(&self) -> &RawExpr<E> {
-        &self.0.as_ref().0
-    }
-    pub fn as_mut(&mut self) -> &mut RawExpr<E> {
-        &mut self.0.as_mut().0
+    pub fn as_ref(&self) -> &UnspannedExpr<E> {
+        &self.kind
     }
     pub fn span(&self) -> Span {
-        self.0.as_ref().1.clone()
+        self.span.clone()
     }
 
-    pub fn new(x: RawExpr<E>, n: Span) -> Self {
-        Expr(Box::new((x, n)))
+    pub fn new(kind: UnspannedExpr<E>, span: Span) -> Self {
+        Expr {
+            kind: Box::new(kind),
+            span,
+        }
     }
 
-    pub fn rewrap<E2>(&self, x: RawExpr<E2>) -> Expr<E2> {
-        Expr(Box::new((x, (self.0).1.clone())))
+    pub fn rewrap<E2>(&self, kind: UnspannedExpr<E2>) -> Expr<E2> {
+        Expr {
+            kind: Box::new(kind),
+            span: self.span.clone(),
+        }
     }
 
     pub fn traverse_resolve_mut<Err, F1>(
@@ -320,21 +261,21 @@ impl<E> Expr<E> {
         E: Clone,
         F1: FnMut(Import<Expr<E>>) -> Result<E, Err>,
     {
-        match self.as_mut() {
-            ExprF::BinOp(BinOp::ImportAlt, l, r) => {
-                let garbage_expr = ExprF::BoolLit(false);
+        match self.kind.as_mut() {
+            ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
+                let garbage_expr = ExprKind::BoolLit(false);
                 let new_self = if l.traverse_resolve_mut(f).is_ok() {
                     l
                 } else {
                     r.traverse_resolve_mut(f)?;
                     r
                 };
-                *self.as_mut() =
-                    std::mem::replace(new_self.as_mut(), garbage_expr);
+                *self.kind =
+                    std::mem::replace(new_self.kind.as_mut(), garbage_expr);
             }
             _ => {
-                self.as_mut().traverse_mut(|e| e.traverse_resolve_mut(f))?;
-                if let ExprF::Import(import) = self.as_mut() {
+                self.kind.traverse_mut(|e| e.traverse_resolve_mut(f))?;
+                if let ExprKind::Import(import) = self.kind.as_mut() {
                     let garbage_import = Import {
                         mode: ImportMode::Code,
                         location: ImportLocation::Missing,
@@ -342,7 +283,7 @@ impl<E> Expr<E> {
                     };
                     // Move out of &mut import
                     let import = std::mem::replace(import, garbage_import);
-                    *self.as_mut() = ExprF::Embed(f(import)?);
+                    *self.kind = ExprKind::Embed(f(import)?);
                 }
             }
         }
@@ -350,16 +291,6 @@ impl<E> Expr<E> {
     }
 }
 
-/// Add an isize to an usize
-/// Returns `None` on over/underflow
-fn add_ui(u: usize, i: isize) -> Option<usize> {
-    Some(if i < 0 {
-        u.checked_sub(i.checked_neg()? as usize)?
-    } else {
-        u.checked_add(i as usize)?
-    })
-}
-
 impl<Label: PartialEq + Clone> V<Label> {
     pub fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
         let V(x, n) = var;
@@ -375,3 +306,73 @@ impl<Label: PartialEq + Clone> V<Label> {
         self.shift(-1, &V(x.clone(), 0))
     }
 }
+
+pub fn trivial_result<T>(x: Result<T, !>) -> T {
+    match x {
+        Ok(x) => x,
+        Err(e) => e,
+    }
+}
+
+/// Add an isize to an usize
+/// Returns `None` on over/underflow
+fn add_ui(u: usize, i: isize) -> Option<usize> {
+    Some(if i < 0 {
+        u.checked_sub(i.checked_neg()? as usize)?
+    } else {
+        u.checked_add(i as usize)?
+    })
+}
+
+impl PartialEq for NaiveDouble {
+    fn eq(&self, other: &Self) -> bool {
+        self.0.to_bits() == other.0.to_bits()
+    }
+}
+
+impl Eq for NaiveDouble {}
+
+impl std::hash::Hash for NaiveDouble {
+    fn hash<H>(&self, state: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        self.0.to_bits().hash(state)
+    }
+}
+
+impl From<f64> for NaiveDouble {
+    fn from(x: f64) -> Self {
+        NaiveDouble(x)
+    }
+}
+
+impl From<NaiveDouble> for f64 {
+    fn from(x: NaiveDouble) -> f64 {
+        x.0
+    }
+}
+
+/// This is only for the specific `Label` type, not generic
+impl From<Label> for V<Label> {
+    fn from(x: Label) -> V<Label> {
+        V(x, 0)
+    }
+}
+
+impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> {
+    fn eq(&self, other: &Self) -> bool {
+        self.kind == other.kind
+    }
+}
+
+impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {}
+
+impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> {
+    fn hash<H>(&self, state: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        self.kind.hash(state)
+    }
+}
diff --git a/dhall/src/syntax/core/import.rs b/dhall/src/syntax/ast/import.rs
index da3e99b..da3e99b 100644
--- a/dhall/src/syntax/core/import.rs
+++ b/dhall/src/syntax/ast/import.rs
diff --git a/dhall/src/syntax/core/label.rs b/dhall/src/syntax/ast/label.rs
index 43c3f53..43c3f53 100644
--- a/dhall/src/syntax/core/label.rs
+++ b/dhall/src/syntax/ast/label.rs
diff --git a/dhall/src/syntax/core/map.rs b/dhall/src/syntax/ast/map.rs
index c4c6126..c4c6126 100644
--- a/dhall/src/syntax/core/map.rs
+++ b/dhall/src/syntax/ast/map.rs
diff --git a/dhall/src/syntax/core/mod.rs b/dhall/src/syntax/ast/mod.rs
index 66bf229..1950154 100644
--- a/dhall/src/syntax/core/mod.rs
+++ b/dhall/src/syntax/ast/mod.rs
@@ -8,6 +8,5 @@ mod span;
 pub use span::*;
 mod text;
 pub use text::*;
-pub mod context;
 pub mod map;
 pub mod visitor;
diff --git a/dhall/src/syntax/core/span.rs b/dhall/src/syntax/ast/span.rs
index f9c7008..f9c7008 100644
--- a/dhall/src/syntax/core/span.rs
+++ b/dhall/src/syntax/ast/span.rs
diff --git a/dhall/src/syntax/core/text.rs b/dhall/src/syntax/ast/text.rs
index fb390ee..fb390ee 100644
--- a/dhall/src/syntax/core/text.rs
+++ b/dhall/src/syntax/ast/text.rs
diff --git a/dhall/src/syntax/core/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index b76d037..b557995 100644
--- a/dhall/src/syntax/core/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -1,7 +1,7 @@
 use crate::syntax::*;
 use std::iter::FromIterator;
 
-/// A visitor trait that can be used to traverse `ExprF`s. We need this pattern so that Rust lets
+/// A visitor trait that can be used to traverse `ExprKind`s. We need this pattern so that Rust lets
 /// us have as much mutability as we can.
 /// For example, `traverse_ref_with_special_handling_of_binders` cannot be made using only
 /// `traverse_ref`, because `traverse_ref` takes a `FnMut` so we would need to pass multiple
@@ -9,7 +9,7 @@ use std::iter::FromIterator;
 /// preventing exactly this ! So we have to be more clever. The visitor pattern allows us to have
 /// only one mutable thing the whole time: the visitor itself. The visitor can then carry around
 /// multiple closures or just one, and Rust is ok with either. See for example TraverseRefVisitor.
-pub trait ExprFVisitor<'a, SE1, SE2, E1, E2>: Sized {
+pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized {
     type Error;
 
     fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error>;
@@ -25,14 +25,14 @@ pub trait ExprFVisitor<'a, SE1, SE2, E1, E2>: Sized {
 
     fn visit(
         self,
-        input: &'a ExprF<SE1, E1>,
-    ) -> Result<ExprF<SE2, E2>, Self::Error> {
+        input: &'a ExprKind<SE1, E1>,
+    ) -> Result<ExprKind<SE2, E2>, Self::Error> {
         visit_ref(self, input)
     }
 }
 
-/// Like `ExprFVisitor`, but by mutable reference
-pub trait ExprFMutVisitor<'a, SE, E>: Sized {
+/// Like `ExprKindVisitor`, but by mutable reference
+pub trait ExprKindMutVisitor<'a, SE, E>: Sized {
     type Error;
 
     fn visit_subexpr(&mut self, subexpr: &'a mut SE)
@@ -49,17 +49,17 @@ pub trait ExprFMutVisitor<'a, SE, E>: Sized {
         self.visit_subexpr(subexpr)
     }
 
-    fn visit(self, input: &'a mut ExprF<SE, E>) -> Result<(), Self::Error> {
+    fn visit(self, input: &'a mut ExprKind<SE, E>) -> Result<(), Self::Error> {
         visit_mut(self, input)
     }
 }
 
 fn visit_ref<'a, V, SE1, SE2, E1, E2>(
     mut v: V,
-    input: &'a ExprF<SE1, E1>,
-) -> Result<ExprF<SE2, E2>, V::Error>
+    input: &'a ExprKind<SE1, E1>,
+) -> Result<ExprKind<SE2, E2>, V::Error>
 where
-    V: ExprFVisitor<'a, SE1, SE2, E1, E2>,
+    V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
 {
     fn vec<'a, T, U, Err, F: FnMut(&'a T) -> Result<U, Err>>(
         x: &'a [T],
@@ -83,7 +83,7 @@ where
     where
         SE1: 'a,
         T: FromIterator<(Label, SE2)>,
-        V: ExprFVisitor<'a, SE1, SE2, E1, E2>,
+        V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
     {
         x.into_iter()
             .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
@@ -96,7 +96,7 @@ where
     where
         SE1: 'a,
         T: FromIterator<(Label, Option<SE2>)>,
-        V: ExprFVisitor<'a, SE1, SE2, E1, E2>,
+        V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
     {
         x.into_iter()
             .map(|(k, x)| {
@@ -111,7 +111,7 @@ where
             .collect()
     }
 
-    use crate::syntax::ExprF::*;
+    use crate::syntax::ExprKind::*;
     Ok(match input {
         Var(v) => Var(v.clone()),
         Lam(l, t, e) => {
@@ -172,14 +172,14 @@ where
 
 fn visit_mut<'a, V, SE, E>(
     mut v: V,
-    input: &'a mut ExprF<SE, E>,
+    input: &'a mut ExprKind<SE, E>,
 ) -> Result<(), V::Error>
 where
-    V: ExprFMutVisitor<'a, SE, E>,
+    V: ExprKindMutVisitor<'a, SE, E>,
 {
     fn vec<'a, V, SE, E>(v: &mut V, x: &'a mut Vec<SE>) -> Result<(), V::Error>
     where
-        V: ExprFMutVisitor<'a, SE, E>,
+        V: ExprKindMutVisitor<'a, SE, E>,
     {
         for x in x {
             v.visit_subexpr(x)?;
@@ -191,7 +191,7 @@ where
         x: &'a mut Option<SE>,
     ) -> Result<(), V::Error>
     where
-        V: ExprFMutVisitor<'a, SE, E>,
+        V: ExprKindMutVisitor<'a, SE, E>,
     {
         if let Some(x) = x {
             v.visit_subexpr(x)?;
@@ -204,7 +204,7 @@ where
     ) -> Result<(), V::Error>
     where
         SE: 'a,
-        V: ExprFMutVisitor<'a, SE, E>,
+        V: ExprKindMutVisitor<'a, SE, E>,
     {
         for (_, x) in x {
             v.visit_subexpr(x)?;
@@ -217,7 +217,7 @@ where
     ) -> Result<(), V::Error>
     where
         SE: 'a,
-        V: ExprFMutVisitor<'a, SE, E>,
+        V: ExprKindMutVisitor<'a, SE, E>,
     {
         for (_, x) in x {
             opt(&mut v, x)?;
@@ -225,7 +225,7 @@ where
         Ok(())
     }
 
-    use crate::syntax::ExprF::*;
+    use crate::syntax::ExprKind::*;
     match input {
         Var(_) | Const(_) | Builtin(_) | BoolLit(_) | NaturalLit(_)
         | IntegerLit(_) | DoubleLit(_) => {}
@@ -293,7 +293,7 @@ pub struct TraverseRefWithBindersVisitor<F1, F2> {
     pub visit_under_binder: F2,
 }
 
-impl<'a, SE, E, SE2, Err, F1, F2> ExprFVisitor<'a, SE, SE2, E, E>
+impl<'a, SE, E, SE2, Err, F1, F2> ExprKindVisitor<'a, SE, SE2, E, E>
     for TraverseRefWithBindersVisitor<F1, F2>
 where
     SE: 'a,
@@ -322,7 +322,7 @@ pub struct TraverseRefVisitor<F1> {
     pub visit_subexpr: F1,
 }
 
-impl<'a, SE, E, SE2, Err, F1> ExprFVisitor<'a, SE, SE2, E, E>
+impl<'a, SE, E, SE2, Err, F1> ExprKindVisitor<'a, SE, SE2, E, E>
     for TraverseRefVisitor<F1>
 where
     SE: 'a,
@@ -343,7 +343,8 @@ pub struct TraverseMutVisitor<F1> {
     pub visit_subexpr: F1,
 }
 
-impl<'a, SE, E, Err, F1> ExprFMutVisitor<'a, SE, E> for TraverseMutVisitor<F1>
+impl<'a, SE, E, Err, F1> ExprKindMutVisitor<'a, SE, E>
+    for TraverseMutVisitor<F1>
 where
     SE: 'a,
     E: 'a,
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 46c9921..254ab07 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -2,12 +2,13 @@ use itertools::Itertools;
 use serde_cbor::value::value as cbor;
 use std::iter::FromIterator;
 
-use crate::semantics::error::DecodeError;
+use crate::error::DecodeError;
 use crate::semantics::phase::DecodedExpr;
 use crate::syntax;
 use crate::syntax::{
-    Expr, ExprF, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
-    Integer, InterpolatedText, Label, Natural, RawExpr, Scheme, Span, URL, V,
+    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
+    Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr,
+    URL, V,
 };
 
 pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
@@ -18,17 +19,17 @@ pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
 }
 
 // Should probably rename this
-fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
     Expr::new(x, Span::Decoded)
 }
 
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
     use cbor::Value::*;
     use syntax::{BinOp, Builtin, Const};
-    use ExprF::*;
+    use ExprKind::*;
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
-            Some(b) => ExprF::Builtin(b),
+            Some(b) => ExprKind::Builtin(b),
             None => match s.as_str() {
                 "True" => BoolLit(true),
                 "False" => BoolLit(false),
@@ -123,7 +124,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t)))
+                EmptyListLit(rc(App(rc(ExprKind::Builtin(Builtin::List)), t)))
             }
             [U64(4), Null, rest @ ..] => {
                 let rest = rest
@@ -139,14 +140,14 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             // Old-style optional literals
             [U64(5), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                App(rc(ExprF::Builtin(Builtin::OptionalNone)), t)
+                App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t)
             }
             [U64(5), t, x] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let t = cbor_value_to_dhall(&t)?;
                 Annot(
                     rc(SomeLit(x)),
-                    rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)),
+                    rc(App(rc(ExprKind::Builtin(Builtin::Optional)), t)),
                 )
             }
             [U64(6), x, y] => {
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 8e13efd..25a545c 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -1,12 +1,12 @@
 use serde_cbor::value::value as cbor;
 use std::vec;
 
-use crate::semantics::error::EncodeError;
+use crate::error::EncodeError;
 use crate::syntax;
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::{
-    Expr, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode, Label,
-    Scheme, V,
+    Expr, ExprKind, FilePrefix, Hash, Import, ImportLocation, ImportMode,
+    Label, Scheme, V,
 };
 
 /// Warning: will fail if `expr` contains an `Embed` node.
@@ -46,7 +46,7 @@ where
     use cbor::Value::{String, I64, U64};
     use std::iter::once;
     use syntax::Builtin;
-    use syntax::ExprF::*;
+    use syntax::ExprKind::*;
 
     use self::Serialize::{RecordMap, UnionMap};
     fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
@@ -110,7 +110,9 @@ where
         SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
         EmptyListLit(x) => match x.as_ref() {
             App(f, a) => match f.as_ref() {
-                ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)),
+                ExprKind::Builtin(Builtin::List) => {
+                    ser_seq!(ser; tag(4), expr(a))
+                }
                 _ => ser_seq!(ser; tag(28), expr(x)),
             },
             _ => ser_seq!(ser; tag(28), expr(x)),
@@ -284,7 +286,7 @@ fn collect_nested_applications<'a, E>(
 ) -> (&'a Expr<E>, Vec<&'a Expr<E>>) {
     fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> {
         match e.as_ref() {
-            ExprF::App(f, a) => {
+            ExprKind::App(f, a) => {
                 vec.push(a);
                 go(f, vec)
             }
@@ -306,7 +308,7 @@ fn collect_nested_lets<'a, E>(
         vec: &mut Vec<LetBinding<'a, E>>,
     ) -> &'a Expr<E> {
         match e.as_ref() {
-            ExprF::Let(l, t, v, e) => {
+            ExprKind::Let(l, t, v, e) => {
                 vec.push((l, t, v));
                 go(e, vec)
             }
diff --git a/dhall/src/syntax/core/context.rs b/dhall/src/syntax/core/context.rs
deleted file mode 100644
index 6844baa..0000000
--- a/dhall/src/syntax/core/context.rs
+++ /dev/null
@@ -1,80 +0,0 @@
-use std::cmp::Eq;
-use std::collections::HashMap;
-use std::hash::Hash;
-
-/// A `(Context a)` associates `Text` labels with values of type `a`
-///
-/// The `Context` is used for type-checking when `(a = Expr)`
-///
-/// * You create a `Context` using `empty` and `insert`
-/// * You transform a `Context` using `fmap`
-/// * You consume a `Context` using `lookup` and `toList`
-///
-/// The difference between a `Context` and a `Map` is that a `Context` lets you
-/// have multiple ordered occurrences of the same key and you can query for the
-/// `n`th occurrence of a given key.
-///
-#[derive(Debug, Clone)]
-pub struct Context<K: Eq + Hash, T>(HashMap<K, Vec<T>>);
-
-impl<K: Hash + Eq + Clone, T> Context<K, T> {
-    /// An empty context with no key-value pairs
-    pub fn new() -> Self {
-        Context(HashMap::new())
-    }
-
-    /// Look up a key by name and index
-    ///
-    /// ```c
-    /// lookup _ _         empty  = Nothing
-    /// lookup k 0 (insert k v c) = Just v
-    /// lookup k n (insert k v c) = lookup k (n - 1) c  -- 1 <= n
-    /// lookup k n (insert j v c) = lookup k  n      c  -- k /= j
-    /// ```
-    pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> {
-        self.0.get(k).and_then(|v| {
-            if n < v.len() {
-                v.get(v.len() - 1 - n)
-            } else {
-                None
-            }
-        })
-    }
-
-    pub fn map<U, F: Fn(&K, &T) -> U>(&self, f: F) -> Context<K, U> {
-        Context(
-            self.0
-                .iter()
-                .map(|(k, vs)| {
-                    ((*k).clone(), vs.iter().map(|v| f(k, v)).collect())
-                })
-                .collect(),
-        )
-    }
-
-    pub fn lookup_all<'a>(&'a self, k: &K) -> impl Iterator<Item = &T> {
-        self.0.get(k).into_iter().flat_map(|v| v.iter())
-    }
-
-    pub fn iter(&self) -> impl Iterator<Item = (&K, &T)> {
-        self.0
-            .iter()
-            .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v)))
-    }
-
-    pub fn iter_keys(&self) -> impl Iterator<Item = (&K, &Vec<T>)> {
-        self.0.iter()
-    }
-}
-
-impl<K: Hash + Eq + Clone, T: Clone> Context<K, T> {
-    /// Add a key-value pair to the `Context`
-    pub fn insert(&self, k: K, v: T) -> Self {
-        let mut ctx = (*self).clone();
-        {
-            let m = ctx.0.entry(k).or_insert_with(Vec::new);
-            m.push(v);
-        }
-        ctx
-    }
-}
diff --git a/dhall/src/syntax/mod.rs b/dhall/src/syntax/mod.rs
index a82e827..512a026 100644
--- a/dhall/src/syntax/mod.rs
+++ b/dhall/src/syntax/mod.rs
@@ -5,10 +5,9 @@
     clippy::type_complexity
 )]
 
-mod core;
-pub use crate::syntax::core::context;
-pub use crate::syntax::core::visitor;
-pub use crate::syntax::core::*;
+mod ast;
+pub use crate::syntax::ast::visitor;
+pub use crate::syntax::ast::*;
 pub use crate::syntax::text::parser::*;
 pub use crate::syntax::text::printer::*;
 pub mod binary;
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index f6b6577..90cb4b1 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -7,13 +7,12 @@ use pest_consume::{match_nodes, Parser};
 
 use crate::semantics::phase::Normalized;
 use crate::syntax;
-use crate::syntax::core;
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
-use crate::syntax::ExprF::*;
+use crate::syntax::ExprKind::*;
 use crate::syntax::{
-    FilePath, FilePrefix, Hash, ImportLocation, ImportMode, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble, RawExpr, Scheme, Span, URL,
-    V,
+    Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer,
+    InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural,
+    Scheme, Span, UnspannedExpr, URL, V,
 };
 
 // This file consumes the parse tree generated by pest and turns it into
@@ -77,10 +76,14 @@ impl crate::syntax::Builtin {
 fn input_to_span(input: ParseInput) -> Span {
     Span::make(input.user_data().clone(), input.as_pair().as_span())
 }
-fn spanned(input: ParseInput, x: RawExpr<Normalized>) -> Expr {
+fn spanned(input: ParseInput, x: UnspannedExpr<Normalized>) -> Expr {
     Expr::new(x, input_to_span(input))
 }
-fn spanned_union(span1: Span, span2: Span, x: RawExpr<Normalized>) -> Expr {
+fn spanned_union(
+    span1: Span,
+    span2: Span,
+    x: UnspannedExpr<Normalized>,
+) -> Expr {
     Expr::new(x, span1.union(&span2))
 }
 
@@ -349,20 +352,20 @@ impl DhallParser {
     }
 
     #[alias(double_literal)]
-    fn NaN(_input: ParseInput) -> ParseResult<core::Double> {
+    fn NaN(_input: ParseInput) -> ParseResult<Double> {
         Ok(std::f64::NAN.into())
     }
     #[alias(double_literal)]
-    fn minus_infinity_literal(_input: ParseInput) -> ParseResult<core::Double> {
+    fn minus_infinity_literal(_input: ParseInput) -> ParseResult<Double> {
         Ok(std::f64::NEG_INFINITY.into())
     }
     #[alias(double_literal)]
-    fn plus_infinity_literal(_input: ParseInput) -> ParseResult<core::Double> {
+    fn plus_infinity_literal(_input: ParseInput) -> ParseResult<Double> {
         Ok(std::f64::INFINITY.into())
     }
 
     #[alias(double_literal)]
-    fn numeric_double_literal(input: ParseInput) -> ParseResult<core::Double> {
+    fn numeric_double_literal(input: ParseInput) -> ParseResult<Double> {
         let s = input.as_str().trim();
         match s.parse::<f64>() {
             Ok(x) if x.is_infinite() => Err(input.error(format!(
@@ -374,7 +377,7 @@ impl DhallParser {
         }
     }
 
-    fn natural_literal(input: ParseInput) -> ParseResult<core::Natural> {
+    fn natural_literal(input: ParseInput) -> ParseResult<Natural> {
         input
             .as_str()
             .trim()
@@ -382,7 +385,7 @@ impl DhallParser {
             .map_err(|e| input.error(format!("{}", e)))
     }
 
-    fn integer_literal(input: ParseInput) -> ParseResult<core::Integer> {
+    fn integer_literal(input: ParseInput) -> ParseResult<Integer> {
         input
             .as_str()
             .trim()
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 8df456b..78942ed 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -2,10 +2,137 @@ use crate::syntax::*;
 use itertools::Itertools;
 use std::fmt::{self, Display};
 
+// There is a one-to-one correspondence between the formatter and the grammar. Each phase is
+// named after a corresponding grammar group, and the structure of the formatter reflects
+// the relationship between the corresponding grammar rules. This leads to the nice property
+// of automatically getting all the parentheses and precedences right.
+#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)]
+enum PrintPhase {
+    Base,
+    Operator,
+    BinOp(ast::BinOp),
+    App,
+    Import,
+    Primitive,
+}
+
+// Wraps an Expr with a phase, so that phase selection can be done separate from the actual
+// printing.
+#[derive(Clone)]
+struct PhasedExpr<'a, E>(&'a Expr<E>, PrintPhase);
+
+impl<'a, E: Display + Clone> PhasedExpr<'a, E> {
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, E> {
+        PhasedExpr(self.0, phase)
+    }
+}
+
+impl<E: Display + Clone> UnspannedExpr<E> {
+    // Annotate subexpressions with the appropriate phase, defaulting to Base
+    fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a, E>, E> {
+        use crate::syntax::ExprKind::*;
+        use PrintPhase::*;
+        let with_base = self.map_ref(|e| PhasedExpr(e, Base));
+        match with_base {
+            Pi(a, b, c) => {
+                if &String::from(&a) == "_" {
+                    Pi(a, b.phase(Operator), c)
+                } else {
+                    Pi(a, b, c)
+                }
+            }
+            Merge(a, b, c) => Merge(
+                a.phase(PrintPhase::Import),
+                b.phase(PrintPhase::Import),
+                c.map(|x| x.phase(PrintPhase::App)),
+            ),
+            ToMap(a, b) => ToMap(
+                a.phase(PrintPhase::Import),
+                b.map(|x| x.phase(PrintPhase::App)),
+            ),
+            Annot(a, b) => Annot(a.phase(Operator), b),
+            ExprKind::BinOp(op, a, b) => ExprKind::BinOp(
+                op,
+                a.phase(PrintPhase::BinOp(op)),
+                b.phase(PrintPhase::BinOp(op)),
+            ),
+            SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)),
+            ExprKind::App(f, a) => ExprKind::App(
+                f.phase(PrintPhase::Import),
+                a.phase(PrintPhase::Import),
+            ),
+            Field(a, b) => Field(a.phase(Primitive), b),
+            Projection(e, ls) => Projection(e.phase(Primitive), ls),
+            ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b),
+            e => e,
+        }
+    }
+
+    fn fmt_phase(
+        &self,
+        f: &mut fmt::Formatter,
+        phase: PrintPhase,
+    ) -> Result<(), fmt::Error> {
+        use crate::syntax::ExprKind::*;
+
+        let needs_paren = match self {
+            Lam(_, _, _)
+            | BoolIf(_, _, _)
+            | Pi(_, _, _)
+            | Let(_, _, _, _)
+            | EmptyListLit(_)
+            | NEListLit(_)
+            | SomeLit(_)
+            | Merge(_, _, _)
+            | ToMap(_, _)
+            | Annot(_, _) => phase > PrintPhase::Base,
+            // Precedence is magically handled by the ordering of BinOps.
+            ExprKind::BinOp(op, _, _) => phase > PrintPhase::BinOp(*op),
+            ExprKind::App(_, _) => phase > PrintPhase::App,
+            Field(_, _) | Projection(_, _) | ProjectionByExpr(_, _) => {
+                phase > PrintPhase::Import
+            }
+            _ => false,
+        };
+
+        if needs_paren {
+            f.write_str("(")?;
+        }
+        self.annotate_with_phases().fmt(f)?;
+        if needs_paren {
+            f.write_str(")")?;
+        }
+
+        Ok(())
+    }
+}
+
+fn fmt_list<T, I, F>(
+    open: &str,
+    sep: &str,
+    close: &str,
+    it: I,
+    f: &mut fmt::Formatter,
+    func: F,
+) -> Result<(), fmt::Error>
+where
+    I: IntoIterator<Item = T>,
+    F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>,
+{
+    f.write_str(open)?;
+    for (i, x) in it.into_iter().enumerate() {
+        if i > 0 {
+            f.write_str(sep)?;
+        }
+        func(x, f)?;
+    }
+    f.write_str(close)
+}
+
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
+impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        use crate::syntax::ExprF::*;
+        use crate::syntax::ExprKind::*;
         match self {
             Lam(a, b, c) => {
                 write!(f, "λ({} : {}) → {}", a, b, c)?;
@@ -53,10 +180,10 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
             Assert(a) => {
                 write!(f, "assert : {}", a)?;
             }
-            ExprF::BinOp(op, a, b) => {
+            ExprKind::BinOp(op, a, b) => {
                 write!(f, "{} {} {}", a, op, b)?;
             }
-            ExprF::App(a, b) => {
+            ExprKind::App(a, b) => {
                 write!(f, "{} {}", a, b)?;
             }
             Field(a, b) => {
@@ -104,147 +231,16 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
     }
 }
 
-// There is a one-to-one correspondence between the formatter and the grammar. Each phase is
-// named after a corresponding grammar group, and the structure of the formatter reflects
-// the relationship between the corresponding grammar rules. This leads to the nice property
-// of automatically getting all the parentheses and precedences right.
-#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)]
-enum PrintPhase {
-    Base,
-    Operator,
-    BinOp(core::BinOp),
-    App,
-    Import,
-    Primitive,
-}
-
-// Wraps an Expr with a phase, so that phase selsction can be done
-// separate from the actual printing
-#[derive(Clone)]
-struct PhasedExpr<'a, A>(&'a Expr<A>, PrintPhase);
-
-impl<'a, A: Display + Clone> Display for PhasedExpr<'a, A> {
-    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        self.0.as_ref().fmt_phase(f, self.1)
-    }
-}
-
-impl<'a, A: Display + Clone> PhasedExpr<'a, A> {
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, A> {
-        PhasedExpr(self.0, phase)
-    }
-}
-
-impl<A: Display + Clone> RawExpr<A> {
-    fn fmt_phase(
-        &self,
-        f: &mut fmt::Formatter,
-        phase: PrintPhase,
-    ) -> Result<(), fmt::Error> {
-        use crate::syntax::ExprF::*;
-        use PrintPhase::*;
-
-        let needs_paren = match self {
-            Lam(_, _, _)
-            | BoolIf(_, _, _)
-            | Pi(_, _, _)
-            | Let(_, _, _, _)
-            | EmptyListLit(_)
-            | NEListLit(_)
-            | SomeLit(_)
-            | Merge(_, _, _)
-            | ToMap(_, _)
-            | Annot(_, _)
-                if phase > Base =>
-            {
-                true
-            }
-            // Precedence is magically handled by the ordering of BinOps.
-            ExprF::BinOp(op, _, _) if phase > PrintPhase::BinOp(*op) => true,
-            ExprF::App(_, _) if phase > PrintPhase::App => true,
-            Field(_, _) | Projection(_, _) | ProjectionByExpr(_, _)
-                if phase > PrintPhase::Import =>
-            {
-                true
-            }
-            _ => false,
-        };
-
-        // Annotate subexpressions with the appropriate phase, defaulting to Base
-        let phased_self = match self.map_ref(|e| PhasedExpr(e, Base)) {
-            Pi(a, b, c) => {
-                if &String::from(&a) == "_" {
-                    Pi(a, b.phase(Operator), c)
-                } else {
-                    Pi(a, b, c)
-                }
-            }
-            Merge(a, b, c) => Merge(
-                a.phase(PrintPhase::Import),
-                b.phase(PrintPhase::Import),
-                c.map(|x| x.phase(PrintPhase::App)),
-            ),
-            ToMap(a, b) => ToMap(
-                a.phase(PrintPhase::Import),
-                b.map(|x| x.phase(PrintPhase::App)),
-            ),
-            Annot(a, b) => Annot(a.phase(Operator), b),
-            ExprF::BinOp(op, a, b) => ExprF::BinOp(
-                op,
-                a.phase(PrintPhase::BinOp(op)),
-                b.phase(PrintPhase::BinOp(op)),
-            ),
-            SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)),
-            ExprF::App(f, a) => ExprF::App(
-                f.phase(PrintPhase::Import),
-                a.phase(PrintPhase::Import),
-            ),
-            Field(a, b) => Field(a.phase(Primitive), b),
-            Projection(e, ls) => Projection(e.phase(Primitive), ls),
-            ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b),
-            e => e,
-        };
-
-        if needs_paren {
-            f.write_str("(")?;
-        }
-
-        // Uses the ExprF<PhasedExpr<_>, _> instance
-        phased_self.fmt(f)?;
-
-        if needs_paren {
-            f.write_str(")")?;
-        }
-        Ok(())
-    }
-}
-
-impl<A: Display + Clone> Display for Expr<A> {
+impl<E: Display + Clone> Display for Expr<E> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
 }
 
-fn fmt_list<T, I, F>(
-    open: &str,
-    sep: &str,
-    close: &str,
-    it: I,
-    f: &mut fmt::Formatter,
-    func: F,
-) -> Result<(), fmt::Error>
-where
-    I: IntoIterator<Item = T>,
-    F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>,
-{
-    f.write_str(open)?;
-    for (i, x) in it.into_iter().enumerate() {
-        if i > 0 {
-            f.write_str(sep)?;
-        }
-        func(x, f)?;
+impl<'a, E: Display + Clone> Display for PhasedExpr<'a, E> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        self.0.as_ref().fmt_phase(f, self.1)
     }
-    f.write_str(close)
 }
 
 impl<SubExpr: Display> Display for InterpolatedText<SubExpr> {
@@ -361,6 +357,7 @@ impl Display for Hash {
         }
     }
 }
+
 impl<SubExpr: Display> Display for Import<SubExpr> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use FilePrefix::*;
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 9e5c744..d73c2d4 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -47,7 +47,7 @@ use std::fs::File;
 use std::io::{Read, Write};
 use std::path::PathBuf;
 
-use crate::semantics::error::{Error, Result};
+use crate::error::{Error, Result};
 use crate::semantics::phase::Parsed;
 
 #[allow(dead_code)]