Merge TypedValue and Value

7 files changed, 232 insertions, 354 deletions

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index deabe44..2bf39c5 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,15 +3,15 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::value::TypedValue;
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 
 #[derive(Debug, Clone)]
 enum CtxItem {
-    Kept(AlphaVar, TypedValue),
-    Replaced(TypedValue),
+    Kept(AlphaVar, Value),
+    Replaced(Value),
 }
 
 #[derive(Debug, Clone)]
@@ -21,21 +21,17 @@ impl TypecheckContext {
     pub fn new() -> Self {
         TypecheckContext(Rc::new(Vec::new()))
     }
-    pub fn insert_type(&self, x: &Label, t: TypedValue) -> Self {
+    pub fn insert_type(&self, x: &Label, t: Value) -> Self {
         let mut vec = self.0.as_ref().clone();
         vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
         TypecheckContext(Rc::new(vec))
     }
-    pub fn insert_value(
-        &self,
-        x: &Label,
-        e: TypedValue,
-    ) -> Result<Self, TypeError> {
+    pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> {
         let mut vec = self.0.as_ref().clone();
         vec.push((x.clone(), CtxItem::Replaced(e)));
         Ok(TypecheckContext(Rc::new(vec)))
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
+    pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
         let mut var = var.clone();
         let mut shift_map: HashMap<Label, _> = HashMap::new();
         for (l, i) in self.0.iter().rev() {
@@ -44,10 +40,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            TypedValue::from_valuef_and_type(
-                                ValueF::Var(newvar),
-                                t,
-                            )
+                            Value::from_valuef_and_type(ValueF::Var(newvar), t)
                         }
                         CtxItem::Replaced(v) => v,
                     });
@@ -101,7 +94,7 @@ impl TypecheckContext {
             )))
         }
     }
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
             .unwrap()
     }
@@ -124,8 +117,8 @@ impl Shift for TypecheckContext {
     }
 }
 
-impl Subst<TypedValue> for CtxItem {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for CtxItem {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
@@ -136,8 +129,8 @@ impl Subst<TypedValue> for CtxItem {
     }
 }
 
-impl Subst<TypedValue> for TypecheckContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for TypecheckContext {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.subst_shift(var, val)
     }
 }
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index c4e3831..8573d11 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -35,7 +35,7 @@ use Form::{Unevaled, NF, WHNF};
 struct ValueInternal {
     form: Form,
     value: ValueF,
-    ty: Option<TypedValue>,
+    ty: Option<Value>,
 }
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
@@ -45,11 +45,6 @@ struct ValueInternal {
 #[derive(Clone)]
 pub struct Value(Rc<RefCell<ValueInternal>>);
 
-/// A value that needs to carry a type for typechecking to work.
-/// TODO: actually enforce this.
-#[derive(Debug, Clone)]
-pub struct TypedValue(Value);
-
 impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
@@ -96,7 +91,7 @@ impl ValueInternal {
         }
     }
 
-    fn get_type(&self) -> Result<&TypedValue, TypeError> {
+    fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
             None => Err(TypeError::new(
@@ -116,7 +111,7 @@ impl Value {
         }
         .into_value()
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value {
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
         ValueInternal {
             form: Unevaled,
             value: v,
@@ -125,7 +120,57 @@ impl Value {
         .into_value()
     }
     pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
-        Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type))
+        Value::from_valuef_and_type(v, Value::from_const(Const::Type))
+    }
+    pub(crate) fn from_const(c: Const) -> Self {
+        match type_of_const(c) {
+            Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t),
+            Err(_) => Value::from_valuef_untyped(ValueF::Const(c)),
+        }
+    }
+    pub fn const_type() -> Self {
+        Value::from_const(Const::Type)
+    }
+
+    pub(crate) fn as_const(&self) -> Option<Const> {
+        match &*self.as_whnf() {
+            ValueF::Const(c) => Some(*c),
+            _ => None,
+        }
+    }
+
+    fn as_internal(&self) -> Ref<ValueInternal> {
+        self.0.borrow()
+    }
+    fn as_internal_mut(&self) -> RefMut<ValueInternal> {
+        self.0.borrow_mut()
+    }
+    /// This is what you want if you want to pattern-match on the value.
+    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
+    /// panics.
+    pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
+        self.do_normalize_whnf();
+        Ref::map(self.as_internal(), ValueInternal::as_whnf)
+    }
+
+    // TODO: rename `normalize_to_expr`
+    pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
+        self.as_whnf().normalize_to_expr()
+    }
+    // TODO: rename `normalize_to_expr_maybe_alpha`
+    pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
+        self.as_whnf().normalize_to_expr_maybe_alpha(true)
+    }
+    // TODO: deprecated
+    pub(crate) fn to_value(&self) -> Value {
+        self.clone()
+    }
+    /// TODO: cloning a valuef can often be avoided
+    pub(crate) fn to_whnf(&self) -> ValueF {
+        self.as_whnf().clone()
+    }
+    pub(crate) fn into_typed(self) -> Typed {
+        Typed::from_value(self)
     }
 
     /// Mutates the contents. If no one else shares this thunk,
@@ -138,20 +183,12 @@ impl Value {
             None => f(&mut self.as_internal_mut()),
         }
     }
-
     /// Normalizes contents to normal form; faster than `normalize_nf` if
     /// no one else shares this thunk.
     pub(crate) fn normalize_mut(&mut self) {
         self.mutate_internal(|vint| vint.normalize_nf())
     }
 
-    fn as_internal(&self) -> Ref<ValueInternal> {
-        self.0.borrow()
-    }
-    fn as_internal_mut(&self) -> RefMut<ValueInternal> {
-        self.0.borrow_mut()
-    }
-
     fn do_normalize_whnf(&self) {
         let borrow = self.as_internal();
         match borrow.form {
@@ -163,7 +200,6 @@ impl Value {
             WHNF | NF => {}
         }
     }
-
     fn do_normalize_nf(&self) {
         let borrow = self.as_internal();
         match borrow.form {
@@ -176,26 +212,14 @@ impl Value {
         }
     }
 
-    // WARNING: avoid normalizing any thunk while holding on to this ref
-    // or you could run into BorrowMut panics
+    /// WARNING: avoid normalizing any thunk while holding on to this ref
+    /// or you could run into BorrowMut panics
+    // TODO: rename to `as_nf`
     pub(crate) fn normalize_nf(&self) -> Ref<ValueF> {
         self.do_normalize_nf();
         Ref::map(self.as_internal(), ValueInternal::as_nf)
     }
 
-    /// This is what you want if you want to pattern-match on the value.
-    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
-    /// panics.
-    pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
-        self.do_normalize_whnf();
-        Ref::map(self.as_internal(), ValueInternal::as_whnf)
-    }
-
-    /// TODO: cloning a valuef can often be avoided
-    pub(crate) fn to_whnf(&self) -> ValueF {
-        self.as_whnf().clone()
-    }
-
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
@@ -211,83 +235,11 @@ impl Value {
         apply_any(self.clone(), th)
     }
 
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> {
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
         Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
     }
 }
 
-impl TypedValue {
-    pub fn from_value(th: Value) -> Self {
-        TypedValue(th)
-    }
-    pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue {
-        TypedValue::from_value(Value::from_valuef_untyped(v))
-    }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self {
-        TypedValue(Value::from_valuef_and_type(v, t))
-    }
-    // TODO: do something with the info that the type is Type. Maybe check
-    // is a type is present ?
-    pub(crate) fn from_value_simple_type(th: Value) -> Self {
-        TypedValue::from_value(th)
-    }
-    pub(crate) fn from_const(c: Const) -> Self {
-        match type_of_const(c) {
-            Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t),
-            Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)),
-        }
-    }
-    pub fn const_type() -> Self {
-        TypedValue::from_const(Const::Type)
-    }
-
-    pub(crate) fn normalize_nf(&self) -> ValueF {
-        self.0.normalize_nf().clone()
-    }
-
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
-    }
-
-    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
-    /// panics.
-    pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
-        self.0.as_whnf()
-    }
-    pub(crate) fn to_whnf(&self) -> ValueF {
-        self.0.to_whnf()
-    }
-    pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
-        self.as_whnf().normalize_to_expr()
-    }
-    pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
-        self.as_whnf().normalize_to_expr_maybe_alpha(true)
-    }
-    pub(crate) fn to_value(&self) -> Value {
-        self.0.clone()
-    }
-    pub(crate) fn into_typed(self) -> Typed {
-        Typed::from_typedvalue(self)
-    }
-    pub(crate) fn as_const(&self) -> Option<Const> {
-        match &*self.as_whnf() {
-            ValueF::Const(c) => Some(*c),
-            _ => None,
-        }
-    }
-
-    pub(crate) fn normalize_mut(&mut self) {
-        self.0.normalize_mut()
-    }
-
-    pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> {
-        self.0.get_type()
-    }
-}
-
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -304,20 +256,14 @@ impl Shift for ValueInternal {
     }
 }
 
-impl Shift for TypedValue {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(TypedValue(self.0.shift(delta, var)?))
-    }
-}
-
-impl Subst<TypedValue> for Value {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for Value {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         Value(self.0.subst_shift(var, val))
     }
 }
 
-impl Subst<TypedValue> for ValueInternal {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for ValueInternal {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
@@ -327,12 +273,7 @@ impl Subst<TypedValue> for ValueInternal {
     }
 }
 
-impl Subst<TypedValue> for TypedValue {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
-        TypedValue(self.0.subst_shift(var, val))
-    }
-}
-
+// TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
         *self.as_whnf() == *other.as_whnf()
@@ -340,13 +281,6 @@ impl std::cmp::PartialEq for Value {
 }
 impl std::cmp::Eq for Value {}
 
-impl std::cmp::PartialEq for TypedValue {
-    fn eq(&self, other: &Self) -> bool {
-        &*self.as_whnf() == &*other.as_whnf()
-    }
-}
-impl std::cmp::Eq for TypedValue {}
-
 impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index de55d2f..0d2655e 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::normalize::OutputSubExpr;
 use crate::phase::Normalized;
@@ -18,8 +18,8 @@ use crate::phase::Normalized;
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum ValueF {
     /// Closures
-    Lam(AlphaLabel, TypedValue, Value),
-    Pi(AlphaLabel, TypedValue, TypedValue),
+    Lam(AlphaLabel, Value, Value),
+    Pi(AlphaLabel, Value, Value),
     // Invariant: the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
@@ -29,20 +29,20 @@ pub enum ValueF {
     NaturalLit(Natural),
     IntegerLit(Integer),
     DoubleLit(NaiveDouble),
-    EmptyOptionalLit(TypedValue),
+    EmptyOptionalLit(Value),
     NEOptionalLit(Value),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
-    EmptyListLit(TypedValue),
+    EmptyListLit(Value),
     NEListLit(Vec<Value>),
     RecordLit(HashMap<Label, Value>),
-    RecordType(HashMap<Label, TypedValue>),
-    UnionType(HashMap<Label, Option<TypedValue>>),
-    UnionConstructor(Label, HashMap<Label, Option<TypedValue>>),
-    UnionLit(Label, Value, HashMap<Label, Option<TypedValue>>),
+    RecordType(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
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Value>>),
-    Equivalence(TypedValue, TypedValue),
+    Equivalence(Value, Value),
     // Invariant: this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Value, Normalized>),
 }
@@ -51,7 +51,7 @@ impl ValueF {
     pub(crate) fn into_value_untyped(self) -> Value {
         Value::from_valuef_untyped(self)
     }
-    pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value {
+    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 {
@@ -333,8 +333,8 @@ impl Shift for ValueF {
     }
 }
 
-impl Subst<TypedValue> for ValueF {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for ValueF {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             ValueF::AppliedBuiltin(b, args) => {
                 ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 0f2f5fc..b34c3a2 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -3,7 +3,7 @@ use std::io::Error as IOError;
 use dhall_syntax::{BinOp, Import, Label, ParseError, V};
 
 use crate::core::context::TypecheckContext;
-use crate::core::value::TypedValue;
+use crate::core::value::Value;
 use crate::phase::resolve::ImportStack;
 use crate::phase::NormalizedSubExpr;
 
@@ -49,28 +49,28 @@ pub struct TypeError {
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
     UnboundVariable(V<Label>),
-    InvalidInputType(TypedValue),
-    InvalidOutputType(TypedValue),
-    NotAFunction(TypedValue),
-    TypeMismatch(TypedValue, TypedValue, TypedValue),
-    AnnotMismatch(TypedValue, TypedValue),
+    InvalidInputType(Value),
+    InvalidOutputType(Value),
+    NotAFunction(Value),
+    TypeMismatch(Value, Value, Value),
+    AnnotMismatch(Value, Value),
     Untyped,
     FieldCollision(Label),
-    InvalidListElement(usize, TypedValue, TypedValue),
-    InvalidListType(TypedValue),
-    InvalidOptionalType(TypedValue),
-    InvalidPredicate(TypedValue),
-    IfBranchMismatch(TypedValue, TypedValue),
-    IfBranchMustBeTerm(bool, TypedValue),
-    InvalidFieldType(Label, TypedValue),
-    NotARecord(Label, TypedValue),
-    MustCombineRecord(TypedValue),
-    MissingRecordField(Label, TypedValue),
-    MissingUnionField(Label, TypedValue),
-    BinOpTypeMismatch(BinOp, TypedValue),
-    InvalidTextInterpolation(TypedValue),
-    Merge1ArgMustBeRecord(TypedValue),
-    Merge2ArgMustBeUnion(TypedValue),
+    InvalidListElement(usize, Value, Value),
+    InvalidListType(Value),
+    InvalidOptionalType(Value),
+    InvalidPredicate(Value),
+    IfBranchMismatch(Value, Value),
+    IfBranchMustBeTerm(bool, Value),
+    InvalidFieldType(Label, Value),
+    NotARecord(Label, Value),
+    MustCombineRecord(Value),
+    MissingRecordField(Label, Value),
+    MissingUnionField(Label, Value),
+    BinOpTypeMismatch(BinOp, Value),
+    InvalidTextInterpolation(Value),
+    Merge1ArgMustBeRecord(Value),
+    Merge2ArgMustBeUnion(Value),
     MergeEmptyNeedsAnnotation,
     MergeHandlerMissingVariant(Label),
     MergeVariantMissingHandler(Label),
@@ -80,14 +80,14 @@ pub(crate) enum TypeMessage {
     ProjectionMustBeRecord,
     ProjectionMissingEntry,
     Sort,
-    RecordMismatch(TypedValue, TypedValue),
+    RecordMismatch(Value, Value),
     RecordTypeDuplicateField,
-    RecordTypeMergeRequiresRecordType(TypedValue),
-    RecordTypeMismatch(TypedValue, TypedValue, TypedValue, TypedValue),
+    RecordTypeMergeRequiresRecordType(Value),
+    RecordTypeMismatch(Value, Value, Value, Value),
     UnionTypeDuplicateField,
-    EquivalenceArgumentMustBeTerm(bool, TypedValue),
-    EquivalenceTypeMismatch(TypedValue, TypedValue),
-    AssertMismatch(TypedValue, TypedValue),
+    EquivalenceArgumentMustBeTerm(bool, Value),
+    EquivalenceTypeMismatch(Value, Value),
+    AssertMismatch(Value, Value),
     AssertMustTakeEquivalence,
 }
 
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index e58e689..91d64c3 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,7 +4,7 @@ use std::path::Path;
 
 use dhall_syntax::{Const, SubExpr};
 
-use crate::core::value::{TypedValue, Value};
+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(TypedValue);
+pub struct Typed(Value);
 
 /// A normalized expression.
 ///
@@ -91,12 +91,12 @@ impl Typed {
     }
 
     pub(crate) fn from_const(c: Const) -> Self {
-        Typed(TypedValue::from_const(c))
+        Typed(Value::from_const(c))
     }
     pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
-        Typed(TypedValue::from_valuef_and_type(v, t.into_typedvalue()))
+        Typed(Value::from_valuef_and_type(v, t.into_value()))
     }
-    pub(crate) fn from_typedvalue(th: TypedValue) -> Self {
+    pub(crate) fn from_value(th: Value) -> Self {
         Typed(th)
     }
     pub fn const_type() -> Self {
@@ -112,7 +112,7 @@ impl Typed {
     pub fn to_value(&self) -> Value {
         self.0.to_value()
     }
-    pub(crate) fn into_typedvalue(self) -> TypedValue {
+    pub(crate) fn into_value(self) -> Value {
         self.0
     }
 
@@ -155,8 +155,8 @@ impl Shift for Normalized {
     }
 }
 
-impl Subst<TypedValue> for Typed {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for Typed {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 }
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 27858d8..821c5fd 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
@@ -26,9 +26,7 @@ macro_rules! make_closure {
     (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
         ValueF::Lam(
             Label::from(stringify!($var)).into(),
-            TypedValue::from_value_simple_type(
-                make_closure!($($ty)*),
-            ),
+            make_closure!($($ty)*),
             make_closure!($($rest)*),
         ).into_value_untyped()
     };
@@ -51,10 +49,10 @@ macro_rules! make_closure {
             make_closure!($($rest)*),
             Value::from_valuef_and_type(
                 ValueF::NaturalLit(1),
-                TypedValue::from_value(make_closure!(Natural))
+                make_closure!(Natural)
             ),
         )).into_value_with_type(
-            TypedValue::from_value(make_closure!(Natural))
+            make_closure!(Natural)
         )
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {
@@ -74,10 +72,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> 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(TypedValue::from_value_simple_type(t.clone())),
-        )),
+        (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))),
         (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
             _ => Err(()),
@@ -199,16 +194,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypedValue::from_valuef_untyped(ValueF::from_builtin(
-                        Natural,
-                    )),
+                    Value::from_valuef_untyped(ValueF::from_builtin(Natural)),
                 );
                 kts.insert("value".into(), t.clone());
                 Ok((
                     r,
-                    EmptyListLit(TypedValue::from_valuef_untyped(RecordType(
-                        kts,
-                    ))),
+                    EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
                 ))
             }
             NEListLit(xs) => {
@@ -252,9 +243,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                             [ var(x, 1) ] # var(xs, 0)
                         )
                     })
-                    .app_valuef(EmptyListLit(
-                        TypedValue::from_value_simple_type(t.clone()),
-                    )),
+                    .app_valuef(EmptyListLit(t.clone())),
             )),
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
@@ -288,9 +277,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                     ValueF::from_builtin(Optional).app_value(t.clone()),
                 )
                 .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
-                .app_valuef(EmptyOptionalLit(
-                    TypedValue::from_value_simple_type(t.clone()),
-                )),
+                .app_valuef(EmptyOptionalLit(t.clone())),
             )),
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
@@ -346,10 +333,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
 
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => {
-            let val = TypedValue::from_value(a);
-            e.subst_shift(&x.into(), &val).to_whnf()
-        }
+        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();
@@ -639,21 +623,18 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                TypedValue::from_valuef_untyped(ValueF::PartialExpr(
-                    ExprF::BinOp(
-                        RecursiveRecordTypeMerge,
-                        v1.to_value(),
-                        v2.to_value(),
-                    ),
-                ))
+                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
+                    RecursiveRecordTypeMerge,
+                    v1.to_value(),
+                    v2.to_value(),
+                )))
             });
             Ret::ValueF(RecordType(kvs))
         }
 
-        (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence(
-            TypedValue::from_value_simple_type(x.clone()),
-            TypedValue::from_value_simple_type(y.clone()),
-        )),
+        (Equivalence, _, _) => {
+            Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
+        }
 
         _ => return None,
     })
@@ -674,18 +655,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::Var(_) => unreachable!(),
         ExprF::Annot(x, _) => Ret::Value(x),
         ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::Lam(x, t, e) => {
-            Ret::ValueF(Lam(x.into(), TypedValue::from_value(t), e))
-        }
-        ExprF::Pi(x, t, e) => Ret::ValueF(Pi(
-            x.into(),
-            TypedValue::from_value(t),
-            TypedValue::from_value(e),
-        )),
-        ExprF::Let(x, _, v, b) => {
-            let v = TypedValue::from_value(v);
-            Ret::Value(b.subst_shift(&x.into(), &v))
-        }
+        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)),
@@ -699,9 +671,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
             let t_borrow = t.as_whnf();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::ValueF(EmptyListLit(
-                        TypedValue::from_value_simple_type(args[0].clone()),
-                    ))
+                    Ret::ValueF(EmptyListLit(args[0].clone()))
                 }
                 _ => {
                     drop(t_borrow);
@@ -715,16 +685,12 @@ 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()
-                .map(|(k, t)| (k, TypedValue::from_value(t)))
-                .collect(),
-        )),
-        ExprF::UnionType(kts) => Ret::ValueF(UnionType(
-            kts.into_iter()
-                .map(|(k, t)| (k, t.map(|t| TypedValue::from_value(t))))
-                .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());
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index e24f5a3..e65881e 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
 };
 
 use crate::core::context::TypecheckContext;
-use crate::core::value::TypedValue;
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
@@ -14,9 +14,9 @@ use crate::phase::Normalized;
 fn tck_pi_type(
     ctx: &TypecheckContext,
     x: Label,
-    tx: TypedValue,
-    te: TypedValue,
-) -> Result<TypedValue, TypeError> {
+    tx: Value,
+    te: Value,
+) -> Result<Value, TypeError> {
     use crate::error::TypeMessage::*;
     let ctx2 = ctx.insert_type(&x, tx.clone());
 
@@ -37,16 +37,16 @@ fn tck_pi_type(
 
     let k = function_check(ka, kb);
 
-    Ok(TypedValue::from_valuef_and_type(
+    Ok(Value::from_valuef_and_type(
         ValueF::Pi(x.into(), tx, te),
-        TypedValue::from_const(k),
+        Value::from_const(k),
     ))
 }
 
 fn tck_record_type(
     ctx: &TypecheckContext,
-    kts: impl IntoIterator<Item = Result<(Label, TypedValue), TypeError>>,
-) -> Result<TypedValue, 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();
@@ -70,18 +70,18 @@ fn tck_record_type(
     // An empty record type has type Type
     let k = k.unwrap_or(Const::Type);
 
-    Ok(TypedValue::from_valuef_and_type(
+    Ok(Value::from_valuef_and_type(
         ValueF::RecordType(new_kts),
-        TypedValue::from_const(k),
+        Value::from_const(k),
     ))
 }
 
 fn tck_union_type<Iter>(
     ctx: &TypecheckContext,
     kts: Iter,
-) -> Result<TypedValue, TypeError>
+) -> Result<Value, TypeError>
 where
-    Iter: IntoIterator<Item = Result<(Label, Option<TypedValue>), TypeError>>,
+    Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
 {
     use crate::error::TypeMessage::*;
     use std::collections::hash_map::Entry;
@@ -115,9 +115,9 @@ where
     // an union type with only unary variants also has type Type
     let k = k.unwrap_or(Const::Type);
 
-    Ok(TypedValue::from_valuef_and_type(
+    Ok(Value::from_valuef_and_type(
         ValueF::UnionType(new_kts),
-        TypedValue::from_const(k),
+        Value::from_const(k),
     ))
 }
 
@@ -130,10 +130,10 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-pub(crate) fn type_of_const(c: Const) -> Result<TypedValue, TypeError> {
+pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> {
     match c {
-        Const::Type => Ok(TypedValue::from_const(Const::Kind)),
-        Const::Kind => Ok(TypedValue::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))
         }
@@ -282,16 +282,16 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 }
 
 // TODO: this can't fail in practise
-pub(crate) fn builtin_to_type(b: Builtin) -> Result<TypedValue, TypeError> {
+pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> {
     type_with(&TypecheckContext::new(), SubExpr::from_builtin(b))
 }
 
 /// Intermediary return type
 enum Ret {
     /// Returns the contained value as is
-    RetWhole(TypedValue),
-    /// Use the contained TypedValue as the type of the input expression
-    RetTypeOnly(TypedValue),
+    RetWhole(Value),
+    /// Use the contained Value as the type of the input expression
+    RetTypeOnly(Value),
 }
 
 /// Type-check an expression and return the expression alongside its type if type-checking
@@ -301,7 +301,7 @@ enum Ret {
 fn type_with(
     ctx: &TypecheckContext,
     e: SubExpr<Normalized>,
-) -> Result<TypedValue, TypeError> {
+) -> Result<Value, TypeError> {
     use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
 
     use Ret::*;
@@ -313,7 +313,7 @@ fn type_with(
             let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value());
             let tb = b.get_type()?.into_owned();
             let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
-            TypedValue::from_valuef_and_type(v, t)
+            Value::from_valuef_and_type(v, t)
         }
         Pi(x, ta, tb) => {
             let ta = type_with(ctx, ta.clone())?;
@@ -331,7 +331,7 @@ 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().into_typedvalue(),
+        Embed(p) => p.clone().into_typed().into_value(),
         Var(var) => match ctx.lookup(&var) {
             Some(typed) => typed.clone(),
             None => {
@@ -352,10 +352,7 @@ fn type_with(
             match ret {
                 RetTypeOnly(typ) => {
                     let expr = expr.map_ref(|typed| typed.to_value());
-                    TypedValue::from_valuef_and_type(
-                        ValueF::PartialExpr(expr),
-                        typ,
-                    )
+                    Value::from_valuef_and_type(ValueF::PartialExpr(expr), typ)
                 }
                 RetWhole(tt) => tt,
             }
@@ -367,7 +364,7 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: &ExprF<TypedValue, Normalized>,
+    e: &ExprF<Value, Normalized>,
 ) -> Result<Ret, TypeError> {
     use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
@@ -466,10 +463,10 @@ fn type_last_layer(
                 ));
             }
 
-            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
+            Ok(RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
                     .app_value(t.to_value()),
-                TypedValue::from_const(Type),
+                Value::from_const(Type),
             )))
         }
         SomeLit(x) => {
@@ -478,10 +475,10 @@ fn type_last_layer(
                 return Err(TypeError::new(ctx, InvalidOptionalType(t)));
             }
 
-            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
+            Ok(RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::Optional)
                     .app_value(t.to_value()),
-                TypedValue::from_const(Type),
+                Value::from_const(Type),
             )))
         }
         RecordType(kts) => Ok(RetWhole(tck_record_type(
@@ -545,7 +542,7 @@ fn type_last_layer(
                 // ))),
             }
         }
-        Const(c) => Ok(RetWhole(TypedValue::from_const(*c))),
+        Const(c) => Ok(RetWhole(Value::from_const(*c))),
         Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)),
         BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
@@ -607,43 +604,38 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: &HashMap<Label, TypedValue>,
-                kts_r: &HashMap<Label, TypedValue>,
-            ) -> Result<TypedValue, TypeError> {
+                kts_l: &HashMap<Label, Value>,
+                kts_r: &HashMap<Label, Value>,
+            ) -> Result<Value, TypeError> {
                 use crate::phase::normalize::outer_join;
 
                 // If the Label exists for both records and the values
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
-                let combine =
-                    |k: &Label,
-                     inner_l: &TypedValue,
-                     inner_r: &TypedValue|
-                     -> Result<TypedValue, TypeError> {
-                        match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) {
-                            (
-                                ValueF::RecordType(inner_l_kvs),
-                                ValueF::RecordType(inner_r_kvs),
-                            ) => combine_record_types(
-                                ctx,
-                                inner_l_kvs,
-                                inner_r_kvs,
-                            ),
-                            (_, _) => Err(TypeError::new(
-                                ctx,
-                                FieldCollision(k.clone()),
-                            )),
+                let combine = |k: &Label,
+                               inner_l: &Value,
+                               inner_r: &Value|
+                 -> Result<Value, TypeError> {
+                    match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) {
+                        (
+                            ValueF::RecordType(inner_l_kvs),
+                            ValueF::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<TypedValue, TypeError>> =
-                    outer_join(
-                        |l| Ok(l.clone()),
-                        |r| Ok(r.clone()),
-                        combine,
-                        kts_l,
-                        kts_r,
-                    );
+                let kts: HashMap<Label, Result<Value, TypeError>> = outer_join(
+                    |l| Ok(l.clone()),
+                    |r| Ok(r.clone()),
+                    combine,
+                    kts_l,
+                    kts_r,
+                );
 
                 Ok(tck_record_type(
                     ctx,
@@ -684,35 +676,30 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: &HashMap<Label, TypedValue>,
-                kts_r: &HashMap<Label, TypedValue>,
-            ) -> Result<TypedValue, TypeError> {
+                kts_l: &HashMap<Label, Value>,
+                kts_r: &HashMap<Label, Value>,
+            ) -> Result<Value, TypeError> {
                 use crate::phase::normalize::intersection_with_key;
 
                 // If the Label exists for both records and the values
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
-                let combine =
-                    |k: &Label,
-                     kts_l_inner: &TypedValue,
-                     kts_r_inner: &TypedValue|
-                     -> Result<TypedValue, TypeError> {
-                        match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf())
-                        {
-                            (
-                                ValueF::RecordType(kvs_l_inner),
-                                ValueF::RecordType(kvs_r_inner),
-                            ) => combine_record_types(
-                                ctx,
-                                kvs_l_inner,
-                                kvs_r_inner,
-                            ),
-                            (_, _) => Err(TypeError::new(
-                                ctx,
-                                FieldCollision(k.clone()),
-                            )),
+                let combine = |k: &Label,
+                               kts_l_inner: &Value,
+                               kts_r_inner: &Value|
+                 -> Result<Value, TypeError> {
+                    match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) {
+                        (
+                            ValueF::RecordType(kvs_l_inner),
+                            ValueF::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(combine, kts_l, kts_r);
 
@@ -747,8 +734,8 @@ fn type_last_layer(
                 k_l
             } else {
                 return Err(mkerr(RecordTypeMismatch(
-                    TypedValue::from_const(k_l),
-                    TypedValue::from_const(k_r),
+                    Value::from_const(k_l),
+                    Value::from_const(k_r),
                     l.clone(),
                     r.clone(),
                 )));
@@ -779,7 +766,7 @@ fn type_last_layer(
             // 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(TypedValue::from_const(k))))
+                .and(Ok(RetTypeOnly(Value::from_const(k))))
         }
         BinOp(o @ ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
@@ -814,7 +801,7 @@ fn type_last_layer(
                 )));
             }
 
-            Ok(RetTypeOnly(TypedValue::from_const(Type)))
+            Ok(RetTypeOnly(Value::from_const(Type)))
         }
         BinOp(o, l, r) => {
             let t = builtin_to_type(match o {
@@ -941,7 +928,7 @@ fn type_last_layer(
                 };
             }
 
-            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
+            Ok(RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::RecordType(new_kts),
                 record_type.get_type()?.into_owned(),
             )))
@@ -952,15 +939,13 @@ fn type_last_layer(
 /// `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.
-pub(crate) fn typecheck(
-    e: SubExpr<Normalized>,
-) -> Result<TypedValue, TypeError> {
+pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> {
     type_with(&TypecheckContext::new(), e)
 }
 
 pub(crate) fn typecheck_with(
     expr: SubExpr<Normalized>,
     ty: SubExpr<Normalized>,
-) -> Result<TypedValue, TypeError> {
+) -> Result<Value, TypeError> {
     typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
 }