Merge pull request #104 from Nadrieril/rework-value

Rework Value

3 files changed, 589 insertions, 870 deletions

diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 778f990..1f7e5f0 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,8 +4,8 @@ use std::path::Path;
 
 use dhall_syntax::{Const, SubExpr};
 
-use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
+use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 
@@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed(TypedThunk);
+pub struct Typed(Value);
 
 /// A normalized expression.
 ///
@@ -41,8 +41,6 @@ pub struct Typed(TypedThunk);
 #[derive(Debug, Clone)]
 pub struct Normalized(Typed);
 
-pub type Type = Typed;
-
 impl Parsed {
     pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
         parse::parse_file(f)
@@ -71,15 +69,10 @@ impl Parsed {
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError> {
-        typecheck::typecheck(self)
-    }
-    pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
-        typecheck::typecheck_with(self, ty)
+        Ok(typecheck::typecheck(self.0)?.into_typed())
     }
-    /// Pretends this expression has been typechecked. Use with care.
-    #[allow(dead_code)]
-    pub(crate) fn skip_typecheck(self) -> Typed {
-        typecheck::skip_typecheck(self)
+    pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
+        Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
     }
 }
 
@@ -97,58 +90,39 @@ impl Typed {
         Normalized(self)
     }
 
-    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
-        Typed(TypedThunk::from_thunk_and_type(th, t))
-    }
-    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
-        Typed(TypedThunk::from_thunk_untyped(th))
-    }
     pub(crate) fn from_const(c: Const) -> Self {
-        Typed(TypedThunk::from_const(c))
+        Typed(Value::from_const(c))
     }
-    pub fn from_value_untyped(v: Value) -> Self {
-        Typed(TypedThunk::from_value_untyped(v))
+    pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
+        Typed(Value::from_valuef_and_type(v, t.into_value()))
     }
-    pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
+    pub(crate) fn from_value(th: Value) -> Self {
         Typed(th)
     }
-
-    pub(crate) fn to_value(&self) -> Value {
-        self.0.to_value()
+    pub fn const_type() -> Self {
+        Typed::from_const(Const::Type)
     }
+
     pub fn to_expr(&self) -> NormalizedSubExpr {
         self.0.to_expr()
     }
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.0.to_expr_alpha()
     }
-    pub fn to_thunk(&self) -> Thunk {
-        self.0.to_thunk()
-    }
-    // Deprecated
-    pub fn to_type(&self) -> Type {
-        self.clone()
+    pub fn to_value(&self) -> Value {
+        self.0.clone()
     }
-    // Deprecated
-    pub(crate) fn into_type(self) -> Type {
-        self
-    }
-    pub(crate) fn into_typethunk(self) -> TypedThunk {
+    pub(crate) fn into_value(self) -> Value {
         self.0
     }
-    pub(crate) fn to_normalized(&self) -> Normalized {
-        self.clone().normalize()
-    }
-    pub(crate) fn as_const(&self) -> Option<Const> {
-        self.0.as_const()
-    }
 
     pub(crate) fn normalize_mut(&mut self) {
         self.0.normalize_mut()
     }
 
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
-        self.0.get_type()
+    #[allow(dead_code)]
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> {
+        Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed()))
     }
 }
 
@@ -164,13 +138,6 @@ impl Normalized {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.0.to_expr_alpha()
     }
-    #[allow(dead_code)]
-    pub(crate) fn to_type(&self) -> Type {
-        self.0.to_type()
-    }
-    pub(crate) fn to_value(&self) -> Value {
-        self.0.to_value()
-    }
     pub(crate) fn into_typed(self) -> Typed {
         self.0
     }
@@ -188,8 +155,8 @@ impl Shift for Normalized {
     }
 }
 
-impl Subst<Typed> for Typed {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for Typed {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 }
@@ -234,7 +201,7 @@ impl std::hash::Hash for Normalized {
 impl Eq for Typed {}
 impl PartialEq for Typed {
     fn eq(&self, other: &Self) -> bool {
-        self.to_value() == other.to_value()
+        self.0 == other.0
     }
 }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fd0197d..a379a4b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,13 +5,11 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::context::NormalizationContext;
-use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
+use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr};
 
-pub(crate) type InputSubExpr = ResolvedSubExpr;
 pub(crate) type OutputSubExpr = NormalizedSubExpr;
 
 // Ad-hoc macro to help construct closures
@@ -22,67 +20,76 @@ macro_rules! make_closure {
             Label::from(stringify!($var)).into(),
             $n
         );
-        Value::Var(var).into_thunk()
+        ValueF::Var(var).into_value_untyped()
     }};
+    // Warning: assumes that $ty, as a dhall value, has type `Type`
     (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        Value::Lam(
+        ValueF::Lam(
             Label::from(stringify!($var)).into(),
-            TypedThunk::from_thunk_untyped(make_closure!($($ty)*)),
+            make_closure!($($ty)*),
             make_closure!($($rest)*),
-        ).into_thunk()
+        ).into_value_untyped()
+    };
+    (Natural) => {
+        ValueF::from_builtin(Builtin::Natural)
+            .into_value_simple_type()
     };
-    (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() };
     (List $($rest:tt)*) => {
-        Value::from_builtin(Builtin::List)
-            .app_thunk(make_closure!($($rest)*))
-            .into_thunk()
+        ValueF::from_builtin(Builtin::List)
+            .app_value(make_closure!($($rest)*))
+            .into_value_simple_type()
     };
-    (Some $($rest:tt)*) => {
-        Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+    (Some($($rest:tt)*)) => {
+        ValueF::NEOptionalLit(make_closure!($($rest)*))
+            .into_value_untyped()
     };
     (1 + $($rest:tt)*) => {
-        Value::PartialExpr(ExprF::BinOp(
+        ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
             make_closure!($($rest)*),
-            Thunk::from_value(Value::NaturalLit(1)),
-        )).into_thunk()
+            Value::from_valuef_and_type(
+                ValueF::NaturalLit(1),
+                make_closure!(Natural)
+            ),
+        )).into_value_with_type(
+            make_closure!(Natural)
+        )
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {
-        Value::PartialExpr(ExprF::BinOp(
+        ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+            ValueF::NEListLit(vec![make_closure!($($head)*)])
+                .into_value_untyped(),
             make_closure!($($tail)*),
-        )).into_thunk()
+        )).into_value_untyped()
     };
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
     use dhall_syntax::Builtin::*;
-    use Value::*;
+    use ValueF::*;
 
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t, r..]) => {
-            Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone()))))
-        }
-        (NaturalIsZero, [n, r..]) => match &*n.as_value() {
+        (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
+        (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
             _ => Err(()),
         },
-        (NaturalEven, [n, r..]) => match &*n.as_value() {
+        (NaturalEven, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
             _ => Err(()),
         },
-        (NaturalOdd, [n, r..]) => match &*n.as_value() {
+        (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
             _ => Err(()),
         },
-        (NaturalToInteger, [n, r..]) => match &*n.as_value() {
+        (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
             _ => Err(()),
         },
-        (NaturalShow, [n, r..]) => match &*n.as_value() {
+        (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
@@ -90,7 +97,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             _ => Err(()),
         },
         (NaturalSubtract, [a, b, r..]) => {
-            match (&*a.as_value(), &*b.as_value()) {
+            match (&*a.as_whnf(), &*b.as_whnf()) {
                 (NaturalLit(a), NaturalLit(b)) => {
                     Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
                 }
@@ -100,7 +107,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                 _ => Err(()),
             }
         }
-        (IntegerShow, [n, r..]) => match &*n.as_value() {
+        (IntegerShow, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
@@ -111,18 +118,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Err(()),
         },
-        (IntegerToDouble, [n, r..]) => match &*n.as_value() {
+        (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
             _ => Err(()),
         },
-        (DoubleShow, [n, r..]) => match &*n.as_value() {
+        (DoubleShow, [n, r..]) => match &*n.as_whnf() {
             DoubleLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
             )),
             _ => Err(()),
         },
-        (TextShow, [v, r..]) => match &*v.as_value() {
+        (TextShow, [v, r..]) => match &*v.as_whnf() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -156,41 +163,44 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             }
             _ => Err(()),
         },
-        (ListLength, [_, l, r..]) => match &*l.as_value() {
+        (ListLength, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(_) => Ok((r, NaturalLit(0))),
             NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
             _ => Err(()),
         },
-        (ListHead, [_, l, r..]) => match &*l.as_value() {
+        (ListHead, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListLast, [_, l, r..]) => match &*l.as_value() {
+        (ListLast, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListReverse, [_, l, r..]) => match &*l.as_value() {
+        (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
             }
             _ => Err(()),
         },
-        (ListIndexed, [_, l, r..]) => match &*l.as_value() {
+        (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(t) => {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypedThunk::from_value(Value::from_builtin(Natural)),
+                    Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
                 );
                 kts.insert("value".into(), t.clone());
-                Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts)))))
+                Ok((
+                    r,
+                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
+                ))
             }
             NEListLit(xs) => {
                 let xs = xs
@@ -199,105 +209,131 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = HashMap::new();
-                        kvs.insert("index".into(), Thunk::from_value(i));
+                        kvs.insert(
+                            "index".into(),
+                            Value::from_valuef_untyped(i),
+                        );
                         kvs.insert("value".into(), e.clone());
-                        Thunk::from_value(RecordLit(kvs))
+                        Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
                 Ok((r, NEListLit(xs)))
             }
             _ => Err(()),
         },
-        (ListBuild, [t, f, r..]) => match &*f.as_value() {
+        (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
-            Value::AppliedBuiltin(ListFold, args) => {
+            ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_value()))
+                    Ok((r, args[1].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
-            _ => Ok((
-                r,
-                f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
-                    .app_thunk({
-                        // Move `t` under new `x` variable
-                        let t1 = t.under_binder(Label::from("x"));
-                        make_closure!(
-                            λ(x : #t) ->
-                            λ(xs : List #t1) ->
-                            [ var(x, 1) ] # var(xs, 0)
-                        )
-                    })
-                    .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
-            )),
+            _ => {
+                let list_t = ValueF::from_builtin(List)
+                    .app_value(t.clone())
+                    .into_value_simple_type();
+                Ok((
+                    r,
+                    f.app_value(list_t.clone())
+                        .app_value({
+                            // Move `t` under new `x` variable
+                            let t1 = t.under_binder(Label::from("x"));
+                            make_closure!(
+                                λ(x : #t) ->
+                                λ(xs : List #t1) ->
+                                [ var(x, 1) ] # var(xs, 0)
+                            )
+                        })
+                        .app_value(
+                            EmptyListLit(t.clone())
+                                .into_value_with_type(list_t),
+                        ),
+                ))
+            }
         },
-        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
-            EmptyListLit(_) => Ok((r, nil.to_value())),
+        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ok((r, nil.to_whnf())),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().rev() {
                     v = cons
                         .clone()
-                        .app_thunk(x.clone())
-                        .app_thunk(v)
-                        .into_thunk();
+                        .app_value(x.clone())
+                        .app_value(v)
+                        .into_value_untyped();
                 }
-                Ok((r, v.to_value()))
+                Ok((r, v.to_whnf()))
             }
             _ => Err(()),
         },
-        (OptionalBuild, [t, f, r..]) => match &*f.as_value() {
+        (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
-            Value::AppliedBuiltin(OptionalFold, args) => {
+            ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_value()))
+                    Ok((r, args[1].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
-            _ => Ok((
-                r,
-                f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
-                    .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
-                    .app_val(EmptyOptionalLit(TypedThunk::from_thunk(
-                        t.clone(),
-                    ))),
-            )),
+            _ => {
+                let optional_t = ValueF::from_builtin(Optional)
+                    .app_value(t.clone())
+                    .into_value_simple_type();
+                Ok((
+                    r,
+                    f.app_value(optional_t.clone())
+                        .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
+                        .app_value(
+                            EmptyOptionalLit(t.clone())
+                                .into_value_with_type(optional_t),
+                        ),
+                ))
+            }
         },
-        (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
-            EmptyOptionalLit(_) => Ok((r, nothing.to_value())),
-            NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+        (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
+            EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
+            NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
             _ => Err(()),
         },
-        (NaturalBuild, [f, r..]) => match &*f.as_value() {
+        (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
-            Value::AppliedBuiltin(NaturalFold, args) => {
+            ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].to_value()))
+                    Ok((r, args[0].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
-            _ => Ok((
-                r,
-                f.app_val(Value::from_builtin(Natural))
-                    .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
-                    .app_val(NaturalLit(0)),
-            )),
+            _ => {
+                let nat_type =
+                    ValueF::from_builtin(Natural).into_value_simple_type();
+                Ok((
+                    r,
+                    f.app_value(nat_type.clone())
+                        .app_value(
+                            make_closure!(λ(x : Natural) -> 1 + var(x, 0)),
+                        )
+                        .app_value(
+                            NaturalLit(0).into_value_with_type(nat_type),
+                        ),
+                ))
+            }
         },
-        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() {
-            NaturalLit(0) => Ok((r, zero.to_value())),
+        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
+            NaturalLit(0) => Ok((r, zero.to_whnf())),
             NaturalLit(n) => {
-                let fold = Value::from_builtin(NaturalFold)
+                let fold = ValueF::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
-                    .app_thunk(t.clone())
-                    .app_thunk(succ.clone())
-                    .app_thunk(zero.clone());
-                Ok((r, succ.app_val(fold)))
+                    .app_value(t.clone())
+                    .app_value(succ.clone())
+                    .app_value(zero.clone())
+                    .into_value_with_type(t.clone());
+                Ok((r, succ.app_value(fold)))
             }
             _ => Err(()),
         },
@@ -307,7 +343,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
         Ok((unconsumed_args, mut v)) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
-                v = v.app_thunk(x);
+                v = v.app_value(x);
             }
             v
         }
@@ -315,22 +351,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
     }
 }
 
-pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value {
-    let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
+    let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
 
-    let f_borrow = f.as_value();
+    let f_borrow = f.as_whnf();
     match &*f_borrow {
-        Value::Lam(x, _, e) => {
-            let val = Typed::from_thunk_untyped(a);
-            e.subst_shift(&x.into(), &val).to_value()
-        }
-        Value::AppliedBuiltin(b, args) => {
+        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+        ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args)
         }
-        Value::UnionConstructor(l, kts) => {
-            Value::UnionLit(l.clone(), a, kts.clone())
+        ValueF::UnionConstructor(l, kts) => {
+            ValueF::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
@@ -340,23 +373,23 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value {
 }
 
 pub(crate) fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
-) -> Vec<InterpolatedTextContents<Thunk>> {
+    elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
     use std::mem::replace;
     use InterpolatedTextContents::{Expr, Text};
 
     fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
         crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Thunk>>,
+        ret: &mut Vec<InterpolatedTextContents<Value>>,
     ) {
         for contents in elts {
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => {
-                    let e_borrow = e.as_value();
+                    let e_borrow = e.as_whnf();
                     match &*e_borrow {
-                        Value::TextLit(elts2) => {
+                        ValueF::TextLit(elts2) => {
                             inner(elts2.iter().cloned(), crnt_str, ret)
                         }
                         _ => {
@@ -381,32 +414,6 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-/// Reduces the imput expression to a Value. Evaluates as little as possible.
-pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
-    match expr.as_ref() {
-        ExprF::Embed(e) => return e.to_value(),
-        ExprF::Var(v) => return ctx.lookup(v),
-        _ => {}
-    }
-
-    // Thunk subexpressions
-    let expr: ExprF<Thunk, Normalized> =
-        expr.as_ref().map_ref_with_special_handling_of_binders(
-            |e| Thunk::new(ctx.clone(), e.clone()),
-            |x, e| Thunk::new(ctx.skip(x), e.clone()),
-        );
-
-    normalize_one_layer(expr)
-}
-
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    Value(Value),
-    Thunk(Thunk),
-    ThunkRef(&'a Thunk),
-    Expr(ExprF<Thunk, Normalized>),
-}
-
 /// Performs an intersection of two HashMaps.
 ///
 /// # Arguments
@@ -441,60 +448,6 @@ where
     kvs
 }
 
-/// Performs an outer join of two HashMaps.
-///
-/// # Arguments
-///
-/// * `ft` - Will convert the values of the first map
-///          into the target value.
-///
-/// * `fu` - Will convert the values of the second map
-///          into the target value.
-///
-/// * `fktu` - Will convert the key and values from both maps
-///           into the target type.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `fktu` function. Otherwise, the
-/// final value will be calculated by either the `ft` or `fu` value
-/// depending on which map the key is present in.
-///
-/// The final map will contain all keys from the two input maps with
-/// also values computed as per above.
-pub(crate) fn outer_join<K, T, U, V>(
-    mut ft: impl FnMut(&T) -> V,
-    mut fu: impl FnMut(&U) -> V,
-    mut fktu: impl FnMut(&K, &T, &U) -> V,
-    map1: &HashMap<K, T>,
-    map2: &HashMap<K, U>,
-) -> HashMap<K, V>
-where
-    K: std::hash::Hash + Eq + Clone,
-{
-    let mut kvs = HashMap::new();
-
-    for (k1, t) in map1 {
-        let v = if let Some(u) = map2.get(k1) {
-            // The key exists in both maps
-            // so use all values for computation
-            fktu(k1, t, u)
-        } else {
-            // Key only exists in map1
-            ft(t)
-        };
-        kvs.insert(k1.clone(), v);
-    }
-
-    for (k1, u) in map2 {
-        // Insert if key was missing in map1
-        kvs.entry(k1.clone()).or_insert(fu(u));
-    }
-
-    kvs
-}
-
 pub(crate) fn merge_maps<K, V>(
     map1: &HashMap<K, V>,
     map2: &HashMap<K, V>,
@@ -520,82 +473,90 @@ where
     kvs
 }
 
-fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+    ValueF(ValueF),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprF<Value, Normalized>),
+}
+
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use Value::{
+    use ValueF::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
     };
-    let x_borrow = x.as_value();
-    let y_borrow = y.as_value();
+    let x_borrow = x.as_whnf();
+    let y_borrow = y.as_whnf();
     Some(match (o, &*x_borrow, &*y_borrow) {
-        (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
-        (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
-        (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)),
-        (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
-        (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)),
-        (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
-        (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
-        (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
-        (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
-        (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)),
-        (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
-        (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)),
-
-        (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
+        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
+        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
+        (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
+        (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
+        (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
+        (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
+        (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
+        (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
+        (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+        (BoolOr, _, _) if x == y => Ret::ValueRef(x),
+        (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
+        (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
+        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)),
+        (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
+        (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
+        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
+        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
+        (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
+
+        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
         (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::Value(NaturalLit(x + y))
+            Ret::ValueF(NaturalLit(x + y))
         }
-        (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)),
-        (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
-        (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
+        (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
+        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+        (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
         (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::Value(NaturalLit(x * y))
+            Ret::ValueF(NaturalLit(x * y))
         }
 
-        (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => {
-            Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
-        }
+        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
+            xs.iter().chain(ys.iter()).cloned().collect(),
+        )),
 
-        (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
-        (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
-        (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit(
+        (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y),
+        (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x),
+        (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
             squash_textlit(x.iter().chain(y.iter()).cloned()),
         )),
         (TextAppend, TextLit(x), _) => {
             use std::iter::once;
             let y = InterpolatedTextContents::Expr(y.clone());
-            Ret::Value(TextLit(squash_textlit(
+            Ret::ValueF(TextLit(squash_textlit(
                 x.iter().cloned().chain(once(y)),
             )))
         }
         (TextAppend, _, TextLit(y)) => {
             use std::iter::once;
             let x = InterpolatedTextContents::Expr(x.clone());
-            Ret::Value(TextLit(squash_textlit(
+            Ret::ValueF(TextLit(squash_textlit(
                 once(x).chain(y.iter().cloned()),
             )))
         }
 
         (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let mut kvs = kvs2.clone();
@@ -603,54 +564,53 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            Ret::Value(RecordLit(kvs))
+            Ret::ValueF(RecordLit(kvs))
         }
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Thunk::from_partial_expr(ExprF::BinOp(
+                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
                     RecursiveRecordMerge,
                     v1.clone(),
                     v2.clone(),
-                ))
+                )))
             });
-            Ret::Value(RecordLit(kvs))
+            Ret::ValueF(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            Ret::ThunkRef(x)
+            Ret::ValueRef(x)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            Ret::ThunkRef(y)
+            Ret::ValueRef(y)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
+                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
                     RecursiveRecordTypeMerge,
-                    v1.to_thunk(),
-                    v2.to_thunk(),
+                    v1.clone(),
+                    v2.clone(),
                 )))
             });
-            Ret::Value(RecordType(kvs))
+            Ret::ValueF(RecordType(kvs))
         }
 
-        (Equivalence, _, _) => Ret::Value(Value::Equivalence(
-            TypedThunk::from_thunk(x.clone()),
-            TypedThunk::from_thunk(y.clone()),
-        )),
+        (Equivalence, _, _) => {
+            Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+        }
 
         _ => return None,
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
-    use Value::{
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+    use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
         TextLit, UnionConstructor, UnionLit, UnionType,
@@ -662,36 +622,25 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         ),
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => Ret::Thunk(x),
+        ExprF::Annot(x, _) => Ret::Value(x),
         ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::Lam(x, t, e) => {
-            Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e))
-        }
-        ExprF::Pi(x, t, e) => Ret::Value(Pi(
-            x.into(),
-            TypedThunk::from_thunk(t),
-            TypedThunk::from_thunk(e),
-        )),
-        ExprF::Let(x, _, v, b) => {
-            let v = Typed::from_thunk_untyped(v);
-            Ret::Thunk(b.subst_shift(&x.into(), &v))
-        }
-        ExprF::App(v, a) => Ret::Value(v.app_thunk(a)),
-        ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)),
-        ExprF::Const(c) => Ret::Value(Value::Const(c)),
-        ExprF::BoolLit(b) => Ret::Value(BoolLit(b)),
-        ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
-        ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
-        ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
-        ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
+        ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
+        ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
+        ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
+        ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
+        ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
+        ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
+        ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
+        ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
+        ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
+        ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
+        ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
         ExprF::EmptyListLit(ref t) => {
             // Check if the type is of the form `List x`
-            let t_borrow = t.as_value();
+            let t_borrow = t.as_whnf();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::Value(EmptyListLit(TypedThunk::from_thunk(
-                        args[0].clone(),
-                    )))
+                    Ret::ValueF(EmptyListLit(args[0].clone()))
                 }
                 _ => {
                     drop(t_borrow);
@@ -700,43 +649,39 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             }
         }
         ExprF::NEListLit(elts) => {
-            Ret::Value(NEListLit(elts.into_iter().collect()))
+            Ret::ValueF(NEListLit(elts.into_iter().collect()))
         }
         ExprF::RecordLit(kvs) => {
-            Ret::Value(RecordLit(kvs.into_iter().collect()))
+            Ret::ValueF(RecordLit(kvs.into_iter().collect()))
+        }
+        ExprF::RecordType(kts) => {
+            Ret::ValueF(RecordType(kts.into_iter().collect()))
+        }
+        ExprF::UnionType(kts) => {
+            Ret::ValueF(UnionType(kts.into_iter().collect()))
         }
-        ExprF::RecordType(kts) => Ret::Value(RecordType(
-            kts.into_iter()
-                .map(|(k, t)| (k, TypedThunk::from_thunk(t)))
-                .collect(),
-        )),
-        ExprF::UnionType(kts) => Ret::Value(UnionType(
-            kts.into_iter()
-                .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t))))
-                .collect(),
-        )),
         ExprF::TextLit(elts) => {
             use InterpolatedTextContents::Expr;
             let elts: Vec<_> = squash_textlit(elts.into_iter());
             // Simplify bare interpolation
             if let [Expr(th)] = elts.as_slice() {
-                Ret::Thunk(th.clone())
+                Ret::Value(th.clone())
             } else {
-                Ret::Value(TextLit(elts))
+                Ret::ValueF(TextLit(elts))
             }
         }
         ExprF::BoolIf(ref b, ref e1, ref e2) => {
-            let b_borrow = b.as_value();
+            let b_borrow = b.as_whnf();
             match &*b_borrow {
-                BoolLit(true) => Ret::ThunkRef(e1),
-                BoolLit(false) => Ret::ThunkRef(e2),
+                BoolLit(true) => Ret::ValueRef(e1),
+                BoolLit(false) => Ret::ValueRef(e2),
                 _ => {
-                    let e1_borrow = e1.as_value();
-                    let e2_borrow = e2.as_value();
+                    let e1_borrow = e1.as_whnf();
+                    let e2_borrow = e2.as_whnf();
                     match (&*e1_borrow, &*e2_borrow) {
                         // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
-                        _ if e1 == e2 => Ret::ThunkRef(e1),
+                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+                        _ if e1 == e2 => Ret::ValueRef(e1),
                         _ => {
                             drop(b_borrow);
                             drop(e1_borrow);
@@ -753,12 +698,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         },
 
         ExprF::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::Value(RecordLit(HashMap::new()))
+            Ret::ValueF(RecordLit(HashMap::new()))
         }
         ExprF::Projection(ref v, ref ls) => {
-            let v_borrow = v.as_value();
+            let v_borrow = v.as_whnf();
             match &*v_borrow {
-                RecordLit(kvs) => Ret::Value(RecordLit(
+                RecordLit(kvs) => Ret::ValueF(RecordLit(
                     ls.iter()
                         .filter_map(|l| {
                             kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -772,17 +717,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
             }
         }
         ExprF::Field(ref v, ref l) => {
-            let v_borrow = v.as_value();
+            let v_borrow = v.as_whnf();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
-                    Some(r) => Ret::Thunk(r.clone()),
+                    Some(r) => Ret::Value(r.clone()),
                     None => {
                         drop(v_borrow);
                         Ret::Expr(expr)
                     }
                 },
                 UnionType(kts) => {
-                    Ret::Value(UnionConstructor(l.clone(), kts.clone()))
+                    Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
                 }
                 _ => {
                     drop(v_borrow);
@@ -792,11 +737,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
         }
 
         ExprF::Merge(ref handlers, ref variant, _) => {
-            let handlers_borrow = handlers.as_value();
-            let variant_borrow = variant.as_value();
+            let handlers_borrow = handlers.as_whnf();
+            let variant_borrow = variant.as_whnf();
             match (&*handlers_borrow, &*variant_borrow) {
                 (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
-                    Some(h) => Ret::Thunk(h.clone()),
+                    Some(h) => Ret::Value(h.clone()),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -804,7 +749,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::Value(h.app_thunk(v.clone())),
+                    Some(h) => Ret::ValueF(h.app_value(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -821,9 +766,22 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
     };
 
     match ret {
-        Ret::Value(v) => v,
-        Ret::Thunk(th) => th.to_value(),
-        Ret::ThunkRef(th) => th.to_value(),
-        Ret::Expr(expr) => Value::PartialExpr(expr),
+        Ret::ValueF(v) => v,
+        Ret::Value(th) => th.as_whnf().clone(),
+        Ret::ValueRef(th) => th.as_whnf().clone(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr),
+    }
+}
+
+/// Normalize a ValueF into WHNF
+pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+    match v {
+        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
+        ValueF::PartialExpr(e) => normalize_one_layer(e),
+        ValueF::TextLit(elts) => {
+            ValueF::TextLit(squash_textlit(elts.into_iter()))
+        }
+        // All other cases are already in WHNF
+        v => v,
     }
 }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 56fb5ed..c47eb78 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,33 +1,29 @@
+use std::cmp::max;
 use std::collections::HashMap;
 
 use dhall_syntax::{
     rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
 };
 
-use crate::core::context::{NormalizationContext, TypecheckContext};
-use crate::core::thunk::{Thunk, TypedThunk};
+use crate::core::context::TypecheckContext;
 use crate::core::value::Value;
+use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
-use crate::phase::{Normalized, Resolved, Type, Typed};
+use crate::phase::Normalized;
 
 fn tck_pi_type(
     ctx: &TypecheckContext,
     x: Label,
-    tx: Type,
-    te: Type,
-) -> Result<Typed, TypeError> {
+    tx: Value,
+    te: Value,
+) -> Result<Value, TypeError> {
     use crate::error::TypeMessage::*;
     let ctx2 = ctx.insert_type(&x, tx.clone());
 
     let ka = match tx.get_type()?.as_const() {
         Some(k) => k,
-        _ => {
-            return Err(TypeError::new(
-                ctx,
-                InvalidInputType(tx.to_normalized()),
-            ))
-        }
+        _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
     };
 
     let kb = match te.get_type()?.as_const() {
@@ -35,68 +31,58 @@ fn tck_pi_type(
         _ => {
             return Err(TypeError::new(
                 &ctx2,
-                InvalidOutputType(te.get_type()?.to_normalized()),
+                InvalidOutputType(te.get_type()?.into_owned()),
             ))
         }
     };
 
     let k = function_check(ka, kb);
 
-    Ok(Typed::from_thunk_and_type(
-        Value::Pi(
-            x.into(),
-            TypedThunk::from_type(tx),
-            TypedThunk::from_type(te),
-        )
-        .into_thunk(),
-        Type::from_const(k),
+    Ok(Value::from_valuef_and_type(
+        ValueF::Pi(x.into(), tx, te),
+        Value::from_const(k),
     ))
 }
 
 fn tck_record_type(
     ctx: &TypecheckContext,
-    kts: impl IntoIterator<Item = Result<(Label, Type), TypeError>>,
-) -> Result<Typed, TypeError> {
+    kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
+) -> Result<Value, TypeError> {
     use crate::error::TypeMessage::*;
     use std::collections::hash_map::Entry;
     let mut new_kts = HashMap::new();
-    // Check that all types are the same const
-    let mut k = None;
+    // An empty record type has type Type
+    let mut k = Const::Type;
     for e in kts {
         let (x, t) = e?;
-        match (k, t.get_type()?.as_const()) {
-            (None, Some(k2)) => k = Some(k2),
-            (Some(k1), Some(k2)) if k1 == k2 => {}
-            _ => {
-                return Err(TypeError::new(
-                    ctx,
-                    InvalidFieldType(x.clone(), t.clone()),
-                ))
-            }
+        // Construct the union of the contained `Const`s
+        match t.get_type()?.as_const() {
+            Some(k2) => k = max(k, k2),
+            None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
         }
-        let entry = new_kts.entry(x.clone());
+        // Check for duplicated entries
+        let entry = new_kts.entry(x);
         match &entry {
             Entry::Occupied(_) => {
                 return Err(TypeError::new(ctx, RecordTypeDuplicateField))
             }
-            Entry::Vacant(_) => {
-                entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
-            }
+            Entry::Vacant(_) => entry.or_insert_with(|| t),
         };
     }
-    // An empty record type has type Type
-    let k = k.unwrap_or(dhall_syntax::Const::Type);
 
-    Ok(Typed::from_thunk_and_type(
-        Value::RecordType(new_kts).into_thunk(),
-        Type::from_const(k),
+    Ok(Value::from_valuef_and_type(
+        ValueF::RecordType(new_kts),
+        Value::from_const(k),
     ))
 }
 
-fn tck_union_type(
+fn tck_union_type<Iter>(
     ctx: &TypecheckContext,
-    kts: impl IntoIterator<Item = Result<(Label, Option<Type>), TypeError>>,
-) -> Result<Typed, TypeError> {
+    kts: Iter,
+) -> Result<Value, TypeError>
+where
+    Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
+{
     use crate::error::TypeMessage::*;
     use std::collections::hash_map::Entry;
     let mut new_kts = HashMap::new();
@@ -111,46 +97,42 @@ fn tck_union_type(
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        InvalidFieldType(x.clone(), t.clone()),
+                        InvalidFieldType(x, t.clone()),
                     ))
                 }
             }
         }
-        let entry = new_kts.entry(x.clone());
+        let entry = new_kts.entry(x);
         match &entry {
             Entry::Occupied(_) => {
                 return Err(TypeError::new(ctx, UnionTypeDuplicateField))
             }
-            Entry::Vacant(_) => entry.or_insert_with(|| {
-                t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
-            }),
+            Entry::Vacant(_) => entry.or_insert_with(|| t),
         };
     }
 
     // An empty union type has type Type;
     // an union type with only unary variants also has type Type
-    let k = k.unwrap_or(dhall_syntax::Const::Type);
+    let k = k.unwrap_or(Const::Type);
 
-    Ok(Typed::from_thunk_and_type(
-        Value::UnionType(new_kts).into_thunk(),
-        Type::from_const(k),
+    Ok(Value::from_valuef_and_type(
+        ValueF::UnionType(new_kts),
+        Value::from_const(k),
     ))
 }
 
 fn function_check(a: Const, b: Const) -> Const {
-    use dhall_syntax::Const::Type;
-    use std::cmp::max;
-    if b == Type {
-        Type
+    if b == Const::Type {
+        Const::Type
     } else {
         max(a, b)
     }
 }
 
-pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> {
+pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> {
     match c {
-        Const::Type => Ok(Type::from_const(Const::Kind)),
-        Const::Kind => Ok(Type::from_const(Const::Sort)),
+        Const::Type => Ok(Value::from_const(Const::Kind)),
+        Const::Kind => Ok(Value::from_const(Const::Sort)),
         Const::Sort => {
             Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
         }
@@ -298,25 +280,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
     }
 }
 
-/// Takes an expression that is meant to contain a Type
-/// and turn it into a type, typechecking it along the way.
-pub(crate) fn mktype(
-    ctx: &TypecheckContext,
-    e: SubExpr<Normalized>,
-) -> Result<Type, TypeError> {
-    Ok(type_with(ctx, e)?.to_type())
-}
-
-pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> {
-    mktype(&TypecheckContext::new(), SubExpr::from_builtin(b))
-}
-
-/// Intermediary return type
-enum Ret {
-    /// Returns the contained value as is
-    RetWhole(Typed),
-    /// Use the contained Type as the type of the input expression
-    RetTypeOnly(Type),
+// TODO: this can't fail in practise
+pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> {
+    type_with(&TypecheckContext::new(), SubExpr::from_builtin(b))
 }
 
 /// Type-check an expression and return the expression alongside its type if type-checking
@@ -326,28 +292,23 @@ enum Ret {
 fn type_with(
     ctx: &TypecheckContext,
     e: SubExpr<Normalized>,
-) -> Result<Typed, TypeError> {
+) -> Result<Value, TypeError> {
     use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
 
-    use Ret::*;
     Ok(match e.as_ref() {
         Lam(x, t, b) => {
-            let tx = mktype(ctx, t.clone())?;
+            let tx = type_with(ctx, t.clone())?;
             let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
-            let v = Value::Lam(
-                x.clone().into(),
-                TypedThunk::from_type(tx.clone()),
-                b.to_thunk(),
-            );
+            let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone());
             let tb = b.get_type()?.into_owned();
-            let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type();
-            Typed::from_thunk_and_type(Thunk::from_value(v), t)
+            let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
+            Value::from_valuef_and_type(v, t)
         }
         Pi(x, ta, tb) => {
-            let ta = mktype(ctx, ta.clone())?;
+            let ta = type_with(ctx, ta.clone())?;
             let ctx2 = ctx.insert_type(x, ta.clone());
-            let tb = mktype(&ctx2, tb.clone())?;
+            let tb = type_with(&ctx2, tb.clone())?;
             return tck_pi_type(ctx, x.clone(), ta, tb);
         }
         Let(x, t, v, e) => {
@@ -360,9 +321,9 @@ fn type_with(
             let v = type_with(ctx, v)?;
             return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
         }
-        Embed(p) => p.clone().into_typed(),
+        Embed(p) => p.clone().into_typed().into_value(),
         Var(var) => match ctx.lookup(&var) {
-            Some(typed) => typed,
+            Some(typed) => typed.clone(),
             None => {
                 return Err(TypeError::new(
                     ctx,
@@ -370,24 +331,13 @@ fn type_with(
                 ))
             }
         },
-        _ => {
+        e => {
             // Typecheck recursively all subexpressions
-            let expr =
-                e.as_ref().traverse_ref_with_special_handling_of_binders(
-                    |e| type_with(ctx, e.clone()),
-                    |_, _| unreachable!(),
-                )?;
-            let ret = type_last_layer(ctx, &expr)?;
-            match ret {
-                RetTypeOnly(typ) => {
-                    let expr = expr.map_ref(|typed| typed.to_thunk());
-                    Typed::from_thunk_and_type(
-                        Thunk::from_partial_expr(expr),
-                        typ,
-                    )
-                }
-                RetWhole(tt) => tt,
-            }
+            let expr = e.traverse_ref_with_special_handling_of_binders(
+                |e| type_with(ctx, e.clone()),
+                |_, _| unreachable!(),
+            )?;
+            type_last_layer(ctx, expr)?
         }
     })
 }
@@ -396,17 +346,25 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: &ExprF<Typed, Normalized>,
-) -> Result<Ret, TypeError> {
+    e: ExprF<Value, Normalized>,
+) -> Result<Value, TypeError> {
     use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
     use dhall_syntax::Builtin::*;
     use dhall_syntax::Const::Type;
     use dhall_syntax::ExprF::*;
+    let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
+
+    /// Intermediary return type
+    enum Ret {
+        /// Returns the contained value as is
+        RetWhole(Value),
+        /// Returns the input expression `e` with the contained value as its type
+        RetTypeOnly(Value),
+    }
     use Ret::*;
-    let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg);
 
-    match e {
+    let ret = match &e {
         Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
@@ -415,456 +373,296 @@ fn type_last_layer(
         }
         App(f, a) => {
             let tf = f.get_type()?;
-            let (x, tx, tb) = match &tf.to_value() {
-                Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()),
-                _ => return Err(mkerr(NotAFunction(f.clone()))),
+            let tf_borrow = tf.as_whnf();
+            let (x, tx, tb) = match &*tf_borrow {
+                ValueF::Pi(x, tx, tb) => (x, tx, tb),
+                _ => return mkerr(NotAFunction(f.clone())),
             };
-            if a.get_type()?.as_ref() != &tx {
-                return Err(mkerr(TypeMismatch(
-                    f.clone(),
-                    tx.to_normalized(),
-                    a.clone(),
-                )));
+            if a.get_type()?.as_ref() != tx {
+                return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
             }
 
-            Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a)))
+            RetTypeOnly(tb.subst_shift(&x.into(), a))
         }
         Annot(x, t) => {
-            let t = t.to_type();
-            if &t != x.get_type()?.as_ref() {
-                return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized())));
+            if t != x.get_type()?.as_ref() {
+                return mkerr(AnnotMismatch(x.clone(), t.clone()));
             }
-            Ok(RetTypeOnly(x.get_type()?.into_owned()))
+            RetTypeOnly(x.get_type()?.into_owned())
         }
         Assert(t) => {
-            match t.to_value() {
-                Value::Equivalence(ref x, ref y) if x == y => {}
-                Value::Equivalence(x, y) => {
-                    return Err(mkerr(AssertMismatch(
-                        x.to_typed(),
-                        y.to_typed(),
-                    )))
+            match &*t.as_whnf() {
+                ValueF::Equivalence(x, y) if x == y => {}
+                ValueF::Equivalence(x, y) => {
+                    return mkerr(AssertMismatch(x.clone(), y.clone()))
                 }
-                _ => return Err(mkerr(AssertMustTakeEquivalence)),
+                _ => return mkerr(AssertMustTakeEquivalence),
             }
-            Ok(RetTypeOnly(t.to_type()))
+            RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
             if x.get_type()?.as_ref() != &builtin_to_type(Bool)? {
-                return Err(mkerr(InvalidPredicate(x.clone())));
+                return mkerr(InvalidPredicate(x.clone()));
             }
 
             if y.get_type()?.get_type()?.as_const() != Some(Type) {
-                return Err(mkerr(IfBranchMustBeTerm(true, y.clone())));
+                return mkerr(IfBranchMustBeTerm(true, y.clone()));
             }
 
             if z.get_type()?.get_type()?.as_const() != Some(Type) {
-                return Err(mkerr(IfBranchMustBeTerm(false, z.clone())));
+                return mkerr(IfBranchMustBeTerm(false, z.clone()));
             }
 
             if y.get_type()? != z.get_type()? {
-                return Err(mkerr(IfBranchMismatch(y.clone(), z.clone())));
+                return mkerr(IfBranchMismatch(y.clone(), z.clone()));
             }
 
-            Ok(RetTypeOnly(y.get_type()?.into_owned()))
+            RetTypeOnly(y.get_type()?.into_owned())
         }
         EmptyListLit(t) => {
-            let t = t.to_type();
-            match &t.to_value() {
-                Value::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+            match &*t.as_whnf() {
+                ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args)
                     if args.len() == 1 => {}
-                _ => {
-                    return Err(TypeError::new(
-                        ctx,
-                        InvalidListType(t.to_normalized()),
-                    ))
-                }
+                _ => return mkerr(InvalidListType(t.clone())),
             }
-            Ok(RetTypeOnly(t))
+            RetTypeOnly(t.clone())
         }
         NEListLit(xs) => {
             let mut iter = xs.iter().enumerate();
             let (_, x) = iter.next().unwrap();
             for (i, y) in iter {
                 if x.get_type()? != y.get_type()? {
-                    return Err(mkerr(InvalidListElement(
+                    return mkerr(InvalidListElement(
                         i,
-                        x.get_type()?.to_normalized(),
+                        x.get_type()?.into_owned(),
                         y.clone(),
-                    )));
+                    ));
                 }
             }
             let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
-                return Err(TypeError::new(
-                    ctx,
-                    InvalidListType(t.to_normalized()),
-                ));
+                return mkerr(InvalidListType(t.into_owned()));
             }
 
-            Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
-                    Value::from_builtin(dhall_syntax::Builtin::List)
-                        .app(t.to_value())
-                        .into_thunk(),
-                    Typed::from_const(Type),
-                )
-                .to_type(),
+            RetTypeOnly(Value::from_valuef_and_type(
+                ValueF::from_builtin(dhall_syntax::Builtin::List)
+                    .app_value(t.into_owned()),
+                Value::from_const(Type),
             ))
         }
         SomeLit(x) => {
             let t = x.get_type()?.into_owned();
             if t.get_type()?.as_const() != Some(Type) {
-                return Err(TypeError::new(
-                    ctx,
-                    InvalidOptionalType(t.to_normalized()),
-                ));
+                return mkerr(InvalidOptionalType(t));
             }
 
-            Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
-                    Value::from_builtin(dhall_syntax::Builtin::Optional)
-                        .app(t.to_value())
-                        .into_thunk(),
-                    Typed::from_const(Type).into_type(),
-                )
-                .to_type(),
+            RetTypeOnly(Value::from_valuef_and_type(
+                ValueF::from_builtin(dhall_syntax::Builtin::Optional)
+                    .app_value(t),
+                Value::from_const(Type),
             ))
         }
-        RecordType(kts) => Ok(RetWhole(tck_record_type(
+        RecordType(kts) => RetWhole(tck_record_type(
             ctx,
-            kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))),
-        )?)),
-        UnionType(kts) => Ok(RetWhole(tck_union_type(
+            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        )?),
+        UnionType(kts) => RetWhole(tck_union_type(
             ctx,
-            kts.iter()
-                .map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))),
-        )?)),
-        RecordLit(kvs) => Ok(RetTypeOnly(
-            tck_record_type(
-                ctx,
-                kvs.iter()
-                    .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
-            )?
-            .into_type(),
-        )),
+            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        )?),
+        RecordLit(kvs) => RetTypeOnly(tck_record_type(
+            ctx,
+            kvs.iter()
+                .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
+        )?),
         Field(r, x) => {
-            match &r.get_type()?.to_value() {
-                Value::RecordType(kts) => match kts.get(&x) {
+            match &*r.get_type()?.as_whnf() {
+                ValueF::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => {
-                        Ok(RetTypeOnly(tth.to_type()))
+                        RetTypeOnly(tth.clone())
                     },
-                    None => Err(mkerr(MissingRecordField(x.clone(),
-                                        r.clone()))),
+                    None => return mkerr(MissingRecordField(x.clone(),
+                                        r.clone())),
                 },
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
-                    let r = r.to_type();
-                    match &r.to_value() {
-                        Value::UnionType(kts) => match kts.get(&x) {
+                    match &*r.as_whnf() {
+                        ValueF::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(t)) => {
-                                // TODO: avoid capture
-                                Ok(RetTypeOnly(
+                                RetTypeOnly(
                                     tck_pi_type(
                                         ctx,
                                         "_".into(),
-                                        t.to_type(),
-                                        r.clone(),
-                                    )?.to_type()
-                                ))
+                                        t.clone(),
+                                        r.under_binder(Label::from("_")),
+                                    )?
+                                )
                             },
                             Some(None) => {
-                                Ok(RetTypeOnly(r.clone()))
+                                RetTypeOnly(r.clone())
                             },
                             None => {
-                                Err(mkerr(MissingUnionField(
+                                return mkerr(MissingUnionField(
                                     x.clone(),
-                                    r.to_normalized(),
-                                )))
+                                    r.clone(),
+                                ))
                             },
                         },
                         _ => {
-                            Err(mkerr(NotARecord(
+                            return mkerr(NotARecord(
                                 x.clone(),
-                                r.to_normalized()
-                            )))
+                                r.clone()
+                            ))
                         },
                     }
                 }
-                // _ => Err(mkerr(NotARecord(
+                // _ => mkerr(NotARecord(
                 //     x,
-                //     r.to_type()?.to_normalized(),
-                // ))),
+                //     r?,
+                // )),
             }
         }
-        Const(c) => Ok(RetWhole(Typed::from_const(*c))),
-        Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)),
-        BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
-        NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
-        IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
-        DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)),
+        Const(c) => RetWhole(Value::from_const(*c)),
+        Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?),
+        BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?),
+        NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?),
+        IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?),
+        DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?),
         TextLit(interpolated) => {
             let text_type = builtin_to_type(Text)?;
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
                     if x.get_type()?.as_ref() != &text_type {
-                        return Err(mkerr(InvalidTextInterpolation(x.clone())));
+                        return mkerr(InvalidTextInterpolation(x.clone()));
                     }
                 }
             }
-            Ok(RetTypeOnly(text_type))
+            RetTypeOnly(text_type)
         }
         BinOp(RightBiasedRecordMerge, l, r) => {
             use crate::phase::normalize::merge_maps;
 
             let l_type = l.get_type()?;
-            let l_kind = l_type.get_type()?;
             let r_type = r.get_type()?;
-            let r_kind = r_type.get_type()?;
-
-            // Check the equality of kinds.
-            // This is to disallow expression such as:
-            // "{ x = Text } // { y = 1 }"
-            if l_kind != r_kind {
-                return Err(mkerr(RecordMismatch(l.clone(), r.clone())));
-            }
 
             // Extract the LHS record type
-            let kts_x = match l_type.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(MustCombineRecord(l.clone()))),
+            let l_type_borrow = l_type.as_whnf();
+            let kts_x = match &*l_type_borrow {
+                ValueF::RecordType(kts) => kts,
+                _ => return mkerr(MustCombineRecord(l.clone())),
             };
 
             // Extract the RHS record type
-            let kts_y = match r_type.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(MustCombineRecord(r.clone()))),
+            let r_type_borrow = r_type.as_whnf();
+            let kts_y = match &*r_type_borrow {
+                ValueF::RecordType(kts) => kts,
+                _ => return mkerr(MustCombineRecord(r.clone())),
             };
 
             // Union the two records, prefering
             // the values found in the RHS.
-            let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone());
+            let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
 
             // Construct the final record type from the union
-            Ok(RetTypeOnly(
-                tck_record_type(
-                    ctx,
-                    kts.iter().map(|(x, v)| Ok((x.clone(), v.to_type()))),
-                )?
-                .into_type(),
-            ))
-        }
-        BinOp(RecursiveRecordMerge, l, r) => {
-            // A recursive function to dig down into
-            // records of records when merging.
-            fn combine_record_types(
-                ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypedThunk>,
-                kts_r: HashMap<Label, TypedThunk>,
-            ) -> Result<Typed, TypeError> {
-                use crate::phase::normalize::outer_join;
-
-                // If the Label exists for both records and Type for the values
-                // are records themselves, then we hit the recursive case.
-                // Otherwise we have a field collision.
-                let combine = |k: &Label,
-                               inner_l: &TypedThunk,
-                               inner_r: &TypedThunk|
-                 -> Result<Typed, TypeError> {
-                    match (inner_l.to_value(), inner_r.to_value()) {
-                        (
-                            Value::RecordType(inner_l_kvs),
-                            Value::RecordType(inner_r_kvs),
-                        ) => {
-                            combine_record_types(ctx, inner_l_kvs, inner_r_kvs)
-                        }
-                        (_, _) => {
-                            Err(TypeError::new(ctx, FieldCollision(k.clone())))
-                        }
-                    }
-                };
-
-                let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
-                    |l| Ok(l.to_type()),
-                    |r| Ok(r.to_type()),
-                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
-                        combine(k, l, r)
-                    },
-                    &kts_l,
-                    &kts_r,
-                );
-
-                Ok(tck_record_type(
-                    ctx,
-                    kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))),
-                )?
-                .into_type())
-            };
-
-            let l_type = l.get_type()?;
-            let l_kind = l_type.get_type()?;
-            let r_type = r.get_type()?;
-            let r_kind = r_type.get_type()?;
-
-            // Check the equality of kinds.
-            // This is to disallow expression such as:
-            // "{ x = Text } // { y = 1 }"
-            if l_kind != r_kind {
-                return Err(mkerr(RecordMismatch(l.clone(), r.clone())));
-            }
-
-            // Extract the LHS record type
-            let kts_x = match l_type.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(MustCombineRecord(l.clone()))),
-            };
-
-            // Extract the RHS record type
-            let kts_y = match r_type.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(MustCombineRecord(r.clone()))),
-            };
-
-            combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r))
+            RetTypeOnly(tck_record_type(
+                ctx,
+                kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+            )?)
         }
+        BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+            ctx,
+            ExprF::BinOp(
+                RecursiveRecordTypeMerge,
+                l.get_type()?.into_owned(),
+                r.get_type()?.into_owned(),
+            ),
+        )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
-            // A recursive function to dig down into
-            // records of records when merging.
-            fn combine_record_types(
-                ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypedThunk>,
-                kts_r: HashMap<Label, TypedThunk>,
-            ) -> Result<Typed, TypeError> {
-                use crate::phase::normalize::intersection_with_key;
-
-                // If the Label exists for both records and Type for the values
-                // are records themselves, then we hit the recursive case.
-                // Otherwise we have a field collision.
-                let combine = |k: &Label,
-                               kts_l_inner: &TypedThunk,
-                               kts_r_inner: &TypedThunk|
-                 -> Result<Typed, TypeError> {
-                    match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
-                        (
-                            Value::RecordType(kvs_l_inner),
-                            Value::RecordType(kvs_r_inner),
-                        ) => {
-                            combine_record_types(ctx, kvs_l_inner, kvs_r_inner)
-                        }
-                        (_, _) => {
-                            Err(TypeError::new(ctx, FieldCollision(k.clone())))
-                        }
-                    }
-                };
-
-                let kts = intersection_with_key(
-                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
-                        combine(k, l, r)
-                    },
-                    &kts_l,
-                    &kts_r,
-                );
-
-                Ok(tck_record_type(
-                    ctx,
-                    kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))),
-                )?
-                .into_type())
-            };
+            use crate::phase::normalize::intersection_with_key;
 
             // Extract the Const of the LHS
-            let k_l = match l.get_type()?.to_value() {
-                Value::Const(k) => k,
+            let k_l = match l.get_type()?.as_const() {
+                Some(k) => k,
                 _ => {
-                    return Err(mkerr(RecordTypeMergeRequiresRecordType(
-                        l.clone(),
-                    )))
+                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
                 }
             };
 
             // Extract the Const of the RHS
-            let k_r = match r.get_type()?.to_value() {
-                Value::Const(k) => k,
+            let k_r = match r.get_type()?.as_const() {
+                Some(k) => k,
                 _ => {
-                    return Err(mkerr(RecordTypeMergeRequiresRecordType(
-                        r.clone(),
-                    )))
+                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
                 }
             };
 
-            // Const values must match for the Records
-            let k = if k_l == k_r {
-                k_l
-            } else {
-                return Err(mkerr(RecordTypeMismatch(
-                    Typed::from_const(k_l),
-                    Typed::from_const(k_r),
-                    l.clone(),
-                    r.clone(),
-                )));
-            };
+            let k = max(k_l, k_r);
 
             // Extract the LHS record type
-            let kts_x = match l.to_value() {
-                Value::RecordType(kts) => kts,
+            let borrow_l = l.as_whnf();
+            let kts_x = match &*borrow_l {
+                ValueF::RecordType(kts) => kts,
                 _ => {
-                    return Err(mkerr(RecordTypeMergeRequiresRecordType(
-                        l.clone(),
-                    )))
+                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
                 }
             };
 
             // Extract the RHS record type
-            let kts_y = match r.to_value() {
-                Value::RecordType(kts) => kts,
+            let borrow_r = r.as_whnf();
+            let kts_y = match &*borrow_r {
+                ValueF::RecordType(kts) => kts,
                 _ => {
-                    return Err(mkerr(RecordTypeMergeRequiresRecordType(
-                        r.clone(),
-                    )))
+                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
                 }
             };
 
             // Ensure that the records combine without a type error
-            // and if not output the final Const value.
-            combine_record_types(ctx, kts_x, kts_y)
-                .and(Ok(RetTypeOnly(Typed::from_const(k))))
+            let kts = intersection_with_key(
+                // If the Label exists for both records, then we hit the recursive case.
+                |_: &Label, l: &Value, r: &Value| {
+                    type_last_layer(
+                        ctx,
+                        ExprF::BinOp(
+                            RecursiveRecordTypeMerge,
+                            l.clone(),
+                            r.clone(),
+                        ),
+                    )
+                },
+                kts_x,
+                kts_y,
+            );
+            tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+
+            RetTypeOnly(Value::from_const(k))
         }
         BinOp(o @ ListAppend, l, r) => {
-            match l.get_type()?.to_value() {
-                Value::AppliedBuiltin(List, _) => {}
-                _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
+            match &*l.get_type()?.as_whnf() {
+                ValueF::AppliedBuiltin(List, _) => {}
+                _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
             }
 
             if l.get_type()? != r.get_type()? {
-                return Err(mkerr(BinOpTypeMismatch(*o, r.clone())));
+                return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
-            Ok(RetTypeOnly(l.get_type()?.into_owned()))
+            RetTypeOnly(l.get_type()?.into_owned())
         }
         BinOp(Equivalence, l, r) => {
             if l.get_type()?.get_type()?.as_const() != Some(Type) {
-                return Err(mkerr(EquivalenceArgumentMustBeTerm(
-                    true,
-                    l.clone(),
-                )));
+                return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone()));
             }
             if r.get_type()?.get_type()?.as_const() != Some(Type) {
-                return Err(mkerr(EquivalenceArgumentMustBeTerm(
-                    false,
-                    r.clone(),
-                )));
+                return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone()));
             }
 
             if l.get_type()? != r.get_type()? {
-                return Err(mkerr(EquivalenceTypeMismatch(
-                    r.clone(),
-                    l.clone(),
-                )));
+                return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
             }
 
-            Ok(RetTypeOnly(Typed::from_const(Type).into_type()))
+            RetTypeOnly(Value::from_const(Type))
         }
         BinOp(o, l, r) => {
             let t = builtin_to_type(match o {
@@ -884,140 +682,136 @@ fn type_last_layer(
             })?;
 
             if l.get_type()?.as_ref() != &t {
-                return Err(mkerr(BinOpTypeMismatch(*o, l.clone())));
+                return mkerr(BinOpTypeMismatch(*o, l.clone()));
             }
 
             if r.get_type()?.as_ref() != &t {
-                return Err(mkerr(BinOpTypeMismatch(*o, r.clone())));
+                return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
-            Ok(RetTypeOnly(t))
+            RetTypeOnly(t)
         }
         Merge(record, union, type_annot) => {
-            let handlers = match record.get_type()?.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))),
+            let record_type = record.get_type()?;
+            let record_borrow = record_type.as_whnf();
+            let handlers = match &*record_borrow {
+                ValueF::RecordType(kts) => kts,
+                _ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
             };
 
-            let variants = match union.get_type()?.to_value() {
-                Value::UnionType(kts) => kts,
-                _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))),
+            let union_type = union.get_type()?;
+            let union_borrow = union_type.as_whnf();
+            let variants = match &*union_borrow {
+                ValueF::UnionType(kts) => kts,
+                _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
             };
 
             let mut inferred_type = None;
-            for (x, handler) in handlers.iter() {
-                let handler_return_type = match variants.get(x) {
-                    // Union alternative with type
-                    Some(Some(variant_type)) => {
-                        let variant_type = variant_type.to_type();
-                        let handler_type = handler.to_type();
-                        let (x, tx, tb) = match &handler_type.to_value() {
-                            Value::Pi(x, tx, tb) => {
-                                (x.clone(), tx.to_type(), tb.to_type())
+            for (x, handler_type) in handlers {
+                let handler_return_type =
+                    match variants.get(x) {
+                        // Union alternative with type
+                        Some(Some(variant_type)) => {
+                            let handler_type_borrow = handler_type.as_whnf();
+                            let (x, tx, tb) = match &*handler_type_borrow {
+                                ValueF::Pi(x, tx, tb) => (x, tx, tb),
+                                _ => {
+                                    return mkerr(NotAFunction(
+                                        handler_type.clone(),
+                                    ))
+                                }
+                            };
+
+                            if variant_type != tx {
+                                return mkerr(TypeMismatch(
+                                    handler_type.clone(),
+                                    tx.clone(),
+                                    variant_type.clone(),
+                                ));
                             }
-                            _ => return Err(mkerr(NotAFunction(handler_type))),
-                        };
-
-                        if &variant_type != &tx {
-                            return Err(mkerr(TypeMismatch(
-                                handler_type,
-                                tx.to_normalized(),
-                                variant_type,
-                            )));
-                        }
 
-                        // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
-                        match tb.over_binder(x) {
-                            Some(x) => x,
-                            None => {
-                                return Err(mkerr(
+                            // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+                            match tb.over_binder(x) {
+                                Some(x) => x,
+                                None => return mkerr(
                                     MergeHandlerReturnTypeMustNotBeDependent,
-                                ))
+                                ),
                             }
                         }
-                    }
-                    // Union alternative without type
-                    Some(None) => handler.to_type(),
-                    None => {
-                        return Err(mkerr(MergeHandlerMissingVariant(
-                            x.clone(),
-                        )))
-                    }
-                };
+                        // Union alternative without type
+                        Some(None) => handler_type.clone(),
+                        None => {
+                            return mkerr(MergeHandlerMissingVariant(x.clone()))
+                        }
+                    };
                 match &inferred_type {
                     None => inferred_type = Some(handler_return_type),
                     Some(t) => {
                         if t != &handler_return_type {
-                            return Err(mkerr(MergeHandlerTypeMismatch));
+                            return mkerr(MergeHandlerTypeMismatch);
                         }
                     }
                 }
             }
             for x in variants.keys() {
                 if !handlers.contains_key(x) {
-                    return Err(mkerr(MergeVariantMissingHandler(x.clone())));
+                    return mkerr(MergeVariantMissingHandler(x.clone()));
                 }
             }
 
             match (inferred_type, type_annot) {
                 (Some(ref t1), Some(t2)) => {
-                    let t2 = t2.to_type();
-                    if t1 != &t2 {
-                        return Err(mkerr(MergeAnnotMismatch));
+                    if t1 != t2 {
+                        return mkerr(MergeAnnotMismatch);
                     }
-                    Ok(RetTypeOnly(t2))
+                    RetTypeOnly(t2.clone())
                 }
-                (Some(t), None) => Ok(RetTypeOnly(t)),
-                (None, Some(t)) => Ok(RetTypeOnly(t.to_type())),
-                (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)),
+                (Some(t), None) => RetTypeOnly(t),
+                (None, Some(t)) => RetTypeOnly(t.clone()),
+                (None, None) => return mkerr(MergeEmptyNeedsAnnotation),
             }
         }
         Projection(record, labels) => {
-            let trecord = record.get_type()?;
-            let kts = match trecord.to_value() {
-                Value::RecordType(kts) => kts,
-                _ => return Err(mkerr(ProjectionMustBeRecord)),
+            let record_type = record.get_type()?;
+            let record_borrow = record_type.as_whnf();
+            let kts = match &*record_borrow {
+                ValueF::RecordType(kts) => kts,
+                _ => return mkerr(ProjectionMustBeRecord),
             };
 
             let mut new_kts = HashMap::new();
             for l in labels {
                 match kts.get(l) {
-                    None => return Err(mkerr(ProjectionMissingEntry)),
+                    None => return mkerr(ProjectionMissingEntry),
                     Some(t) => new_kts.insert(l.clone(), t.clone()),
                 };
             }
 
-            Ok(RetTypeOnly(
-                Typed::from_thunk_and_type(
-                    Value::RecordType(new_kts).into_thunk(),
-                    trecord.get_type()?.into_owned(),
-                )
-                .to_type(),
+            RetTypeOnly(Value::from_valuef_and_type(
+                ValueF::RecordType(new_kts),
+                record_type.get_type()?.into_owned(),
             ))
         }
-    }
+    };
+
+    Ok(match ret {
+        RetTypeOnly(typ) => {
+            Value::from_valuef_and_type(ValueF::PartialExpr(e), typ)
+        }
+        RetWhole(v) => v,
+    })
 }
 
-/// `typeOf` is the same as `type_with` with an empty context, meaning that the
+/// `type_of` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-fn type_of(e: SubExpr<Normalized>) -> Result<Typed, TypeError> {
-    let ctx = TypecheckContext::new();
-    let e = type_with(&ctx, e)?;
-    // Ensure `e` has a type (i.e. `e` is not `Sort`)
-    e.get_type()?;
-    Ok(e)
+pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> {
+    type_with(&TypecheckContext::new(), e)
 }
 
-pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
-    type_of(e.0)
-}
-
-pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
-    let expr: SubExpr<_> = e.0;
-    let ty: SubExpr<_> = ty.to_expr();
-    type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
-}
-pub(crate) fn skip_typecheck(e: Resolved) -> Typed {
-    Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0))
+pub(crate) fn typecheck_with(
+    expr: SubExpr<Normalized>,
+    ty: SubExpr<Normalized>,
+) -> Result<Value, TypeError> {
+    typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
 }