Merge branch 'refactor-typechecking'

9 files changed, 1719 insertions, 756 deletions

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index bb1a4e4..4d55f4a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,4 +1,5 @@
 use crate::imports::ImportRoot;
+use crate::normalize::{Thunk, Value};
 use dhall_core::*;
 use std::marker::PhantomData;
 
@@ -10,6 +11,8 @@ macro_rules! derive_other_traits {
             }
         }
 
+        impl<'a> std::cmp::Eq for $ty<'a> {}
+
         impl<'a> std::fmt::Display for $ty<'a> {
             fn fmt(
                 &self,
@@ -21,34 +24,149 @@ macro_rules! derive_other_traits {
     };
 }
 
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
 pub(crate) struct Parsed<'a>(
     pub(crate) SubExpr<Span<'a>, Import>,
     pub(crate) ImportRoot,
 );
 derive_other_traits!(Parsed);
 
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
 pub(crate) struct Resolved<'a>(
     pub(crate) SubExpr<Span<'a>, Normalized<'static>>,
 );
 derive_other_traits!(Resolved);
 
-#[derive(Debug, Clone, Eq)]
+pub(crate) use self::typed::TypedInternal;
+
+#[derive(Debug, Clone)]
 pub(crate) struct Typed<'a>(
-    pub(crate) SubExpr<X, Normalized<'static>>,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
-derive_other_traits!(Typed);
 
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
 pub(crate) struct Normalized<'a>(
-    pub(crate) SubExpr<X, X>,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
-derive_other_traits!(Normalized);
+
+impl<'a> std::cmp::PartialEq for Normalized<'a> {
+    fn eq(&self, other: &Self) -> bool {
+        self.to_expr() == other.to_expr()
+    }
+}
+
+impl<'a> std::cmp::Eq for Normalized<'a> {}
+
+impl<'a> std::fmt::Display for Normalized<'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+        self.to_expr().fmt(f)
+    }
+}
+
+mod typed {
+    use super::{Type, Typed};
+    use crate::normalize::{Thunk, Value};
+    use crate::typecheck::{
+        TypeError, TypeInternal, TypeMessage, TypecheckContext,
+    };
+    use dhall_core::{Const, Label, SubExpr, V, X};
+    use std::borrow::Cow;
+    use std::marker::PhantomData;
+
+    #[derive(Debug, Clone)]
+    pub(crate) enum TypedInternal {
+        // The `Sort` higher-kinded type doesn't have a type
+        Sort,
+        // Any other value, along with its type
+        Value(Thunk, Option<Type<'static>>),
+    }
+
+    impl TypedInternal {
+        pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+            TypedInternal::Value(th, Some(t))
+        }
+
+        pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+            TypedInternal::Value(th, None)
+        }
+
+        // TODO: Avoid cloning if possible
+        pub(crate) fn to_value(&self) -> Value {
+            match self {
+                TypedInternal::Value(th, _) => th.normalize_whnf().clone(),
+                TypedInternal::Sort => Value::Const(Const::Sort),
+            }
+        }
+
+        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+            self.to_value().normalize_to_expr()
+        }
+
+        pub(crate) fn to_thunk(&self) -> Thunk {
+            match self {
+                TypedInternal::Value(th, _) => th.clone(),
+                TypedInternal::Sort => {
+                    Thunk::from_whnf(Value::Const(Const::Sort))
+                }
+            }
+        }
+
+        pub(crate) fn to_type(&self) -> Type<'static> {
+            match self {
+                TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
+                TypedInternal::Value(th, _) => match &*th.normalize_whnf() {
+                    Value::Const(c) => Type(TypeInternal::Const(*c)),
+                    _ => Type(TypeInternal::Typed(Box::new(Typed(
+                        self.clone(),
+                        PhantomData,
+                    )))),
+                },
+            }
+        }
+
+        pub(crate) fn get_type(
+            &self,
+        ) -> Result<Cow<'_, Type<'static>>, TypeError> {
+            match self {
+                TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+                TypedInternal::Value(_, None) => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Untyped,
+                )),
+                TypedInternal::Sort => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Sort,
+                )),
+            }
+        }
+
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.shift(delta, var),
+                    t.as_ref().map(|x| x.shift(delta, var)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
+
+        pub(crate) fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &Typed<'static>,
+        ) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.subst_shift(var, val),
+                    t.as_ref().map(|x| x.subst_shift(var, val)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
+    }
+}
 
 /// A Dhall expression representing a simple type.
 ///
@@ -56,13 +174,15 @@ derive_other_traits!(Normalized);
 /// `Bool`, `{ x: Integer }` or `Natural -> Text`.
 ///
 /// For a more general notion of "type", see [Type].
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
 pub struct SimpleType<'a>(
     pub(crate) SubExpr<X, X>,
     pub(crate) PhantomData<&'a ()>,
 );
 derive_other_traits!(SimpleType);
 
+pub(crate) use crate::typecheck::TypeInternal;
+
 /// A Dhall expression representing a (possibly higher-kinded) type.
 ///
 /// This includes [SimpleType]s but also higher-kinded expressions like
@@ -70,12 +190,10 @@ derive_other_traits!(SimpleType);
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Type<'a>(pub(crate) TypeInternal<'a>);
 
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum TypeInternal<'a> {
-    Expr(Box<Normalized<'a>>),
-    Const(dhall_core::Const),
-    /// The type of `Sort`
-    SuperType,
+impl<'a> std::fmt::Display for Type<'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+        self.to_normalized().fmt(f)
+    }
 }
 
 // Exposed for the macros
@@ -98,50 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> {
 #[doc(hidden)]
 impl<'a> From<Normalized<'a>> for Typed<'a> {
     fn from(x: Normalized<'a>) -> Typed<'a> {
-        Typed(x.0.embed_absurd(), x.1, x.2)
+        Typed(x.0, x.1)
     }
 }
 
-#[doc(hidden)]
-impl<'a> Typed<'a> {
-    pub(crate) fn as_expr(&self) -> &SubExpr<X, Normalized<'a>> {
-        &self.0
-    }
-}
-
-#[doc(hidden)]
 impl<'a> Normalized<'a> {
-    pub(crate) fn as_expr(&self) -> &SubExpr<X, X> {
-        &self.0
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData)
     }
-    pub(crate) fn into_expr(self) -> SubExpr<X, X> {
-        self.0
+    // Deprecated
+    pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
+        self.0.to_expr()
     }
-    pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
-        Normalized(self.0, self.1, PhantomData)
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+        self.0.to_expr()
     }
-    pub(crate) fn into_type(self) -> Type<'a> {
-        Type(match self.0.as_ref() {
-            ExprF::Const(c) => TypeInternal::Const(*c),
-            _ => TypeInternal::Expr(Box::new(self)),
-        })
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
-}
-
-#[doc(hidden)]
-impl<'a> Type<'a> {
-    pub(crate) fn unnote<'b>(self) -> Type<'b> {
-        use TypeInternal::*;
-        Type(match self.0 {
-            Expr(e) => Expr(Box::new(e.unnote())),
-            Const(c) => Const(c),
-            SuperType => SuperType,
-        })
+    #[allow(dead_code)]
+    pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
+        Normalized(self.0, PhantomData)
     }
 }
 
-impl<'a> SimpleType<'a> {
-    pub(crate) fn into_type(self) -> Type<'a> {
-        Normalized(self.0, Some(Type::const_type()), PhantomData).into_type()
+impl<'a> Typed<'a> {
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+    }
+    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+        Typed(TypedInternal::from_thunk_untyped(th), PhantomData)
+    }
+    pub(crate) fn const_sort() -> Self {
+        Typed(TypedInternal::Sort, PhantomData)
     }
 }
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index c85b962..6e4361f 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -4,6 +4,8 @@
 #![feature(label_break_value)]
 #![feature(non_exhaustive)]
 #![feature(bind_by_move_pattern_guards)]
+#![feature(try_trait)]
+#![feature(inner_deref)]
 #![cfg_attr(test, feature(custom_inner_attributes))]
 #![allow(
     clippy::type_complexity,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f092c4d..f991a2e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,48 +4,68 @@ use std::rc::Rc;
 
 use dhall_core::context::Context;
 use dhall_core::{
-    rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText,
+    rc, Builtin, Const, ExprF, Integer, InterpolatedText,
     InterpolatedTextContents, Label, Natural, SubExpr, V, X,
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, Typed};
+use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
 
 impl<'a> Typed<'a> {
+    /// Reduce an expression to its normal form, performing beta reduction
+    ///
+    /// `normalize` does not type-check the expression.  You may want to type-check
+    /// expressions before normalizing them since normalization can convert an
+    /// ill-typed expression into a well-typed expression.
+    ///
+    /// However, `normalize` will not fail if the expression is ill-typed and will
+    /// leave ill-typed sub-expressions unevaluated.
+    ///
     pub fn normalize(self) -> Normalized<'a> {
-        Normalized(normalize(self.0), self.1, self.2)
+        let internal = match self.0 {
+            TypedInternal::Sort => TypedInternal::Sort,
+            TypedInternal::Value(thunk, t) => {
+                // TODO: stupid but needed for now
+                let thunk =
+                    Thunk::from_normalized_expr(thunk.normalize_to_expr());
+                thunk.normalize_nf();
+                TypedInternal::Value(thunk, t)
+            }
+        };
+        Normalized(internal, self.1)
     }
-    /// Pretends this expression is normalized. Use with care.
-    #[allow(dead_code)]
-    pub fn skip_normalize(self) -> Normalized<'a> {
-        Normalized(
-            self.0.unroll().squash_embed(|e| e.0.clone()),
-            self.1,
-            self.2,
-        )
+
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        Typed(self.0.shift(delta, var), self.1)
     }
-}
 
-fn shift0_mut<N, E>(delta: isize, label: &Label, in_expr: &mut SubExpr<N, E>) {
-    let new_expr = shift0(delta, label, &in_expr);
-    std::mem::replace(in_expr, new_expr);
-}
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &Typed<'static>,
+    ) -> Self {
+        Typed(self.0.subst_shift(var, val), self.1)
+    }
+
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
+    }
 
-fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
-    let new_expr = shift(delta, var, &in_expr);
-    std::mem::replace(in_expr, new_expr);
+    pub(crate) fn to_thunk(&self) -> Thunk {
+        self.0.to_thunk()
+    }
 }
 
-fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
+fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
     use dhall_core::Builtin::*;
-    use WHNF::*;
+    use Value::*;
 
     let ret = match b {
         OptionalNone => improved_slice_patterns::match_vec!(args;
-            [t] => EmptyOptionalLit(Now::from_whnf(t)),
+            [t] => EmptyOptionalLit(TypeThunk::from_whnf(t)),
         ),
         NaturalIsZero => improved_slice_patterns::match_vec!(args;
             [NaturalLit(n)] => BoolLit(n == 0),
@@ -93,12 +113,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 let mut kts = BTreeMap::new();
                 kts.insert(
                     "index".into(),
-                    Now::from_whnf(
-                        WHNF::from_builtin(Natural)
+                    TypeThunk::from_whnf(
+                        Value::from_builtin(Natural)
                     ),
                 );
                 kts.insert("value".into(), t);
-                EmptyListLit(Now::from_whnf(RecordType(kts)))
+                EmptyListLit(TypeThunk::from_whnf(RecordType(kts)))
             },
             [_, NEListLit(xs)] => {
                 let xs = xs
@@ -107,9 +127,9 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = BTreeMap::new();
-                        kvs.insert("index".into(), Now::from_whnf(i));
+                        kvs.insert("index".into(), Thunk::from_whnf(i));
                         kvs.insert("value".into(), e);
-                        Now::from_whnf(RecordLit(kvs))
+                        Thunk::from_whnf(RecordLit(kvs))
                     })
                     .collect();
                 NEListLit(xs)
@@ -117,7 +137,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
         ),
         ListBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(ListFold, args)] => {
+            [_, Value::AppliedBuiltin(ListFold, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -127,13 +147,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [t, g] => g
-                .app(WHNF::from_builtin(List).app(t.clone()))
-                .app(ListConsClosure(Now::from_whnf(t.clone()), None))
-                .app(EmptyListLit(Now::from_whnf(t))),
+                .app(Value::from_builtin(List).app(t.clone()))
+                .app(ListConsClosure(TypeThunk::from_whnf(t.clone()), None))
+                .app(EmptyListLit(TypeThunk::from_whnf(t))),
         ),
         ListFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(ListBuild, args)] => {
+            [_, Value::AppliedBuiltin(ListBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -145,14 +165,14 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.normalize()).app(v);
+                    v = cons.clone().app_thunk(x).app(v);
                 }
                 v
             }
         ),
         OptionalBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(OptionalFold, args)] => {
+            [_, Value::AppliedBuiltin(OptionalFold, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -161,13 +181,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [t, g] => g
-                .app(WHNF::from_builtin(Optional).app(t.clone()))
-                .app(OptionalSomeClosure(Now::from_whnf(t.clone())))
-                .app(EmptyOptionalLit(Now::from_whnf(t))),
+                .app(Value::from_builtin(Optional).app(t.clone()))
+                .app(OptionalSomeClosure(TypeThunk::from_whnf(t.clone())))
+                .app(EmptyOptionalLit(TypeThunk::from_whnf(t))),
         ),
         OptionalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [_, WHNF::AppliedBuiltin(OptionalBuild, args)] => {
+            [_, Value::AppliedBuiltin(OptionalBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 2 {
                     args.remove(1)
@@ -179,12 +199,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.normalize())
+                just.app_thunk(x)
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [WHNF::AppliedBuiltin(NaturalFold, args)] => {
+            [Value::AppliedBuiltin(NaturalFold, args)] => {
                 let mut args = args;
                 if args.len() >= 1 {
                     args.remove(0)
@@ -193,13 +213,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
                 }
             },
             [g] => g
-                .app(WHNF::from_builtin(Natural))
+                .app(Value::from_builtin(Natural))
                 .app(NaturalSuccClosure)
                 .app(NaturalLit(0)),
         ),
         NaturalFold => improved_slice_patterns::match_vec!(args;
             // fold/build fusion
-            [WHNF::AppliedBuiltin(NaturalBuild, args)] => {
+            [Value::AppliedBuiltin(NaturalBuild, args)] => {
                 let mut args = args;
                 if args.len() >= 1 {
                     args.remove(0)
@@ -209,7 +229,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
             },
             [NaturalLit(0), _, _, zero] => zero,
             [NaturalLit(n), t, succ, zero] => {
-                let fold = WHNF::from_builtin(NaturalFold)
+                let fold = Value::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
                     .app(t)
                     .app(succ.clone())
@@ -228,222 +248,233 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 
 #[derive(Debug, Clone)]
 enum EnvItem {
-    Expr(WHNF),
-    Skip(usize),
+    Thunk(Thunk),
+    Skip(V<Label>),
+}
+
+impl EnvItem {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        use EnvItem::*;
+        match self {
+            Thunk(e) => Thunk(e.shift(delta, var)),
+            Skip(v) => Skip(v.shift(delta, var)),
+        }
+    }
+
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &Typed<'static>,
+    ) -> Self {
+        match self {
+            EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
+            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
+            EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
+        }
+    }
 }
 
 #[derive(Debug, Clone)]
-struct NormalizationContext(Rc<Context<Label, EnvItem>>);
+pub(crate) struct NormalizationContext(Rc<Context<Label, EnvItem>>);
 
 impl NormalizationContext {
-    fn new() -> Self {
+    pub(crate) fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
     }
-    fn insert(&self, x: &Label, e: WHNF) -> Self {
+    fn insert(&self, x: &Label, e: Thunk) -> Self {
         NormalizationContext(Rc::new(
-            self.0.insert(x.clone(), EnvItem::Expr(e)),
+            self.0.insert(x.clone(), EnvItem::Thunk(e)),
         ))
     }
     fn skip(&self, x: &Label) -> Self {
         NormalizationContext(Rc::new(
             self.0
-                .map(|l, e| {
-                    use EnvItem::*;
-                    match e {
-                        Expr(e) => {
-                            let mut e = e.clone();
-                            e.shift0(1, x);
-                            Expr(e)
-                        }
-                        Skip(n) if l == x => Skip(*n + 1),
-                        Skip(n) => Skip(*n),
-                    }
-                })
-                .insert(x.clone(), EnvItem::Skip(0)),
+                .map(|_, e| e.shift(1, &x.into()))
+                .insert(x.clone(), EnvItem::Skip(x.into())),
         ))
     }
-    fn lookup(&self, var: &V<Label>) -> WHNF {
+    fn lookup(&self, var: &V<Label>) -> Value {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
-            Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(m)) => {
-                WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m))))
+            Some(EnvItem::Thunk(t)) => t.normalize_whnf().clone(),
+            Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
+            None => Value::Var(var.clone()),
+        }
+    }
+    pub(crate) fn from_typecheck_ctx(
+        tc_ctx: &crate::typecheck::TypecheckContext,
+    ) -> Self {
+        use crate::typecheck::EnvItem::*;
+        let mut ctx = Context::new();
+        for (k, vs) in tc_ctx.0.iter_keys() {
+            for v in vs.iter() {
+                let new_item = match v {
+                    Type(var, _) => EnvItem::Skip(var.clone()),
+                    Value(e) => EnvItem::Thunk(Thunk::new(
+                        NormalizationContext::new(),
+                        e.as_expr().embed_absurd(),
+                    )),
+                };
+                ctx = ctx.insert(k.clone(), new_item);
             }
-            None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
         }
+        NormalizationContext(Rc::new(ctx))
+    }
+
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
+    }
+
+    fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
+        NormalizationContext(Rc::new(
+            self.0.map(|_, e| e.subst_shift(var, val)),
+        ))
     }
 }
 
-/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
-/// be limited to syntactic expressions: either written by the user or meant to be printed.
-/// The rule is the following: we must _not_ construct values of type `Expr` while normalizing,
-/// but only construct `WHNF`s.
-///
-/// WHNFs store subexpressions unnormalized, to enable lazy normalization. They approximate
-/// what's called Weak Head Normal-Form (WHNF). This means that the expression is normalized as
-/// little as possible, but just enough to know the first constructor of the normal form. This is
-/// identical to full normalization for simple types like integers, but for e.g. a record literal
-/// this means knowing just the field names.
-///
-/// Each variant captures the relevant contexts when it is constructed. Conceptually each
-/// subexpression has its own context, but in practice some contexts can be shared when sensible, to
-/// avoid unnecessary allocations.
+/// A semantic value.
 #[derive(Debug, Clone)]
-enum WHNF {
+pub(crate) enum Value {
     /// Closures
-    Lam(Label, Now, (NormalizationContext, InputSubExpr)),
-    AppliedBuiltin(Builtin, Vec<WHNF>),
+    Lam(Label, Thunk, Thunk),
+    AppliedBuiltin(Builtin, Vec<Value>),
     /// `λ(x: a) -> Some x`
-    OptionalSomeClosure(Now),
+    OptionalSomeClosure(TypeThunk),
     /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
     /// `λ(xs : List a) -> [ x ] # xs`
-    ListConsClosure(Now, Option<Now>),
+    ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
+    Pi(Label, TypeThunk, TypeThunk),
 
+    Var(V<Label>),
+    Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
     IntegerLit(Integer),
-    EmptyOptionalLit(Now),
-    NEOptionalLit(Now),
-    EmptyListLit(Now),
-    NEListLit(Vec<Now>),
-    RecordLit(BTreeMap<Label, Now>),
-    RecordType(BTreeMap<Label, Now>),
-    UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
-    UnionConstructor(
-        NormalizationContext,
-        Label,
-        BTreeMap<Label, Option<InputSubExpr>>,
-    ),
-    UnionLit(
-        Label,
-        Now,
-        (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
-    ),
-    TextLit(Vec<InterpolatedTextContents<Now>>),
+    EmptyOptionalLit(TypeThunk),
+    NEOptionalLit(Thunk),
+    EmptyListLit(TypeThunk),
+    NEListLit(Vec<Thunk>),
+    RecordLit(BTreeMap<Label, Thunk>),
+    RecordType(BTreeMap<Label, TypeThunk>),
+    UnionType(BTreeMap<Label, Option<TypeThunk>>),
+    UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
+    UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
+    TextLit(Vec<InterpolatedTextContents<Thunk>>),
+    /// Invariant: This must not contain a value captured by one of the variants above.
+    PartialExpr(Box<ExprF<Value, Label, X, X>>),
     Expr(OutputSubExpr),
 }
 
-impl WHNF {
+impl Value {
+    pub(crate) fn into_thunk(self) -> Thunk {
+        Thunk::from_whnf(self)
+    }
+
     /// Convert the value back to a (normalized) syntactic expression
-    fn normalize_to_expr(self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
         match self {
-            WHNF::Lam(x, t, (ctx, e)) => {
-                let ctx2 = ctx.skip(&x);
-                rc(ExprF::Lam(
-                    x.clone(),
-                    t.normalize().normalize_to_expr(),
-                    normalize_whnf(ctx2, e).normalize_to_expr(),
-                ))
-            }
-            WHNF::AppliedBuiltin(b, args) => {
-                let mut e = WHNF::Expr(rc(ExprF::Builtin(b)));
+            Value::Lam(x, t, e) => rc(ExprF::Lam(
+                x.clone(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
+            )),
+            Value::AppliedBuiltin(b, args) => {
+                let mut e = rc(ExprF::Builtin(*b));
                 for v in args {
-                    e = e.app(v);
+                    e = rc(ExprF::App(e, v.normalize_to_expr()));
                 }
-                e.normalize_to_expr()
+                e
             }
-            WHNF::OptionalSomeClosure(n) => {
-                let a = n.normalize().normalize_to_expr();
+            Value::OptionalSomeClosure(n) => {
+                let a = n.normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
-            WHNF::ListConsClosure(n, None) => {
-                let a = n.normalize().normalize_to_expr();
+            Value::ListConsClosure(n, None) => {
+                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
-                let a1 = shift0(1, &"x".into(), &a);
+                let a1 = a.shift(1, &Label::from("x").into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
-            WHNF::ListConsClosure(n, Some(v)) => {
-                let v = v.normalize().normalize_to_expr();
-                let a = n.normalize().normalize_to_expr();
+            Value::ListConsClosure(n, Some(v)) => {
+                let v = v.normalize_to_expr();
+                let a = n.normalize_to_expr();
+                // Avoid accidental capture of the new `xs` variable
+                let v = v.shift(1, &Label::from("xs").into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
-            WHNF::NaturalSuccClosure => {
+            Value::NaturalSuccClosure => {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
-            WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
-            WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
-            WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
-            WHNF::EmptyOptionalLit(n) => {
-                WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone)))
-                    .app(n.normalize())
-                    .normalize_to_expr()
-            }
-            WHNF::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize().normalize_to_expr()))
+            Value::Pi(x, t, e) => rc(ExprF::Pi(
+                x.clone(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
+            )),
+            Value::Var(v) => rc(ExprF::Var(v.clone())),
+            Value::Const(c) => rc(ExprF::Const(*c)),
+            Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
+            Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
+            Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
+            Value::EmptyOptionalLit(n) => rc(ExprF::App(
+                rc(ExprF::Builtin(Builtin::OptionalNone)),
+                n.normalize_to_expr(),
+            )),
+            Value::NEOptionalLit(n) => {
+                rc(ExprF::SomeLit(n.normalize_to_expr()))
             }
-            WHNF::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr()))
+            Value::EmptyListLit(n) => {
+                rc(ExprF::EmptyListLit(n.normalize_to_expr()))
             }
-            WHNF::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.into_iter()
-                    .map(|n| n.normalize().normalize_to_expr())
-                    .collect(),
+            Value::NEListLit(elts) => rc(ExprF::NEListLit(
+                elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
             )),
-            WHNF::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.into_iter()
-                    .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+            Value::RecordLit(kvs) => rc(ExprF::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
-            WHNF::RecordType(kts) => rc(ExprF::RecordType(
-                kts.into_iter()
-                    .map(|(k, v)| (k, v.normalize().normalize_to_expr()))
+            Value::RecordType(kts) => rc(ExprF::RecordType(
+                kts.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
-            WHNF::UnionType(ctx, kts) => rc(ExprF::UnionType(
-                kts.into_iter()
+            Value::UnionType(kts) => rc(ExprF::UnionType(
+                kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
-            WHNF::UnionConstructor(ctx, l, kts) => {
+            Value::UnionConstructor(l, kts) => {
                 let kts = kts
-                    .into_iter()
+                    .iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect();
-                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l))
+                rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
-            WHNF::UnionLit(l, v, (kts_ctx, kts)) => rc(ExprF::UnionLit(
-                l,
-                v.normalize().normalize_to_expr(),
-                kts.into_iter()
+            Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
+                l.clone(),
+                v.normalize_to_expr(),
+                kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k,
-                            v.map(|v| {
-                                normalize_whnf(kts_ctx.clone(), v)
-                                    .normalize_to_expr()
-                            }),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
-            WHNF::TextLit(elts) => {
+            Value::TextLit(elts) => {
                 fn normalize_textlit(
-                    elts: Vec<InterpolatedTextContents<Now>>,
+                    elts: &Vec<InterpolatedTextContents<Thunk>>,
                 ) -> InterpolatedText<OutputSubExpr> {
-                    elts.into_iter()
+                    elts.iter()
                         .flat_map(|contents| {
                             use InterpolatedTextContents::{Expr, Text};
                             let new_interpolated = match contents {
-                                Expr(n) => match n.normalize() {
-                                    WHNF::TextLit(elts2) => {
+                                Expr(n) => match &*n.normalize_nf() {
+                                    Value::TextLit(elts2) => {
                                         normalize_textlit(elts2)
                                     }
                                     e => InterpolatedText::from((
@@ -454,7 +485,7 @@ impl WHNF {
                                         )],
                                     )),
                                 },
-                                Text(s) => InterpolatedText::from(s),
+                                Text(s) => InterpolatedText::from(s.clone()),
                             };
                             new_interpolated.into_iter()
                         })
@@ -463,197 +494,776 @@ impl WHNF {
 
                 rc(ExprF::TextLit(normalize_textlit(elts)))
             }
-            WHNF::Expr(e) => e,
+            Value::PartialExpr(e) => {
+                rc(e.map_ref_simple(|v| v.normalize_to_expr()))
+            }
+            Value::Expr(e) => e.clone(),
         }
     }
 
-    /// Apply to a value
-    fn app(self, val: WHNF) -> WHNF {
-        match (self, val) {
-            (WHNF::Lam(x, _, (ctx, e)), val) => {
-                let ctx2 = ctx.insert(&x, val);
-                normalize_whnf(ctx2, e)
-            }
-            (WHNF::AppliedBuiltin(b, mut args), val) => {
-                args.push(val);
-                apply_builtin(b, args)
-            }
-            (WHNF::OptionalSomeClosure(_), val) => {
-                WHNF::NEOptionalLit(Now::from_whnf(val))
-            }
-            (WHNF::ListConsClosure(t, None), val) => {
-                WHNF::ListConsClosure(t, Some(Now::from_whnf(val)))
+    // Deprecated
+    pub(crate) fn normalize(&self) -> Value {
+        match self {
+            Value::Lam(x, t, e) => {
+                Value::Lam(x.clone(), t.normalize(), e.normalize())
             }
-            (WHNF::ListConsClosure(_, Some(x)), WHNF::EmptyListLit(_)) => {
-                WHNF::NEListLit(vec![x])
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.normalize()).collect(),
+            ),
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.normalize())
             }
-            (WHNF::ListConsClosure(_, Some(x)), WHNF::NEListLit(mut xs)) => {
-                xs.insert(0, x);
-                WHNF::NEListLit(xs)
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
+                t.normalize(),
+                v.as_ref().map(|v| v.normalize()),
+            ),
+            Value::Pi(x, t, e) => {
+                Value::Pi(x.clone(), t.normalize(), e.normalize())
             }
-            (WHNF::NaturalSuccClosure, WHNF::NaturalLit(n)) => {
-                WHNF::NaturalLit(n + 1)
+            Value::Var(v) => Value::Var(v.clone()),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.normalize())
             }
-            (WHNF::UnionConstructor(ctx, l, kts), val) => {
-                WHNF::UnionLit(l, Now::from_whnf(val), (ctx, kts))
+            Value::NEOptionalLit(th) => Value::NEOptionalLit(th.normalize()),
+            Value::EmptyListLit(tth) => Value::EmptyListLit(tth.normalize()),
+            Value::NEListLit(elts) => {
+                Value::NEListLit(elts.iter().map(|v| v.normalize()).collect())
             }
-            // Can't do anything useful, convert to expr
-            (f, a) => WHNF::Expr(rc(ExprF::App(
-                f.normalize_to_expr(),
-                a.normalize_to_expr(),
-            ))),
+            Value::RecordLit(kvs) => Value::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize()))
+                    .collect(),
+            ),
+            Value::RecordType(kvs) => Value::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.normalize()))
+                    .collect(),
+            ),
+            Value::UnionType(kts) => Value::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
+                x.clone(),
+                v.normalize(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.normalize()))
+                    })
+                    .collect(),
+            ),
+            Value::TextLit(elts) => Value::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.normalize()),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_simple(|v| v.normalize()),
+            )),
+            Value::Expr(e) => Value::Expr(e.clone()),
         }
     }
 
-    fn from_builtin(b: Builtin) -> WHNF {
-        WHNF::AppliedBuiltin(b, vec![])
-    }
-
-    fn shift0(&mut self, delta: isize, label: &Label) {
+    pub(crate) fn normalize_mut(&mut self) {
         match self {
-            WHNF::NaturalSuccClosure
-            | WHNF::BoolLit(_)
-            | WHNF::NaturalLit(_)
-            | WHNF::IntegerLit(_) => {}
-            WHNF::EmptyOptionalLit(n)
-            | WHNF::NEOptionalLit(n)
-            | WHNF::OptionalSomeClosure(n)
-            | WHNF::EmptyListLit(n) => {
-                n.shift0(delta, label);
+            Value::NaturalSuccClosure
+            | Value::Var(_)
+            | Value::Const(_)
+            | Value::BoolLit(_)
+            | Value::NaturalLit(_)
+            | Value::IntegerLit(_)
+            | Value::Expr(_) => {}
+
+            Value::EmptyOptionalLit(tth)
+            | Value::OptionalSomeClosure(tth)
+            | Value::EmptyListLit(tth) => {
+                tth.normalize_mut();
+            }
+
+            Value::NEOptionalLit(th) => {
+                th.normalize_mut();
+            }
+            Value::Lam(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
             }
-            WHNF::Lam(_, t, (_, e)) => {
-                t.shift0(delta, label);
-                shift_mut(delta, &V(label.clone(), 1), e);
+            Value::Pi(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
             }
-            WHNF::AppliedBuiltin(_, args) => {
+            Value::AppliedBuiltin(_, args) => {
                 for x in args.iter_mut() {
-                    x.shift0(delta, label);
+                    x.normalize_mut();
                 }
             }
-            WHNF::ListConsClosure(t, v) => {
-                t.shift0(delta, label);
+            Value::ListConsClosure(t, v) => {
+                t.normalize_mut();
                 for x in v.iter_mut() {
-                    x.shift0(delta, label);
+                    x.normalize_mut();
                 }
             }
-            WHNF::NEListLit(elts) => {
+            Value::NEListLit(elts) => {
                 for x in elts.iter_mut() {
-                    x.shift0(delta, label);
+                    x.normalize_mut();
+                }
+            }
+            Value::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
                 }
             }
-            WHNF::RecordLit(kvs) | WHNF::RecordType(kvs) => {
+            Value::RecordType(kvs) => {
                 for x in kvs.values_mut() {
-                    x.shift0(delta, label);
+                    x.normalize_mut();
                 }
             }
-            WHNF::UnionType(_, kts) | WHNF::UnionConstructor(_, _, kts) => {
+            Value::UnionType(kts) | Value::UnionConstructor(_, kts) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift0_mut(delta, label, x);
+                    x.normalize_mut();
                 }
             }
-            WHNF::UnionLit(_, v, (_, kts)) => {
-                v.shift0(delta, label);
+            Value::UnionLit(_, v, kts) => {
+                v.normalize_mut();
                 for x in kts.values_mut().flat_map(|opt| opt) {
-                    shift0_mut(delta, label, x);
+                    x.normalize_mut();
                 }
             }
-            WHNF::TextLit(elts) => {
+            Value::TextLit(elts) => {
                 for x in elts.iter_mut() {
                     use InterpolatedTextContents::{Expr, Text};
                     match x {
-                        Expr(n) => n.shift0(delta, label),
+                        Expr(n) => n.normalize_mut(),
                         Text(_) => {}
                     }
                 }
             }
-            WHNF::Expr(e) => shift0_mut(delta, label, e),
+            Value::PartialExpr(e) => {
+                // TODO: need map_mut_simple
+                *self = Value::PartialExpr(Box::new(
+                    e.map_ref_simple(|v| v.normalize()),
+                ))
+            }
+        }
+    }
+
+    /// Apply to a value
+    pub(crate) fn app(self, val: Value) -> Value {
+        self.app_thunk(val.into_thunk())
+    }
+
+    /// Apply to a thunk
+    pub(crate) fn app_thunk(self, th: Thunk) -> Value {
+        let fallback = |f: Value, a: Thunk| {
+            Value::PartialExpr(Box::new(ExprF::App(
+                f,
+                a.normalize_whnf().clone(),
+            )))
+        };
+
+        match self {
+            Value::Lam(x, _, e) => {
+                let val = Typed(
+                    TypedInternal::Value(th, None),
+                    std::marker::PhantomData,
+                );
+                e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
+            }
+            Value::AppliedBuiltin(b, mut args) => {
+                args.push(th.normalize_whnf().clone());
+                apply_builtin(b, args)
+            }
+            Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th),
+            Value::ListConsClosure(t, None) => {
+                Value::ListConsClosure(t, Some(th))
+            }
+            Value::ListConsClosure(t, Some(x)) => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::EmptyListLit(_) => Value::NEListLit(vec![x]),
+                    Value::NEListLit(xs) => {
+                        let mut xs = xs.clone();
+                        xs.insert(0, x);
+                        Value::NEListLit(xs)
+                    }
+                    _ => {
+                        drop(v);
+                        fallback(Value::ListConsClosure(t, Some(x)), th)
+                    }
+                }
+            }
+            Value::NaturalSuccClosure => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::NaturalLit(n) => Value::NaturalLit(n + 1),
+                    _ => {
+                        drop(v);
+                        fallback(Value::NaturalSuccClosure, th)
+                    }
+                }
+            }
+            Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts),
+            f => fallback(f, th),
+        }
+    }
+
+    pub(crate) fn from_builtin(b: Builtin) -> Value {
+        Value::AppliedBuiltin(b, vec![])
+    }
+
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        match self {
+            Value::Lam(x, t, e) => Value::Lam(
+                x.clone(),
+                t.shift(delta, var),
+                e.shift(delta, &var.shift(1, &x.into())),
+            ),
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.shift(delta, var)).collect(),
+            ),
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.shift(delta, var))
+            }
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
+                t.shift(delta, var),
+                v.as_ref().map(|v| v.shift(delta, var)),
+            ),
+            Value::Pi(x, t, e) => Value::Pi(
+                x.clone(),
+                t.shift(delta, var),
+                e.shift(delta, &var.shift(1, &x.into())),
+            ),
+            Value::Var(v) => Value::Var(v.shift(delta, var)),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.shift(delta, var))
+            }
+            Value::NEOptionalLit(th) => {
+                Value::NEOptionalLit(th.shift(delta, var))
+            }
+            Value::EmptyListLit(tth) => {
+                Value::EmptyListLit(tth.shift(delta, var))
+            }
+            Value::NEListLit(elts) => Value::NEListLit(
+                elts.iter().map(|v| v.shift(delta, var)).collect(),
+            ),
+            Value::RecordLit(kvs) => Value::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.shift(delta, var)))
+                    .collect(),
+            ),
+            Value::RecordType(kvs) => Value::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.shift(delta, var)))
+                    .collect(),
+            ),
+            Value::UnionType(kts) => Value::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
+                x.clone(),
+                v.shift(delta, var),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
+                    })
+                    .collect(),
+            ),
+            Value::TextLit(elts) => Value::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.shift(delta, var)),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.shift(delta, var),
+                    |x, v| v.shift(delta, &var.shift(1, &x.into())),
+                    X::clone,
+                    X::clone,
+                    Label::clone,
+                ),
+            )),
+            Value::Expr(e) => Value::Expr(e.shift(delta, var)),
+        }
+    }
+
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &Typed<'static>,
+    ) -> Self {
+        match self {
+            Value::Lam(x, t, e) => Value::Lam(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(
+                    &var.shift(1, &x.into()),
+                    &val.shift(1, &x.into()),
+                ),
+            ),
+            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
+                *b,
+                args.iter().map(|v| v.subst_shift(var, val)).collect(),
+            ),
+            Value::NaturalSuccClosure => Value::NaturalSuccClosure,
+            Value::OptionalSomeClosure(tth) => {
+                Value::OptionalSomeClosure(tth.subst_shift(var, val))
+            }
+            Value::ListConsClosure(t, v) => Value::ListConsClosure(
+                t.subst_shift(var, val),
+                v.as_ref().map(|v| v.subst_shift(var, val)),
+            ),
+            Value::Pi(x, t, e) => Value::Pi(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(
+                    &var.shift(1, &x.into()),
+                    &val.shift(1, &x.into()),
+                ),
+            ),
+            Value::Var(v) if v == var => val.to_value().clone(),
+            Value::Var(v) => Value::Var(v.shift(-1, var)),
+            Value::Const(c) => Value::Const(*c),
+            Value::BoolLit(b) => Value::BoolLit(*b),
+            Value::NaturalLit(n) => Value::NaturalLit(*n),
+            Value::IntegerLit(n) => Value::IntegerLit(*n),
+            Value::EmptyOptionalLit(tth) => {
+                Value::EmptyOptionalLit(tth.subst_shift(var, val))
+            }
+            Value::NEOptionalLit(th) => {
+                Value::NEOptionalLit(th.subst_shift(var, val))
+            }
+            Value::EmptyListLit(tth) => {
+                Value::EmptyListLit(tth.subst_shift(var, val))
+            }
+            Value::NEListLit(elts) => Value::NEListLit(
+                elts.iter().map(|v| v.subst_shift(var, val)).collect(),
+            ),
+            Value::RecordLit(kvs) => Value::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+                    .collect(),
+            ),
+            Value::RecordType(kvs) => Value::RecordType(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+                    .collect(),
+            ),
+            Value::UnionType(kts) => Value::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionConstructor(x, kts) => Value::UnionConstructor(
+                x.clone(),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            Value::UnionLit(x, v, kts) => Value::UnionLit(
+                x.clone(),
+                v.subst_shift(var, val),
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+                    })
+                    .collect(),
+            ),
+            Value::TextLit(elts) => Value::TextLit(
+                elts.iter()
+                    .map(|contents| {
+                        use InterpolatedTextContents::{Expr, Text};
+                        match contents {
+                            Expr(th) => Expr(th.subst_shift(var, val)),
+                            Text(s) => Text(s.clone()),
+                        }
+                    })
+                    .collect(),
+            ),
+            Value::PartialExpr(e) => Value::PartialExpr(Box::new(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.subst_shift(var, val),
+                    |x, v| {
+                        v.subst_shift(
+                            &var.shift(1, &x.into()),
+                            &val.shift(1, &x.into()),
+                        )
+                    },
+                    X::clone,
+                    X::clone,
+                    Label::clone,
+                ),
+            )),
+            Value::Expr(e) => Value::Expr(
+                e.subst_shift(var, &val.clone().normalize().as_expr()),
+            ),
+        }
+    }
+}
+
+mod thunk {
+    use super::{
+        normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr,
+        Value,
+    };
+    use crate::expr::Typed;
+    use dhall_core::{Label, V};
+    use std::cell::{Ref, RefCell};
+    use std::rc::Rc;
+
+    #[derive(Debug, Clone, Copy)]
+    enum Marker {
+        /// Weak Head Normal Form, i.e. subexpressions may not be normalized
+        WHNF,
+        /// Normal form, i.e. completely normalized
+        NF,
+    }
+    use Marker::{NF, WHNF};
+
+    #[derive(Debug)]
+    enum ThunkInternal {
+        /// Non-normalized value alongside a normalization context
+        Unnormalized(NormalizationContext, InputSubExpr),
+        /// Partially normalized value.
+        /// Invariant: if the marker is `NF`, the value must be fully normalized
+        Value(Marker, Value),
+    }
+
+    /// Stores a possibl unevaluated value. Uses RefCell to ensure that
+    /// the value gets normalized at most once.
+    #[derive(Debug, Clone)]
+    pub struct Thunk(Rc<RefCell<ThunkInternal>>);
+
+    impl ThunkInternal {
+        fn into_thunk(self) -> Thunk {
+            Thunk(Rc::new(RefCell::new(self)))
+        }
+
+        fn normalize_whnf(&mut self) {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    *self = ThunkInternal::Value(
+                        WHNF,
+                        normalize_whnf(ctx.clone(), e.clone()),
+                    )
+                }
+                // Already at least in WHNF
+                ThunkInternal::Value(_, _) => {}
+            }
+        }
+
+        fn normalize_nf(&mut self) {
+            self.normalize_whnf();
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::Value(m @ WHNF, v) => {
+                    v.normalize_mut();
+                    *m = NF;
+                }
+                // Already in NF
+                ThunkInternal::Value(NF, _) => {}
+            }
+        }
+
+        // Always use normalize_whnf before
+        fn as_whnf(&self) -> &Value {
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::Value(_, v) => v,
+            }
+        }
+
+        // Always use normalize_nf before
+        fn as_nf(&self) -> &Value {
+            match self {
+                ThunkInternal::Unnormalized(_, _) => unreachable!(),
+                ThunkInternal::Value(WHNF, _) => unreachable!(),
+                ThunkInternal::Value(NF, v) => v,
+            }
+        }
+
+        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    ThunkInternal::Unnormalized(
+                        ctx.shift(delta, var),
+                        e.clone(),
+                    )
+                }
+                ThunkInternal::Value(m, v) => {
+                    ThunkInternal::Value(*m, v.shift(delta, var))
+                }
+            }
+        }
+
+        fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
+            match self {
+                ThunkInternal::Unnormalized(ctx, e) => {
+                    ThunkInternal::Unnormalized(
+                        ctx.subst_shift(var, val),
+                        e.clone(),
+                    )
+                }
+                ThunkInternal::Value(_, v) => {
+                    // The resulting value may not stay in normal form after substitution
+                    ThunkInternal::Value(WHNF, v.subst_shift(var, val))
+                }
+            }
+        }
+    }
+
+    impl Thunk {
+        pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
+            ThunkInternal::Unnormalized(ctx, e).into_thunk()
+        }
+
+        pub(crate) fn from_whnf(v: Value) -> Thunk {
+            ThunkInternal::Value(WHNF, v).into_thunk()
+        }
+
+        pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk {
+            Thunk::new(NormalizationContext::new(), e.embed_absurd())
+        }
+
+        // Deprecated
+        pub(crate) fn normalize(&self) -> Thunk {
+            self.normalize_nf();
+            self.clone()
+        }
+
+        // Normalizes contents to normal form; faster than `normalize_nf` if
+        // no one else shares this thunk
+        pub(crate) fn normalize_mut(&mut self) {
+            match Rc::get_mut(&mut self.0) {
+                // Mutate directly if sole owner
+                Some(refcell) => RefCell::get_mut(refcell).normalize_nf(),
+                // Otherwise mutate through the refcell
+                None => self.0.borrow_mut().normalize_nf(),
+            }
+        }
+
+        // WARNING: avoid normalizing any thunk while holding on to this ref
+        // or you will run into BorrowMut panics
+        pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
+            self.0.borrow_mut().normalize_whnf();
+            Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
+        }
+
+        // WARNING: avoid normalizing any thunk while holding on to this ref
+        // or you will run into BorrowMut panics
+        pub(crate) fn normalize_nf(&self) -> Ref<Value> {
+            self.0.borrow_mut().normalize_nf();
+            Ref::map(self.0.borrow(), ThunkInternal::as_nf)
+        }
+
+        pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+            self.normalize_nf().normalize_to_expr()
+        }
+
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            self.0.borrow().shift(delta, var).into_thunk()
+        }
+
+        pub(crate) fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &Typed<'static>,
+        ) -> Self {
+            self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
 }
 
-/// Normalize-on-write smart container. Contains either a (partially) normalized value or a
-/// non-normalized value alongside a normalization context.
-/// The name is a pun on std::borrow::Cow.
+pub(crate) use thunk::Thunk;
+
+/// A thunk in type position.
 #[derive(Debug, Clone)]
-enum Now {
-    Normalized(Box<WHNF>),
-    Unnormalized(NormalizationContext, InputSubExpr),
+pub(crate) enum TypeThunk {
+    Thunk(Thunk),
+    Type(Type<'static>),
 }
 
-impl Now {
-    fn new(ctx: NormalizationContext, e: InputSubExpr) -> Now {
-        Now::Unnormalized(ctx, e)
+impl TypeThunk {
+    fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk {
+        TypeThunk::from_thunk(Thunk::new(ctx, e))
+    }
+
+    fn from_whnf(v: Value) -> TypeThunk {
+        TypeThunk::from_thunk(Thunk::from_whnf(v))
+    }
+
+    fn from_thunk(th: Thunk) -> TypeThunk {
+        TypeThunk::Thunk(th)
+    }
+
+    pub(crate) fn from_type(t: Type<'static>) -> TypeThunk {
+        TypeThunk::Type(t)
+    }
+
+    // Deprecated
+    fn normalize(&self) -> TypeThunk {
+        match self {
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
+            TypeThunk::Type(t) => TypeThunk::Type(t.clone()),
+        }
+    }
+
+    fn normalize_mut(&mut self) {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize_mut(),
+            TypeThunk::Type(_) => {}
+        }
+    }
+
+    pub(crate) fn normalize_nf(&self) -> Value {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
+            TypeThunk::Type(t) => t.to_value().normalize(),
+        }
     }
 
-    fn from_whnf(v: WHNF) -> Now {
-        Now::Normalized(Box::new(v))
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr()
     }
 
-    fn normalize(self) -> WHNF {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
-            Now::Normalized(v) => *v,
-            Now::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
+            TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-    fn shift0(&mut self, delta: isize, label: &Label) {
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &Typed<'static>,
+    ) -> Self {
         match self {
-            Now::Normalized(v) => v.shift0(delta, label),
-            Now::Unnormalized(_, e) => shift0_mut(delta, label, e),
+            TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
+            TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
         }
     }
 }
 
-/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
-fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
+/// Reduces the imput expression to Value. See doc on `Value` for details.
+fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
     match expr.as_ref() {
         ExprF::Var(v) => ctx.lookup(&v),
         ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
         ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
-        // TODO: wasteful to retraverse everything
-        ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()),
+        ExprF::Embed(e) => e.to_value(),
         ExprF::Let(x, _, r, b) => {
-            let r = normalize_whnf(ctx.clone(), r.clone());
-            normalize_whnf(ctx.insert(x, r), b.clone())
+            let t = Thunk::new(ctx.clone(), r.clone());
+            normalize_whnf(ctx.insert(x, t), b.clone())
         }
-        ExprF::Lam(x, t, e) => WHNF::Lam(
+        ExprF::Lam(x, t, e) => Value::Lam(
             x.clone(),
-            Now::new(ctx.clone(), t.clone()),
-            (ctx, e.clone()),
+            Thunk::new(ctx.clone(), t.clone()),
+            Thunk::new(ctx.skip(x), e.clone()),
         ),
-        ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]),
-        ExprF::BoolLit(b) => WHNF::BoolLit(*b),
-        ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
+        ExprF::Builtin(b) => Value::from_builtin(*b),
+        ExprF::Const(c) => Value::Const(*c),
+        ExprF::BoolLit(b) => Value::BoolLit(*b),
+        ExprF::NaturalLit(n) => Value::NaturalLit(*n),
         ExprF::OldOptionalLit(None, e) => {
-            WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+            Value::EmptyOptionalLit(TypeThunk::new(ctx, e.clone()))
         }
         ExprF::OldOptionalLit(Some(e), _) => {
-            WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
+            Value::NEOptionalLit(Thunk::new(ctx, e.clone()))
+        }
+        ExprF::SomeLit(e) => Value::NEOptionalLit(Thunk::new(ctx, e.clone())),
+        ExprF::EmptyListLit(e) => {
+            Value::EmptyListLit(TypeThunk::new(ctx, e.clone()))
         }
-        ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())),
-        ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
-        ExprF::NEListLit(elts) => WHNF::NEListLit(
+        ExprF::NEListLit(elts) => Value::NEListLit(
             elts.iter()
-                .map(|e| Now::new(ctx.clone(), e.clone()))
+                .map(|e| Thunk::new(ctx.clone(), e.clone()))
                 .collect(),
         ),
-        ExprF::RecordLit(kvs) => WHNF::RecordLit(
+        ExprF::RecordLit(kvs) => Value::RecordLit(
             kvs.iter()
-                .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
+                .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone())))
                 .collect(),
         ),
-        ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()),
-        ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
+        ExprF::UnionType(kts) => Value::UnionType(
+            kts.iter()
+                .map(|(k, t)| {
+                    (
+                        k.clone(),
+                        t.as_ref()
+                            .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
+                    )
+                })
+                .collect(),
+        ),
+        ExprF::UnionLit(l, x, kts) => Value::UnionLit(
             l.clone(),
-            Now::new(ctx.clone(), x.clone()),
-            (ctx, kts.clone()),
+            Thunk::new(ctx.clone(), x.clone()),
+            kts.iter()
+                .map(|(k, t)| {
+                    (
+                        k.clone(),
+                        t.as_ref()
+                            .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
+                    )
+                })
+                .collect(),
         ),
-        ExprF::TextLit(elts) => WHNF::TextLit(
+        ExprF::TextLit(elts) => Value::TextLit(
             elts.iter()
                 .map(|contents| {
                     use InterpolatedTextContents::{Expr, Text};
                     match contents {
-                        Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+                        Expr(n) => Expr(Thunk::new(ctx.clone(), n.clone())),
                         Text(s) => Text(s.clone()),
                     }
                 })
@@ -662,13 +1272,13 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         ExprF::BoolIf(b, e1, e2) => {
             let b = normalize_whnf(ctx.clone(), b.clone());
             match b {
-                WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
-                WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
+                Value::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
+                Value::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
                 b => {
                     let e1 = normalize_whnf(ctx.clone(), e1.clone());
                     let e2 = normalize_whnf(ctx, e2.clone());
                     match (e1, e2) {
-                        (WHNF::BoolLit(true), WHNF::BoolLit(false)) => b,
+                        (Value::BoolLit(true), Value::BoolLit(false)) => b,
                         (e1, e2) => {
                             normalize_last_layer(ExprF::BoolIf(b, e1, e2))
                         }
@@ -678,7 +1288,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
         }
         expr => {
             // Recursively normalize subexpressions
-            let expr: ExprF<WHNF, Label, X, X> = expr
+            let expr: ExprF<Value, Label, X, X> = expr
                 .map_ref_with_special_handling_of_binders(
                     |e| normalize_whnf(ctx.clone(), e.clone()),
                     |x, e| normalize_whnf(ctx.skip(x), e.clone()),
@@ -693,9 +1303,9 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
 }
 
 /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
+fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
     use dhall_core::BinOp::*;
-    use WHNF::*;
+    use Value::*;
 
     match expr {
         ExprF::App(v, a) => v.app(a),
@@ -741,9 +1351,9 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
         ExprF::BinOp(TextAppend, TextLit(x), y) if x.is_empty() => y,
         ExprF::BinOp(TextAppend, x, TextLit(y)) if y.is_empty() => x,
 
-        ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts),
+        ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
         ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
-            Some(r) => r.normalize(),
+            Some(r) => r.normalize_whnf().clone(),
             None => {
                 // Couldn't do anything useful, so just normalize subexpressions
                 Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
@@ -759,18 +1369,16 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
         ),
         ExprF::Merge(RecordLit(mut handlers), e, t) => {
             let e = match e {
-                UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l)
-                {
-                    Some(h) => return h.normalize(),
-                    None => UnionConstructor(ctor_ctx, l, kts),
+                UnionConstructor(l, kts) => match handlers.remove(&l) {
+                    Some(h) => return h.normalize_whnf().clone(),
+                    None => UnionConstructor(l, kts),
                 },
-                UnionLit(l, v, (kts_ctx, kts)) => match handlers.remove(&l) {
+                UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
-                        let h = h.normalize();
-                        let v = v.normalize();
-                        return h.app(v);
+                        let h = h.normalize_whnf().clone();
+                        return h.app_thunk(v);
                     }
-                    None => UnionLit(l, v, (kts_ctx, kts)),
+                    None => UnionLit(l, v, kts),
                 },
                 e => e,
             };
@@ -778,29 +1386,13 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
             Expr(rc(ExprF::Merge(
                 RecordLit(handlers).normalize_to_expr(),
                 e.normalize_to_expr(),
-                t.map(WHNF::normalize_to_expr),
+                t.as_ref().map(Value::normalize_to_expr),
             )))
         }
-        // Couldn't do anything useful, so just normalize subexpressions
-        expr => {
-            Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr())))
-        }
+        expr => PartialExpr(Box::new(expr)),
     }
 }
 
-/// Reduce an expression to its normal form, performing beta reduction
-///
-/// `normalize` does not type-check the expression.  You may want to type-check
-/// expressions before normalizing them since normalization can convert an
-/// ill-typed expression into a well-typed expression.
-///
-/// However, `normalize` will not fail if the expression is ill-typed and will
-/// leave ill-typed sub-expressions unevaluated.
-///
-fn normalize(e: InputSubExpr) -> OutputSubExpr {
-    normalize_whnf(NormalizationContext::new(), e).normalize_to_expr()
-}
-
 #[cfg(test)]
 mod spec_tests {
     #![rustfmt::skip]
@@ -866,7 +1458,7 @@ mod spec_tests {
     norm!(success_prelude_List_head_1, "prelude/List/head/1");
     norm!(success_prelude_List_indexed_0, "prelude/List/indexed/0");
     norm!(success_prelude_List_indexed_1, "prelude/List/indexed/1");
-    norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0");
+    // norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0");
     norm!(success_prelude_List_iterate_1, "prelude/List/iterate/1");
     norm!(success_prelude_List_last_0, "prelude/List/last/0");
     norm!(success_prelude_List_last_1, "prelude/List/last/1");
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index 196bda1..6f143cb 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -7,7 +7,7 @@ use std::borrow::Cow;
 impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
     fn from_str(s: &'a str, ty: Option<&Type>) -> Result<Self> {
         let expr = Normalized::from_str(s, ty)?;
-        T::deserialize(Deserializer(Cow::Owned(expr.0)))
+        T::deserialize(Deserializer(Cow::Owned(expr.to_expr())))
     }
 }
 
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 7f85b5c..ecd6e43 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -71,7 +71,7 @@ pub fn run_test_with_bigger_stack(
 ) -> std::result::Result<(), String> {
     // Many tests stack overflow in debug mode
     let base_path: String = base_path.to_string();
-    stacker::grow(4 * 1024 * 1024, move || {
+    stacker::grow(6 * 1024 * 1024, move || {
         run_test(&base_path, feature, status)
             .map_err(|e| e.to_string())
             .map(|_| ())
@@ -130,17 +130,16 @@ pub fn run_test(
             match feature {
                 Parser => unreachable!(),
                 Import => {
-                    // Not sure whether to normalize or not
-                    let expr = expr.skip_typecheck().skip_normalize();
+                    let expr = expr.skip_typecheck().normalize();
                     assert_eq_display!(expr, expected);
                 }
                 Typecheck => {
-                    expr.typecheck_with(&expected.into_type())?;
+                    expr.typecheck_with(&expected.to_type())?;
                 }
                 TypeInference => {
                     let expr = expr.typecheck()?;
-                    let ty = expr.get_type()?;
-                    assert_eq_display!(ty.as_normalized()?.as_ref(), &expected);
+                    let ty = expr.get_type()?.into_owned();
+                    assert_eq_display!(ty.to_normalized(), expected);
                 }
                 Normalization => {
                     let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs
index 43eb2ac..99ca5ee 100644
--- a/dhall/src/traits/deserialize.rs
+++ b/dhall/src/traits/deserialize.rs
@@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> {
 
 impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> {
     fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> {
-        Ok(Normalized::from_str(s, ty)?.into_type())
+        Ok(Normalized::from_str(s, ty)?.to_type())
     }
 }
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index d4faf45..74c2e0a 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -1,7 +1,8 @@
 use crate::expr::*;
 use crate::traits::StaticType;
-use crate::typecheck::{type_of_const, TypeError, TypeMessage};
-use dhall_core::context::Context;
+#[allow(unused_imports)]
+use crate::typecheck::{TypeError, TypeMessage, TypecheckContext};
+#[allow(unused_imports)]
 use dhall_core::{Const, ExprF};
 use std::borrow::Cow;
 
@@ -17,40 +18,18 @@ impl<T: StaticType> DynamicType for T {
 
 impl<'a> DynamicType for Type<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        match &self.0 {
-            TypeInternal::Expr(e) => e.get_type(),
-            TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))),
-            TypeInternal::SuperType => Err(TypeError::new(
-                &Context::new(),
-                dhall_core::rc(ExprF::Const(Const::Sort)),
-                TypeMessage::Untyped,
-            )),
-        }
+        self.get_type()
     }
 }
 
 impl<'a> DynamicType for Normalized<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        match &self.1 {
-            Some(t) => Ok(Cow::Borrowed(t)),
-            None => Err(TypeError::new(
-                &Context::new(),
-                self.0.embed_absurd(),
-                TypeMessage::Untyped,
-            )),
-        }
+        self.0.get_type()
     }
 }
 
 impl<'a> DynamicType for Typed<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        match &self.1 {
-            Some(t) => Ok(Cow::Borrowed(t)),
-            None => Err(TypeError::new(
-                &Context::new(),
-                self.0.clone(),
-                TypeMessage::Untyped,
-            )),
-        }
+        self.0.get_type()
     }
 }
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index e92ce78..df6a177 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -33,17 +33,18 @@ pub trait SimpleStaticType {
 }
 
 fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> {
-    SimpleType(x, std::marker::PhantomData)
+    x.into()
 }
 
 impl<T: SimpleStaticType> StaticType for T {
     fn get_static_type() -> Type<'static> {
-        crate::expr::Normalized(
-            T::get_simple_static_type().into(),
-            Some(Type::const_type()),
-            std::marker::PhantomData,
+        crate::expr::Normalized::from_thunk_and_type(
+            crate::normalize::Thunk::from_normalized_expr(
+                T::get_simple_static_type().into(),
+            ),
+            Type::const_type(),
         )
-        .into_type()
+        .to_type()
     }
 }
 
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index b26f845..78538aa 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,10 +1,11 @@
 #![allow(non_snake_case)]
 use std::borrow::Borrow;
 use std::borrow::Cow;
+use std::collections::BTreeMap;
 use std::fmt;
-use std::marker::PhantomData;
 
 use crate::expr::*;
+use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
 use crate::traits::DynamicType;
 use dhall_core;
 use dhall_core::context::Context;
@@ -22,94 +23,226 @@ impl<'a> Resolved<'a> {
         ty: &Type,
     ) -> Result<Typed<'static>, TypeError> {
         let expr: SubExpr<_, _> = self.0.unnote();
-        let ty: SubExpr<_, _> = ty.clone().unnote().embed()?;
-        type_of(dhall::subexpr!(expr: ty))
+        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd();
+        type_of(rc(ExprF::Annot(expr, ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
     #[allow(dead_code)]
     pub fn skip_typecheck(self) -> Typed<'a> {
-        Typed(self.0.unnote(), None, PhantomData)
+        Typed::from_thunk_untyped(Thunk::new(
+            NormalizationContext::new(),
+            self.0.unnote(),
+        ))
     }
 }
+
 impl<'a> Typed<'a> {
-    fn get_type_move(self) -> Result<Type<'static>, TypeError> {
-        let (expr, ty) = (self.0, self.1);
-        ty.ok_or_else(|| {
-            TypeError::new(&Context::new(), expr, TypeMessage::Untyped)
-        })
+    fn to_type(&self) -> Type<'a> {
+        match &self.to_value() {
+            Value::Const(c) => Type(TypeInternal::Const(*c)),
+            _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
+        }
     }
 }
+
 impl<'a> Normalized<'a> {
-    // Expose the outermost constructor
-    fn unroll_ref(&self) -> &Expr<X, X> {
-        self.as_expr().as_ref()
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        Normalized(self.0.shift(delta, var), self.1)
     }
-    fn shift0(&self, delta: isize, label: &Label) -> Self {
-        // shift the type too ?
-        Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
+    pub(crate) fn to_type(self) -> Type<'a> {
+        self.0.to_type()
     }
 }
-impl Normalized<'static> {
-    fn embed<N>(self) -> SubExpr<N, Normalized<'static>> {
-        rc(ExprF::Embed(self))
+
+impl<'a> Type<'a> {
+    pub(crate) fn to_normalized(&self) -> Normalized<'a> {
+        self.0.to_normalized()
+    }
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+        self.0.to_expr()
+    }
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
+    }
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+        self.0.get_type()
+    }
+    fn as_const(&self) -> Option<Const> {
+        self.0.as_const()
+    }
+    fn internal(&self) -> &TypeInternal<'a> {
+        &self.0
+    }
+    fn internal_whnf(&self) -> Option<Value> {
+        self.0.whnf()
+    }
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        Type(self.0.shift(delta, var))
+    }
+    pub(crate) fn subst_shift(
+        &self,
+        var: &V<Label>,
+        val: &Typed<'static>,
+    ) -> Self {
+        Type(self.0.subst_shift(var, val))
+    }
+
+    fn const_sort() -> Self {
+        Type(TypeInternal::Const(Const::Sort))
+    }
+    fn const_kind() -> Self {
+        Type(TypeInternal::Const(Const::Kind))
+    }
+    pub(crate) fn const_type() -> Self {
+        Type(TypeInternal::Const(Const::Type))
     }
 }
-impl<'a> Type<'a> {
-    pub(crate) fn as_normalized(
+
+impl TypeThunk {
+    fn to_type(
         &self,
-    ) -> Result<Cow<Normalized<'a>>, TypeError> {
-        match &self.0 {
-            TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)),
-            TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))),
-            TypeInternal::SuperType => Err(TypeError::new(
-                &Context::new(),
-                rc(ExprF::Const(Const::Sort)),
-                TypeMessage::Untyped,
-            )),
+        ctx: &TypecheckContext,
+    ) -> Result<Type<'static>, TypeError> {
+        match self {
+            TypeThunk::Type(t) => Ok(t.clone()),
+            TypeThunk::Thunk(th) => {
+                // TODO: rule out statically
+                mktype(ctx, th.normalize_to_expr().embed_absurd())
+            }
+        }
+    }
+}
+
+/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should
+/// be limited to syntactic expressions: either written by the user or meant to be printed.
+/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking,
+/// but only construct `TypeInternal`s.
+#[derive(Debug, Clone)]
+pub(crate) enum TypeInternal<'a> {
+    Const(Const),
+    /// This must not contain a Const value.
+    Typed(Box<Typed<'a>>),
+}
+
+impl<'a> TypeInternal<'a> {
+    fn to_typed(&self) -> Typed<'a> {
+        match self {
+            TypeInternal::Typed(e) => e.as_ref().clone(),
+            TypeInternal::Const(c) => const_to_typed(*c),
         }
     }
-    pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
-        match self.0 {
-            TypeInternal::Expr(e) => Ok(*e),
-            TypeInternal::Const(c) => Ok(const_to_normalized(c)),
-            TypeInternal::SuperType => Err(TypeError::new(
-                &Context::new(),
-                rc(ExprF::Const(Const::Sort)),
-                TypeMessage::Untyped,
-            )),
+    fn to_normalized(&self) -> Normalized<'a> {
+        self.to_typed().normalize()
+    }
+    fn to_expr(&self) -> SubExpr<X, X> {
+        self.to_normalized().to_expr()
+    }
+    fn to_value(&self) -> Value {
+        self.to_typed().to_value().clone()
+    }
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+        Ok(match self {
+            TypeInternal::Typed(e) => e.get_type()?,
+            TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?),
+        })
+    }
+    fn as_const(&self) -> Option<Const> {
+        match self {
+            TypeInternal::Const(c) => Some(*c),
+            _ => None,
         }
     }
-    // Expose the outermost constructor
-    fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, TypeError> {
-        match self.as_normalized()? {
-            Cow::Borrowed(e) => Ok(Cow::Borrowed(e.unroll_ref())),
-            Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
+    fn whnf(&self) -> Option<Value> {
+        match self {
+            TypeInternal::Typed(e) => Some(e.to_value()),
+            _ => None,
         }
     }
-    fn shift0(&self, delta: isize, label: &Label) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use TypeInternal::*;
-        Type(match &self.0 {
-            Expr(e) => Expr(Box::new(e.shift0(delta, label))),
+        match self {
+            Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
-            SuperType => SuperType,
-        })
+        }
+    }
+    fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
+        use TypeInternal::*;
+        match self {
+            Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
+            Const(c) => Const(*c),
+        }
     }
+}
 
-    fn const_sort() -> Self {
-        Type(TypeInternal::Const(Const::Sort))
+impl<'a> Eq for TypeInternal<'a> {}
+impl<'a> PartialEq for TypeInternal<'a> {
+    fn eq(&self, other: &Self) -> bool {
+        self.to_normalized() == other.to_normalized()
     }
-    fn const_kind() -> Self {
-        Type(TypeInternal::Const(Const::Kind))
+}
+
+#[derive(Debug, Clone)]
+pub(crate) enum EnvItem {
+    Type(V<Label>, Type<'static>),
+    Value(Normalized<'static>),
+}
+
+impl EnvItem {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        use EnvItem::*;
+        match self {
+            Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
+            Value(e) => Value(e.shift(delta, var)),
+        }
     }
-    pub(crate) fn const_type() -> Self {
-        Type(TypeInternal::Const(Const::Type))
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct TypecheckContext(pub(crate) Context<Label, EnvItem>);
+
+impl TypecheckContext {
+    pub(crate) fn new() -> Self {
+        TypecheckContext(Context::new())
+    }
+    pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self {
+        TypecheckContext(
+            self.0.map(|_, e| e.shift(1, &x.into())).insert(
+                x.clone(),
+                EnvItem::Type(x.into(), t.shift(1, &x.into())),
+            ),
+        )
+    }
+    pub(crate) fn insert_value(
+        &self,
+        x: &Label,
+        t: Normalized<'static>,
+    ) -> Self {
+        TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
+    }
+    pub(crate) fn lookup(
+        &self,
+        var: &V<Label>,
+    ) -> Option<Cow<'_, Type<'static>>> {
+        let V(x, n) = var;
+        match self.0.lookup(x, *n) {
+            Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
+            Some(EnvItem::Value(t)) => Some(t.get_type()?),
+            None => None,
+        }
+    }
+    fn to_normalization_ctx(&self) -> NormalizationContext {
+        NormalizationContext::from_typecheck_ctx(self)
     }
 }
-impl Type<'static> {
-    fn embed<N>(self) -> Result<SubExpr<N, Normalized<'static>>, TypeError> {
-        Ok(self.into_normalized()?.embed())
+
+impl PartialEq for TypecheckContext {
+    fn eq(&self, _: &Self) -> bool {
+        // don't count contexts when comparing stuff
+        // this is dirty but needed for now
+        true
     }
 }
+impl Eq for TypecheckContext {}
 
 fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
@@ -192,38 +325,45 @@ where
             (_, _) => false,
         }
     }
-    match (&eL0.borrow().0, &eR0.borrow().0) {
-        (TypeInternal::SuperType, TypeInternal::SuperType) => true,
-        (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
-        (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+    match (eL0.borrow().internal(), eR0.borrow().internal()) {
+        // (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
+        // (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+        _ => {
             let mut ctx = vec![];
-            go(&mut ctx, l.as_expr(), r.as_expr())
+            go(
+                &mut ctx,
+                &eL0.borrow().to_expr(),
+                &eR0.borrow().to_expr(),
+            )
         }
-        _ => false,
+        // _ => false,
     }
 }
 
-fn const_to_normalized<'a>(c: Const) -> Normalized<'a> {
-    Normalized(
-        rc(ExprF::Const(c)),
-        Some(Type(match c {
-            Const::Type => TypeInternal::Const(Const::Kind),
-            Const::Kind => TypeInternal::Const(Const::Sort),
-            Const::Sort => TypeInternal::SuperType,
-        })),
-        PhantomData,
-    )
+fn const_to_typed<'a>(c: Const) -> Typed<'a> {
+    match c {
+        Const::Sort => Typed::const_sort(),
+        _ => Typed::from_thunk_and_type(
+            Value::Const(c).into_thunk(),
+            type_of_const(c).unwrap(),
+        ),
+    }
 }
 
 fn const_to_type<'a>(c: Const) -> Type<'a> {
     Type(TypeInternal::Const(c))
 }
 
-pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> {
+fn type_of_const<'a>(c: Const) -> Result<Type<'a>, TypeError> {
     match c {
-        Const::Type => Type::const_kind(),
-        Const::Kind => Type::const_sort(),
-        Const::Sort => Type(TypeInternal::SuperType),
+        Const::Type => Ok(Type::const_kind()),
+        Const::Kind => Ok(Type::const_sort()),
+        Const::Sort => {
+            return Err(TypeError::new(
+                &TypecheckContext::new(),
+                TypeMessage::Sort,
+            ))
+        }
     }
 }
 
@@ -302,59 +442,198 @@ macro_rules! ensure_equal {
     };
 }
 
-// Do not use with Const because they will never match
-macro_rules! ensure_matches {
-    ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => {
-        match $x.unroll_ref()? {
-            Cow::Borrowed(e) => match e {
-                $pat => $branch,
-                _ => return Err($err),
-            },
-            // Can't pattern match because lifetimes
-            Cow::Owned(_) => return Err($err),
-        }
-    };
-}
-
 // Ensure the provided type has type `Type`
 macro_rules! ensure_simple_type {
     ($x:expr, $err:expr $(,)*) => {{
-        let k = ensure_is_const!($x.get_type()?, $err);
-        if k != Type {
-            return Err($err);
+        match $x.get_type()?.as_const() {
+            Some(dhall_core::Const::Type) => {}
+            _ => return Err($err),
         }
     }};
 }
 
-macro_rules! ensure_is_const {
-    ($x:expr, $err:expr $(,)*) => {
-        match $x.unroll_ref()?.as_ref() {
-            Const(k) => *k,
-            _ => return Err($err),
-        }
-    };
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum TypeIntermediate {
+    Pi(TypecheckContext, Label, Type<'static>, Type<'static>),
+    RecordType(TypecheckContext, BTreeMap<Label, Type<'static>>),
+    UnionType(TypecheckContext, BTreeMap<Label, Option<Type<'static>>>),
+    ListType(TypecheckContext, Type<'static>),
+    OptionalType(TypecheckContext, Type<'static>),
+}
+
+impl TypeIntermediate {
+    fn typecheck(self) -> Result<Typed<'static>, TypeError> {
+        let mkerr = |ctx, msg| TypeError::new(ctx, msg);
+        Ok(match &self {
+            TypeIntermediate::Pi(ctx, x, ta, tb) => {
+                let ctx2 = ctx.insert_type(x, ta.clone());
+
+                let kA = match ta.get_type()?.as_const() {
+                    Some(k) => k,
+                    _ => {
+                        return Err(mkerr(
+                            ctx,
+                            InvalidInputType(ta.clone().to_normalized()),
+                        ))
+                    }
+                };
+
+                let kB = match tb.get_type()?.as_const() {
+                    Some(k) => k,
+                    _ => {
+                        return Err(mkerr(
+                            &ctx2,
+                            InvalidOutputType(
+                                tb.clone()
+                                    .to_normalized()
+                                    .get_type()?
+                                    .to_normalized(),
+                            ),
+                        ))
+                    }
+                };
+
+                let k = match function_check(kA, kB) {
+                    Ok(k) => k,
+                    Err(()) => {
+                        return Err(mkerr(
+                            ctx,
+                            NoDependentTypes(
+                                ta.clone().to_normalized(),
+                                tb.clone()
+                                    .to_normalized()
+                                    .get_type()?
+                                    .to_normalized(),
+                            ),
+                        ))
+                    }
+                };
+
+                Typed::from_thunk_and_type(
+                    Value::Pi(
+                        x.clone(),
+                        TypeThunk::from_type(ta.clone()),
+                        TypeThunk::from_type(tb.clone()),
+                    )
+                    .into_thunk(),
+                    const_to_type(k),
+                )
+            }
+            TypeIntermediate::RecordType(ctx, kts) => {
+                // Check that all types are the same const
+                let mut k = None;
+                for (x, t) in kts {
+                    match (k, t.get_type()?.as_const()) {
+                        (None, Some(k2)) => k = Some(k2),
+                        (Some(k1), Some(k2)) if k1 == k2 => {}
+                        _ => {
+                            return Err(mkerr(
+                                ctx,
+                                InvalidFieldType(x.clone(), t.clone()),
+                            ))
+                        }
+                    }
+                }
+                // An empty record type has type Type
+                let k = k.unwrap_or(dhall_core::Const::Type);
+
+                Typed::from_thunk_and_type(
+                    Value::RecordType(
+                        kts.iter()
+                            .map(|(k, t)| {
+                                (k.clone(), TypeThunk::from_type(t.clone()))
+                            })
+                            .collect(),
+                    )
+                    .into_thunk(),
+                    const_to_type(k),
+                )
+            }
+            TypeIntermediate::UnionType(ctx, kts) => {
+                // Check that all types are the same const
+                let mut k = None;
+                for (x, t) in kts {
+                    if let Some(t) = t {
+                        match (k, t.get_type()?.as_const()) {
+                            (None, Some(k2)) => k = Some(k2),
+                            (Some(k1), Some(k2)) if k1 == k2 => {}
+                            _ => {
+                                return Err(mkerr(
+                                    ctx,
+                                    InvalidFieldType(x.clone(), t.clone()),
+                                ))
+                            }
+                        }
+                    }
+                }
+
+                // An empty union type has type Type;
+                // an union type with only unary variants also has type Type
+                let k = k.unwrap_or(dhall_core::Const::Type);
+
+                Typed::from_thunk_and_type(
+                    Value::UnionType(
+                        kts.iter()
+                            .map(|(k, t)| {
+                                (
+                                    k.clone(),
+                                    t.as_ref().map(|t| {
+                                        TypeThunk::from_type(t.clone())
+                                    }),
+                                )
+                            })
+                            .collect(),
+                    )
+                    .into_thunk(),
+                    const_to_type(k),
+                )
+            }
+            TypeIntermediate::ListType(ctx, t) => {
+                ensure_simple_type!(
+                    t,
+                    mkerr(ctx, InvalidListType(t.clone().to_normalized())),
+                );
+                Typed::from_thunk_and_type(
+                    Value::from_builtin(Builtin::List)
+                        .app(t.to_value())
+                        .into_thunk(),
+                    const_to_type(Const::Type),
+                )
+            }
+            TypeIntermediate::OptionalType(ctx, t) => {
+                ensure_simple_type!(
+                    t,
+                    mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())),
+                );
+                Typed::from_thunk_and_type(
+                    Value::from_builtin(Builtin::Optional)
+                        .app(t.to_value())
+                        .into_thunk(),
+                    const_to_type(Const::Type),
+                )
+            }
+        })
+    }
 }
 
 /// Takes an expression that is meant to contain a Type
 /// and turn it into a type, typechecking it along the way.
 fn mktype(
-    ctx: &Context<Label, Type<'static>>,
+    ctx: &TypecheckContext,
     e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Type<'static>, TypeError> {
-    Ok(type_with(ctx, e)?.normalize().into_type())
-}
-
-fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> {
-    SimpleType(e, PhantomData).into_type()
+    Ok(type_with(ctx, e)?.to_type())
 }
 
-fn simple_type_from_builtin<'a>(b: Builtin) -> Type<'a> {
-    into_simple_type(rc(ExprF::Builtin(b)))
+fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> {
+    mktype(&TypecheckContext::new(), rc(ExprF::Builtin(b)))
 }
 
 /// Intermediary return type
 enum Ret {
-    /// Returns the contained Type as is
+    /// Returns the contained value as is
+    RetTyped(Typed<'static>),
+    /// Use the contained Type as the type of the input expression
     RetType(Type<'static>),
     /// Returns an expression that must be typechecked and
     /// turned into a Type first.
@@ -364,55 +643,32 @@ enum Ret {
 /// Type-check an expression and return the expression alongside its type if type-checking
 /// succeeded, or an error if type-checking failed
 fn type_with(
-    ctx: &Context<Label, Type<'static>>,
+    ctx: &TypecheckContext,
     e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Typed<'static>, TypeError> {
     use dhall_core::ExprF::*;
-    let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, e.clone(), msg);
 
     use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t = mktype(ctx, t.clone())?;
-            let ctx2 =
-                ctx.insert(x.clone(), t.clone()).map(|_, e| e.shift0(1, x));
+            let tx = mktype(ctx, t.clone())?;
+            let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
-            Ok(RetExpr(Pi(
-                x.clone(),
-                t.embed()?,
-                b.get_type_move()?.embed()?,
-            )))
+            let tb = b.get_type()?.into_owned();
+            Ok(RetType(
+                TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
         Pi(x, ta, tb) => {
             let ta = mktype(ctx, ta.clone())?;
-            let kA = ensure_is_const!(
-                &ta.get_type()?,
-                mkerr(InvalidInputType(ta.into_normalized()?)),
-            );
-
-            let ctx2 =
-                ctx.insert(x.clone(), ta.clone()).map(|_, e| e.shift0(1, x));
-            let tb = type_with(&ctx2, tb.clone())?;
-            let kB = ensure_is_const!(
-                &tb.get_type()?,
-                TypeError::new(
-                    &ctx2,
-                    e.clone(),
-                    InvalidOutputType(tb.get_type_move()?.into_normalized()?),
-                ),
-            );
-
-            let k = match function_check(kA, kB) {
-                Ok(k) => k,
-                Err(()) => {
-                    return Err(mkerr(NoDependentTypes(
-                        ta.clone().into_normalized()?,
-                        tb.get_type_move()?.into_normalized()?,
-                    )))
-                }
-            };
-
-            Ok(RetExpr(Const(k)))
+            let ctx2 = ctx.insert_type(x, ta.clone());
+            let tb = mktype(&ctx2, tb.clone())?;
+            Ok(RetTyped(
+                TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb)
+                    .typecheck()?,
+            ))
         }
         Let(x, t, v, e) => {
             let v = if let Some(t) = t {
@@ -422,43 +678,52 @@ fn type_with(
             };
 
             let v = type_with(ctx, v)?.normalize();
-            let e = type_with(
-                ctx,
-                // TODO: Use a substitution context
-                subst_shift(&V(x.clone(), 0), &v.embed(), e),
-            )?;
+            let e = type_with(&ctx.insert_value(x, v.clone()), e.clone())?;
 
-            Ok(RetType(e.get_type_move()?))
+            Ok(RetType(e.get_type()?.into_owned()))
+        }
+        OldOptionalLit(None, t) => {
+            let t = t.clone();
+            let e = dhall::subexpr!(None t);
+            return type_with(ctx, e);
+        }
+        OldOptionalLit(Some(x), t) => {
+            let t = t.clone();
+            let x = x.clone();
+            let e = dhall::subexpr!(Some x : Optional t);
+            return type_with(ctx, e);
         }
-        Embed(p) => return Ok(p.clone().into()),
+        Embed(p) => Ok(RetTyped(p.clone().into())),
         _ => type_last_layer(
             ctx,
             // Typecheck recursively all subexpressions
             e.as_ref()
-                .traverse_ref_simple(|e| type_with(ctx, e.clone()))?,
-            e.clone(),
+                .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?,
         ),
     }?;
-    match ret {
-        RetExpr(ret) => Ok(Typed(e, Some(mktype(ctx, rc(ret))?), PhantomData)),
-        RetType(typ) => Ok(Typed(e, Some(typ), PhantomData)),
-    }
+    Ok(match ret {
+        RetExpr(ret) => Typed::from_thunk_and_type(
+            Thunk::new(ctx.to_normalization_ctx(), e),
+            mktype(ctx, rc(ret))?,
+        ),
+        RetType(typ) => Typed::from_thunk_and_type(
+            Thunk::new(ctx.to_normalization_ctx(), e),
+            typ,
+        ),
+        RetTyped(tt) => tt,
+    })
 }
 
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
 fn type_last_layer(
-    ctx: &Context<Label, Type<'static>>,
+    ctx: &TypecheckContext,
     e: ExprF<Typed<'static>, Label, X, Normalized<'static>>,
-    original_e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Ret, TypeError> {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
-    use dhall_core::Const::*;
     use dhall_core::ExprF::*;
-    let mkerr = |msg: TypeMessage<'static>| {
-        TypeError::new(ctx, original_e.clone(), msg)
-    };
+    let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, msg);
 
     use Ret::*;
     match e {
@@ -466,40 +731,43 @@ fn type_last_layer(
         Pi(_, _, _) => unreachable!(),
         Let(_, _, _, _) => unreachable!(),
         Embed(_) => unreachable!(),
-        Var(V(x, n)) => match ctx.lookup(&x, n) {
-            Some(e) => Ok(RetType(e.clone())),
-            None => Err(mkerr(UnboundVariable)),
+        Var(var) => match ctx.lookup(&var) {
+            Some(e) => Ok(RetType(e.into_owned())),
+            None => Err(mkerr(UnboundVariable(var.clone()))),
         },
         App(f, a) => {
             let tf = f.get_type()?;
-            let (x, tx, tb) = ensure_matches!(tf,
-                Pi(x, tx, tb) => (x, tx, tb),
-                mkerr(NotAFunction(f))
-            );
-            let tx = mktype(ctx, tx.embed_absurd())?;
-            ensure_equal!(a.get_type()?, &tx, {
-                mkerr(TypeMismatch(f, tx.into_normalized()?, a))
+            let tf_internal = tf.internal_whnf();
+            let (x, tx, tb) = match &tf_internal {
+                Some(Value::Pi(
+                    x,
+                    TypeThunk::Type(tx),
+                    TypeThunk::Type(tb),
+                )) => (x, tx, tb),
+                Some(Value::Pi(_, _, _)) => {
+                    panic!("ICE: this should not have happened")
+                }
+                _ => return Err(mkerr(NotAFunction(f.clone()))),
+            };
+            ensure_equal!(a.get_type()?, tx, {
+                mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
-            Ok(RetExpr(Let(
-                x.clone(),
-                None,
-                a.normalize().embed(),
-                tb.embed_absurd(),
-            )))
+
+            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
         }
         Annot(x, t) => {
-            let t = t.normalize().into_type();
+            let t = t.to_type();
             ensure_equal!(
                 &t,
                 x.get_type()?,
-                mkerr(AnnotMismatch(x, t.into_normalized()?))
+                mkerr(AnnotMismatch(x, t.to_normalized()))
             );
-            Ok(RetType(x.get_type_move()?))
+            Ok(RetType(x.get_type()?.into_owned()))
         }
         BoolIf(x, y, z) => {
             ensure_equal!(
                 x.get_type()?,
-                &simple_type_from_builtin(Bool),
+                &builtin_to_type(Bool)?,
                 mkerr(InvalidPredicate(x)),
             );
 
@@ -519,162 +787,174 @@ fn type_last_layer(
                 mkerr(IfBranchMismatch(y, z))
             );
 
-            Ok(RetType(y.get_type_move()?))
+            Ok(RetType(y.get_type()?.into_owned()))
         }
         EmptyListLit(t) => {
-            let t = t.normalize().into_type();
-            ensure_simple_type!(
-                t,
-                mkerr(InvalidListType(t.into_normalized()?)),
-            );
-            let t = t.embed()?;
-            Ok(RetExpr(dhall::expr!(List t)))
+            let t = t.to_type();
+            Ok(RetType(
+                TypeIntermediate::ListType(ctx.clone(), t)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
         NEListLit(xs) => {
             let mut iter = xs.into_iter().enumerate();
             let (_, x) = iter.next().unwrap();
-            ensure_simple_type!(
-                x.get_type()?,
-                mkerr(InvalidListType(x.get_type_move()?.into_normalized()?)),
-            );
             for (i, y) in iter {
                 ensure_equal!(
                     x.get_type()?,
                     y.get_type()?,
                     mkerr(InvalidListElement(
                         i,
-                        x.get_type_move()?.into_normalized()?,
+                        x.get_type()?.to_normalized(),
                         y
                     ))
                 );
             }
-            let t = x.get_type_move()?;
-            let t = t.embed()?;
-            Ok(RetExpr(dhall::expr!(List t)))
-        }
-        OldOptionalLit(None, t) => {
-            let t = t.normalize().embed();
-            let e = dhall::subexpr!(None t);
-            Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
-        }
-        OldOptionalLit(Some(x), t) => {
-            let t = t.normalize().embed();
-            let x = x.normalize().embed();
-            let e = dhall::subexpr!(Some x : Optional t);
-            Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
+            let t = x.get_type()?.into_owned();
+            Ok(RetType(
+                TypeIntermediate::ListType(ctx.clone(), t)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
         SomeLit(x) => {
-            let tx = x.get_type_move()?;
-            ensure_simple_type!(
-                tx,
-                mkerr(InvalidOptionalType(tx.into_normalized()?)),
-            );
-            let t = tx.embed()?;
-            Ok(RetExpr(dhall::expr!(Optional t)))
+            let t = x.get_type()?.into_owned();
+            Ok(RetType(
+                TypeIntermediate::OptionalType(ctx.clone(), t)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
         RecordType(kts) => {
-            // Check that all types are the same const
-            let mut k = None;
-            for (x, t) in kts {
-                let k2 = ensure_is_const!(
-                    t.get_type()?,
-                    mkerr(InvalidFieldType(x, t))
-                );
-                match k {
-                    None => k = Some(k2),
-                    Some(k1) if k1 != k2 => {
-                        return Err(mkerr(InvalidFieldType(x, t)))
-                    }
-                    Some(_) => {}
-                }
-            }
-            // An empty record type has type Type
-            let k = k.unwrap_or(dhall_core::Const::Type);
-            Ok(RetType(const_to_type(k)))
+            let kts: BTreeMap<_, _> = kts
+                .into_iter()
+                .map(|(x, t)| Ok((x, t.to_type())))
+                .collect::<Result<_, _>>()?;
+            Ok(RetTyped(
+                TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
+            ))
         }
         UnionType(kts) => {
-            // Check that all types are the same const
-            let mut k = None;
-            for (x, t) in kts {
-                if let Some(t) = t {
-                    let k2 = ensure_is_const!(
-                        t.get_type()?,
-                        mkerr(InvalidFieldType(x, t))
-                    );
-                    match k {
-                        None => k = Some(k2),
-                        Some(k1) if k1 != k2 => {
-                            return Err(mkerr(InvalidFieldType(x, t)))
-                        }
-                        Some(_) => {}
-                    }
-                }
-            }
-            // An empty union type has type Type
-            // An union type with only unary variants has type Type
-            let k = k.unwrap_or(dhall_core::Const::Type);
-            Ok(RetType(const_to_type(k)))
+            let kts: BTreeMap<_, _> = kts
+                .into_iter()
+                .map(|(x, t)| {
+                    Ok((
+                        x,
+                        match t {
+                            None => None,
+                            Some(t) => Some(t.to_type()),
+                        },
+                    ))
+                })
+                .collect::<Result<_, _>>()?;
+            Ok(RetTyped(
+                TypeIntermediate::UnionType(ctx.clone(), kts).typecheck()?,
+            ))
         }
         RecordLit(kvs) => {
             let kts = kvs
                 .into_iter()
-                .map(|(x, v)| {
-                    let t = v.get_type_move()?.embed()?;
-                    Ok((x, t))
-                })
+                .map(|(x, v)| Ok((x, v.get_type()?.into_owned())))
                 .collect::<Result<_, _>>()?;
-            Ok(RetExpr(RecordType(kts)))
+            Ok(RetType(
+                TypeIntermediate::RecordType(ctx.clone(), kts)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
         UnionLit(x, v, kvs) => {
             let mut kts: std::collections::BTreeMap<_, _> = kvs
                 .into_iter()
                 .map(|(x, v)| {
-                    let t = v.map(|x| x.normalize().embed());
+                    let t = match v {
+                        Some(x) => Some(x.to_type()),
+                        None => None,
+                    };
                     Ok((x, t))
                 })
                 .collect::<Result<_, _>>()?;
-            let t = v.get_type_move()?.embed()?;
+            let t = v.get_type()?.into_owned();
             kts.insert(x, Some(t));
-            Ok(RetExpr(UnionType(kts)))
+            Ok(RetType(
+                TypeIntermediate::UnionType(ctx.clone(), kts)
+                    .typecheck()?
+                    .to_type(),
+            ))
         }
-        Field(r, x) => match r.get_type()?.unroll_ref()?.as_ref() {
-            RecordType(kts) => match kts.get(&x) {
-                Some(t) => Ok(RetExpr(t.unroll().embed_absurd())),
-                None => Err(mkerr(MissingRecordField(x, r))),
-            },
-            _ => {
-                let r = r.normalize();
-                match r.as_expr().as_ref() {
-                    UnionType(kts) => match kts.get(&x) {
-                        // Constructor has type T -> < x: T, ... >
-                        // TODO: use "_" instead of x
-                        Some(Some(t)) => Ok(RetExpr(Pi(
-                            x.clone(),
-                            t.embed_absurd(),
-                            r.embed(),
-                        ))),
-                        Some(None) => Ok(RetType(r.into_type())),
-                        None => Err(mkerr(MissingUnionField(x, r))),
+        Field(r, x) => {
+            let tr = r.get_type()?;
+            let tr_internal = tr.internal_whnf();
+            match &tr_internal {
+                Some(Value::RecordType(kts)) => match kts.get(&x) {
+                    Some(tth) => {
+                        let tth = tth.clone();
+                        drop(tr_internal);
+                        Ok(RetType(tth.to_type(ctx)?))
                     },
-                    _ => Err(mkerr(NotARecord(x, r))),
+                    None => Err(mkerr(MissingRecordField(x, r.clone()))),
+                },
+                // TODO: branch here only when r.get_type() is a Const
+                _ => {
+                    let r = r.to_type();
+                    let r_internal = r.internal_whnf();
+                    match &r_internal {
+                        Some(Value::UnionType(kts)) => match kts.get(&x) {
+                            // Constructor has type T -> < x: T, ... >
+                            // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
+                            Some(Some(t)) => {
+                                let t = t.clone();
+                                drop(r_internal);
+                                Ok(RetType(
+                                    TypeIntermediate::Pi(
+                                        ctx.clone(),
+                                        x.clone(),
+                                        t.to_type(ctx)?,
+                                        r,
+                                    )
+                                    .typecheck()?
+                                    .to_type(),
+                                ))
+                            },
+                            Some(None) => {
+                                drop(r_internal);
+                                Ok(RetType(r))
+                            },
+                            None => {
+                                drop(r_internal);
+                                Err(mkerr(MissingUnionField(
+                                    x,
+                                    r.to_normalized(),
+                                )))
+                            },
+                        },
+                        _ => {
+                            drop(r_internal);
+                            Err(mkerr(NotARecord(
+                                x,
+                                r.to_normalized()
+                            )))
+                        },
+                    }
                 }
+                // _ => Err(mkerr(NotARecord(
+                //     x,
+                //     r.to_type()?.to_normalized(),
+                // ))),
             }
-        },
-        Const(c) => Ok(RetType(type_of_const(c))),
+        }
+        Const(c) => Ok(RetTyped(const_to_typed(c))),
         Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
-        BoolLit(_) => Ok(RetType(simple_type_from_builtin(Bool))),
-        NaturalLit(_) => Ok(RetType(simple_type_from_builtin(Natural))),
-        IntegerLit(_) => Ok(RetType(simple_type_from_builtin(Integer))),
-        DoubleLit(_) => Ok(RetType(simple_type_from_builtin(Double))),
+        BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
+        NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
+        IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
+        DoubleLit(_) => Ok(RetType(builtin_to_type(Double)?)),
         // TODO: check type of interpolations
-        TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))),
+        TextLit(_) => Ok(RetType(builtin_to_type(Text)?)),
         BinOp(o @ ListAppend, l, r) => {
-            match l.get_type()?.unroll_ref()?.as_ref() {
-                App(f, _) => match f.as_ref() {
-                    Builtin(List) => {}
-                    _ => return Err(mkerr(BinOpTypeMismatch(o, l))),
-                },
-                _ => return Err(mkerr(BinOpTypeMismatch(o, l))),
+            match l.get_type()?.internal_whnf() {
+                Some(Value::AppliedBuiltin(List, _)) => {}
+                _ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))),
             }
 
             ensure_equal!(
@@ -686,7 +966,7 @@ fn type_last_layer(
             Ok(RetType(l.get_type()?.into_owned()))
         }
         BinOp(o, l, r) => {
-            let t = simple_type_from_builtin(match o {
+            let t = builtin_to_type(match o {
                 BoolAnd => Bool,
                 BoolOr => Bool,
                 BoolEQ => Bool,
@@ -696,7 +976,7 @@ fn type_last_layer(
                 TextAppend => Text,
                 ListAppend => unreachable!(),
                 _ => return Err(mkerr(Unimplemented)),
-            });
+            })?;
 
             ensure_equal!(l.get_type()?, &t, mkerr(BinOpTypeMismatch(o, l)));
 
@@ -714,17 +994,17 @@ fn type_last_layer(
 fn type_of(
     e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Typed<'static>, TypeError> {
-    let ctx = Context::new();
+    let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
-    // Ensure the inferred type isn't SuperType
-    e.get_type()?.as_normalized()?;
+    // Ensure `e` has a type (i.e. `e` is not `Sort`)
+    e.get_type()?;
     Ok(e)
 }
 
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage<'a> {
-    UnboundVariable,
+    UnboundVariable(V<Label>),
     InvalidInputType(Normalized<'a>),
     InvalidOutputType(Normalized<'a>),
     NotAFunction(Typed<'a>),
@@ -737,41 +1017,45 @@ pub(crate) enum TypeMessage<'a> {
     InvalidPredicate(Typed<'a>),
     IfBranchMismatch(Typed<'a>, Typed<'a>),
     IfBranchMustBeTerm(bool, Typed<'a>),
-    InvalidFieldType(Label, Typed<'a>),
+    InvalidFieldType(Label, Type<'a>),
     NotARecord(Label, Normalized<'a>),
     MissingRecordField(Label, Typed<'a>),
     MissingUnionField(Label, Normalized<'a>),
     BinOpTypeMismatch(BinOp, Typed<'a>),
     NoDependentTypes(Normalized<'a>, Normalized<'a>),
+    Sort,
     Unimplemented,
 }
 
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError {
-    context: Context<Label, Type<'static>>,
-    current: SubExpr<X, Normalized<'static>>,
     type_message: TypeMessage<'static>,
+    context: TypecheckContext,
 }
 
 impl TypeError {
     pub(crate) fn new(
-        context: &Context<Label, Type<'static>>,
-        current: SubExpr<X, Normalized<'static>>,
+        context: &TypecheckContext,
         type_message: TypeMessage<'static>,
     ) -> Self {
         TypeError {
             context: context.clone(),
-            current,
             type_message,
         }
     }
 }
 
+impl From<TypeError> for std::option::NoneError {
+    fn from(_: TypeError) -> std::option::NoneError {
+        std::option::NoneError
+    }
+}
+
 impl ::std::error::Error for TypeMessage<'static> {
     fn description(&self) -> &str {
         match *self {
-            UnboundVariable => "Unbound variable",
+            // UnboundVariable => "Unbound variable",
             InvalidInputType(_) => "Invalid function input",
             InvalidOutputType(_) => "Invalid function output",
             NotAFunction(_) => "Not a function",
@@ -784,28 +1068,28 @@ impl ::std::error::Error for TypeMessage<'static> {
 impl fmt::Display for TypeMessage<'static> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         match self {
-            UnboundVariable => {
-                f.write_str(include_str!("errors/UnboundVariable.txt"))
-            }
-            TypeMismatch(e0, e1, e2) => {
-                let template = include_str!("errors/TypeMismatch.txt");
-                let s = template
-                    .replace("$txt0", &format!("{}", e0.as_expr()))
-                    .replace("$txt1", &format!("{}", e1.as_expr()))
-                    .replace("$txt2", &format!("{}", e2.as_expr()))
-                    .replace(
-                        "$txt3",
-                        &format!(
-                            "{}",
-                            e2.get_type()
-                                .unwrap()
-                                .as_normalized()
-                                .unwrap()
-                                .as_expr()
-                        ),
-                    );
-                f.write_str(&s)
-            }
+            // UnboundVariable(_) => {
+            //     f.write_str(include_str!("errors/UnboundVariable.txt"))
+            // }
+            // TypeMismatch(e0, e1, e2) => {
+            //     let template = include_str!("errors/TypeMismatch.txt");
+            //     let s = template
+            //         .replace("$txt0", &format!("{}", e0.as_expr()))
+            //         .replace("$txt1", &format!("{}", e1.as_expr()))
+            //         .replace("$txt2", &format!("{}", e2.as_expr()))
+            //         .replace(
+            //             "$txt3",
+            //             &format!(
+            //                 "{}",
+            //                 e2.get_type()
+            //                     .unwrap()
+            //                     .as_normalized()
+            //                     .unwrap()
+            //                     .as_expr()
+            //             ),
+            //         );
+            //     f.write_str(&s)
+            // }
             _ => f.write_str("Unhandled error message"),
         }
     }