Merge pull request #131 from Nadrieril/hir

Decouple main expression types

18 files changed, 1817 insertions, 1830 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 907d449..61de0c7 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,11 +1,12 @@
 use crate::semantics::{
-    typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+    skip_resolve, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
 };
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V,
+    InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr,
+    V,
 };
 use crate::Normalized;
 use std::collections::HashMap;
@@ -14,32 +15,26 @@ use std::convert::TryInto;
 /// A partially applied builtin.
 /// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
-pub(crate) struct BuiltinClosure<Value> {
+pub(crate) struct BuiltinClosure<Nir> {
     pub env: NzEnv,
     pub b: Builtin,
     /// Arguments applied to the closure so far.
-    pub args: Vec<Value>,
-    /// Keeps the types of the partial applications around to be able to convert back to TyExpr.
-    /// If the args so far are `x_1`, ..., `x_n`, this contains the types of `b`, `b x1`, ...,
-    /// `b x_1 x_2 ... x_(n-1)`.
-    pub types: Vec<Value>,
+    pub args: Vec<Nir>,
 }
 
-impl BuiltinClosure<Value> {
+impl BuiltinClosure<Nir> {
     pub fn new(b: Builtin, env: NzEnv) -> Self {
         BuiltinClosure {
             env,
             b,
             args: Vec::new(),
-            types: Vec::new(),
         }
     }
 
-    pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind {
+    pub fn apply(&self, a: Nir) -> NirKind {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a.clone())).collect();
-        let types = self.types.iter().cloned().chain(once(f_ty)).collect();
-        apply_builtin(self.b, args, ret_ty, types, self.env.clone())
+        apply_builtin(self.b, args, self.env.clone())
     }
     /// This doesn't break the invariant because we already checked that the appropriate arguments
     /// did not normalize to something that allows evaluation to proceed.
@@ -48,24 +43,20 @@ impl BuiltinClosure<Value> {
             x.normalize();
         }
     }
-    pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind {
-        TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold(
+    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+        HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
-            |acc, (v, ty)| {
+            |acc, v| {
                 ExprKind::App(
-                    TyExpr::new(
-                        TyExprKind::Expr(acc),
-                        Some(ty.clone()),
-                        Span::Artificial,
-                    ),
-                    v.to_tyexpr(venv),
+                    Hir::new(HirKind::Expr(acc), Span::Artificial),
+                    v.to_hir(venv),
                 )
             },
         ))
     }
 }
 
-pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+pub(crate) fn rc(x: UnspannedExpr) -> Expr {
     Expr::new(x, Span::Artificial)
 }
 
@@ -125,9 +116,9 @@ macro_rules! make_type {
     };
 }
 
-pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+pub(crate) fn type_of_builtin(b: Builtin) -> Hir {
     use Builtin::*;
-    match b {
+    let expr = match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
         List | Optional => make_type!(
             Type -> Type
@@ -210,7 +201,8 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
         OptionalNone => make_type!(
             forall (A: Type) -> Optional A
         ),
-    }
+    };
+    skip_resolve(&expr).unwrap()
 }
 
 // Ad-hoc macro to help construct closures
@@ -249,7 +241,7 @@ macro_rules! make_closure {
         rc(ExprKind::BinOp(
             BinOp::NaturalPlus,
             make_closure!($($v)*),
-            rc(ExprKind::NaturalLit(1))
+            rc(ExprKind::Lit(LitKind::Natural(1)))
         ))
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
@@ -264,148 +256,140 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    ty: &Value,
-    types: Vec<Value>,
-    env: NzEnv,
-) -> ValueKind {
-    use Builtin::*;
-    use ValueKind::*;
+fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
+    use LitKind::{Bool, Double, Integer, Natural};
+    use NirKind::*;
 
     // Small helper enum
     enum Ret {
-        ValueKind(ValueKind),
-        Value(Value),
+        NirKind(NirKind),
+        Nir(Nir),
         DoneAsIs,
     }
-    let make_closure = |e| typecheck(&e).unwrap().eval(&env);
+    let make_closure = |e| {
+        typecheck(&skip_resolve(&e).unwrap())
+            .unwrap()
+            .eval(env.clone())
+    };
 
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
-        (NaturalIsZero, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
+        (Builtin::OptionalNone, [t]) => {
+            Ret::NirKind(EmptyOptionalLit(t.clone()))
+        }
+        (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalEven, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
+        (Builtin::NaturalEven, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalOdd, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
+        (Builtin::NaturalOdd, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalToInteger, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
+        (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalShow, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::Value(Value::from_text(n)),
+        (Builtin::NaturalShow, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
-            (NaturalLit(a), NaturalLit(b)) => {
-                Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
+        (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
+            (Lit(Natural(a)), Lit(Natural(b))) => {
+                Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 })))
             }
-            (NaturalLit(0), _) => Ret::Value(b.clone()),
-            (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
-            _ if a == b => Ret::ValueKind(NaturalLit(0)),
+            (Lit(Natural(0)), _) => Ret::Nir(b.clone()),
+            (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+            _ if a == b => Ret::NirKind(Lit(Natural(0))),
             _ => Ret::DoneAsIs,
         },
-        (IntegerShow, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
+        (Builtin::IntegerShow, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
                 let s = if *n < 0 {
                     n.to_string()
                 } else {
                     format!("+{}", n)
                 };
-                Ret::Value(Value::from_text(s))
+                Ret::Nir(Nir::from_text(s))
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerToDouble, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
-                Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
+        (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
+                Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64))))
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerNegate, [n]) => match &*n.kind() {
-            IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+        (Builtin::IntegerNegate, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))),
             _ => Ret::DoneAsIs,
         },
-        (IntegerClamp, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
-                Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+        (Builtin::IntegerClamp, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
+                Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0))))
             }
             _ => Ret::DoneAsIs,
         },
-        (DoubleShow, [n]) => match &*n.kind() {
-            DoubleLit(n) => Ret::Value(Value::from_text(n)),
+        (Builtin::DoubleShow, [n]) => match &*n.kind() {
+            Lit(Double(n)) => Ret::Nir(Nir::from_text(n)),
             _ => Ret::DoneAsIs,
         },
-        (TextShow, [v]) => match &*v.kind() {
+        (Builtin::TextShow, [v]) => match &*v.kind() {
             TextLit(tlit) => {
                 if let Some(s) = tlit.as_text() {
                     // Printing InterpolatedText takes care of all the escaping
                     let txt: InterpolatedText<Normalized> =
                         std::iter::once(InterpolatedTextContents::Text(s))
                             .collect();
-                    Ret::Value(Value::from_text(txt))
+                    Ret::Nir(Nir::from_text(txt))
                 } else {
                     Ret::DoneAsIs
                 }
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLength, [_, l]) => match &*l.kind() {
-            EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
-            NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
+        (Builtin::ListLength, [_, l]) => match &*l.kind() {
+            EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))),
+            NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))),
             _ => Ret::DoneAsIs,
         },
-        (ListHead, [_, l]) => match &*l.kind() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+        (Builtin::ListHead, [_, l]) => match &*l.kind() {
+            EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => {
-                Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
+                Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLast, [_, l]) => match &*l.kind() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
-            NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
+        (Builtin::ListLast, [_, l]) => match &*l.kind() {
+            EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => Ret::NirKind(NEOptionalLit(
                 xs.iter().rev().next().unwrap().clone(),
             )),
             _ => Ret::DoneAsIs,
         },
-        (ListReverse, [_, l]) => match &*l.kind() {
-            EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
+        (Builtin::ListReverse, [_, l]) => match &*l.kind() {
+            EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())),
             NEListLit(xs) => {
-                Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
+                Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect()))
             }
             _ => Ret::DoneAsIs,
         },
-        (ListIndexed, [_, l]) => {
-            let l_whnf = l.kind();
-            match &*l_whnf {
+        (Builtin::ListIndexed, [t, l]) => {
+            match l.kind() {
                 EmptyListLit(_) | NEListLit(_) => {
-                    // Extract the type of the list elements
-                    let t = match &*l_whnf {
-                        EmptyListLit(t) => t.clone(),
-                        NEListLit(xs) => xs[0].get_type_not_sort(),
-                        _ => unreachable!(),
-                    };
-
                     // Construct the returned record type: { index: Natural, value: t }
                     let mut kts = HashMap::new();
-                    kts.insert("index".into(), Value::from_builtin(Natural));
-                    kts.insert("value".into(), t.clone());
-                    let t = Value::from_kind_and_type(
-                        RecordType(kts),
-                        Value::from_const(Type),
+                    kts.insert(
+                        "index".into(),
+                        Nir::from_builtin(Builtin::Natural),
                     );
+                    kts.insert("value".into(), t.clone());
+                    let t = Nir::from_kind(RecordType(kts));
 
                     // Construct the new list, with added indices
-                    let list = match &*l_whnf {
+                    let list = match l.kind() {
                         EmptyListLit(_) => EmptyListLit(t),
                         NEListLit(xs) => NEListLit(
                             xs.iter()
@@ -414,31 +398,23 @@ fn apply_builtin(
                                     let mut kvs = HashMap::new();
                                     kvs.insert(
                                         "index".into(),
-                                        Value::from_kind_and_type(
-                                            NaturalLit(i),
-                                            Value::from_builtin(
-                                                Builtin::Natural,
-                                            ),
-                                        ),
+                                        Nir::from_kind(Lit(Natural(i))),
                                     );
                                     kvs.insert("value".into(), e.clone());
-                                    Value::from_kind_and_type(
-                                        RecordLit(kvs),
-                                        t.clone(),
-                                    )
+                                    Nir::from_kind(RecordLit(kvs))
                                 })
                                 .collect(),
                         ),
                         _ => unreachable!(),
                     };
-                    Ret::ValueKind(list)
+                    Ret::NirKind(list)
                 }
                 _ => Ret::DoneAsIs,
             }
         }
-        (ListBuild, [t, f]) => {
-            let list_t = Value::from_builtin(List).app(t.clone());
-            Ret::Value(
+        (Builtin::ListBuild, [t, f]) => {
+            let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
+            Ret::Nir(
                 f.app(list_t.clone())
                     .app(
                         make_closure(make_closure!(
@@ -449,23 +425,24 @@ fn apply_builtin(
                         ))
                         .app(t.clone()),
                     )
-                    .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+                    .app(EmptyListLit(t.clone()).into_nir()),
             )
         }
-        (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
-            EmptyListLit(_) => Ret::Value(nil.clone()),
+        (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
+            EmptyListLit(_) => Ret::Nir(nil.clone()),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().cloned().rev() {
                     v = cons.app(x).app(v);
                 }
-                Ret::Value(v)
+                Ret::Nir(v)
             }
             _ => Ret::DoneAsIs,
         },
-        (OptionalBuild, [t, f]) => {
-            let optional_t = Value::from_builtin(Optional).app(t.clone());
-            Ret::Value(
+        (Builtin::OptionalBuild, [t, f]) => {
+            let optional_t =
+                Nir::from_builtin(Builtin::Optional).app(t.clone());
+            Ret::Nir(
                 f.app(optional_t.clone())
                     .app(
                         make_closure(make_closure!(
@@ -475,61 +452,47 @@ fn apply_builtin(
                         ))
                         .app(t.clone()),
                     )
-                    .app(
-                        EmptyOptionalLit(t.clone())
-                            .into_value_with_type(optional_t),
-                    ),
+                    .app(EmptyOptionalLit(t.clone()).into_nir()),
             )
         }
-        (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
-            EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
-            NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
+        (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
+            EmptyOptionalLit(_) => Ret::Nir(nothing.clone()),
+            NEOptionalLit(x) => Ret::Nir(just.app(x.clone())),
             _ => Ret::DoneAsIs,
         },
-        (NaturalBuild, [f]) => Ret::Value(
-            f.app(Value::from_builtin(Natural))
+        (Builtin::NaturalBuild, [f]) => Ret::Nir(
+            f.app(Nir::from_builtin(Builtin::Natural))
                 .app(make_closure(make_closure!(
                     λ(x : Natural) ->
                     1 + var(x)
                 )))
-                .app(
-                    NaturalLit(0)
-                        .into_value_with_type(Value::from_builtin(Natural)),
-                ),
+                .app(Lit(Natural(0)).into_nir()),
         ),
 
-        (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
-            NaturalLit(0) => Ret::Value(zero.clone()),
-            NaturalLit(n) => {
-                let fold = Value::from_builtin(NaturalFold)
-                    .app(
-                        NaturalLit(n - 1)
-                            .into_value_with_type(Value::from_builtin(Natural)),
-                    )
+        (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
+            Lit(Natural(0)) => Ret::Nir(zero.clone()),
+            Lit(Natural(n)) => {
+                let fold = Nir::from_builtin(Builtin::NaturalFold)
+                    .app(Lit(Natural(n - 1)).into_nir())
                     .app(t.clone())
                     .app(succ.clone())
                     .app(zero.clone());
-                Ret::Value(succ.app(fold))
+                Ret::Nir(succ.app(fold))
             }
             _ => Ret::DoneAsIs,
         },
         _ => Ret::DoneAsIs,
     };
     match ret {
-        Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
-        Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure {
-            b,
-            args,
-            types,
-            env,
-        }),
+        Ret::NirKind(v) => v,
+        Ret::Nir(v) => v.kind().clone(),
+        Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
     }
 }
 
-impl<Value: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Value> {
+impl<Nir: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Nir> {
     fn eq(&self, other: &Self) -> bool {
         self.b == other.b && self.args == other.args
     }
 }
-impl<Value: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Value> {}
+impl<Nir: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Nir> {}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 98fdf5a..87033c9 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -5,4 +5,5 @@ pub mod resolve;
 pub mod tck;
 pub(crate) use self::builtins::*;
 pub(crate) use self::nze::*;
+pub(crate) use self::resolve::*;
 pub(crate) use self::tck::*;
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,
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
deleted file mode 100644
index 3acf114..0000000
--- a/dhall/src/semantics/resolve.rs
+++ /dev/null
@@ -1,181 +0,0 @@
-use std::collections::HashMap;
-use std::path::{Path, PathBuf};
-
-use crate::error::{Error, ImportError};
-use crate::syntax;
-use crate::syntax::{FilePath, ImportLocation, URL};
-use crate::{Normalized, NormalizedExpr, Parsed, Resolved};
-
-type Import = syntax::Import<NormalizedExpr>;
-
-/// A root from which to resolve relative imports.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ImportRoot {
-    LocalDir(PathBuf),
-}
-
-type ImportCache = HashMap<Import, Normalized>;
-
-pub(crate) type ImportStack = Vec<Import>;
-
-fn resolve_import(
-    import: &Import,
-    root: &ImportRoot,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Normalized, ImportError> {
-    use self::ImportRoot::*;
-    use syntax::FilePrefix::*;
-    use syntax::ImportLocation::*;
-    let cwd = match root {
-        LocalDir(cwd) => cwd,
-    };
-    match &import.location {
-        Local(prefix, path) => {
-            let path_buf: PathBuf = path.file_path.iter().collect();
-            let path_buf = match prefix {
-                // TODO: fail gracefully
-                Parent => cwd.parent().unwrap().join(path_buf),
-                Here => cwd.join(path_buf),
-                _ => unimplemented!("{:?}", import),
-            };
-            Ok(load_import(&path_buf, import_cache, import_stack).map_err(
-                |e| ImportError::Recursive(import.clone(), Box::new(e)),
-            )?)
-        }
-        _ => unimplemented!("{:?}", import),
-    }
-}
-
-fn load_import(
-    f: &Path,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Normalized, Error> {
-    Ok(
-        do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
-            .typecheck()?
-            .normalize(),
-    )
-}
-
-fn do_resolve_expr(
-    parsed: Parsed,
-    import_cache: &mut ImportCache,
-    import_stack: &ImportStack,
-) -> Result<Resolved, ImportError> {
-    let Parsed(mut expr, root) = parsed;
-    let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
-        if import_stack.contains(&import) {
-            return Err(ImportError::ImportCycle(import_stack.clone(), import));
-        }
-        match import_cache.get(&import) {
-            Some(expr) => Ok(expr.clone()),
-            None => {
-                // Copy the import stack and push the current import
-                let mut import_stack = import_stack.clone();
-                import_stack.push(import.clone());
-
-                // Resolve the import recursively
-                let expr = resolve_import(
-                    &import,
-                    &root,
-                    import_cache,
-                    &import_stack,
-                )?;
-
-                // Add the import to the cache
-                import_cache.insert(import, expr.clone());
-                Ok(expr)
-            }
-        }
-    };
-    expr.traverse_resolve_mut(&mut resolve)?;
-    Ok(Resolved(expr))
-}
-
-pub(crate) fn resolve(e: Parsed) -> Result<Resolved, ImportError> {
-    do_resolve_expr(e, &mut HashMap::new(), &Vec::new())
-}
-
-pub(crate) fn skip_resolve_expr(
-    parsed: Parsed,
-) -> Result<Resolved, ImportError> {
-    let mut expr = parsed.0;
-    let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
-        Err(ImportError::UnexpectedImport(import))
-    };
-    expr.traverse_resolve_mut(&mut resolve)?;
-    Ok(Resolved(expr))
-}
-
-pub trait Canonicalize {
-    fn canonicalize(&self) -> Self;
-}
-
-impl Canonicalize for FilePath {
-    fn canonicalize(&self) -> FilePath {
-        let mut file_path = Vec::new();
-        let mut file_path_components = self.file_path.clone().into_iter();
-
-        loop {
-            let component = file_path_components.next();
-            match component.as_ref() {
-                // ───────────────────
-                // canonicalize(ε) = ε
-                None => break,
-
-                // canonicalize(directory₀) = directory₁
-                // ───────────────────────────────────────
-                // canonicalize(directory₀/.) = directory₁
-                Some(c) if c == "." => continue,
-
-                Some(c) if c == ".." => match file_path_components.next() {
-                    // canonicalize(directory₀) = ε
-                    // ────────────────────────────
-                    // canonicalize(directory₀/..) = /..
-                    None => file_path.push("..".to_string()),
-
-                    // canonicalize(directory₀) = directory₁/..
-                    // ──────────────────────────────────────────────
-                    // canonicalize(directory₀/..) = directory₁/../..
-                    Some(ref c) if c == ".." => {
-                        file_path.push("..".to_string());
-                        file_path.push("..".to_string());
-                    }
-
-                    // canonicalize(directory₀) = directory₁/component
-                    // ───────────────────────────────────────────────  ; If "component" is not
-                    // canonicalize(directory₀/..) = directory₁         ; ".."
-                    Some(_) => continue,
-                },
-
-                // canonicalize(directory₀) = directory₁
-                // ─────────────────────────────────────────────────────────  ; If no other
-                // canonicalize(directory₀/component) = directory₁/component  ; rule matches
-                Some(c) => file_path.push(c.clone()),
-            }
-        }
-
-        FilePath { file_path }
-    }
-}
-
-impl<SE: Copy> Canonicalize for ImportLocation<SE> {
-    fn canonicalize(&self) -> ImportLocation<SE> {
-        match self {
-            ImportLocation::Local(prefix, file) => {
-                ImportLocation::Local(*prefix, file.canonicalize())
-            }
-            ImportLocation::Remote(url) => ImportLocation::Remote(URL {
-                scheme: url.scheme,
-                authority: url.authority.clone(),
-                path: url.path.canonicalize(),
-                query: url.query.clone(),
-                headers: url.headers.clone(),
-            }),
-            ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
-            ImportLocation::Missing => ImportLocation::Missing,
-        }
-    }
-}
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
new file mode 100644
index 0000000..43676cc
--- /dev/null
+++ b/dhall/src/semantics/resolve/env.rs
@@ -0,0 +1,104 @@
+use std::collections::HashMap;
+
+use crate::error::{Error, ImportError};
+use crate::semantics::{AlphaVar, Import, TypedHir, VarEnv};
+use crate::syntax::{Label, V};
+
+/// Environment for resolving names.
+#[derive(Debug, Clone)]
+pub(crate) struct NameEnv {
+    names: Vec<Label>,
+}
+
+pub(crate) type ImportCache = HashMap<Import, TypedHir>;
+pub(crate) type ImportStack = Vec<Import>;
+
+/// Environment for resolving imports
+#[derive(Debug, Clone)]
+pub(crate) struct ImportEnv {
+    cache: ImportCache,
+    stack: ImportStack,
+}
+
+impl NameEnv {
+    pub fn new() -> Self {
+        NameEnv { names: Vec::new() }
+    }
+    pub fn as_varenv(&self) -> VarEnv {
+        VarEnv::from_size(self.names.len())
+    }
+
+    pub fn insert(&self, x: &Label) -> Self {
+        let mut env = self.clone();
+        env.insert_mut(x);
+        env
+    }
+    pub fn insert_mut(&mut self, x: &Label) {
+        self.names.push(x.clone())
+    }
+    pub fn remove_mut(&mut self) {
+        self.names.pop();
+    }
+
+    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
+        let V(name, idx) = var;
+        let (idx, _) = self
+            .names
+            .iter()
+            .rev()
+            .enumerate()
+            .filter(|(_, n)| *n == name)
+            .nth(*idx)?;
+        Some(AlphaVar::new(idx))
+    }
+    pub fn label_var(&self, var: &AlphaVar) -> V {
+        let name = &self.names[self.names.len() - 1 - var.idx()];
+        let idx = self
+            .names
+            .iter()
+            .rev()
+            .take(var.idx())
+            .filter(|n| *n == name)
+            .count();
+        V(name.clone(), idx)
+    }
+}
+
+impl ImportEnv {
+    pub fn new() -> Self {
+        ImportEnv {
+            cache: HashMap::new(),
+            stack: Vec::new(),
+        }
+    }
+
+    pub fn handle_import(
+        &mut self,
+        import: Import,
+        mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<TypedHir, Error>,
+    ) -> Result<TypedHir, Error> {
+        if self.stack.contains(&import) {
+            return Err(
+                ImportError::ImportCycle(self.stack.clone(), import).into()
+            );
+        }
+        Ok(match self.cache.get(&import) {
+            Some(expr) => expr.clone(),
+            None => {
+                // Push the current import on the stack
+                self.stack.push(import.clone());
+
+                // Resolve the import recursively
+                let expr = do_resolve(self, &import)?;
+
+                // Remove import from the stack.
+                self.stack.pop();
+
+                // Add the import to the cache
+                self.cache.insert(import, expr.clone());
+
+                expr
+            }
+        })
+    }
+}
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
new file mode 100644
index 0000000..2f3464a
--- /dev/null
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -0,0 +1,135 @@
+use crate::error::TypeError;
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
+use crate::syntax::{Expr, ExprKind, Span, V};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct AlphaVar {
+    idx: usize,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum HirKind {
+    /// A resolved variable (i.e. a DeBruijn index)
+    Var(AlphaVar),
+    /// Result of resolving an import.
+    Import(Hir, Type),
+    // Forbidden ExprKind variants: Var, Import, Completion
+    Expr(ExprKind<Hir>),
+}
+
+// An expression with resolved variables and imports.
+#[derive(Debug, Clone)]
+pub(crate) struct Hir {
+    kind: Box<HirKind>,
+    span: Span,
+}
+
+impl AlphaVar {
+    pub(crate) fn new(idx: usize) -> Self {
+        AlphaVar { idx }
+    }
+    pub(crate) fn idx(&self) -> usize {
+        self.idx
+    }
+}
+
+impl Hir {
+    pub fn new(kind: HirKind, span: Span) -> Self {
+        Hir {
+            kind: Box::new(kind),
+            span,
+        }
+    }
+
+    pub fn kind(&self) -> &HirKind {
+        &*self.kind
+    }
+    pub fn span(&self) -> Span {
+        self.span.clone()
+    }
+
+    /// Converts a closed Hir expr back to the corresponding AST expression.
+    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        hir_to_expr(self, opts, &mut NameEnv::new())
+    }
+    /// Converts a closed Hir expr back to the corresponding AST expression.
+    pub fn to_expr_noopts(&self) -> NormalizedExpr {
+        let opts = ToExprOptions { alpha: false };
+        self.to_expr(opts)
+    }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        let opts = ToExprOptions { alpha: false };
+        let mut env = env.as_nameenv().clone();
+        hir_to_expr(self, opts, &mut env)
+    }
+
+    /// Typecheck the Hir.
+    pub fn typecheck<'hir>(
+        &'hir self,
+        env: &TyEnv,
+    ) -> Result<Tir<'hir>, TypeError> {
+        type_with(env, self, None)
+    }
+
+    /// Eval the Hir. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+        Nir::new_thunk(env.into(), self.clone())
+    }
+    /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
+    /// needed on demand.
+    pub fn eval_closed_expr(&self) -> Nir {
+        self.eval(NzEnv::new())
+    }
+    /// Eval a closed Hir fully and recursively;
+    pub fn rec_eval_closed_expr(&self) -> Nir {
+        let val = self.eval_closed_expr();
+        val.normalize();
+        val
+    }
+}
+
+fn hir_to_expr(
+    hir: &Hir,
+    opts: ToExprOptions,
+    env: &mut NameEnv,
+) -> NormalizedExpr {
+    let kind = match hir.kind() {
+        HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
+        HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
+        HirKind::Import(hir, _) => {
+            return hir_to_expr(hir, opts, &mut NameEnv::new())
+        }
+        HirKind::Expr(e) => {
+            let e = e.map_ref_maybe_binder(|l, hir| {
+                if let Some(l) = l {
+                    env.insert_mut(l);
+                }
+                let e = hir_to_expr(hir, opts, env);
+                if let Some(_) = l {
+                    env.remove_mut();
+                }
+                e
+            });
+
+            match e {
+                ExprKind::Lam(_, t, e) if opts.alpha => {
+                    ExprKind::Lam("_".into(), t, e)
+                }
+                ExprKind::Pi(_, t, e) if opts.alpha => {
+                    ExprKind::Pi("_".into(), t, e)
+                }
+                e => e,
+            }
+        }
+    };
+    Expr::new(kind, hir.span())
+}
+
+impl std::cmp::PartialEq for Hir {
+    fn eq(&self, other: &Self) -> bool {
+        self.kind == other.kind
+    }
+}
+impl std::cmp::Eq for Hir {}
diff --git a/dhall/src/semantics/resolve/mod.rs b/dhall/src/semantics/resolve/mod.rs
new file mode 100644
index 0000000..517907b
--- /dev/null
+++ b/dhall/src/semantics/resolve/mod.rs
@@ -0,0 +1,6 @@
+pub mod env;
+pub mod hir;
+pub mod resolve;
+pub(crate) use env::*;
+pub(crate) use hir::*;
+pub(crate) use resolve::*;
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
new file mode 100644
index 0000000..82800ec
--- /dev/null
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -0,0 +1,231 @@
+use std::borrow::Cow;
+use std::path::{Path, PathBuf};
+
+use crate::error::ErrorBuilder;
+use crate::error::{Error, ImportError};
+use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
+use crate::syntax;
+use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
+use crate::{Parsed, ParsedExpr, Resolved};
+
+// TODO: evaluate import headers
+pub(crate) type Import = syntax::Import<()>;
+
+/// Owned Hir with a type. Different from Tir because the Hir is owned.
+pub(crate) type TypedHir = (Hir, Type);
+
+/// A root from which to resolve relative imports.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ImportRoot {
+    LocalDir(PathBuf),
+}
+
+fn resolve_one_import(
+    env: &mut ImportEnv,
+    import: &Import,
+    root: &ImportRoot,
+) -> Result<TypedHir, Error> {
+    use self::ImportRoot::*;
+    use syntax::FilePrefix::*;
+    use syntax::ImportLocation::*;
+    let cwd = match root {
+        LocalDir(cwd) => cwd,
+    };
+    match &import.location {
+        Local(prefix, path) => {
+            let path_buf: PathBuf = path.file_path.iter().collect();
+            let path_buf = match prefix {
+                // TODO: fail gracefully
+                Parent => cwd.parent().unwrap().join(path_buf),
+                Here => cwd.join(path_buf),
+                _ => unimplemented!("{:?}", import),
+            };
+            Ok(load_import(env, &path_buf)?)
+        }
+        _ => unimplemented!("{:?}", import),
+    }
+}
+
+fn load_import(env: &mut ImportEnv, f: &Path) -> Result<TypedHir, Error> {
+    let parsed = Parsed::parse_file(f)?;
+    let typed = resolve_with_env(env, parsed)?.typecheck()?;
+    Ok((typed.normalize().to_hir(), typed.ty().clone()))
+}
+
+/// Desugar the first level of the expression.
+fn desugar(expr: &Expr) -> Cow<'_, Expr> {
+    match expr.kind() {
+        ExprKind::Completion(ty, compl) => {
+            let ty_field_default = Expr::new(
+                ExprKind::Field(ty.clone(), "default".into()),
+                expr.span(),
+            );
+            let merged = Expr::new(
+                ExprKind::BinOp(
+                    BinOp::RightBiasedRecordMerge,
+                    ty_field_default,
+                    compl.clone(),
+                ),
+                expr.span(),
+            );
+            let ty_field_type = Expr::new(
+                ExprKind::Field(ty.clone(), "Type".into()),
+                expr.span(),
+            );
+            Cow::Owned(Expr::new(
+                ExprKind::Annot(merged, ty_field_type),
+                expr.span(),
+            ))
+        }
+        _ => Cow::Borrowed(expr),
+    }
+}
+
+/// Traverse the expression, handling import alternatives and passing
+/// found imports to the provided function. Also resolving names.
+fn traverse_resolve_expr(
+    name_env: &mut NameEnv,
+    expr: &Expr,
+    f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
+) -> Result<Hir, Error> {
+    let expr = desugar(expr);
+    Ok(match expr.kind() {
+        ExprKind::Var(var) => match name_env.unlabel_var(&var) {
+            Some(v) => Hir::new(HirKind::Var(v), expr.span()),
+            None => mkerr(
+                ErrorBuilder::new(format!("unbound variable `{}`", var))
+                    .span_err(expr.span(), "not found in this scope")
+                    .format(),
+            )?,
+        },
+        ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
+            match traverse_resolve_expr(name_env, l, f) {
+                Ok(l) => l,
+                Err(_) => {
+                    match traverse_resolve_expr(name_env, r, f) {
+                        Ok(r) => r,
+                        // TODO: keep track of the other error too
+                        Err(e) => return Err(e),
+                    }
+                }
+            }
+        }
+        kind => {
+            let kind = kind.traverse_ref_maybe_binder(|l, e| {
+                if let Some(l) = l {
+                    name_env.insert_mut(l);
+                }
+                let hir = traverse_resolve_expr(name_env, e, f)?;
+                if let Some(_) = l {
+                    name_env.remove_mut();
+                }
+                Ok::<_, Error>(hir)
+            })?;
+            let kind = match kind {
+                ExprKind::Import(import) => {
+                    // TODO: evaluate import headers
+                    let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
+                    let imported = f(import)?;
+                    HirKind::Import(imported.0, imported.1)
+                }
+                kind => HirKind::Expr(kind),
+            };
+            Hir::new(kind, expr.span())
+        }
+    })
+}
+
+fn resolve_with_env(
+    env: &mut ImportEnv,
+    parsed: Parsed,
+) -> Result<Resolved, Error> {
+    let Parsed(expr, root) = parsed;
+    let resolved =
+        traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| {
+            env.handle_import(import, |env, import| {
+                resolve_one_import(env, import, &root)
+            })
+        })?;
+    Ok(Resolved(resolved))
+}
+
+pub(crate) fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
+    resolve_with_env(&mut ImportEnv::new(), parsed)
+}
+
+pub(crate) fn skip_resolve(expr: &ParsedExpr) -> Result<Hir, Error> {
+    traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| {
+        Err(ImportError::UnexpectedImport(import).into())
+    })
+}
+
+pub trait Canonicalize {
+    fn canonicalize(&self) -> Self;
+}
+
+impl Canonicalize for FilePath {
+    fn canonicalize(&self) -> FilePath {
+        let mut file_path = Vec::new();
+        let mut file_path_components = self.file_path.clone().into_iter();
+
+        loop {
+            let component = file_path_components.next();
+            match component.as_ref() {
+                // ───────────────────
+                // canonicalize(ε) = ε
+                None => break,
+
+                // canonicalize(directory₀) = directory₁
+                // ───────────────────────────────────────
+                // canonicalize(directory₀/.) = directory₁
+                Some(c) if c == "." => continue,
+
+                Some(c) if c == ".." => match file_path_components.next() {
+                    // canonicalize(directory₀) = ε
+                    // ────────────────────────────
+                    // canonicalize(directory₀/..) = /..
+                    None => file_path.push("..".to_string()),
+
+                    // canonicalize(directory₀) = directory₁/..
+                    // ──────────────────────────────────────────────
+                    // canonicalize(directory₀/..) = directory₁/../..
+                    Some(ref c) if c == ".." => {
+                        file_path.push("..".to_string());
+                        file_path.push("..".to_string());
+                    }
+
+                    // canonicalize(directory₀) = directory₁/component
+                    // ───────────────────────────────────────────────  ; If "component" is not
+                    // canonicalize(directory₀/..) = directory₁         ; ".."
+                    Some(_) => continue,
+                },
+
+                // canonicalize(directory₀) = directory₁
+                // ─────────────────────────────────────────────────────────  ; If no other
+                // canonicalize(directory₀/component) = directory₁/component  ; rule matches
+                Some(c) => file_path.push(c.clone()),
+            }
+        }
+
+        FilePath { file_path }
+    }
+}
+
+impl<SE: Copy> Canonicalize for ImportLocation<SE> {
+    fn canonicalize(&self) -> ImportLocation<SE> {
+        match self {
+            ImportLocation::Local(prefix, file) => {
+                ImportLocation::Local(*prefix, file.canonicalize())
+            }
+            ImportLocation::Remote(url) => ImportLocation::Remote(URL {
+                scheme: url.scheme,
+                authority: url.authority.clone(),
+                path: url.path.canonicalize(),
+                query: url.query.clone(),
+                headers: url.headers.clone(),
+            }),
+            ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
+            ImportLocation::Missing => ImportLocation::Missing,
+        }
+    }
+}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fc711c..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,5 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
-use crate::syntax::{Label, V};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
+use crate::syntax::Label;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy)]
@@ -7,23 +7,20 @@ pub(crate) struct VarEnv {
     size: usize,
 }
 
-/// Environment for resolving names.
-#[derive(Debug, Clone)]
-pub(crate) struct NameEnv {
-    names: Vec<Label>,
-}
-
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
 pub(crate) struct TyEnv {
     names: NameEnv,
-    items: NzEnv,
+    items: ValEnv<Type>,
 }
 
 impl VarEnv {
     pub fn new() -> Self {
         VarEnv { size: 0 }
     }
+    pub fn from_size(size: usize) -> Self {
+        VarEnv { size }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -41,84 +38,42 @@ impl VarEnv {
     }
 }
 
-impl NameEnv {
-    pub fn new() -> Self {
-        NameEnv { names: Vec::new() }
-    }
-    pub fn as_varenv(&self) -> VarEnv {
-        VarEnv {
-            size: self.names.len(),
-        }
-    }
-
-    pub fn insert(&self, x: &Label) -> Self {
-        let mut env = self.clone();
-        env.insert_mut(x);
-        env
-    }
-    pub fn insert_mut(&mut self, x: &Label) {
-        self.names.push(x.clone())
-    }
-    pub fn remove_mut(&mut self) {
-        self.names.pop();
-    }
-
-    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
-        let V(name, idx) = var;
-        let (idx, _) = self
-            .names
-            .iter()
-            .rev()
-            .enumerate()
-            .filter(|(_, n)| *n == name)
-            .nth(*idx)?;
-        Some(AlphaVar::new(idx))
-    }
-    pub fn label_var(&self, var: &AlphaVar) -> V {
-        let name = &self.names[self.names.len() - 1 - var.idx()];
-        let idx = self
-            .names
-            .iter()
-            .rev()
-            .take(var.idx())
-            .filter(|n| *n == name)
-            .count();
-        V(name.clone(), idx)
-    }
-}
-
 impl TyEnv {
     pub fn new() -> Self {
         TyEnv {
             names: NameEnv::new(),
-            items: NzEnv::new(),
+            items: ValEnv::new(),
         }
     }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-    pub fn as_nzenv(&self) -> &NzEnv {
-        &self.items
+    pub fn to_nzenv(&self) -> NzEnv {
+        self.items.discard_types()
     }
     pub fn as_nameenv(&self) -> &NameEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_type(t),
+            items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_value(e),
+            items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_ty(&var);
-        Some((var, ty))
+    pub fn lookup(&self, var: &AlphaVar) -> Type {
+        self.items.lookup_ty(&var)
+    }
+}
+
+impl<'a> From<&'a TyEnv> for NzEnv {
+    fn from(x: &'a TyEnv) -> Self {
+        x.to_nzenv()
     }
 }
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 1df2a48..93c8f48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
 pub mod env;
-pub mod tyexpr;
+pub mod tir;
 pub mod typecheck;
 pub(crate) use env::*;
-pub(crate) use tyexpr::*;
+pub(crate) use tir::*;
 pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
new file mode 100644
index 0000000..aeb7bf9
--- /dev/null
+++ b/dhall/src/semantics/tck/tir.rs
@@ -0,0 +1,175 @@
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
+use crate::NormalizedExpr;
+
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+    val: Nir,
+    univ: Universe,
+}
+
+/// A hir expression plus its inferred type.
+/// Stands for "Typed intermediate representation"
+#[derive(Debug, Clone)]
+pub(crate) struct Tir<'hir> {
+    hir: &'hir Hir,
+    ty: Type,
+}
+
+impl Universe {
+    pub fn from_const(c: Const) -> Self {
+        Universe(match c {
+            Const::Type => 0,
+            Const::Kind => 1,
+            Const::Sort => 2,
+        })
+    }
+    pub fn as_const(self) -> Option<Const> {
+        match self.0 {
+            0 => Some(Const::Type),
+            1 => Some(Const::Kind),
+            2 => Some(Const::Sort),
+            _ => None,
+        }
+    }
+    pub fn next(self) -> Self {
+        Universe(self.0 + 1)
+    }
+}
+
+impl Type {
+    pub fn new(val: Nir, univ: Universe) -> Self {
+        Type { val, univ }
+    }
+    /// Creates a new Type and infers its universe by re-typechecking its value.
+    /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
+    /// PiClosure.
+    pub fn new_infer_universe(
+        env: &TyEnv,
+        val: Nir,
+    ) -> Result<Self, TypeError> {
+        let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
+        let u = match c {
+            Some(c) => c.to_universe(),
+            None => unreachable!(
+                "internal type error: this is not a type: {:?}",
+                val
+            ),
+        };
+        Ok(Type::new(val, u))
+    }
+    pub fn from_const(c: Const) -> Self {
+        Self::new(Nir::from_const(c), c.to_universe().next())
+    }
+    pub fn from_builtin(b: Builtin) -> Self {
+        use Builtin::*;
+        match b {
+            Bool | Natural | Integer | Double | Text => {}
+            _ => unreachable!("this builtin is not a type: {}", b),
+        }
+
+        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+    }
+
+    /// Get the type of this type
+    pub fn ty(&self) -> Universe {
+        self.univ
+    }
+
+    pub fn to_nir(&self) -> Nir {
+        self.val.clone()
+    }
+    pub fn as_nir(&self) -> &Nir {
+        &self.val
+    }
+    pub fn into_nir(self) -> Nir {
+        self.val
+    }
+    pub fn as_const(&self) -> Option<Const> {
+        self.val.as_const()
+    }
+    pub fn kind(&self) -> &NirKind {
+        self.val.kind()
+    }
+
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.val.to_hir(venv)
+    }
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+    }
+}
+
+impl<'hir> Tir<'hir> {
+    pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+        Tir { hir, ty }
+    }
+
+    pub fn span(&self) -> Span {
+        self.as_hir().span()
+    }
+    pub fn ty(&self) -> &Type {
+        &self.ty
+    }
+
+    pub fn to_hir(&self) -> Hir {
+        self.as_hir().clone()
+    }
+    pub fn as_hir(&self) -> &Hir {
+        &self.hir
+    }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        self.as_hir().to_expr_tyenv(env)
+    }
+
+    /// Eval the Tir. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+        self.as_hir().eval(env.into())
+    }
+    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+        if self.ty().as_const().is_none() {
+            return mkerr(
+                ErrorBuilder::new(format!(
+                    "Expected a type, found: `{}`",
+                    self.to_expr_tyenv(env),
+                ))
+                .span_err(
+                    self.span(),
+                    format!(
+                        "this has type: `{}`",
+                        self.ty().to_expr_tyenv(env)
+                    ),
+                )
+                .help(format!(
+                    "An expression in type position must have type `Type`, \
+                     `Kind` or `Sort`",
+                ))
+                .format(),
+            );
+        }
+        Ok(())
+    }
+    /// Evaluate to a Type.
+    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+        self.ensure_is_type(env)?;
+        Ok(Type::new(
+            self.eval(env),
+            self.ty()
+                .as_const()
+                .expect("case handled in ensure_is_type")
+                .to_universe(),
+        ))
+    }
+}
+
+impl From<Const> for Universe {
+    fn from(x: Const) -> Universe {
+        Universe::from_const(x)
+    }
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
deleted file mode 100644
index 1886646..0000000
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ /dev/null
@@ -1,137 +0,0 @@
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
-use crate::syntax::{ExprKind, Span, V};
-use crate::Normalized;
-use crate::{NormalizedExpr, ToExprOptions};
-
-pub(crate) type Type = Value;
-
-/// Stores an alpha-normalized variable.
-#[derive(Debug, Clone, Copy)]
-pub struct AlphaVar {
-    idx: usize,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
-    Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr, Normalized>),
-}
-
-// An expression with inferred types at every node and resolved variables.
-#[derive(Clone)]
-pub(crate) struct TyExpr {
-    kind: Box<TyExprKind>,
-    ty: Option<Type>,
-    span: Span,
-}
-
-impl AlphaVar {
-    pub(crate) fn new(idx: usize) -> Self {
-        AlphaVar { idx }
-    }
-    pub(crate) fn idx(&self) -> usize {
-        self.idx
-    }
-}
-
-impl TyExpr {
-    pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
-        TyExpr {
-            kind: Box::new(kind),
-            ty,
-            span,
-        }
-    }
-
-    pub fn kind(&self) -> &TyExprKind {
-        &*self.kind
-    }
-    pub fn span(&self) -> Span {
-        self.span.clone()
-    }
-    pub fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
-    }
-
-    /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &mut NameEnv::new())
-    }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        let opts = ToExprOptions {
-            normalize: true,
-            alpha: false,
-        };
-        let mut env = env.as_nameenv().clone();
-        tyexpr_to_expr(self, opts, &mut env)
-    }
-
-    /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.clone())
-    }
-    /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
-    /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Value {
-        self.eval(&NzEnv::new())
-    }
-    /// Eval a closed TyExpr fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Value {
-        let mut val = self.eval_closed_expr();
-        val.normalize_mut();
-        val
-    }
-}
-
-fn tyexpr_to_expr<'a>(
-    tyexpr: &'a TyExpr,
-    opts: ToExprOptions,
-    env: &mut NameEnv,
-) -> NormalizedExpr {
-    rc(match tyexpr.kind() {
-        TyExprKind::Var(v) if opts.alpha => {
-            ExprKind::Var(V("_".into(), v.idx()))
-        }
-        TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
-        TyExprKind::Expr(e) => {
-            let e = e.map_ref_maybe_binder(|l, tye| {
-                if let Some(l) = l {
-                    env.insert_mut(l);
-                }
-                let e = tyexpr_to_expr(tye, opts, env);
-                if let Some(_) = l {
-                    env.remove_mut();
-                }
-                e
-            });
-
-            match e {
-                ExprKind::Lam(_, t, e) if opts.alpha => {
-                    ExprKind::Lam("_".into(), t, e)
-                }
-                ExprKind::Pi(_, t, e) if opts.alpha => {
-                    ExprKind::Pi("_".into(), t, e)
-                }
-                e => e,
-            }
-        }
-    })
-}
-
-impl std::fmt::Debug for TyExpr {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let mut x = fmt.debug_struct("TyExpr");
-        x.field("kind", self.kind());
-        if let Some(ty) = self.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
-        x.finish()
-    }
-}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd9a8fa..972326b 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,34 +5,44 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
-    TyExprKind, Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
+    NirKind, Tir, TyEnv, Type,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
 };
-use crate::Normalized;
 
-fn type_of_recordtype<'a>(
-    span: Span,
-    tys: impl Iterator<Item = Cow<'a, TyExpr>>,
-) -> Result<Type, TypeError> {
-    let span_err = |msg: &str| {
-        mkerr(
-            ErrorBuilder::new(msg.to_string())
-                .span_err(span.clone(), msg.to_string())
-                .format(),
-        )
+fn check_rectymerge(
+    span: &Span,
+    env: &TyEnv,
+    x: Nir,
+    y: Nir,
+) -> Result<(), TypeError> {
+    let kts_x = match x.kind() {
+        NirKind::RecordType(kts) => kts,
+        _ => {
+            return mk_span_err(
+                span.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
     };
-    // An empty record type has type Type
-    let mut k = Const::Type;
-    for t in tys {
-        match t.get_type()?.as_const() {
-            Some(c) => k = max(k, c),
-            None => return span_err("InvalidFieldType"),
+    let kts_y = match y.kind() {
+        NirKind::RecordType(kts) => kts,
+        _ => {
+            return mk_span_err(
+                span.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
+    };
+    for (k, tx) in kts_x {
+        if let Some(ty) = kts_y.get(k) {
+            // TODO: store Type in RecordType ?
+            check_rectymerge(span, env, tx.clone(), ty.clone())?;
         }
     }
-    Ok(Value::from_const(k))
+    Ok(())
 }
 
 fn function_check(a: Const, b: Const) -> Const {
@@ -43,90 +53,62 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
-    Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
+    Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
+}
+
+pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
+    mkerr(
+        ErrorBuilder::new(msg.to_string())
+            .span_err(span, msg.to_string())
+            .format(),
+    )
 }
 
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<TyExpr, Normalized>,
+    ekind: ExprKind<Tir<'_>>,
     span: Span,
-) -> Result<TyExpr, TypeError> {
-    let span_err = |msg: &str| {
-        mkerr(
-            ErrorBuilder::new(msg.to_string())
-                .span_err(span.clone(), msg.to_string())
-                .format(),
-        )
-    };
+) -> Result<Type, TypeError> {
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
-        ExprKind::Import(..) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
         ExprKind::Var(..)
         | ExprKind::Const(Const::Sort)
-        | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
-
-        ExprKind::Lam(binder, annot, body) => {
-            let body_ty = body.get_type()?;
-            let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
-            let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
-            type_one_layer(env, pi_ekind, Span::Artificial)?
-                .eval(env.as_nzenv())
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
+        | ExprKind::Annot(..) => {
+            unreachable!("This case should have been handled in type_with")
         }
-        ExprKind::Pi(_, annot, body) => {
-            let ks = match annot.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(
-                        ErrorBuilder::new(format!(
-                            "Invalid input type: `{}`",
-                            annot.get_type()?.to_expr_tyenv(env),
-                        ))
-                        .span_err(
-                            annot.span(),
-                            format!(
-                                "this has type: `{}`",
-                                annot.get_type()?.to_expr_tyenv(env)
-                            ),
-                        )
-                        .help(format!(
-                            "The input type of a function must have type \
-                             `Type`, `Kind` or `Sort`",
-                        ))
-                        .format(),
-                    );
-                }
-            };
-            let kt = match body.get_type()?.as_const() {
-                Some(k) => k,
-                _ => return span_err("Invalid output type"),
-            };
 
-            Value::from_const(function_check(ks, kt))
-        }
-        ExprKind::Let(_, _, _, body) => body.get_type()?,
-
-        ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
-        ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
+        ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
+        ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
-            let t_expr = type_of_builtin(*b);
-            let t_tyexpr = type_with(env, &t_expr)?;
-            t_tyexpr.eval(env.as_nzenv())
-        }
-        ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
-        ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
-        ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
-        ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
+            let t_hir = type_of_builtin(*b);
+            typecheck(&t_hir)?.eval_to_type(env)?
+        }
+        ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
+        ExprKind::Lit(LitKind::Natural(_)) => {
+            Type::from_builtin(Builtin::Natural)
+        }
+        ExprKind::Lit(LitKind::Integer(_)) => {
+            Type::from_builtin(Builtin::Integer)
+        }
+        ExprKind::Lit(LitKind::Double(_)) => {
+            Type::from_builtin(Builtin::Double)
+        }
         ExprKind::TextLit(interpolated) => {
-            let text_type = Value::from_builtin(Builtin::Text);
+            let text_type = Type::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
-                    if x.get_type()? != text_type {
+                    if *x.ty() != text_type {
                         return span_err("InvalidTextInterpolation");
                     }
                 }
@@ -134,9 +116,9 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval(env.as_nzenv());
-            match &*t.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+            let t = t.eval_to_type(env)?;
+            match t.kind() {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
                     ..
@@ -149,49 +131,57 @@ fn type_one_layer(
             let mut iter = xs.iter();
             let x = iter.next().unwrap();
             for y in iter {
-                if x.get_type()? != y.get_type()? {
+                if x.ty() != y.ty() {
                     return span_err("InvalidListElement");
                 }
             }
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
+            if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
-            Value::from_builtin(Builtin::List).app(t)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
         }
         ExprKind::SomeLit(x) => {
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
+            if x.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            Value::from_builtin(Builtin::Optional).app(t)
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::Optional)
+                .app(t)
+                .to_type(Const::Type)
         }
         ExprKind::RecordLit(kvs) => {
             use std::collections::hash_map::Entry;
             let mut kts = HashMap::new();
+            // An empty record type has type Type
+            let mut k = Const::Type;
             for (x, v) in kvs {
                 // Check for duplicated entries
                 match kts.entry(x.clone()) {
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.get_type()?),
+                    Entry::Vacant(e) => e.insert(v.ty().to_nir()),
                 };
+
+                // Check that the fields have a valid kind
+                match v.ty().ty().as_const() {
+                    Some(c) => k = max(k, c),
+                    None => return span_err("InvalidFieldType"),
+                }
             }
 
-            let ty = type_of_recordtype(
-                span.clone(),
-                kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
-            )?;
-            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
         }
         ExprKind::RecordType(kts) => {
             use std::collections::hash_map::Entry;
             let mut seen_fields = HashMap::new();
-            for (x, _) in kts {
+            // An empty record type has type Type
+            let mut k = Const::Type;
+
+            for (x, t) in kts {
                 // Check for duplicated entries
                 match seen_fields.entry(x.clone()) {
                     Entry::Occupied(_) => {
@@ -199,12 +189,15 @@ fn type_one_layer(
                     }
                     Entry::Vacant(e) => e.insert(()),
                 };
+
+                // Check the type is a Const and compute final type
+                match t.ty().as_const() {
+                    Some(c) => k = max(k, c),
+                    None => return span_err("InvalidFieldType"),
+                }
             }
 
-            type_of_recordtype(
-                span.clone(),
-                kts.iter().map(|(_, t)| Cow::Borrowed(t)),
-            )?
+            Type::from_const(k)
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -213,7 +206,7 @@ fn type_one_layer(
             let mut k = None;
             for (x, t) in kts {
                 if let Some(t) = t {
-                    match (k, t.get_type()?.as_const()) {
+                    match (k, t.ty().as_const()) {
                         (None, Some(k2)) => k = Some(k2),
                         (Some(k1), Some(k2)) if k1 == k2 => {}
                         _ => return span_err("InvalidFieldType"),
@@ -231,80 +224,52 @@ fn type_one_layer(
             // an union type with only unary variants also has type Type
             let k = k.unwrap_or(Const::Type);
 
-            Value::from_const(k)
+            Type::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
-            match &*scrut.get_type()?.kind() {
-                ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => tth.clone(),
+            match scrut.ty().kind() {
+                NirKind::RecordType(kts) => match kts.get(&x) {
+                    Some(val) => Type::new_infer_universe(env, val.clone())?,
                     None => return span_err("MissingRecordField"),
                 },
-                // TODO: branch here only when scrut.get_type() is a Const
-                _ => {
-                    let scrut_nf = scrut.eval(env.as_nzenv());
-                    match scrut_nf.kind() {
-                        ValueKind::UnionType(kts) => match kts.get(x) {
+                NirKind::Const(_) => {
+                    let scrut = scrut.eval_to_type(env)?;
+                    match scrut.kind() {
+                        NirKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
-                                // Can't fail because uniontypes must have type Const(_).
-                                let kt = scrut.get_type()?.as_const().unwrap();
-                                // The type of the field must be Const smaller than `kt`, thus the
-                                // function type has type `kt`.
-                                let pi_ty = Value::from_const(kt);
-
-                                Value::from_kind_and_type(
-                                    ValueKind::PiClosure {
-                                        binder: Binder::new(x.clone()),
-                                        annot: ty.clone(),
-                                        closure: Closure::new_constant(
-                                            scrut_nf,
-                                        ),
-                                    },
-                                    pi_ty,
-                                )
+                                Nir::from_kind(NirKind::PiClosure {
+                                    binder: Binder::new(x.clone()),
+                                    annot: ty.clone(),
+                                    closure: Closure::new_constant(
+                                        scrut.to_nir(),
+                                    ),
+                                })
+                                .to_type(scrut.ty())
                             }
-                            Some(None) => scrut_nf,
+                            Some(None) => scrut,
                             None => return span_err("MissingUnionField"),
                         },
                         _ => return span_err("NotARecord"),
                     }
-                } // _ => span_err("NotARecord"),
-            }
-        }
-        ExprKind::Annot(x, t) => {
-            let t = t.eval(env.as_nzenv());
-            let x_ty = x.get_type()?;
-            if x_ty != t {
-                return span_err(&format!(
-                    "annot mismatch: ({} : {}) : {}",
-                    x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
-                    t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
-                ));
-                // return span_err(format!(
-                //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
-                //     t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
-                // ));
-                // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
+                }
+                _ => return span_err("NotARecord"),
             }
-            x_ty
         }
         ExprKind::Assert(t) => {
-            let t = t.eval(env.as_nzenv());
-            match &*t.kind() {
-                ValueKind::Equivalence(x, y) if x == y => {}
-                ValueKind::Equivalence(..) => {
-                    return span_err("AssertMismatch")
-                }
+            let t = t.eval_to_type(env)?;
+            match t.kind() {
+                NirKind::Equivalence(x, y) if x == y => {}
+                NirKind::Equivalence(..) => return span_err("AssertMismatch"),
                 _ => return span_err("AssertMustTakeEquivalence"),
             }
             t
         }
         ExprKind::App(f, arg) => {
-            match f.get_type()?.kind() {
-                ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.get_type()? != *annot {
+            match f.ty().kind() {
+                // TODO: store Type in closure
+                NirKind::PiClosure { annot, closure, .. } => {
+                    if arg.ty().as_nir() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -320,25 +285,25 @@ fn type_one_layer(
                                 arg.span(),
                                 format!(
                                     "but this has type: {}",
-                                    arg.get_type()?.to_expr_tyenv(env),
+                                    arg.ty().to_expr_tyenv(env),
                                 ),
                             )
                             .note(format!(
                                 "expected type `{}`\n   found type `{}`",
                                 annot.to_expr_tyenv(env),
-                                arg.get_type()?.to_expr_tyenv(env),
+                                arg.ty().to_expr_tyenv(env),
                             ))
                             .format(),
                         );
                     }
 
-                    let arg_nf = arg.eval(env.as_nzenv());
-                    closure.apply(arg_nf)
+                    let arg_nf = arg.eval(env);
+                    Type::new_infer_universe(env, closure.apply(arg_nf))?
                 }
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
                         "expected function, found `{}`",
-                        f.get_type()?.to_expr_tyenv(env)
+                        f.ty().to_expr_tyenv(env)
                     ))
                     .span_err(
                         f.span(),
@@ -349,33 +314,30 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-                return span_err("IfBranchMustBeTerm");
-            }
-            if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+            if y.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
-            if y.get_type()? != z.get_type()? {
+            if y.ty() != z.ty() {
                 return span_err("IfBranchMismatch");
             }
 
-            y.get_type()?
+            y.ty().clone()
         }
         ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
-            let x_type = x.get_type()?;
-            let y_type = y.get_type()?;
+            let x_type = x.ty();
+            let y_type = y.ty();
 
             // Extract the LHS record type
             let kts_x = match x_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
             // Extract the RHS record type
             let kts_y = match y_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("MustCombineRecord"),
             };
 
@@ -385,80 +347,59 @@ fn type_one_layer(
                 Ok(r_t.clone())
             })?;
 
-            // Construct the final record type
-            let ty = type_of_recordtype(
-                span.clone(),
-                kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
-            )?;
-            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+            let u = max(x.ty().ty(), y.ty().ty());
+            Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            let ekind = ExprKind::BinOp(
-                BinOp::RecursiveRecordTypeMerge,
-                x.get_type()?.to_tyexpr(env.as_varenv()),
-                y.get_type()?.to_tyexpr(env.as_varenv()),
+            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
+
+            let hir = Hir::new(
+                HirKind::Expr(ExprKind::BinOp(
+                    BinOp::RecursiveRecordTypeMerge,
+                    x.ty().to_hir(env.as_varenv()),
+                    y.ty().to_hir(env.as_varenv()),
+                )),
+                span.clone(),
             );
-            type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
+            let x_u = x.ty().ty();
+            let y_u = y.ty().ty();
+            Type::new(hir.eval(env), max(x_u, y_u))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.eval(env.as_nzenv());
-            let y_val = y.eval(env.as_nzenv());
-            let kts_x = match x_val.kind() {
-                ValueKind::RecordType(kts) => kts,
-                _ => return span_err("RecordTypeMergeRequiresRecordType"),
-            };
-            let kts_y = match y_val.kind() {
-                ValueKind::RecordType(kts) => kts,
-                _ => return span_err("RecordTypeMergeRequiresRecordType"),
-            };
-            for (k, tx) in kts_x {
-                if let Some(ty) = kts_y.get(k) {
-                    type_one_layer(
-                        env,
-                        ExprKind::BinOp(
-                            BinOp::RecursiveRecordTypeMerge,
-                            tx.to_tyexpr(env.as_varenv()),
-                            ty.to_tyexpr(env.as_varenv()),
-                        ),
-                        Span::Artificial,
-                    )?;
-                }
-            }
+            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
 
             // A RecordType's type is always a const
-            let xk = x.get_type()?.as_const().unwrap();
-            let yk = y.get_type()?.as_const().unwrap();
-            Value::from_const(max(xk, yk))
+            let xk = x.ty().as_const().unwrap();
+            let yk = y.ty().as_const().unwrap();
+            Type::from_const(max(xk, yk))
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
-            let l_ty = l.get_type()?;
-            match &*l_ty.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+            match l.ty().kind() {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
                 }) => {}
                 _ => return span_err("BinOpTypeMismatch"),
             }
 
-            if l_ty != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("BinOpTypeMismatch");
             }
 
-            l_ty
+            l.ty().clone()
         }
         ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-            if l.get_type()? != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+            if l.ty().ty().as_const() != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
-            Value::from_const(Const::Type)
+            Type::from_const(Const::Type)
         }
         ExprKind::BinOp(o, l, r) => {
-            let t = Value::from_builtin(match o {
+            let t = Type::from_builtin(match o {
                 BinOp::BoolAnd
                 | BinOp::BoolOr
                 | BinOp::BoolEQ
@@ -473,27 +414,27 @@ fn type_one_layer(
                 BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
             });
 
-            if l.get_type()? != t {
+            if *l.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
-            if r.get_type()? != t {
+            if *r.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
             t
         }
         ExprKind::Merge(record, union, type_annot) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let handlers = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("Merge1ArgMustBeRecord"),
             };
 
-            let union_type = union.get_type()?;
+            let union_type = union.ty();
             let variants = match union_type.kind() {
-                ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::UnionType(kts) => Cow::Borrowed(kts),
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::Optional,
                     args,
                     ..
@@ -509,10 +450,10 @@ fn type_one_layer(
 
             let mut inferred_type = None;
             for (x, handler_type) in handlers {
-                let handler_return_type = match variants.get(x) {
+                let handler_return_type: Type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => match handler_type.kind() {
-                        ValueKind::PiClosure { closure, annot, .. } => {
+                        NirKind::PiClosure { closure, annot, .. } => {
                             if variant_type != annot {
                                 return mkerr(
                                     ErrorBuilder::new(format!(
@@ -543,8 +484,11 @@ fn type_one_layer(
                                 );
                             }
 
+                            // TODO: this actually doesn't check anything yet
                             match closure.remove_binder() {
-                                Ok(v) => v,
+                                Ok(v) => {
+                                    Type::new_infer_universe(env, v.clone())?
+                                }
                                 Err(()) => {
                                     return span_err(
                                         "MergeReturnTypeIsDependent",
@@ -588,7 +532,9 @@ fn type_one_layer(
                         }
                     },
                     // Union alternative without type
-                    Some(None) => handler_type.clone(),
+                    Some(None) => {
+                        Type::new_infer_universe(env, handler_type.clone())?
+                    }
                     None => return span_err("MergeHandlerMissingVariant"),
                 };
                 match &inferred_type {
@@ -606,8 +552,10 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot =
-                type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
+            let type_annot = type_annot
+                .as_ref()
+                .map(|t| t.eval_to_type(env))
+                .transpose()?;
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -621,9 +569,12 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            let record_t = record.get_type()?;
+            if record.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("`toMap` only accepts records of type `Type`");
+            }
+            let record_t = record.ty();
             let kts = match record_t.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => {
                     return span_err("The argument to `toMap` must be a record")
                 }
@@ -638,12 +589,12 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval(env.as_nzenv());
+                let annot_val = annot.eval_to_type(env)?;
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
                 let arg = match annot_val.kind() {
-                    ValueKind::AppliedBuiltin(BuiltinClosure {
+                    NirKind::AppliedBuiltin(BuiltinClosure {
                         b: Builtin::List,
                         args,
                         ..
@@ -651,14 +602,14 @@ fn type_one_layer(
                     _ => return span_err(err_msg),
                 };
                 let kts = match arg.kind() {
-                    ValueKind::RecordType(kts) => kts,
+                    NirKind::RecordType(kts) => kts,
                     _ => return span_err(err_msg),
                 };
                 if kts.len() != 2 {
                     return span_err(err_msg);
                 }
                 match kts.get(&"mapKey".into()) {
-                    Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
                     _ => return span_err(err_msg),
                 }
                 match kts.get(&"mapValue".into()) {
@@ -668,11 +619,6 @@ fn type_one_layer(
                 annot_val
             } else {
                 let entry_type = kts.iter().next().unwrap().1.clone();
-                if entry_type.get_type()?.as_const() != Some(Const::Type) {
-                    return span_err(
-                        "`toMap` only accepts records of type `Type`",
-                    );
-                }
                 for (_, t) in kts.iter() {
                     if *t != entry_type {
                         return span_err(
@@ -682,16 +628,13 @@ fn type_one_layer(
                 }
 
                 let mut kts = HashMap::new();
-                kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
                 kts.insert("mapValue".into(), entry_type);
-                let output_type = Value::from_builtin(Builtin::List).app(
-                    Value::from_kind_and_type(
-                        ValueKind::RecordType(kts),
-                        Value::from_const(Const::Type),
-                    ),
-                );
+                let output_type: Type = Nir::from_builtin(Builtin::List)
+                    .app(Nir::from_kind(NirKind::RecordType(kts)))
+                    .to_type(Const::Type);
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval(env.as_nzenv());
+                    let annot_val = annot.eval_to_type(env)?;
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -700,9 +643,9 @@ fn type_one_layer(
             }
         }
         ExprKind::Projection(record, labels) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
@@ -722,21 +665,21 @@ fn type_one_layer(
                 };
             }
 
-            Value::from_kind_and_type(
-                ValueKind::RecordType(new_kts),
-                record_type.get_type()?,
-            )
+            Type::new_infer_universe(
+                env,
+                Nir::from_kind(NirKind::RecordType(new_kts)),
+            )?
         }
         ExprKind::ProjectionByExpr(record, selection) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let rec_kts = match record_type.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval(env.as_nzenv());
+            let selection_val = selection.eval_to_type(env)?;
             let sel_kts = match selection_val.kind() {
-                ValueKind::RecordType(kts) => kts,
+                NirKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
             };
 
@@ -753,110 +696,119 @@ fn type_one_layer(
 
             selection_val
         }
-        ExprKind::Completion(ty, compl) => {
-            let ty_field_default = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "default".into()),
-                span.clone(),
-            )?;
-            let ty_field_type = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "Type".into()),
-                span.clone(),
-            )?;
-            let merge = type_one_layer(
-                env,
-                ExprKind::BinOp(
-                    BinOp::RightBiasedRecordMerge,
-                    ty_field_default,
-                    compl.clone(),
-                ),
-                span.clone(),
-            )?;
-            return type_one_layer(
-                env,
-                ExprKind::Annot(merge, ty_field_type),
-                span.clone(),
-            );
-        }
     };
 
-    Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
+    Ok(ty)
 }
 
-/// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(
+/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
+/// to compare with.
+pub(crate) fn type_with<'hir>(
     env: &TyEnv,
-    expr: &Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    let (tyekind, ty) = match expr.as_ref() {
-        ExprKind::Var(var) => match env.lookup(&var) {
-            Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
-            None => {
-                return mkerr(
-                    ErrorBuilder::new(format!("unbound variable `{}`", var))
-                        .span_err(expr.span(), "not found in this scope")
-                        .format(),
-                )
-            }
-        },
-        ExprKind::Const(Const::Sort) => {
-            (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
-        }
-        ExprKind::Embed(p) => {
-            return Ok(p.clone().into_value().to_tyexpr_noenv())
-        }
-        ekind => {
-            let ekind = match ekind {
-                ExprKind::Lam(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
-                    let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
-                    ExprKind::Lam(binder.clone(), annot, body)
-                }
-                ExprKind::Pi(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
-                    let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
-                    ExprKind::Pi(binder.clone(), annot, body)
-                }
-                ExprKind::Let(binder, annot, val, body) => {
-                    let val = if let Some(t) = annot {
-                        t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
-                    } else {
-                        val.clone()
-                    };
-                    let val = type_with(env, &val)?;
-                    val.get_type()?; // Ensure val is not Sort
-                    let val_nf = val.eval(&env.as_nzenv());
-                    let body_env = env.insert_value(&binder, val_nf);
-                    let body = type_with(&body_env, body)?;
-                    ExprKind::Let(binder.clone(), None, val, body)
+    hir: &'hir Hir,
+    annot: Option<Type>,
+) -> Result<Tir<'hir>, TypeError> {
+    let tir = match hir.kind() {
+        HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
+        HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
+        HirKind::Expr(ExprKind::Var(_)) => {
+            unreachable!("Hir should contain no unresolved variables")
+        }
+        HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+            return mk_span_err(hir.span(), "Sort does not have a type")
+        }
+        HirKind::Expr(ExprKind::Annot(x, t)) => {
+            let t = match t.kind() {
+                HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+                    Type::from_const(Const::Sort)
                 }
-                _ => ekind.traverse_ref(|e| type_with(env, e))?,
+                _ => type_with(env, t, None)?.eval_to_type(env)?,
             };
-            return type_one_layer(env, ekind, expr.span());
+            type_with(env, x, Some(t))?
+        }
+
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_nf = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_nf);
+            let body = type_with(&body_env, body, None)?;
+
+            let u_annot = annot.ty().as_const().unwrap();
+            let u_body = match body.ty().ty().as_const() {
+                Some(k) => k,
+                _ => return mk_span_err(hir.span(), "Invalid output type"),
+            };
+            let u = function_check(u_annot, u_body).to_universe();
+            let ty_hir = Hir::new(
+                HirKind::Expr(ExprKind::Pi(
+                    binder.clone(),
+                    annot.to_hir(),
+                    body.ty().to_hir(body_env.as_varenv()),
+                )),
+                hir.span(),
+            );
+            let ty = Type::new(ty_hir.eval(env), u);
+
+            Tir::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_val = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_val);
+            let body = type_with(&body_env, body, None)?;
+            body.ensure_is_type(env)?;
+
+            let ks = annot.ty().as_const().unwrap();
+            let kt = body.ty().as_const().unwrap();
+            let ty = Type::from_const(function_check(ks, kt));
+            Tir::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
+            let val_annot = annot
+                .as_ref()
+                .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?))
+                .transpose()?;
+            let val = type_with(env, &val, val_annot)?;
+            let val_nf = val.eval(env);
+            let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
+            let body = type_with(&body_env, body, None)?;
+            let ty = body.ty().clone();
+            Tir::from_hir(hir, ty)
+        }
+        HirKind::Expr(ekind) => {
+            let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
+            let ty = type_one_layer(env, ekind, hir.span())?;
+            Tir::from_hir(hir, ty)
         }
     };
 
-    Ok(TyExpr::new(tyekind, ty, expr.span()))
+    if let Some(annot) = annot {
+        if *tir.ty() != annot {
+            return mk_span_err(
+                hir.span(),
+                &format!(
+                    "annot mismatch: {} != {}",
+                    tir.ty().to_expr_tyenv(env),
+                    annot.to_expr_tyenv(env)
+                ),
+            );
+        }
+    }
+
+    Ok(tir)
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
-    let res = type_with(&TyEnv::new(), e)?;
-    // Ensure that the inferred type exists (i.e. this is not Sort)
-    res.get_type()?;
-    Ok(res)
+pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
+    type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(
-    expr: &Expr<Normalized>,
-    ty: Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+pub(crate) fn typecheck_with<'hir>(
+    hir: &'hir Hir,
+    ty: Hir,
+) -> Result<Tir<'hir>, TypeError> {
+    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
+    type_with(&TyEnv::new(), hir, Some(ty))
 }