Merge pull request #105 from Nadrieril/keep-type-info

Store type information everywhere in `Value`

7 files changed, 506 insertions, 456 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5367c86..21ac288 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,19 +1,18 @@
-use std::borrow::Cow;
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
-use dhall_syntax::Const;
+use dhall_syntax::{Builtin, Const};
 
 use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
-use crate::phase::typecheck::const_to_value;
+use crate::phase::normalize::{apply_any, normalize_whnf};
+use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
-enum Form {
+pub(crate) enum Form {
     /// No constraints; expression may not be normalized at all.
     Unevaled,
     /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
@@ -28,13 +27,14 @@ enum Form {
 }
 use Form::{Unevaled, NF, WHNF};
 
-#[derive(Debug)]
 /// Partially normalized value.
 /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 /// Invariant: if `form` is `NF`, `value` must be fully normalized
+#[derive(Debug)]
 struct ValueInternal {
     form: Form,
     value: ValueF,
+    /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
 }
 
@@ -42,7 +42,7 @@ struct ValueInternal {
 /// sharing computation automatically. Uses a RefCell to share computation.
 /// Can optionally store a type from typechecking to preserve type information.
 #[derive(Clone)]
-pub struct Value(Rc<RefCell<ValueInternal>>);
+pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
 impl ValueInternal {
     fn into_value(self) -> Value {
@@ -53,15 +53,30 @@ impl ValueInternal {
     }
 
     fn normalize_whnf(&mut self) {
-        take_mut::take(self, |vint| match &vint.form {
-            Unevaled => ValueInternal {
-                form: WHNF,
-                value: normalize_whnf(vint.value),
-                ty: vint.ty,
+        take_mut::take_or_recover(
+            self,
+            // Dummy value in case the other closure panics
+            || ValueInternal {
+                form: Unevaled,
+                value: ValueF::Const(Const::Type),
+                ty: None,
             },
-            // Already in WHNF
-            WHNF | NF => vint,
-        })
+            |vint| match (&vint.form, &vint.ty) {
+                (Unevaled, Some(ty)) => ValueInternal {
+                    form: WHNF,
+                    value: normalize_whnf(vint.value, &ty),
+                    ty: vint.ty,
+                },
+                // `value` is `Sort`
+                (Unevaled, None) => ValueInternal {
+                    form: NF,
+                    value: ValueF::Const(Const::Sort),
+                    ty: None,
+                },
+                // Already in WHNF
+                (WHNF, _) | (NF, _) => vint,
+            },
+        )
     }
     fn normalize_nf(&mut self) {
         match self.form {
@@ -81,39 +96,41 @@ impl ValueInternal {
     fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
+            None => {
+                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+            }
         }
     }
 }
 
 impl Value {
-    pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
+    fn new(value: ValueF, form: Form, ty: Value) -> Value {
         ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: None,
+            form,
+            value,
+            ty: Some(ty),
         }
         .into_value()
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+    pub(crate) fn const_sort() -> Value {
         ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: Some(t),
+            form: NF,
+            value: ValueF::Const(Const::Sort),
+            ty: None,
         }
         .into_value()
     }
-    pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
-        Value::from_valuef_and_type(v, Value::from_const(Const::Type))
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+        Value::new(v, Unevaled, t)
+    }
+    pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+        Value::new(v, WHNF, t)
     }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
     }
-    pub fn const_type() -> Self {
-        Value::from_const(Const::Type)
+    pub(crate) fn from_builtin(b: Builtin) -> Self {
+        builtin_to_value(b)
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
@@ -156,10 +173,14 @@ impl Value {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.as_whnf().normalize_to_expr_maybe_alpha(true)
     }
-    /// TODO: cloning a valuef can often be avoided
-    pub(crate) fn to_whnf(&self) -> ValueF {
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
         self.as_whnf().clone()
     }
+    /// Before discarding type information, check that it matches the expected return type.
+    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+        self.check_type(ty);
+        self.to_whnf_ignore_type()
+    }
     pub(crate) fn into_typed(self) -> Typed {
         Typed::from_value(self)
     }
@@ -205,16 +226,40 @@ impl Value {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         self.as_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app_value(&self, th: Value) -> ValueF {
-        apply_any(self.clone(), th)
+    pub(crate) fn app(&self, v: Value) -> Value {
+        let body_t = match &*self.get_type_not_sort().as_whnf() {
+            ValueF::Pi(x, t, e) => {
+                v.check_type(t);
+                e.subst_shift(&x.into(), &v)
+            }
+            _ => unreachable!("Internal type error"),
+        };
+        Value::from_valuef_and_type_whnf(
+            apply_any(self.clone(), v, &body_t),
+            body_t,
+        )
     }
 
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
-        Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
+    /// In debug mode, panic if the provided type doesn't match the value's type.
+    /// Otherwise does nothing.
+    pub(crate) fn check_type(&self, ty: &Value) {
+        debug_assert_eq!(
+            Some(ty),
+            self.get_type().ok().as_ref(),
+            "Internal type error"
+        );
+    }
+    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+        Ok(self.as_internal().get_type()?.clone())
+    }
+    /// When we know the value isn't `Sort`, this gets the type directly
+    pub(crate) fn get_type_not_sort(&self) -> Value {
+        self.get_type()
+            .expect("Internal type error: value is `Sort` but shouldn't be")
     }
 }
 
@@ -236,7 +281,17 @@ impl Shift for ValueInternal {
 
 impl Subst<Value> for Value {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        Value(self.0.subst_shift(var, val))
+        match &*self.as_valuef() {
+            // If the var matches, we can just reuse the provided value instead of copying it.
+            // We also check that the types match, if in debug mode.
+            ValueF::Var(v) if v == var => {
+                if let Ok(self_ty) = self.get_type() {
+                    val.check_type(&self_ty.subst_shift(var, val));
+                }
+                val.clone()
+            }
+            _ => Value(self.0.subst_shift(var, val)),
+        }
     }
 }
 
@@ -262,8 +317,17 @@ impl std::cmp::Eq for Value {}
 impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
-        fmt.debug_tuple(&format!("Value@{:?}", &vint.form))
-            .field(&vint.value)
-            .finish()
+        if let ValueF::Const(c) = &vint.value {
+            write!(fmt, "{:?}", c)
+        } else {
+            let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
+            x.field("value", &vint.value);
+            if let Some(ty) = vint.ty.as_ref() {
+                x.field("type", &ty);
+            } else {
+                x.field("type", &None::<()>);
+            }
+            x.finish()
+        }
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 0c3058d..9ea2467 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,8 +7,7 @@ use dhall_syntax::{
 
 use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::OutputSubExpr;
-use crate::phase::Normalized;
+use crate::phase::{Normalized, NormalizedSubExpr};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
 /// normalized on-demand.
@@ -16,11 +15,11 @@ use crate::phase::Normalized;
 /// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
 /// recursively normalize as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ValueF {
+pub(crate) enum ValueF {
     /// Closures
     Lam(AlphaLabel, Value, Value),
     Pi(AlphaLabel, Value, Value),
-    // Invariant: the evaluation must not be able to progress further.
+    // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
     Var(AlphaVar),
@@ -34,32 +33,26 @@ pub enum ValueF {
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(Value),
     NEListLit(Vec<Value>),
-    RecordLit(HashMap<Label, Value>),
     RecordType(HashMap<Label, Value>),
+    RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
     UnionConstructor(Label, HashMap<Label, Option<Value>>),
     UnionLit(Label, Value, HashMap<Label, Option<Value>>),
-    // Invariant: this must not contain interpolations that are themselves TextLits, and
+    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Value>>),
     Equivalence(Value, Value),
-    // Invariant: this must not contain a value captured by one of the variants above.
+    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Value, Normalized>),
 }
 
 impl ValueF {
-    pub(crate) fn into_value_untyped(self) -> Value {
-        Value::from_valuef_untyped(self)
-    }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_value_simple_type(self) -> Value {
-        Value::from_valuef_simple_type(self)
-    }
 
     /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
         self.normalize_to_expr_maybe_alpha(false)
     }
     /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -67,7 +60,7 @@ impl ValueF {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         match self {
             ValueF::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
@@ -257,22 +250,7 @@ impl ValueF {
         }
     }
 
-    /// Apply to a valuef
-    pub(crate) fn app(self, val: ValueF) -> ValueF {
-        self.app_valuef(val)
-    }
-
-    /// Apply to a valuef
-    pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
-        self.app_value(val.into_value_untyped())
-    }
-
-    /// Apply to a value
-    pub fn app_value(self, th: Value) -> ValueF {
-        Value::from_valuef_untyped(self).app_value(th)
-    }
-
-    pub fn from_builtin(b: Builtin) -> ValueF {
+    pub(crate) fn from_builtin(b: Builtin) -> ValueF {
         ValueF::AppliedBuiltin(b, vec![])
     }
 }
@@ -355,7 +333,7 @@ impl Subst<Value> for ValueF {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
             ),
-            ValueF::Var(v) if v == var => val.to_whnf(),
+            ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
             ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
             ValueF::Const(c) => ValueF::Const(*c),
             ValueF::BoolLit(b) => ValueF::BoolLit(*b),
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13a9d7e..2ddaf3d 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -54,7 +54,6 @@ pub(crate) enum TypeMessage {
     NotAFunction(Value),
     TypeMismatch(Value, Value, Value),
     AnnotMismatch(Value, Value),
-    Untyped,
     InvalidListElement(usize, Value, Value),
     InvalidListType(Value),
     InvalidOptionalType(Value),
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 1f7e5f0..ecf04e9 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,8 +1,7 @@
-use std::borrow::Cow;
 use std::fmt::Display;
 use std::path::Path;
 
-use dhall_syntax::{Const, SubExpr};
+use dhall_syntax::{Builtin, Const, SubExpr};
 
 use crate::core::value::Value;
 use crate::core::valuef::ValueF;
@@ -93,13 +92,13 @@ impl Typed {
     pub(crate) fn from_const(c: Const) -> Self {
         Typed(Value::from_const(c))
     }
-    pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
         Typed(Value::from_valuef_and_type(v, t.into_value()))
     }
     pub(crate) fn from_value(th: Value) -> Self {
         Typed(th)
     }
-    pub fn const_type() -> Self {
+    pub(crate) fn const_type() -> Self {
         Typed::from_const(Const::Type)
     }
 
@@ -109,7 +108,7 @@ impl Typed {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.0.to_expr_alpha()
     }
-    pub fn to_value(&self) -> Value {
+    pub(crate) fn to_value(&self) -> Value {
         self.0.clone()
     }
     pub(crate) fn into_value(self) -> Value {
@@ -121,8 +120,41 @@ impl Typed {
     }
 
     #[allow(dead_code)]
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> {
-        Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed()))
+    pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
+        Ok(self.0.get_type()?.into_typed())
+    }
+
+    pub fn make_builtin_type(b: Builtin) -> Self {
+        Typed::from_value(Value::from_builtin(b))
+    }
+    pub fn make_optional_type(t: Typed) -> Self {
+        Typed::from_value(
+            Value::from_builtin(Builtin::Optional).app(t.to_value()),
+        )
+    }
+    pub fn make_list_type(t: Typed) -> Self {
+        Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value()))
+    }
+    pub fn make_record_type(
+        kts: impl Iterator<Item = (String, Typed)>,
+    ) -> Self {
+        Typed::from_valuef_and_type(
+            ValueF::RecordType(
+                kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+            ),
+            Typed::const_type(),
+        )
+    }
+    pub fn make_union_type(
+        kts: impl Iterator<Item = (String, Option<Typed>)>,
+    ) -> Self {
+        Typed::from_valuef_and_type(
+            ValueF::UnionType(
+                kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+                    .collect(),
+            ),
+            Typed::const_type(),
+        )
     }
 }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a379a4b..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,5 +1,6 @@
 use std::collections::HashMap;
 
+use dhall_syntax::Const::Type;
 use dhall_syntax::{
     BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
     NaiveDouble,
@@ -7,42 +8,43 @@ use dhall_syntax::{
 
 use crate::core::value::Value;
 use crate::core::valuef::ValueF;
-use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
-
-pub(crate) type OutputSubExpr = NormalizedSubExpr;
+use crate::core::var::{AlphaLabel, Shift, Subst};
+use crate::phase::Normalized;
 
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
     (#$var:ident) => { $var.clone() };
-    (var($var:ident, $n:expr)) => {{
+    (var($var:ident, $n:expr, $($ty:tt)*)) => {{
         let var = crate::core::var::AlphaVar::from_var_and_alpha(
             Label::from(stringify!($var)).into(),
             $n
         );
-        ValueF::Var(var).into_value_untyped()
+        ValueF::Var(var)
+            .into_value_with_type(make_closure!($($ty)*))
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
-    (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ValueF::Lam(
-            Label::from(stringify!($var)).into(),
-            make_closure!($($ty)*),
-            make_closure!($($rest)*),
-        ).into_value_untyped()
-    };
+    (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+        let var: AlphaLabel = Label::from(stringify!($var)).into();
+        let ty = make_closure!($($ty)*);
+        let body = make_closure!($($body)*);
+        let body_ty = body.get_type_not_sort();
+        let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+            .into_value_with_type(Value::from_const(Type));
+        ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+    }};
     (Natural) => {
-        ValueF::from_builtin(Builtin::Natural)
-            .into_value_simple_type()
+        Value::from_builtin(Builtin::Natural)
     };
     (List $($rest:tt)*) => {
-        ValueF::from_builtin(Builtin::List)
-            .app_value(make_closure!($($rest)*))
-            .into_value_simple_type()
-    };
-    (Some($($rest:tt)*)) => {
-        ValueF::NEOptionalLit(make_closure!($($rest)*))
-            .into_value_untyped()
+        Value::from_builtin(Builtin::List)
+            .app(make_closure!($($rest)*))
     };
+    (Some($($rest:tt)*)) => {{
+        let v = make_closure!($($rest)*);
+        let v_type = v.get_type_not_sort();
+        let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
+        ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+    }};
     (1 + $($rest:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
@@ -55,81 +57,99 @@ macro_rules! make_closure {
             make_closure!(Natural)
         )
     };
-    ([ $($head:tt)* ] # $($tail:tt)*) => {
+    ([ $($head:tt)* ] # $($tail:tt)*) => {{
+        let head = make_closure!($($head)*);
+        let tail = make_closure!($($tail)*);
+        let list_type = tail.get_type_not_sort();
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![make_closure!($($head)*)])
-                .into_value_untyped(),
-            make_closure!($($tail)*),
-        )).into_value_untyped()
-    };
+            ValueF::NEListLit(vec![head])
+                .into_value_with_type(list_type.clone()),
+            tail,
+        )).into_value_with_type(list_type)
+    }};
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
+pub(crate) fn apply_builtin(
+    b: Builtin,
+    args: Vec<Value>,
+    ty: &Value,
+) -> ValueF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
-    // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
+    // Small helper enum
+    enum Ret<'a> {
+        ValueF(ValueF),
+        Value(Value),
+        // For applications that can return a function, it's important to keep the remaining
+        // arguments to apply them to the resulting function.
+        ValueWithRemainingArgs(&'a [Value], Value),
+        DoneAsIs,
+    }
+
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
-        (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
-            _ => Err(()),
+        (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+        (NaturalIsZero, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
-            _ => Err(()),
+        (NaturalEven, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
-            _ => Err(()),
+        (NaturalOdd, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
-            _ => Err(()),
+        (NaturalToInteger, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+            _ => Ret::DoneAsIs,
         },
-        (NaturalShow, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((
-                r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
-            )),
-            _ => Err(()),
+        (NaturalShow, [n]) => match &*n.as_whnf() {
+            NaturalLit(n) => {
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+                    n.to_string(),
+                )]))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (NaturalSubtract, [a, b, r..]) => {
-            match (&*a.as_whnf(), &*b.as_whnf()) {
-                (NaturalLit(a), NaturalLit(b)) => {
-                    Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
-                }
-                (NaturalLit(0), b) => Ok((r, b.clone())),
-                (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
-                _ if a == b => Ok((r, NaturalLit(0))),
-                _ => Err(()),
+        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+            (NaturalLit(a), NaturalLit(b)) => {
+                Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
             }
-        }
-        (IntegerShow, [n, r..]) => match &*n.as_whnf() {
+            (NaturalLit(0), _) => Ret::Value(b.clone()),
+            (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+            _ if a == b => Ret::ValueF(NaturalLit(0)),
+            _ => Ret::DoneAsIs,
+        },
+        (IntegerShow, [n]) => match &*n.as_whnf() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
                 } else {
                     format!("+{}", n)
                 };
-                Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)])))
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
-            IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
-            _ => Err(()),
+        (IntegerToDouble, [n]) => match &*n.as_whnf() {
+            IntegerLit(n) => {
+                Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (DoubleShow, [n, r..]) => match &*n.as_whnf() {
-            DoubleLit(n) => Ok((
-                r,
-                TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
-            )),
-            _ => Err(()),
+        (DoubleShow, [n]) => match &*n.as_whnf() {
+            DoubleLit(n) => {
+                Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+                    n.to_string(),
+                )]))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (TextShow, [v, r..]) => match &*v.as_whnf() {
+        (TextShow, [v]) => match &*v.as_whnf() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -138,10 +158,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         let txt: InterpolatedText<Normalized> =
                             std::iter::empty().collect();
                         let s = txt.to_string();
-                        Ok((
-                            r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)]),
-                        ))
+                        Ret::ValueF(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
                     // interpolations, there is a single Text item) in the literal.
@@ -153,221 +172,238 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                             ))
                             .collect();
                         let s = txt.to_string();
-                        Ok((
-                            r,
-                            TextLit(vec![InterpolatedTextContents::Text(s)]),
-                        ))
+                        Ret::ValueF(TextLit(vec![
+                            InterpolatedTextContents::Text(s),
+                        ]))
                     }
-                    _ => Err(()),
+                    _ => Ret::DoneAsIs,
                 }
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, NaturalLit(0))),
-            NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
-            _ => Err(()),
+        (ListLength, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+            NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+            _ => Ret::DoneAsIs,
         },
-        (ListHead, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
+        (ListHead, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => {
-                Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
+                Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (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(()),
+        (ListLast, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+            NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+                xs.iter().rev().next().unwrap().clone(),
+            )),
+            _ => Ret::DoneAsIs,
         },
-        (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
+        (ListReverse, [_, l]) => match &*l.as_whnf() {
+            EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
             NEListLit(xs) => {
-                Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
+                Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(t) => {
-                let mut kts = HashMap::new();
-                kts.insert(
-                    "index".into(),
-                    Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
-                );
-                kts.insert("value".into(), t.clone());
-                Ok((
-                    r,
-                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
-                ))
-            }
-            NEListLit(xs) => {
-                let xs = xs
-                    .iter()
-                    .enumerate()
-                    .map(|(i, e)| {
-                        let i = NaturalLit(i);
-                        let mut kvs = HashMap::new();
-                        kvs.insert(
-                            "index".into(),
-                            Value::from_valuef_untyped(i),
-                        );
-                        kvs.insert("value".into(), e.clone());
-                        Value::from_valuef_untyped(RecordLit(kvs))
-                    })
-                    .collect();
-                Ok((r, NEListLit(xs)))
+        (ListIndexed, [_, l]) => {
+            let l_whnf = l.as_whnf();
+            match &*l_whnf {
+                EmptyListLit(_) | NEListLit(_) => {
+                    // Extract the type of the list elements
+                    let t = match &*l_whnf {
+                        EmptyListLit(t) => t.clone(),
+                        NEListLit(xs) => xs[0].get_type_not_sort(),
+                        _ => unreachable!(),
+                    };
+
+                    // Construct the returned record type: { index: Natural, value: t }
+                    let mut kts = HashMap::new();
+                    kts.insert("index".into(), Value::from_builtin(Natural));
+                    kts.insert("value".into(), t.clone());
+                    let t = Value::from_valuef_and_type(
+                        RecordType(kts),
+                        Value::from_const(Type),
+                    );
+
+                    // Construct the new list, with added indices
+                    let list = match &*l_whnf {
+                        EmptyListLit(_) => EmptyListLit(t),
+                        NEListLit(xs) => NEListLit(
+                            xs.iter()
+                                .enumerate()
+                                .map(|(i, e)| {
+                                    let mut kvs = HashMap::new();
+                                    kvs.insert(
+                                        "index".into(),
+                                        Value::from_valuef_and_type(
+                                            NaturalLit(i),
+                                            Value::from_builtin(
+                                                Builtin::Natural,
+                                            ),
+                                        ),
+                                    );
+                                    kvs.insert("value".into(), e.clone());
+                                    Value::from_valuef_and_type(
+                                        RecordLit(kvs),
+                                        t.clone(),
+                                    )
+                                })
+                                .collect(),
+                        ),
+                        _ => unreachable!(),
+                    };
+                    Ret::ValueF(list)
+                }
+                _ => Ret::DoneAsIs,
             }
-            _ => Err(()),
-        },
-        (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
+        }
+        (ListBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_whnf()))
+                    Ret::Value(args[1].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
             _ => {
-                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 list_t = Value::from_builtin(List).app(t.clone());
+                Ret::Value(
+                    f.app(list_t.clone())
+                        .app({
+                            // Move `t` under new variables
                             let t1 = t.under_binder(Label::from("x"));
+                            let t2 = t1.under_binder(Label::from("xs"));
                             make_closure!(
                                 λ(x : #t) ->
                                 λ(xs : List #t1) ->
-                                [ var(x, 1) ] # var(xs, 0)
+                                [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
                             )
                         })
-                        .app_value(
+                        .app(
                             EmptyListLit(t.clone())
                                 .into_value_with_type(list_t),
                         ),
-                ))
+                )
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, nil.to_whnf())),
+            EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
             NEListLit(xs) => {
                 let mut v = nil.clone();
-                for x in xs.iter().rev() {
-                    v = cons
-                        .clone()
-                        .app_value(x.clone())
-                        .app_value(v)
-                        .into_value_untyped();
+                for x in xs.iter().cloned().rev() {
+                    v = cons.app(x).app(v);
                 }
-                Ok((r, v.to_whnf()))
+                Ret::ValueWithRemainingArgs(r, v)
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
+        (OptionalBuild, [t, f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_whnf()))
+                    Ret::Value(args[1].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
             _ => {
-                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(
+                let optional_t = Value::from_builtin(Optional).app(t.clone());
+                Ret::Value(
+                    f.app(optional_t.clone())
+                        .app({
+                            let t1 = t.under_binder(Label::from("x"));
+                            make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+                        })
+                        .app(
                             EmptyOptionalLit(t.clone())
                                 .into_value_with_type(optional_t),
                         ),
-                ))
+                )
             }
         },
         (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(()),
+            EmptyOptionalLit(_) => {
+                Ret::ValueWithRemainingArgs(r, nothing.clone())
+            }
+            NEOptionalLit(x) => {
+                Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+            }
+            _ => Ret::DoneAsIs,
         },
-        (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
+        (NaturalBuild, [f]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].to_whnf()))
+                    Ret::Value(args[0].clone())
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
                 }
             }
-            _ => {
-                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),
-                        ),
-                ))
-            }
+            _ => Ret::Value(
+                f.app(Value::from_builtin(Natural))
+                    .app(make_closure!(
+                        λ(x : Natural) -> 1 + var(x, 0, Natural)
+                    ))
+                    .app(
+                        NaturalLit(0)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    ),
+            ),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
-            NaturalLit(0) => Ok((r, zero.to_whnf())),
+            NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
             NaturalLit(n) => {
-                let fold = ValueF::from_builtin(NaturalFold)
-                    .app(NaturalLit(n - 1))
-                    .app_value(t.clone())
-                    .app_value(succ.clone())
-                    .app_value(zero.clone())
-                    .into_value_with_type(t.clone());
-                Ok((r, succ.app_value(fold)))
+                let fold = Value::from_builtin(NaturalFold)
+                    .app(
+                        NaturalLit(n - 1)
+                            .into_value_with_type(Value::from_builtin(Natural)),
+                    )
+                    .app(t.clone())
+                    .app(succ.clone())
+                    .app(zero.clone());
+                Ret::ValueWithRemainingArgs(r, succ.app(fold))
             }
-            _ => Err(()),
+            _ => Ret::DoneAsIs,
         },
-        _ => Err(()),
+        _ => Ret::DoneAsIs,
     };
     match ret {
-        Ok((unconsumed_args, mut v)) => {
+        Ret::ValueF(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
-                v = v.app_value(x);
+                v = v.app(x);
             }
-            v
+            v.to_whnf_check_type(ty)
         }
-        Err(()) => AppliedBuiltin(b, args),
+        Ret::DoneAsIs => AppliedBuiltin(b, args),
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
-    let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+        ValueF::Lam(x, _, e) => {
+            e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+        }
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
-            apply_builtin(*b, args)
+            apply_builtin(*b, args, ty)
         }
         ValueF::UnionConstructor(l, kts) => {
             ValueF::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
-            fallback(f, a)
+            ValueF::PartialExpr(ExprF::App(f, a))
         }
     }
 }
@@ -414,53 +450,20 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-/// Performs an intersection of two HashMaps.
-///
-/// # Arguments
-///
-/// * `f` - Will compute the final value from the intersecting
-///         key and the values from both maps.
-///
-/// # Description
-///
-/// If the key is present in both maps then the final value for
-/// that key is computed via the `f` function.
-///
-/// The final map will contain the shared keys from the
-/// two input maps with the final computed value from `f`.
-pub(crate) fn intersection_with_key<K, T, U, V>(
-    mut f: 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 (k, t) in map1 {
-        // Only insert in the final map if the key exists in both
-        if let Some(u) = map2.get(k) {
-            kvs.insert(k.clone(), f(k, t, u));
-        }
-    }
-
-    kvs
-}
-
-pub(crate) fn merge_maps<K, V>(
+pub(crate) fn merge_maps<K, V, F, Err>(
     map1: &HashMap<K, V>,
     map2: &HashMap<K, V>,
-    mut f: impl FnMut(&V, &V) -> V,
-) -> HashMap<K, V>
+    mut f: F,
+) -> Result<HashMap<K, V>, Err>
 where
+    F: FnMut(&K, &V, &V) -> Result<V, Err>,
     K: std::hash::Hash + Eq + Clone,
     V: Clone,
 {
     let mut kvs = HashMap::new();
     for (x, v2) in map2 {
         let newv = if let Some(v1) = map1.get(x) {
-            f(v1, v2)
+            f(x, v1, v2)?
         } else {
             v2.clone()
         };
@@ -470,7 +473,7 @@ where
         // Insert only if key not already present
         kvs.entry(x.clone()).or_insert_with(|| v1.clone());
     }
-    kvs
+    Ok(kvs)
 }
 
 // Small helper enum to avoid repetition
@@ -481,7 +484,12 @@ enum Ret<'a> {
     Expr(ExprF<Value, Normalized>),
 }
 
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(
+    o: BinOp,
+    x: &'a Value,
+    y: &'a Value,
+    ty: &Value,
+) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -574,62 +582,62 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordMerge,
-                    v1.clone(),
-                    v2.clone(),
-                )))
-            });
+            let ty_borrow = ty.as_whnf();
+            let kts = match &*ty_borrow {
+                RecordType(kts) => kts,
+                _ => unreachable!("Internal type error"),
+            };
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+                Ok(Value::from_valuef_and_type(
+                    ValueF::PartialExpr(ExprF::BinOp(
+                        RecursiveRecordMerge,
+                        v1.clone(),
+                        v2.clone(),
+                    )),
+                    kts.get(k).expect("Internal type error").clone(),
+                ))
+            })?;
             Ret::ValueF(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
-                    RecursiveRecordTypeMerge,
-                    v1.clone(),
-                    v2.clone(),
-                )))
-            });
-            Ret::ValueF(RecordType(kvs))
-        }
-
-        (Equivalence, _, _) => {
-            Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+        (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
+            unreachable!("This case should have been handled in typecheck")
         }
 
         _ => return None,
     })
 }
 
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(
+    expr: ExprF<Value, Normalized>,
+    ty: &Value,
+) -> ValueF {
     use ValueF::{
-        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
-        NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
-        TextLit, UnionConstructor, UnionLit, UnionType,
+        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+        NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+        UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
         ExprF::Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprF::Embed(_) => unreachable!(),
-        ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => Ret::Value(x),
+        // Those cases have already been completely handled in the typechecking phase (using
+        // `RetWhole`), so they won't appear here.
+        ExprF::Lam(_, _, _)
+        | ExprF::Pi(_, _, _)
+        | ExprF::Let(_, _, _, _)
+        | ExprF::Embed(_)
+        | ExprF::Const(_)
+        | ExprF::Builtin(_)
+        | ExprF::Var(_)
+        | ExprF::Annot(_, _)
+        | ExprF::RecordType(_)
+        | ExprF::UnionType(_) => {
+            unreachable!("This case should have been handled in typecheck")
+        }
         ExprF::Assert(_) => Ret::Expr(expr),
-        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::App(v, a) => Ret::Value(v.app(a)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
         ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
         ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -654,12 +662,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::RecordLit(kvs) => {
             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::TextLit(elts) => {
             use InterpolatedTextContents::Expr;
             let elts: Vec<_> = squash_textlit(elts.into_iter());
@@ -692,7 +694,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
                 }
             }
         }
-        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
+        ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
@@ -749,7 +751,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::ValueF(h.app_value(v.clone())),
+                    Some(h) => Ret::Value(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
@@ -767,17 +769,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
 
     match ret {
         Ret::ValueF(v) => v,
-        Ret::Value(th) => th.as_whnf().clone(),
-        Ret::ValueRef(th) => th.as_whnf().clone(),
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
         Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
     match v {
-        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
-        ValueF::PartialExpr(e) => normalize_one_layer(e),
+        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+        ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
         ValueF::TextLit(elts) => {
             ValueF::TextLit(squash_textlit(elts.into_iter()))
         }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 1ea87d1..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -31,7 +31,7 @@ fn tck_pi_type(
         _ => {
             return Err(TypeError::new(
                 &ctx2,
-                InvalidOutputType(te.get_type()?.into_owned()),
+                InvalidOutputType(te.get_type()?),
             ))
         }
     };
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
-    match c {
-        Const::Type => Ok(const_to_value(Const::Kind)),
-        Const::Kind => Ok(const_to_value(Const::Sort)),
-        Const::Sort => {
-            Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
-        }
-    }
-}
-
 pub(crate) fn const_to_value(c: Const) -> Value {
     let v = ValueF::Const(c);
-    match type_of_const(c) {
-        Ok(t) => Value::from_valuef_and_type(v, t),
-        Err(_) => Value::from_valuef_untyped(v),
+    match c {
+        Const::Type => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+        }
+        Const::Kind => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+        }
+        Const::Sort => Value::const_sort(),
     }
 }
 
@@ -291,7 +286,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     let ctx = TypecheckContext::new();
     Value::from_valuef_and_type(
-        ValueF::PartialExpr(ExprF::Builtin(b)),
+        ValueF::from_builtin(b),
         type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
     )
 }
@@ -307,14 +302,15 @@ fn type_with(
     use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
 
     Ok(match e.as_ref() {
-        Lam(x, t, b) => {
-            let tx = type_with(ctx, t.clone())?;
-            let ctx2 = ctx.insert_type(x, tx.clone());
-            let b = type_with(&ctx2, b.clone())?;
-            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)?;
-            Value::from_valuef_and_type(v, t)
+        Lam(var, annot, body) => {
+            let annot = type_with(ctx, annot.clone())?;
+            let ctx2 = ctx.insert_type(var, annot.clone());
+            let body = type_with(&ctx2, body.clone())?;
+            let body_type = body.get_type()?;
+            Value::from_valuef_and_type(
+                ValueF::Lam(var.clone().into(), annot.clone(), body),
+                tck_pi_type(ctx, var.clone(), annot, body_type)?,
+            )
         }
         Pi(x, ta, tb) => {
             let ta = type_with(ctx, ta.clone())?;
@@ -389,17 +385,17 @@ fn type_last_layer(
                 ValueF::Pi(x, tx, tb) => (x, tx, tb),
                 _ => return mkerr(NotAFunction(f.clone())),
             };
-            if a.get_type()?.as_ref() != tx {
+            if &a.get_type()? != tx {
                 return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
             }
 
             RetTypeOnly(tb.subst_shift(&x.into(), a))
         }
         Annot(x, t) => {
-            if t != x.get_type()?.as_ref() {
+            if &x.get_type()? != t {
                 return mkerr(AnnotMismatch(x.clone(), t.clone()));
             }
-            RetTypeOnly(x.get_type()?.into_owned())
+            RetWhole(x.clone())
         }
         Assert(t) => {
             match &*t.as_whnf() {
@@ -412,7 +408,7 @@ fn type_last_layer(
             RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
-            if x.get_type()?.as_ref() != &builtin_to_value(Bool) {
+            if &*x.get_type()?.as_whnf() != &ValueF::from_builtin(Bool) {
                 return mkerr(InvalidPredicate(x.clone()));
             }
 
@@ -428,7 +424,7 @@ fn type_last_layer(
                 return mkerr(IfBranchMismatch(y.clone(), z.clone()));
             }
 
-            RetTypeOnly(y.get_type()?.into_owned())
+            RetTypeOnly(y.get_type()?)
         }
         EmptyListLit(t) => {
             match &*t.as_whnf() {
@@ -445,33 +441,27 @@ fn type_last_layer(
                 if x.get_type()? != y.get_type()? {
                     return mkerr(InvalidListElement(
                         i,
-                        x.get_type()?.into_owned(),
+                        x.get_type()?,
                         y.clone(),
                     ));
                 }
             }
             let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidListType(t.into_owned()));
+                return mkerr(InvalidListType(t));
             }
 
-            RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app_value(t.into_owned()),
-                Value::from_const(Type),
-            ))
+            RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
         }
         SomeLit(x) => {
-            let t = x.get_type()?.into_owned();
+            let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
                 return mkerr(InvalidOptionalType(t));
             }
 
-            RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app_value(t),
-                Value::from_const(Type),
-            ))
+            RetTypeOnly(
+                Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
+            )
         }
         RecordType(kts) => RetWhole(tck_record_type(
             ctx,
@@ -483,8 +473,7 @@ fn type_last_layer(
         )?),
         RecordLit(kvs) => RetTypeOnly(tck_record_type(
             ctx,
-            kvs.iter()
-                .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
+            kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
         )?),
         Field(r, x) => {
             match &*r.get_type()?.as_whnf() {
@@ -545,7 +534,7 @@ fn type_last_layer(
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
-                    if x.get_type()?.as_ref() != &text_type {
+                    if x.get_type()? != text_type {
                         return mkerr(InvalidTextInterpolation(x.clone()));
                     }
                 }
@@ -574,7 +563,9 @@ fn type_last_layer(
 
             // 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| {
+                Ok(r_t.clone())
+            })?;
 
             // Construct the final record type from the union
             RetTypeOnly(tck_record_type(
@@ -586,30 +577,12 @@ fn type_last_layer(
             ctx,
             ExprF::BinOp(
                 RecursiveRecordTypeMerge,
-                l.get_type()?.into_owned(),
-                r.get_type()?.into_owned(),
+                l.get_type()?,
+                r.get_type()?,
             ),
         )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
-            use crate::phase::normalize::intersection_with_key;
-
-            // Extract the Const of the LHS
-            let k_l = match l.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
-                }
-            };
-
-            // Extract the Const of the RHS
-            let k_r = match r.get_type()?.as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
-                }
-            };
-
-            let k = max(k_l, k_r);
+            use crate::phase::normalize::merge_maps;
 
             // Extract the LHS record type
             let borrow_l = l.as_whnf();
@@ -630,9 +603,11 @@ fn type_last_layer(
             };
 
             // Ensure that the records combine without a type error
-            let kts = intersection_with_key(
+            let kts = merge_maps(
+                kts_x,
+                kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |_: &Label, l: &Value, r: &Value| {
+                |_, l: &Value, r: &Value| {
                     type_last_layer(
                         ctx,
                         ExprF::BinOp(
@@ -642,12 +617,9 @@ fn type_last_layer(
                         ),
                     )
                 },
-                kts_x,
-                kts_y,
-            );
-            tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+            )?;
 
-            RetTypeOnly(Value::from_const(k))
+            RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
@@ -659,7 +631,7 @@ fn type_last_layer(
                 return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
-            RetTypeOnly(l.get_type()?.into_owned())
+            RetTypeOnly(l.get_type()?)
         }
         BinOp(Equivalence, l, r) => {
             if l.get_type()?.get_type()?.as_const() != Some(Type) {
@@ -673,7 +645,10 @@ fn type_last_layer(
                 return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
             }
 
-            RetTypeOnly(Value::from_const(Type))
+            RetWhole(Value::from_valuef_and_type(
+                ValueF::Equivalence(l.clone(), r.clone()),
+                Value::from_const(Type),
+            ))
         }
         BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
@@ -692,11 +667,11 @@ fn type_last_layer(
                 Equivalence => unreachable!(),
             });
 
-            if l.get_type()?.as_ref() != &t {
+            if l.get_type()? != t {
                 return mkerr(BinOpTypeMismatch(*o, l.clone()));
             }
 
-            if r.get_type()?.as_ref() != &t {
+            if r.get_type()? != t {
                 return mkerr(BinOpTypeMismatch(*o, r.clone()));
             }
 
@@ -800,7 +775,7 @@ fn type_last_layer(
 
             RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::RecordType(new_kts),
-                record_type.get_type()?.into_owned(),
+                record_type.get_type()?,
             ))
         }
     };
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index be4805d..8f16a12 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -185,7 +185,7 @@ pub fn run_test(
                 }
                 TypeInference => {
                     let expr = expr.typecheck()?;
-                    let ty = expr.get_type()?.into_owned().normalize();
+                    let ty = expr.get_type()?.normalize();
                     assert_eq_display!(ty, expected);
                 }
                 Normalization => {