Merge pull request #131 from Nadrieril/hir

Decouple main expression types

6 files changed, 716 insertions, 933 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..55050ed 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Nir, NirKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -9,18 +9,20 @@ pub(crate) enum NzVar {
 }
 
 #[derive(Debug, Clone)]
-enum NzEnvItem {
+enum EnvItem<Type> {
     // Variable is bound with given type
-    Kept(Value),
+    Kept(Type),
     // Variable has been replaced by corresponding value
-    Replaced(Value),
+    Replaced(Nir, Type),
 }
 
 #[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
-    items: Vec<NzEnvItem>,
+pub(crate) struct ValEnv<Type> {
+    items: Vec<EnvItem<Type>>,
 }
 
+pub(crate) type NzEnv = ValEnv<()>;
+
 impl NzVar {
     pub fn new(idx: usize) -> Self {
         NzVar::Bound(idx)
@@ -44,33 +46,49 @@ impl NzVar {
     }
 }
 
-impl NzEnv {
+impl<Type: Clone> ValEnv<Type> {
     pub fn new() -> Self {
-        NzEnv { items: Vec::new() }
+        ValEnv { items: Vec::new() }
+    }
+    pub fn discard_types(&self) -> ValEnv<()> {
+        let items = self
+            .items
+            .iter()
+            .map(|i| match i {
+                EnvItem::Kept(_) => EnvItem::Kept(()),
+                EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
+            })
+            .collect();
+        ValEnv { items }
     }
 
-    pub fn insert_type(&self, t: Value) -> Self {
+    pub fn insert_type(&self, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Kept(t));
+        env.items.push(EnvItem::Kept(ty));
         env
     }
-    pub fn insert_value(&self, e: Value) -> Self {
+    pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Replaced(e));
+        env.items.push(EnvItem::Replaced(e, ty));
         env
     }
-    pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+    pub fn lookup_val(&self, var: &AlphaVar) -> NirKind {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
-            NzEnvItem::Replaced(x) => x.kind().clone(),
+            EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
+            EnvItem::Replaced(x, _) => x.kind().clone(),
         }
     }
-    pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+    pub fn lookup_ty(&self, var: &AlphaVar) -> Type {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(ty) => ty.clone(),
-            NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+            EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
         }
     }
 }
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+    fn from(x: &'a NzEnv) -> Self {
+        x.clone()
+    }
+}
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 2c8d907..2648339 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,9 +1,9 @@
 pub mod env;
 pub mod lazy;
+pub mod nir;
 pub mod normalize;
-pub mod value;
 pub mod var;
 pub(crate) use env::*;
+pub(crate) use nir::*;
 pub(crate) use normalize::*;
-pub(crate) use value::*;
 pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
new file mode 100644
index 0000000..4ed66b7
--- /dev/null
+++ b/dhall/src/semantics/nze/nir.rs
@@ -0,0 +1,510 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::semantics::nze::lazy;
+use crate::semantics::{
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+};
+use crate::syntax::{
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+    Span,
+};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+/// Stands for "Normalized intermediate representation"
+#[derive(Clone)]
+pub(crate) struct Nir(Rc<NirInternal>);
+
+#[derive(Debug)]
+struct NirInternal {
+    kind: lazy::Lazy<Thunk, NirKind>,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+pub(crate) enum Thunk {
+    /// A completely unnormalized expression.
+    Thunk { env: NzEnv, body: Hir },
+    /// A partially normalized expression that may need to go through `normalize_one_layer`.
+    PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+    /// Normal closure
+    Closure { env: NzEnv, body: Hir },
+    /// Closure that ignores the argument passed
+    ConstantClosure { body: Nir },
+}
+
+/// A text literal with interpolations.
+// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
+// text values must be merged.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
+
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Nirs in a NirKind are in WHNF, and recursively so, then the NirKind is in
+/// Normal Form (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.
+/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Nir`s to get to the NF.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum NirKind {
+    /// Closures
+    LamClosure {
+        binder: Binder,
+        annot: Nir,
+        closure: Closure,
+    },
+    PiClosure {
+        binder: Binder,
+        annot: Nir,
+        closure: Closure,
+    },
+    AppliedBuiltin(BuiltinClosure<Nir>),
+
+    Var(NzVar),
+    Const(Const),
+    Lit(LitKind),
+    EmptyOptionalLit(Nir),
+    NEOptionalLit(Nir),
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
+    EmptyListLit(Nir),
+    NEListLit(Vec<Nir>),
+    RecordType(HashMap<Label, Nir>),
+    RecordLit(HashMap<Label, Nir>),
+    UnionType(HashMap<Label, Option<Nir>>),
+    UnionConstructor(Label, HashMap<Label, Option<Nir>>),
+    UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
+    TextLit(TextLit),
+    Equivalence(Nir, Nir),
+    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
+    PartialExpr(ExprKind<Nir>),
+}
+
+impl Nir {
+    /// Construct a Nir from a completely unnormalized expression.
+    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+        NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
+    }
+    /// Construct a Nir from a partially normalized expression that's not in WHNF.
+    pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
+        // TODO: env
+        let env = NzEnv::new();
+        NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
+    }
+    /// Make a Nir from a NirKind
+    pub(crate) fn from_kind(v: NirKind) -> Nir {
+        NirInternal::from_whnf(v).into_nir()
+    }
+    pub(crate) fn from_const(c: Const) -> Self {
+        let v = NirKind::Const(c);
+        NirInternal::from_whnf(v).into_nir()
+    }
+    pub(crate) fn from_builtin(b: Builtin) -> Self {
+        Self::from_builtin_env(b, &NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+        Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
+    }
+    pub(crate) fn from_text(txt: impl ToString) -> Self {
+        Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
+    }
+
+    pub(crate) fn as_const(&self) -> Option<Const> {
+        match &*self.kind() {
+            NirKind::Const(c) => Some(*c),
+            _ => None,
+        }
+    }
+
+    /// This is what you want if you want to pattern-match on the value.
+    pub(crate) fn kind(&self) -> &NirKind {
+        self.0.kind()
+    }
+
+    pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+        Type::new(self.clone(), u.into())
+    }
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        self.to_hir_noenv().to_expr(opts)
+    }
+    pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+    }
+
+    pub(crate) fn normalize(&self) {
+        self.0.normalize()
+    }
+
+    pub(crate) fn app(&self, v: Nir) -> Nir {
+        Nir::from_kind(apply_any(self.clone(), v))
+    }
+
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
+            ExprKind::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+                    })
+                    .collect(),
+            )
+        };
+
+        let hir = match &*self.kind() {
+            NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+            NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+            self_kind => HirKind::Expr(match self_kind {
+                NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
+                    unreachable!()
+                }
+                NirKind::LamClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Lam(
+                    binder.to_label(),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
+                ),
+                NirKind::PiClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Pi(
+                    binder.to_label(),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
+                ),
+                NirKind::Const(c) => ExprKind::Const(*c),
+                NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+                NirKind::EmptyOptionalLit(n) => ExprKind::App(
+                    Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
+                    n.to_hir(venv),
+                ),
+                NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+                NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+                    HirKind::Expr(ExprKind::App(
+                        Nir::from_builtin(Builtin::List).to_hir(venv),
+                        n.to_hir(venv),
+                    )),
+                    Span::Artificial,
+                )),
+                NirKind::NEListLit(elts) => ExprKind::NEListLit(
+                    elts.iter().map(|v| v.to_hir(venv)).collect(),
+                ),
+                NirKind::TextLit(elts) => ExprKind::TextLit(
+                    elts.iter()
+                        .map(|t| t.map_ref(|v| v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::RecordLit(kvs) => ExprKind::RecordLit(
+                    kvs.iter()
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::RecordType(kts) => ExprKind::RecordType(
+                    kts.iter()
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::UnionType(kts) => map_uniontype(kts),
+                NirKind::UnionConstructor(l, kts) => ExprKind::Field(
+                    Hir::new(
+                        HirKind::Expr(map_uniontype(kts)),
+                        Span::Artificial,
+                    ),
+                    l.clone(),
+                ),
+                NirKind::UnionLit(l, v, kts) => ExprKind::App(
+                    Hir::new(
+                        HirKind::Expr(ExprKind::Field(
+                            Hir::new(
+                                HirKind::Expr(map_uniontype(kts)),
+                                Span::Artificial,
+                            ),
+                            l.clone(),
+                        )),
+                        Span::Artificial,
+                    ),
+                    v.to_hir(venv),
+                ),
+                NirKind::Equivalence(x, y) => ExprKind::BinOp(
+                    BinOp::Equivalence,
+                    x.to_hir(venv),
+                    y.to_hir(venv),
+                ),
+                NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+            }),
+        };
+
+        Hir::new(hir, Span::Artificial)
+    }
+    pub fn to_hir_noenv(&self) -> Hir {
+        self.to_hir(VarEnv::new())
+    }
+}
+
+impl NirInternal {
+    fn from_whnf(k: NirKind) -> Self {
+        NirInternal {
+            kind: lazy::Lazy::new_completed(k),
+        }
+    }
+    fn from_thunk(th: Thunk) -> Self {
+        NirInternal {
+            kind: lazy::Lazy::new(th),
+        }
+    }
+    fn into_nir(self) -> Nir {
+        Nir(Rc::new(self))
+    }
+
+    fn kind(&self) -> &NirKind {
+        &self.kind
+    }
+    fn normalize(&self) {
+        self.kind().normalize();
+    }
+}
+
+impl NirKind {
+    pub(crate) fn into_nir(self) -> Nir {
+        Nir::from_kind(self)
+    }
+
+    pub(crate) fn normalize(&self) {
+        match self {
+            NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+
+            NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
+                tth.normalize();
+            }
+
+            NirKind::NEOptionalLit(th) => {
+                th.normalize();
+            }
+            NirKind::LamClosure { annot, closure, .. }
+            | NirKind::PiClosure { annot, closure, .. } => {
+                annot.normalize();
+                closure.normalize();
+            }
+            NirKind::AppliedBuiltin(closure) => closure.normalize(),
+            NirKind::NEListLit(elts) => {
+                for x in elts.iter() {
+                    x.normalize();
+                }
+            }
+            NirKind::RecordLit(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            NirKind::RecordType(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            NirKind::UnionLit(_, v, kts) => {
+                v.normalize();
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            NirKind::TextLit(tlit) => tlit.normalize(),
+            NirKind::Equivalence(x, y) => {
+                x.normalize();
+                y.normalize();
+            }
+            NirKind::PartialExpr(e) => {
+                e.map_ref(Nir::normalize);
+            }
+        }
+    }
+
+    pub(crate) fn from_builtin(b: Builtin) -> NirKind {
+        NirKind::from_builtin_env(b, NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+        NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+    }
+}
+
+impl Thunk {
+    fn new(env: NzEnv, body: Hir) -> Self {
+        Thunk::Thunk { env, body }
+    }
+    fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
+        Thunk::PartialExpr { env, expr }
+    }
+    fn eval(self) -> NirKind {
+        match self {
+            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+        }
+    }
+}
+
+impl Closure {
+    pub fn new(env: &NzEnv, body: Hir) -> Self {
+        Closure::Closure {
+            env: env.clone(),
+            body,
+        }
+    }
+    /// New closure that ignores its argument
+    pub fn new_constant(body: Nir) -> Self {
+        Closure::ConstantClosure { body }
+    }
+
+    pub fn apply(&self, val: Nir) -> Nir {
+        match self {
+            Closure::Closure { env, body, .. } => {
+                body.eval(env.insert_value(val, ()))
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+    fn apply_var(&self, var: NzVar) -> Nir {
+        match self {
+            Closure::Closure { .. } => {
+                self.apply(Nir::from_kind(NirKind::Var(var)))
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+
+    // TODO: somehow normalize the body. Might require to pass an env.
+    pub fn normalize(&self) {}
+
+    /// Convert this closure to a Hir expression
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.apply_var(NzVar::new(venv.size()))
+            .to_hir(venv.insert())
+    }
+    /// If the closure variable is free in the closure, return Err. Otherwise, return the value
+    /// with that free variable remove.
+    pub fn remove_binder(&self) -> Result<Nir, ()> {
+        match self {
+            Closure::Closure { .. } => {
+                let v = NzVar::fresh();
+                // TODO: handle case where variable is used in closure
+                // TODO: return information about where the variable is used
+                Ok(self.apply_var(v))
+            }
+            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+        }
+    }
+}
+
+impl TextLit {
+    pub fn new(
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+    ) -> Self {
+        TextLit(squash_textlit(elts))
+    }
+    pub fn interpolate(v: Nir) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Expr(v)])
+    }
+    pub fn from_text(s: String) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Text(s)])
+    }
+
+    pub fn concat(&self, other: &TextLit) -> TextLit {
+        TextLit::new(self.iter().chain(other.iter()).cloned())
+    }
+    pub fn is_empty(&self) -> bool {
+        self.0.is_empty()
+    }
+    /// If the literal consists of only one interpolation and not text, return the interpolated
+    /// value.
+    pub fn as_single_expr(&self) -> Option<&Nir> {
+        use InterpolatedTextContents::Expr;
+        if let [Expr(v)] = self.0.as_slice() {
+            Some(v)
+        } else {
+            None
+        }
+    }
+    /// If there are no interpolations, return the corresponding text value.
+    pub fn as_text(&self) -> Option<String> {
+        use InterpolatedTextContents::Text;
+        if self.is_empty() {
+            Some(String::new())
+        } else if let [Text(s)] = self.0.as_slice() {
+            Some(s.clone())
+        } else {
+            None
+        }
+    }
+    pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
+        self.0.iter()
+    }
+    /// Normalize the contained values. This does not break the invariant because we have already
+    /// ensured that no contained values normalize to a TextLit.
+    pub fn normalize(&self) {
+        for x in self.0.iter() {
+            x.map_ref(Nir::normalize);
+        }
+    }
+}
+
+impl lazy::Eval<NirKind> for Thunk {
+    fn eval(self) -> NirKind {
+        self.eval()
+    }
+}
+
+/// Compare two values for equality modulo alpha/beta-equivalence.
+impl std::cmp::PartialEq for Nir {
+    fn eq(&self, other: &Self) -> bool {
+        Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+    }
+}
+impl std::cmp::Eq for Nir {}
+
+impl std::cmp::PartialEq for Thunk {
+    fn eq(&self, _other: &Self) -> bool {
+        unreachable!(
+            "Trying to compare thunks but we should only compare WHNFs"
+        )
+    }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+    fn eq(&self, other: &Self) -> bool {
+        let v = NzVar::fresh();
+        self.apply_var(v) == other.apply_var(v)
+    }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Nir {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let vint: &NirInternal = &self.0;
+        let kind = vint.kind();
+        if let NirKind::Const(c) = kind {
+            return write!(fmt, "{:?}", c);
+        }
+        let mut x = fmt.debug_struct(&format!("Nir@WHNF"));
+        x.field("kind", kind);
+        x.finish()
+    }
+}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index a00b7ff..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,49 +3,39 @@ use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
 use crate::semantics::{
-    Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
-    ValueKind,
+    Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
+    BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
 };
-use crate::Normalized;
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
     match f.kind() {
-        ValueKind::LamClosure { closure, .. } => {
-            closure.apply(a).to_whnf_check_type(ty)
+        NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
+        NirKind::AppliedBuiltin(closure) => closure.apply(a),
+        NirKind::UnionConstructor(l, kts) => {
+            NirKind::UnionLit(l.clone(), a, kts.clone())
         }
-        ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type().unwrap(), ty)
-        }
-        ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
-            l.clone(),
-            a,
-            kts.clone(),
-            uniont.clone(),
-            f.get_type().unwrap(),
-        ),
-        _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
+        _ => NirKind::PartialExpr(ExprKind::App(f, a)),
     }
 }
 
 pub(crate) fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-) -> Vec<InterpolatedTextContents<Value>> {
+    elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+) -> Vec<InterpolatedTextContents<Nir>> {
     use std::mem::replace;
     use InterpolatedTextContents::{Expr, Text};
 
     fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
         crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Value>>,
+        ret: &mut Vec<InterpolatedTextContents<Nir>>,
     ) {
         for contents in elts {
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => match e.kind() {
-                    ValueKind::TextLit(elts2) => {
+                    NirKind::TextLit(elts2) => {
                         inner(elts2.iter().cloned(), crnt_str, ret)
                     }
                     _ => {
@@ -96,86 +86,77 @@ where
 
 // Small helper enum to avoid repetition
 enum Ret<'a> {
-    ValueKind(ValueKind),
-    Value(Value),
-    ValueRef(&'a Value),
-    Expr(ExprKind<Value, Normalized>),
+    NirKind(NirKind),
+    Nir(Nir),
+    NirRef(&'a Nir),
+    Expr(ExprKind<Nir>),
 }
 
-fn apply_binop<'a>(
-    o: BinOp,
-    x: &'a Value,
-    y: &'a Value,
-    ty: &Value,
-) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use ValueKind::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-    };
+    use LitKind::{Bool, Natural};
+    use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+
     Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
-        (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::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::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::ValueKind(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+        (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y),
+        (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x),
+        (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))),
+        (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))),
+        (BoolAnd, _, _) if x == y => Ret::NirRef(x),
+        (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))),
+        (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))),
+        (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y),
+        (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x),
+        (BoolOr, _, _) if x == y => Ret::NirRef(x),
+        (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y),
+        (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x),
+        (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))),
+        (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))),
+        (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y),
+        (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x),
+        (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))),
+        (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))),
 
-        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
-        (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueKind(NaturalLit(x + y))
+        (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
+        (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
+        (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
+            Ret::NirKind(Lit(Natural(x + y)))
         }
-        (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::ValueKind(NaturalLit(x * y))
+        (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))),
+        (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+        (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y),
+        (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x),
+        (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
+            Ret::NirKind(Lit(Natural(x * y)))
         }
 
-        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
-            NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
-        ),
+        (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
+            xs.iter().chain(ys.iter()).cloned().collect(),
+        )),
 
-        (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
-            Ret::ValueRef(x)
+        (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
+        (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
+        (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
+            Ret::NirKind(NirKind::TextLit(x.concat(y)))
         }
-        (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
-            Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
-        }
-        (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
-            ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
-        ),
-        (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
-            ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
-        ),
+        (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
+            x.concat(&TextLit::interpolate(y.clone())),
+        )),
+        (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
+            TextLit::interpolate(x.clone()).concat(y),
+        )),
 
         (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
+            Ret::NirRef(x)
         }
         (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
+            Ret::NirRef(y)
         }
         (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let mut kvs = kvs2.clone();
@@ -183,32 +164,25 @@ fn apply_binop<'a>(
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            Ret::ValueKind(RecordLit(kvs))
+            Ret::NirKind(RecordLit(kvs))
         }
-        (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
+        (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
+            Ret::NirRef(x)
         }
         (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
+            Ret::NirRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kts = match ty.kind() {
-                RecordType(kts) => kts,
-                _ => unreachable!("Internal type error"),
-            };
-            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_partial_expr(
-                    ExprKind::BinOp(
-                        RecursiveRecordMerge,
-                        v1.clone(),
-                        v2.clone(),
-                    ),
-                    kts.get(k).expect("Internal type error").clone(),
-                ))
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+                Ok(Nir::from_partial_expr(ExprKind::BinOp(
+                    RecursiveRecordMerge,
+                    v1.clone(),
+                    v2.clone(),
+                )))
             })?;
-            Ret::ValueKind(RecordLit(kvs))
+            Ret::NirKind(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
@@ -216,118 +190,107 @@ fn apply_binop<'a>(
                 kts_x,
                 kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |_, l: &Value, r: &Value| {
-                    Ok(Value::from_partial_expr(
-                        ExprKind::BinOp(
-                            RecursiveRecordTypeMerge,
-                            l.clone(),
-                            r.clone(),
-                        ),
-                        ty.clone(),
-                    ))
+                |_, l: &Nir, r: &Nir| {
+                    Ok(Nir::from_partial_expr(ExprKind::BinOp(
+                        RecursiveRecordTypeMerge,
+                        l.clone(),
+                        r.clone(),
+                    )))
                 },
             )?;
-            Ret::ValueKind(RecordType(kts))
+            Ret::NirKind(RecordType(kts))
         }
 
         (Equivalence, _, _) => {
-            Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+            Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
         }
 
         _ => return None,
     })
 }
 
-pub(crate) fn normalize_one_layer(
-    expr: ExprKind<Value, Normalized>,
-    ty: &Value,
-    env: &NzEnv,
-) -> ValueKind {
-    use ValueKind::{
-        BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
-        NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
-        RecordType, UnionConstructor, UnionLit, UnionType,
+pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+    use LitKind::Bool;
+    use NirKind::{
+        EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+        PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+        UnionType,
     };
 
     let ret = match expr {
-        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.
-        ExprKind::Lam(..)
-        | ExprKind::Pi(..)
-        | ExprKind::Let(..)
-        | ExprKind::Embed(_)
-        | ExprKind::Var(_) => {
-            unreachable!("This case should have been handled in typecheck")
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
         }
-        ExprKind::Annot(x, _) => Ret::Value(x),
-        ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
-        ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+        ExprKind::Var(..)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..) => unreachable!(
+            "This case should have been handled in normalize_hir_whnf"
+        ),
+
+        ExprKind::Annot(x, _) => Ret::Nir(x),
+        ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
+        ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
         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::App(v, a) => Ret::Nir(v.app(a)),
+        ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())),
+        ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
                     ..
                 }) if args.len() == 1 => args[0].clone(),
                 _ => panic!("internal type error"),
             };
-            Ret::ValueKind(ValueKind::EmptyListLit(arg))
+            Ret::NirKind(NirKind::EmptyListLit(arg))
         }
         ExprKind::NEListLit(elts) => {
-            Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+            Ret::NirKind(NEListLit(elts.into_iter().collect()))
         }
         ExprKind::RecordLit(kvs) => {
-            Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+            Ret::NirKind(RecordLit(kvs.into_iter().collect()))
         }
         ExprKind::RecordType(kvs) => {
-            Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+            Ret::NirKind(RecordType(kvs.into_iter().collect()))
         }
         ExprKind::UnionType(kvs) => {
-            Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+            Ret::NirKind(UnionType(kvs.into_iter().collect()))
         }
         ExprKind::TextLit(elts) => {
             let tlit = TextLit::new(elts.into_iter());
             // Simplify bare interpolation
             if let Some(v) = tlit.as_single_expr() {
-                Ret::Value(v.clone())
+                Ret::Nir(v.clone())
             } else {
-                Ret::ValueKind(ValueKind::TextLit(tlit))
+                Ret::NirKind(NirKind::TextLit(tlit))
             }
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             match b.kind() {
-                BoolLit(true) => Ret::ValueRef(e1),
-                BoolLit(false) => Ret::ValueRef(e2),
+                Lit(Bool(true)) => Ret::NirRef(e1),
+                Lit(Bool(false)) => Ret::NirRef(e2),
                 _ => {
                     match (e1.kind(), e2.kind()) {
                         // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
-                        _ if e1 == e2 => Ret::ValueRef(e1),
+                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+                        _ if e1 == e2 => Ret::NirRef(e1),
                         _ => Ret::Expr(expr),
                     }
                 }
             }
         }
-        ExprKind::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) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
 
         ExprKind::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::ValueKind(RecordLit(HashMap::new()))
+            Ret::NirKind(RecordLit(HashMap::new()))
         }
         ExprKind::Projection(ref v, ref ls) => match v.kind() {
-            RecordLit(kvs) => Ret::ValueKind(RecordLit(
+            RecordLit(kvs) => Ret::NirKind(RecordLit(
                 ls.iter()
                     .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
                     .collect(),
@@ -335,7 +298,6 @@ pub(crate) fn normalize_one_layer(
             PartialExpr(ExprKind::Projection(v2, _)) => {
                 return normalize_one_layer(
                     ExprKind::Projection(v2.clone(), ls.clone()),
-                    ty,
                     env,
                 )
             }
@@ -343,63 +305,42 @@ pub(crate) fn normalize_one_layer(
         },
         ExprKind::Field(ref v, ref l) => match v.kind() {
             RecordLit(kvs) => match kvs.get(l) {
-                Some(r) => Ret::Value(r.clone()),
+                Some(r) => Ret::Nir(r.clone()),
                 None => Ret::Expr(expr),
             },
-            UnionType(kts) => Ret::ValueKind(UnionConstructor(
-                l.clone(),
-                kts.clone(),
-                v.get_type().unwrap(),
-            )),
+            UnionType(kts) => {
+                Ret::NirKind(UnionConstructor(l.clone(), kts.clone()))
+            }
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
                 x,
                 y,
             )) => match (x.kind(), y.kind()) {
                 (_, RecordLit(kvs)) => match kvs.get(l) {
-                    Some(r) => Ret::Value(r.clone()),
+                    Some(r) => Ret::Nir(r.clone()),
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
                 },
                 (RecordLit(kvs), _) => match kvs.get(l) {
                     Some(r) => Ret::Expr(ExprKind::Field(
-                        Value::from_kind_and_type(
-                            PartialExpr(ExprKind::BinOp(
-                                BinOp::RightBiasedRecordMerge,
-                                Value::from_kind_and_type(
-                                    RecordLit({
-                                        let mut kvs = HashMap::new();
-                                        kvs.insert(l.clone(), r.clone());
-                                        kvs
-                                    }),
-                                    Value::from_kind_and_type(
-                                        RecordType({
-                                            let mut kvs = HashMap::new();
-                                            kvs.insert(
-                                                l.clone(),
-                                                r.get_type_not_sort(),
-                                            );
-                                            kvs
-                                        }),
-                                        r.get_type_not_sort()
-                                            .get_type_not_sort(),
-                                    ),
-                                ),
-                                y.clone(),
-                            )),
-                            v.get_type_not_sort(),
-                        ),
+                        Nir::from_kind(PartialExpr(ExprKind::BinOp(
+                            BinOp::RightBiasedRecordMerge,
+                            Nir::from_kind(RecordLit({
+                                let mut kvs = HashMap::new();
+                                kvs.insert(l.clone(), r.clone());
+                                kvs
+                            })),
+                            y.clone(),
+                        ))),
                         l.clone(),
                     )),
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -416,7 +357,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -426,7 +366,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -438,25 +377,24 @@ pub(crate) fn normalize_one_layer(
         ExprKind::ProjectionByExpr(_, _) => {
             unimplemented!("selection by expression")
         }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
 
         ExprKind::Merge(ref handlers, ref variant, _) => {
             match handlers.kind() {
                 RecordLit(kvs) => match variant.kind() {
-                    UnionConstructor(l, _, _) => match kvs.get(l) {
-                        Some(h) => Ret::Value(h.clone()),
+                    UnionConstructor(l, _) => match kvs.get(l) {
+                        Some(h) => Ret::Nir(h.clone()),
                         None => Ret::Expr(expr),
                     },
-                    UnionLit(l, v, _, _, _) => match kvs.get(l) {
-                        Some(h) => Ret::Value(h.app(v.clone())),
+                    UnionLit(l, v, _) => match kvs.get(l) {
+                        Some(h) => Ret::Nir(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
                     EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
-                        Some(h) => Ret::Value(h.clone()),
+                        Some(h) => Ret::Nir(h.clone()),
                         None => Ret::Expr(expr),
                     },
                     NEOptionalLit(v) => match kvs.get(&"Some".into()) {
-                        Some(h) => Ret::Value(h.app(v.clone())),
+                        Some(h) => Ret::Nir(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
                     _ => Ret::Expr(expr),
@@ -467,37 +405,24 @@ pub(crate) fn normalize_one_layer(
         ExprKind::ToMap(ref v, ref annot) => match v.kind() {
             RecordLit(kvs) if kvs.is_empty() => {
                 match annot.as_ref().map(|v| v.kind()) {
-                    Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+                    Some(NirKind::AppliedBuiltin(BuiltinClosure {
                         b: Builtin::List,
                         args,
                         ..
                     })) if args.len() == 1 => {
-                        Ret::ValueKind(EmptyListLit(args[0].clone()))
+                        Ret::NirKind(EmptyListLit(args[0].clone()))
                     }
                     _ => Ret::Expr(expr),
                 }
             }
-            RecordLit(kvs) => Ret::ValueKind(NEListLit(
+            RecordLit(kvs) => Ret::NirKind(NEListLit(
                 kvs.iter()
                     .sorted_by_key(|(k, _)| k.clone())
                     .map(|(k, v)| {
                         let mut rec = HashMap::new();
-                        let mut rec_ty = HashMap::new();
-                        rec.insert("mapKey".into(), Value::from_text(k));
+                        rec.insert("mapKey".into(), Nir::from_text(k));
                         rec.insert("mapValue".into(), v.clone());
-                        rec_ty.insert(
-                            "mapKey".into(),
-                            Value::from_builtin(Builtin::Text),
-                        );
-                        rec_ty.insert("mapValue".into(), v.get_type_not_sort());
-
-                        Value::from_kind_and_type(
-                            ValueKind::RecordLit(rec),
-                            Value::from_kind_and_type(
-                                ValueKind::RecordType(rec_ty),
-                                Value::from_const(Const::Type),
-                            ),
-                        )
+                        Nir::from_kind(NirKind::RecordLit(rec))
                     })
                     .collect(),
             )),
@@ -506,45 +431,41 @@ pub(crate) fn normalize_one_layer(
     };
 
     match ret {
-        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) => ValueKind::PartialExpr(expr),
+        Ret::NirKind(v) => v,
+        Ret::Nir(v) => v.kind().clone(),
+        Ret::NirRef(v) => v.kind().clone(),
+        Ret::Expr(expr) => NirKind::PartialExpr(expr),
     }
 }
 
-/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
-    match tye.kind() {
-        TyExprKind::Var(var) => env.lookup_val(var),
-        TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+    match hir.kind() {
+        HirKind::Var(var) => env.lookup_val(var),
+        HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
-            ValueKind::LamClosure {
+            NirKind::LamClosure {
                 binder: Binder::new(binder.clone()),
-                annot: annot.clone(),
-                closure: Closure::new(annot, env, body.clone()),
+                annot: annot,
+                closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
-            let closure = Closure::new(annot.clone(), env, body.clone());
-            ValueKind::PiClosure {
+            NirKind::PiClosure {
                 binder: Binder::new(binder.clone()),
                 annot,
-                closure,
+                closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+        HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
             let val = val.eval(env);
-            body.eval(&env.insert_value(val)).kind().clone()
+            body.eval(env.insert_value(val, ())).kind().clone()
         }
-        TyExprKind::Expr(e) => {
-            let ty = match tye.get_type() {
-                Ok(ty) => ty,
-                Err(_) => return ValueKind::Const(Const::Sort),
-            };
-            let e = e.map_ref(|tye| tye.eval(env));
-            normalize_one_layer(e, &ty, env)
+        HirKind::Expr(e) => {
+            let e = e.map_ref(|hir| hir.eval(env));
+            normalize_one_layer(e, env)
         }
     }
 }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
deleted file mode 100644
index 607aa0d..0000000
--- a/dhall/src/semantics/nze/value.rs
+++ /dev/null
@@ -1,666 +0,0 @@
-use std::collections::HashMap;
-use std::rc::Rc;
-
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
-use crate::semantics::{
-    apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    TyEnv,
-};
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural, Span,
-};
-use crate::{Normalized, NormalizedExpr, ToExprOptions};
-
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
-/// automatically. Uses a Rc<RefCell> to share computation.
-/// If you compare for equality two `Value`s, 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<ValueInternal>);
-
-#[derive(Debug)]
-struct ValueInternal {
-    kind: lazy::Lazy<Thunk, ValueKind>,
-    /// This is None if and only if `form` is `Sort` (which doesn't have a type)
-    ty: Option<Value>,
-    span: Span,
-}
-
-/// An unevaluated subexpression
-#[derive(Debug, Clone)]
-pub(crate) enum Thunk {
-    /// A completely unnormalized expression.
-    Thunk { env: NzEnv, body: TyExpr },
-    /// A partially normalized expression that may need to go through `normalize_one_layer`.
-    PartialExpr {
-        env: NzEnv,
-        expr: ExprKind<Value, Normalized>,
-        ty: Value,
-    },
-}
-
-/// An unevaluated subexpression that takes an argument.
-#[derive(Debug, Clone)]
-pub(crate) enum Closure {
-    /// Normal closure
-    Closure {
-        arg_ty: Value,
-        env: NzEnv,
-        body: TyExpr,
-    },
-    /// Closure that ignores the argument passed
-    ConstantClosure { body: Value },
-}
-
-/// A text literal with interpolations.
-// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
-// text values must be merged.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
-
-/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
-/// normalized up to the first constructor, but subexpressions may not be fully normalized.
-/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
-/// Normal Form (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.
-/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
-/// we only need to recursively normalize its sub-`Value`s to get to the NF.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
-    /// Closures
-    LamClosure {
-        binder: Binder,
-        annot: Value,
-        closure: Closure,
-    },
-    PiClosure {
-        binder: Binder,
-        annot: Value,
-        closure: Closure,
-    },
-    AppliedBuiltin(BuiltinClosure<Value>),
-
-    Var(NzVar),
-    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>>),
-    // Also keep the type of the uniontype around
-    UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
-    // Also keep the type of the uniontype and the constructor around
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
-    TextLit(TextLit),
-    Equivalence(Value, Value),
-    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
-    PartialExpr(ExprKind<Value, Normalized>),
-}
-
-impl Value {
-    pub(crate) fn const_sort() -> Value {
-        ValueInternal::from_whnf(
-            ValueKind::Const(Const::Sort),
-            None,
-            Span::Artificial,
-        )
-        .into_value()
-    }
-    /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
-        ValueInternal::from_thunk(
-            Thunk::new(env, tye.clone()),
-            tye.get_type().ok(),
-            tye.span().clone(),
-        )
-        .into_value()
-    }
-    /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(
-        e: ExprKind<Value, Normalized>,
-        ty: Value,
-    ) -> Value {
-        // TODO: env
-        let env = NzEnv::new();
-        ValueInternal::from_thunk(
-            Thunk::from_partial_expr(env, e, ty.clone()),
-            Some(ty),
-            Span::Artificial,
-        )
-        .into_value()
-    }
-    /// Make a Value from a ValueKind
-    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
-        ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
-    }
-    pub(crate) fn from_const(c: Const) -> Self {
-        let v = ValueKind::Const(c);
-        match c {
-            Const::Type => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Kind))
-            }
-            Const::Kind => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Sort))
-            }
-            Const::Sort => Value::const_sort(),
-        }
-    }
-    pub(crate) fn from_builtin(b: Builtin) -> Self {
-        Self::from_builtin_env(b, &NzEnv::new())
-    }
-    pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::from_builtin_env(b, env.clone()),
-            typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
-        )
-    }
-    pub(crate) fn from_text(txt: impl ToString) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::TextLit(TextLit::from_text(txt.to_string())),
-            Value::from_builtin(Builtin::Text),
-        )
-    }
-
-    pub(crate) fn as_const(&self) -> Option<Const> {
-        match &*self.kind() {
-            ValueKind::Const(c) => Some(*c),
-            _ => None,
-        }
-    }
-    // pub(crate) fn span(&self) -> Span {
-    //     self.0.span.clone()
-    // }
-
-    /// 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 kind(&self) -> &ValueKind {
-        self.0.kind()
-    }
-
-    /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        if opts.normalize {
-            self.normalize();
-        }
-
-        self.to_tyexpr_noenv().to_expr(opts)
-    }
-    pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
-    }
-    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
-        self.kind().clone()
-    }
-    /// Before discarding type information, check that it matches the expected return type.
-    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
-        self.check_type(ty);
-        self.to_whnf_ignore_type()
-    }
-
-    /// Normalizes contents to normal form; faster than `normalize` if
-    /// no one else shares this.
-    pub(crate) fn normalize_mut(&mut self) {
-        match Rc::get_mut(&mut self.0) {
-            // Mutate directly if sole owner
-            Some(vint) => vint.normalize_mut(),
-            // Otherwise mutate through the refcell
-            None => self.normalize(),
-        }
-    }
-    pub(crate) fn normalize(&self) {
-        self.0.normalize()
-    }
-
-    pub(crate) fn app(&self, v: Value) -> Value {
-        let body_t = match &*self.get_type_not_sort().kind() {
-            ValueKind::PiClosure { annot, closure, .. } => {
-                v.check_type(annot);
-                closure.apply(v.clone())
-            }
-            _ => unreachable!("Internal type error"),
-        };
-        Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
-    }
-
-    /// In debug mode, panic if the provided type doesn't match the value's type.
-    /// Otherwise does nothing.
-    pub(crate) fn check_type(&self, _ty: &Value) {
-        // TODO: reenable
-        // debug_assert_eq!(
-        //     Some(ty),
-        //     self.get_type().ok().as_ref(),
-        //     "Internal type error"
-        // );
-    }
-    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
-        Ok(self.0.get_type()?.clone())
-    }
-    /// When we know the value isn't `Sort`, this gets the type directly
-    pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.get_type()
-            .expect("Internal type error: value is `Sort` but shouldn't be")
-    }
-
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
-        let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
-            ExprKind::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
-                    })
-                    .collect(),
-            )
-        };
-
-        let tye = match &*self.kind() {
-            ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
-            ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
-            self_kind => TyExprKind::Expr(match self_kind {
-                ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
-                    unreachable!()
-                }
-                ValueKind::LamClosure {
-                    binder,
-                    annot,
-                    closure,
-                } => ExprKind::Lam(
-                    binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
-                ),
-                ValueKind::PiClosure {
-                    binder,
-                    annot,
-                    closure,
-                } => ExprKind::Pi(
-                    binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
-                ),
-                ValueKind::Const(c) => ExprKind::Const(*c),
-                ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
-                ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
-                ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
-                ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
-                ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                    Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
-                    n.to_tyexpr(venv),
-                ),
-                ValueKind::NEOptionalLit(n) => {
-                    ExprKind::SomeLit(n.to_tyexpr(venv))
-                }
-                ValueKind::EmptyListLit(n) => {
-                    ExprKind::EmptyListLit(TyExpr::new(
-                        TyExprKind::Expr(ExprKind::App(
-                            Value::from_builtin(Builtin::List).to_tyexpr(venv),
-                            n.to_tyexpr(venv),
-                        )),
-                        Some(Value::from_const(Const::Type)),
-                        Span::Artificial,
-                    ))
-                }
-                ValueKind::NEListLit(elts) => ExprKind::NEListLit(
-                    elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
-                ),
-                ValueKind::TextLit(elts) => ExprKind::TextLit(
-                    elts.iter()
-                        .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
-                        .collect(),
-                ),
-                ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
-                    kvs.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
-                        .collect(),
-                ),
-                ValueKind::RecordType(kts) => ExprKind::RecordType(
-                    kts.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
-                        .collect(),
-                ),
-                ValueKind::UnionType(kts) => map_uniontype(kts),
-                ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
-                    TyExpr::new(
-                        TyExprKind::Expr(map_uniontype(kts)),
-                        Some(t.clone()),
-                        Span::Artificial,
-                    ),
-                    l.clone(),
-                ),
-                ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
-                    TyExpr::new(
-                        TyExprKind::Expr(ExprKind::Field(
-                            TyExpr::new(
-                                TyExprKind::Expr(map_uniontype(kts)),
-                                Some(uniont.clone()),
-                                Span::Artificial,
-                            ),
-                            l.clone(),
-                        )),
-                        Some(ctort.clone()),
-                        Span::Artificial,
-                    ),
-                    v.to_tyexpr(venv),
-                ),
-                ValueKind::Equivalence(x, y) => ExprKind::BinOp(
-                    BinOp::Equivalence,
-                    x.to_tyexpr(venv),
-                    y.to_tyexpr(venv),
-                ),
-                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
-            }),
-        };
-
-        TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
-    }
-    pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr(VarEnv::new())
-    }
-}
-
-impl ValueInternal {
-    fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
-        ValueInternal {
-            kind: lazy::Lazy::new_completed(k),
-            ty,
-            span,
-        }
-    }
-    fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
-        ValueInternal {
-            kind: lazy::Lazy::new(th),
-            ty,
-            span,
-        }
-    }
-    fn into_value(self) -> Value {
-        Value(Rc::new(self))
-    }
-
-    fn kind(&self) -> &ValueKind {
-        &self.kind
-    }
-    fn normalize(&self) {
-        self.kind().normalize();
-    }
-    // TODO: deprecated
-    fn normalize_mut(&mut self) {
-        self.normalize();
-    }
-
-    fn get_type(&self) -> Result<&Value, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
-    }
-}
-
-impl ValueKind {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_kind_and_type(self, t)
-    }
-
-    pub(crate) fn normalize(&self) {
-        match self {
-            ValueKind::Var(..)
-            | ValueKind::Const(_)
-            | ValueKind::BoolLit(_)
-            | ValueKind::NaturalLit(_)
-            | ValueKind::IntegerLit(_)
-            | ValueKind::DoubleLit(_) => {}
-
-            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
-                tth.normalize();
-            }
-
-            ValueKind::NEOptionalLit(th) => {
-                th.normalize();
-            }
-            ValueKind::LamClosure { annot, closure, .. }
-            | ValueKind::PiClosure { annot, closure, .. } => {
-                annot.normalize();
-                closure.normalize();
-            }
-            ValueKind::AppliedBuiltin(closure) => closure.normalize(),
-            ValueKind::NEListLit(elts) => {
-                for x in elts.iter() {
-                    x.normalize();
-                }
-            }
-            ValueKind::RecordLit(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            ValueKind::RecordType(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            ValueKind::UnionType(kts)
-            | ValueKind::UnionConstructor(_, kts, _) => {
-                for x in kts.values().flat_map(|opt| opt) {
-                    x.normalize();
-                }
-            }
-            ValueKind::UnionLit(_, v, kts, _, _) => {
-                v.normalize();
-                for x in kts.values().flat_map(|opt| opt) {
-                    x.normalize();
-                }
-            }
-            ValueKind::TextLit(tlit) => tlit.normalize(),
-            ValueKind::Equivalence(x, y) => {
-                x.normalize();
-                y.normalize();
-            }
-            ValueKind::PartialExpr(e) => {
-                e.map_ref(Value::normalize);
-            }
-        }
-    }
-
-    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
-        ValueKind::from_builtin_env(b, NzEnv::new())
-    }
-    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
-        ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
-    }
-}
-
-impl Thunk {
-    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
-        Thunk::Thunk {
-            env: env.clone(),
-            body,
-        }
-    }
-    pub fn from_partial_expr(
-        env: NzEnv,
-        expr: ExprKind<Value, Normalized>,
-        ty: Value,
-    ) -> Self {
-        Thunk::PartialExpr { env, expr, ty }
-    }
-    pub fn eval(self) -> ValueKind {
-        match self {
-            Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
-            Thunk::PartialExpr { env, expr, ty } => {
-                normalize_one_layer(expr, &ty, &env)
-            }
-        }
-    }
-}
-
-impl Closure {
-    pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
-        Closure::Closure {
-            arg_ty,
-            env: env.clone(),
-            body,
-        }
-    }
-    /// New closure that ignores its argument
-    pub fn new_constant(body: Value) -> Self {
-        Closure::ConstantClosure { body }
-    }
-
-    pub fn apply(&self, val: Value) -> Value {
-        match self {
-            Closure::Closure { env, body, .. } => {
-                body.eval(&env.insert_value(val))
-            }
-            Closure::ConstantClosure { body, .. } => body.clone(),
-        }
-    }
-    fn apply_var(&self, var: NzVar) -> Value {
-        match self {
-            Closure::Closure { arg_ty, .. } => {
-                let val = Value::from_kind_and_type(
-                    ValueKind::Var(var),
-                    arg_ty.clone(),
-                );
-                self.apply(val)
-            }
-            Closure::ConstantClosure { body, .. } => body.clone(),
-        }
-    }
-
-    // TODO: somehow normalize the body. Might require to pass an env.
-    pub fn normalize(&self) {}
-    /// Convert this closure to a TyExpr
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
-        self.apply_var(NzVar::new(venv.size()))
-            .to_tyexpr(venv.insert())
-    }
-    /// If the closure variable is free in the closure, return Err. Otherwise, return the value
-    /// with that free variable remove.
-    pub fn remove_binder(&self) -> Result<Value, ()> {
-        match self {
-            Closure::Closure { .. } => {
-                let v = NzVar::fresh();
-                // TODO: handle case where variable is used in closure
-                // TODO: return information about where the variable is used
-                Ok(self.apply_var(v))
-            }
-            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
-        }
-    }
-}
-
-impl TextLit {
-    pub fn new(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-    ) -> Self {
-        TextLit(squash_textlit(elts))
-    }
-    pub fn interpolate(v: Value) -> TextLit {
-        TextLit(vec![InterpolatedTextContents::Expr(v)])
-    }
-    pub fn from_text(s: String) -> TextLit {
-        TextLit(vec![InterpolatedTextContents::Text(s)])
-    }
-
-    pub fn concat(&self, other: &TextLit) -> TextLit {
-        TextLit::new(self.iter().chain(other.iter()).cloned())
-    }
-    pub fn is_empty(&self) -> bool {
-        self.0.is_empty()
-    }
-    /// If the literal consists of only one interpolation and not text, return the interpolated
-    /// value.
-    pub fn as_single_expr(&self) -> Option<&Value> {
-        use InterpolatedTextContents::Expr;
-        if let [Expr(v)] = self.0.as_slice() {
-            Some(v)
-        } else {
-            None
-        }
-    }
-    /// If there are no interpolations, return the corresponding text value.
-    pub fn as_text(&self) -> Option<String> {
-        use InterpolatedTextContents::Text;
-        if self.is_empty() {
-            Some(String::new())
-        } else if let [Text(s)] = self.0.as_slice() {
-            Some(s.clone())
-        } else {
-            None
-        }
-    }
-    pub fn iter(
-        &self,
-    ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
-        self.0.iter()
-    }
-    /// Normalize the contained values. This does not break the invariant because we have already
-    /// ensured that no contained values normalize to a TextLit.
-    pub fn normalize(&self) {
-        for x in self.0.iter() {
-            x.map_ref(Value::normalize);
-        }
-    }
-}
-
-impl lazy::Eval<ValueKind> for Thunk {
-    fn eval(self) -> ValueKind {
-        self.eval()
-    }
-}
-
-/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
-    fn eq(&self, other: &Self) -> bool {
-        Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
-    }
-}
-impl std::cmp::Eq for Value {}
-
-impl std::cmp::PartialEq for Thunk {
-    fn eq(&self, _other: &Self) -> bool {
-        unreachable!(
-            "Trying to compare thunks but we should only compare WHNFs"
-        )
-    }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for Closure {
-    fn eq(&self, other: &Self) -> bool {
-        let v = NzVar::fresh();
-        self.apply_var(v) == other.apply_var(v)
-    }
-}
-impl std::cmp::Eq for Closure {}
-
-impl std::fmt::Debug for Value {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let vint: &ValueInternal = &self.0;
-        let kind = vint.kind();
-        if let ValueKind::Const(c) = kind {
-            return write!(fmt, "{:?}", c);
-        }
-        let mut x = fmt.debug_struct(&format!("Value@WHNF"));
-        x.field("kind", kind);
-        if let Some(ty) = vint.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
-        x.finish()
-    }
-}
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
index 264b81d..413c759 100644
--- a/dhall/src/semantics/nze/var.rs
+++ b/dhall/src/semantics/nze/var.rs
@@ -1,7 +1,7 @@
 use crate::syntax::Label;
 
 // Exactly like a Label, but equality returns always true.
-// This is so that ValueKind equality is exactly alpha-equivalence.
+// This is so that NirKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct Binder {
     name: Label,