From 29016b78736dca857e4e7f7c4dc68ed5e30c28bb Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 19 Aug 2019 12:25:09 +0200
Subject: s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible

---
 dhall/src/core/value.rs      |  38 ++++-----
 dhall/src/core/valuef.rs     |   7 +-
 dhall/src/error/mod.rs       |  20 ++---
 dhall/src/phase/mod.rs       |  15 ++--
 dhall/src/phase/normalize.rs |  94 ++++++++++----------
 dhall/src/phase/typecheck.rs | 198 ++++++++++++++++++++-----------------------
 dhall/src/tests.rs           |   2 +-
 7 files changed, 182 insertions(+), 192 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index ef43e3e..213a2bd 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -193,23 +193,17 @@ impl Value {
         Ref::map(self.as_internal(), ValueInternal::as_nf)
     }
 
-    /// WARNING: avoid normalizing any thunk while holding on to this ref
-    /// or you could run into BorrowMut panics
-    /// TODO: deprecated because of misleading name
-    pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
-        self.as_whnf()
-    }
-
-    /// WARNING: avoid normalizing any thunk while holding on to this ref
-    /// or you could run into BorrowMut panics
+    /// 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: deprecated because of misleading name
-    pub(crate) fn to_valuef(&self) -> ValueF {
-        self.as_valuef().clone()
+    /// 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(
@@ -275,14 +269,19 @@ impl TypedValue {
         TypedValue(Value::from_valuef_and_type(v, t))
     }
 
-    pub(crate) fn to_valuef(&self) -> ValueF {
-        self.0.to_valuef()
+    /// 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.to_valuef().normalize_to_expr()
+        self.as_whnf().normalize_to_expr()
     }
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
-        self.to_valuef().normalize_to_expr_maybe_alpha(true)
+        self.as_whnf().normalize_to_expr_maybe_alpha(true)
     }
     pub(crate) fn to_value(&self) -> Value {
         self.0.clone()
@@ -294,8 +293,7 @@ impl TypedValue {
         Typed::from_typedvalue(self)
     }
     pub(crate) fn as_const(&self) -> Option<Const> {
-        // TODO: avoid clone
-        match &self.to_valuef() {
+        match &*self.as_whnf() {
             ValueF::Const(c) => Some(*c),
             _ => None,
         }
@@ -357,14 +355,14 @@ impl Subst<Typed> for TypedValue {
 
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
-        *self.as_valuef() == *other.as_valuef()
+        *self.as_whnf() == *other.as_whnf()
     }
 }
 impl std::cmp::Eq for Value {}
 
 impl std::cmp::PartialEq for TypedValue {
     fn eq(&self, other: &Self) -> bool {
-        self.to_valuef() == other.to_valuef()
+        &*self.as_whnf() == &*other.as_whnf()
     }
 }
 impl std::cmp::Eq for TypedValue {}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 9e6e8c8..0ba1d59 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -12,8 +12,9 @@ use crate::phase::{Normalized, Typed};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
 /// normalized on-demand.
-/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence
-/// (normalization). Equality will normalize as needed.
+/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
+/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
+/// recursively normalize as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum ValueF {
     /// Closures
@@ -348,7 +349,7 @@ impl Subst<Typed> 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_valuef(),
+            ValueF::Var(v) if v == var => val.to_whnf(),
             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 8f6ff51..34a89c0 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -4,7 +4,7 @@ use dhall_syntax::{BinOp, Import, Label, ParseError, V};
 
 use crate::core::context::TypecheckContext;
 use crate::phase::resolve::ImportStack;
-use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
+use crate::phase::{NormalizedSubExpr, Type, Typed};
 
 pub type Result<T> = std::result::Result<T, Error>;
 
@@ -48,24 +48,24 @@ pub struct TypeError {
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
     UnboundVariable(V<Label>),
-    InvalidInputType(Normalized),
-    InvalidOutputType(Normalized),
+    InvalidInputType(Typed),
+    InvalidOutputType(Typed),
     NotAFunction(Typed),
-    TypeMismatch(Typed, Normalized, Typed),
-    AnnotMismatch(Typed, Normalized),
+    TypeMismatch(Typed, Typed, Typed),
+    AnnotMismatch(Typed, Typed),
     Untyped,
     FieldCollision(Label),
-    InvalidListElement(usize, Normalized, Typed),
-    InvalidListType(Normalized),
-    InvalidOptionalType(Normalized),
+    InvalidListElement(usize, Typed, Typed),
+    InvalidListType(Typed),
+    InvalidOptionalType(Typed),
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
     InvalidFieldType(Label, Type),
-    NotARecord(Label, Normalized),
+    NotARecord(Label, Typed),
     MustCombineRecord(Typed),
     MissingRecordField(Label, Typed),
-    MissingUnionField(Label, Normalized),
+    MissingUnionField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
     InvalidTextInterpolation(Typed),
     Merge1ArgMustBeRecord(Typed),
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index c18f976..a38e9d3 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,4 +1,5 @@
 use std::borrow::Cow;
+use std::cell::Ref;
 use std::fmt::Display;
 use std::path::Path;
 
@@ -111,8 +112,13 @@ impl Typed {
         Typed::from_const(Const::Type)
     }
 
-    pub(crate) fn to_valuef(&self) -> ValueF {
-        self.0.to_valuef()
+    /// 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 fn to_expr(&self) -> NormalizedSubExpr {
         self.0.to_expr()
@@ -134,9 +140,6 @@ impl Typed {
     pub(crate) fn into_typedvalue(self) -> TypedValue {
         self.0
     }
-    pub(crate) fn to_normalized(&self) -> Normalized {
-        self.clone().normalize()
-    }
     pub(crate) fn as_const(&self) -> Option<Const> {
         self.0.as_const()
     }
@@ -229,7 +232,7 @@ impl std::hash::Hash for Normalized {
 impl Eq for Typed {}
 impl PartialEq for Typed {
     fn eq(&self, other: &Self) -> bool {
-        self.to_valuef() == other.to_valuef()
+        self.0 == other.0
     }
 }
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 6c65e43..785a75f 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -68,23 +68,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             r,
             EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())),
         )),
-        (NaturalIsZero, [n, r..]) => match &*n.as_valuef() {
+        (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
             _ => Err(()),
         },
-        (NaturalEven, [n, r..]) => match &*n.as_valuef() {
+        (NaturalEven, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
             _ => Err(()),
         },
-        (NaturalOdd, [n, r..]) => match &*n.as_valuef() {
+        (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
             _ => Err(()),
         },
-        (NaturalToInteger, [n, r..]) => match &*n.as_valuef() {
+        (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
             _ => Err(()),
         },
-        (NaturalShow, [n, r..]) => match &*n.as_valuef() {
+        (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
@@ -92,7 +92,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             _ => Err(()),
         },
         (NaturalSubtract, [a, b, r..]) => {
-            match (&*a.as_valuef(), &*b.as_valuef()) {
+            match (&*a.as_whnf(), &*b.as_whnf()) {
                 (NaturalLit(a), NaturalLit(b)) => {
                     Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
                 }
@@ -102,7 +102,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 _ => Err(()),
             }
         }
-        (IntegerShow, [n, r..]) => match &*n.as_valuef() {
+        (IntegerShow, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
@@ -113,18 +113,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => Err(()),
         },
-        (IntegerToDouble, [n, r..]) => match &*n.as_valuef() {
+        (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
             _ => Err(()),
         },
-        (DoubleShow, [n, r..]) => match &*n.as_valuef() {
+        (DoubleShow, [n, r..]) => match &*n.as_whnf() {
             DoubleLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
             )),
             _ => Err(()),
         },
-        (TextShow, [v, r..]) => match &*v.as_valuef() {
+        (TextShow, [v, r..]) => match &*v.as_whnf() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -158,33 +158,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => Err(()),
         },
-        (ListLength, [_, l, r..]) => match &*l.as_valuef() {
+        (ListLength, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(_) => Ok((r, NaturalLit(0))),
             NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
             _ => Err(()),
         },
-        (ListHead, [_, l, r..]) => match &*l.as_valuef() {
+        (ListHead, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListLast, [_, l, r..]) => match &*l.as_valuef() {
+        (ListLast, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
             }
             _ => Err(()),
         },
-        (ListReverse, [_, l, r..]) => match &*l.as_valuef() {
+        (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
             NEListLit(xs) => {
                 Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
             }
             _ => Err(()),
         },
-        (ListIndexed, [_, l, r..]) => match &*l.as_valuef() {
+        (ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
             EmptyListLit(t) => {
                 let mut kts = HashMap::new();
                 kts.insert(
@@ -210,11 +210,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => Err(()),
         },
-        (ListBuild, [t, f, r..]) => match &*f.as_valuef() {
+        (ListBuild, [t, f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(ListFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_valuef()))
+                    Ok((r, args[1].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -237,8 +237,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                     )),
             )),
         },
-        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() {
-            EmptyListLit(_) => Ok((r, nil.to_valuef())),
+        (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
+            EmptyListLit(_) => Ok((r, nil.to_whnf())),
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().rev() {
@@ -248,15 +248,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         .app_value(v)
                         .into_value();
                 }
-                Ok((r, v.to_valuef()))
+                Ok((r, v.to_whnf()))
             }
             _ => Err(()),
         },
-        (OptionalBuild, [t, f, r..]) => match &*f.as_valuef() {
+        (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(OptionalFold, args) => {
                 if args.len() >= 2 {
-                    Ok((r, args[1].to_valuef()))
+                    Ok((r, args[1].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -273,18 +273,16 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 )),
             )),
         },
-        (OptionalFold, [_, v, _, just, nothing, r..]) => {
-            match &*v.as_valuef() {
-                EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())),
-                NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
-                _ => Err(()),
-            }
-        }
-        (NaturalBuild, [f, r..]) => match &*f.as_valuef() {
+        (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
+            EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
+            NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
+            _ => Err(()),
+        },
+        (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
             // fold/build fusion
             ValueF::AppliedBuiltin(NaturalFold, args) => {
                 if !args.is_empty() {
-                    Ok((r, args[0].to_valuef()))
+                    Ok((r, args[0].to_whnf()))
                 } else {
                     // Do we really need to handle this case ?
                     unimplemented!()
@@ -297,8 +295,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                     .app_valuef(NaturalLit(0)),
             )),
         },
-        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() {
-            NaturalLit(0) => Ok((r, zero.to_valuef())),
+        (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
+            NaturalLit(0) => Ok((r, zero.to_whnf())),
             NaturalLit(n) => {
                 let fold = ValueF::from_builtin(NaturalFold)
                     .app(NaturalLit(n - 1))
@@ -326,11 +324,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
 pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
     let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
 
-    let f_borrow = f.as_valuef();
+    let f_borrow = f.as_whnf();
     match &*f_borrow {
         ValueF::Lam(x, _, e) => {
             let val = Typed::from_value_untyped(a);
-            e.subst_shift(&x.into(), &val).to_valuef()
+            e.subst_shift(&x.into(), &val).to_whnf()
         }
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
@@ -362,7 +360,7 @@ pub(crate) fn squash_textlit(
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => {
-                    let e_borrow = e.as_valuef();
+                    let e_borrow = e.as_whnf();
                     match &*e_borrow {
                         ValueF::TextLit(elts2) => {
                             inner(elts2.iter().cloned(), crnt_str, ret)
@@ -520,8 +518,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
     };
-    let x_borrow = x.as_valuef();
-    let y_borrow = y.as_valuef();
+    let x_borrow = x.as_whnf();
+    let y_borrow = y.as_whnf();
     Some(match (o, &*x_borrow, &*y_borrow) {
         (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
         (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
@@ -678,7 +676,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
         ExprF::EmptyListLit(ref t) => {
             // Check if the type is of the form `List x`
-            let t_borrow = t.as_valuef();
+            let t_borrow = t.as_whnf();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
                     Ret::ValueF(EmptyListLit(
@@ -718,13 +716,13 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
             }
         }
         ExprF::BoolIf(ref b, ref e1, ref e2) => {
-            let b_borrow = b.as_valuef();
+            let b_borrow = b.as_whnf();
             match &*b_borrow {
                 BoolLit(true) => Ret::ValueRef(e1),
                 BoolLit(false) => Ret::ValueRef(e2),
                 _ => {
-                    let e1_borrow = e1.as_valuef();
-                    let e2_borrow = e2.as_valuef();
+                    let e1_borrow = e1.as_whnf();
+                    let e2_borrow = e2.as_whnf();
                     match (&*e1_borrow, &*e2_borrow) {
                         // Simplify `if b then True else False`
                         (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
@@ -748,7 +746,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
             Ret::ValueF(RecordLit(HashMap::new()))
         }
         ExprF::Projection(ref v, ref ls) => {
-            let v_borrow = v.as_valuef();
+            let v_borrow = v.as_whnf();
             match &*v_borrow {
                 RecordLit(kvs) => Ret::ValueF(RecordLit(
                     ls.iter()
@@ -764,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
             }
         }
         ExprF::Field(ref v, ref l) => {
-            let v_borrow = v.as_valuef();
+            let v_borrow = v.as_whnf();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
                     Some(r) => Ret::Value(r.clone()),
@@ -784,8 +782,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         }
 
         ExprF::Merge(ref handlers, ref variant, _) => {
-            let handlers_borrow = handlers.as_valuef();
-            let variant_borrow = variant.as_valuef();
+            let handlers_borrow = handlers.as_whnf();
+            let variant_borrow = variant.as_whnf();
             match (&*handlers_borrow, &*variant_borrow) {
                 (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
                     Some(h) => Ret::Value(h.clone()),
@@ -814,8 +812,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
 
     match ret {
         Ret::ValueF(v) => v,
-        Ret::Value(th) => th.to_valuef(),
-        Ret::ValueRef(th) => th.to_valuef(),
+        Ret::Value(th) => th.as_whnf().clone(),
+        Ret::ValueRef(th) => th.as_whnf().clone(),
         Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4154afe..c303ada 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -22,12 +22,7 @@ fn tck_pi_type(
 
     let ka = match tx.get_type()?.as_const() {
         Some(k) => k,
-        _ => {
-            return Err(TypeError::new(
-                ctx,
-                InvalidInputType(tx.to_normalized()),
-            ))
-        }
+        _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
     };
 
     let kb = match te.get_type()?.as_const() {
@@ -35,7 +30,7 @@ fn tck_pi_type(
         _ => {
             return Err(TypeError::new(
                 &ctx2,
-                InvalidOutputType(te.get_type()?.to_normalized()),
+                InvalidOutputType(te.get_type()?.into_owned()),
             ))
         }
     };
@@ -415,18 +410,14 @@ fn type_last_layer(
         }
         App(f, a) => {
             let tf = f.get_type()?;
-            let (x, tx, tb) = match &tf.to_valuef() {
+            let (x, tx, tb) = match &*tf.as_whnf() {
                 ValueF::Pi(x, tx, tb) => {
                     (x.clone(), tx.to_type(), tb.to_type())
                 }
                 _ => return Err(mkerr(NotAFunction(f.clone()))),
             };
             if a.get_type()?.as_ref() != &tx {
-                return Err(mkerr(TypeMismatch(
-                    f.clone(),
-                    tx.to_normalized(),
-                    a.clone(),
-                )));
+                return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone())));
             }
 
             Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a)))
@@ -434,13 +425,13 @@ fn type_last_layer(
         Annot(x, t) => {
             let t = t.to_type();
             if &t != x.get_type()?.as_ref() {
-                return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized())));
+                return Err(mkerr(AnnotMismatch(x.clone(), t)));
             }
             Ok(RetTypeOnly(x.get_type()?.into_owned()))
         }
         Assert(t) => {
-            match t.to_valuef() {
-                ValueF::Equivalence(ref x, ref y) if x == y => {}
+            match &*t.as_whnf() {
+                ValueF::Equivalence(x, y) if x == y => {}
                 ValueF::Equivalence(x, y) => {
                     return Err(mkerr(AssertMismatch(
                         x.to_typed(),
@@ -472,14 +463,11 @@ fn type_last_layer(
         }
         EmptyListLit(t) => {
             let t = t.to_type();
-            match &t.to_valuef() {
+            match &*t.as_whnf() {
                 ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args)
                     if args.len() == 1 => {}
                 _ => {
-                    return Err(TypeError::new(
-                        ctx,
-                        InvalidListType(t.to_normalized()),
-                    ))
+                    return Err(TypeError::new(ctx, InvalidListType(t.clone())))
                 }
             }
             Ok(RetTypeOnly(t))
@@ -491,7 +479,7 @@ fn type_last_layer(
                 if x.get_type()? != y.get_type()? {
                     return Err(mkerr(InvalidListElement(
                         i,
-                        x.get_type()?.to_normalized(),
+                        x.get_type()?.into_owned(),
                         y.clone(),
                     )));
                 }
@@ -500,14 +488,14 @@ fn type_last_layer(
             if t.get_type()?.as_const() != Some(Type) {
                 return Err(TypeError::new(
                     ctx,
-                    InvalidListType(t.to_normalized()),
+                    InvalidListType(t.into_owned()),
                 ));
             }
 
             Ok(RetTypeOnly(
                 Typed::from_value_and_type(
                     ValueF::from_builtin(dhall_syntax::Builtin::List)
-                        .app(t.to_valuef())
+                        .app_value(t.to_value())
                         .into_value(),
                     Typed::from_const(Type),
                 )
@@ -517,16 +505,13 @@ fn type_last_layer(
         SomeLit(x) => {
             let t = x.get_type()?.into_owned();
             if t.get_type()?.as_const() != Some(Type) {
-                return Err(TypeError::new(
-                    ctx,
-                    InvalidOptionalType(t.to_normalized()),
-                ));
+                return Err(TypeError::new(ctx, InvalidOptionalType(t)));
             }
 
             Ok(RetTypeOnly(
                 Typed::from_value_and_type(
                     ValueF::from_builtin(dhall_syntax::Builtin::Optional)
-                        .app(t.to_valuef())
+                        .app_value(t.to_value())
                         .into_value(),
                     Typed::from_const(Type).into_type(),
                 )
@@ -551,7 +536,7 @@ fn type_last_layer(
             .into_type(),
         )),
         Field(r, x) => {
-            match &r.get_type()?.to_valuef() {
+            match &*r.get_type()?.as_whnf() {
                 ValueF::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => {
                         Ok(RetTypeOnly(tth.to_type()))
@@ -561,8 +546,7 @@ fn type_last_layer(
                 },
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
-                    let r = r.to_type();
-                    match &r.to_valuef() {
+                    match &*r.as_whnf() {
                         ValueF::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(t)) => {
@@ -581,21 +565,21 @@ fn type_last_layer(
                             None => {
                                 Err(mkerr(MissingUnionField(
                                     x.clone(),
-                                    r.to_normalized(),
+                                    r.clone(),
                                 )))
                             },
                         },
                         _ => {
                             Err(mkerr(NotARecord(
                                 x.clone(),
-                                r.to_normalized()
+                                r.clone()
                             )))
                         },
                     }
                 }
                 // _ => Err(mkerr(NotARecord(
                 //     x,
-                //     r.to_type()?.to_normalized(),
+                //     r.to_type()?,
                 // ))),
             }
         }
@@ -633,20 +617,22 @@ fn type_last_layer(
             }
 
             // Extract the LHS record type
-            let kts_x = match l_type.to_valuef() {
+            let l_type_borrow = l_type.as_whnf();
+            let kts_x = match &*l_type_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(l.clone()))),
             };
 
             // Extract the RHS record type
-            let kts_y = match r_type.to_valuef() {
+            let r_type_borrow = r_type.as_whnf();
+            let kts_y = match &*r_type_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(r.clone()))),
             };
 
             // Union the two records, prefering
             // the values found in the RHS.
-            let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone());
+            let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
 
             // Construct the final record type from the union
             Ok(RetTypeOnly(
@@ -662,8 +648,8 @@ 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>,
+                kts_l: &HashMap<Label, TypedValue>,
+                kts_r: &HashMap<Label, TypedValue>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::outer_join;
 
@@ -674,7 +660,7 @@ fn type_last_layer(
                                inner_l: &TypedValue,
                                inner_r: &TypedValue|
                  -> Result<Typed, TypeError> {
-                    match (inner_l.to_valuef(), inner_r.to_valuef()) {
+                    match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) {
                         (
                             ValueF::RecordType(inner_l_kvs),
                             ValueF::RecordType(inner_r_kvs),
@@ -690,11 +676,9 @@ fn type_last_layer(
                 let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
                     |l| Ok(l.to_type()),
                     |r| Ok(r.to_type()),
-                    |k: &Label, l: &TypedValue, r: &TypedValue| {
-                        combine(k, l, r)
-                    },
-                    &kts_l,
-                    &kts_r,
+                    combine,
+                    kts_l,
+                    kts_r,
                 );
 
                 Ok(tck_record_type(
@@ -717,13 +701,15 @@ fn type_last_layer(
             }
 
             // Extract the LHS record type
-            let kts_x = match l_type.to_valuef() {
+            let l_type_borrow = l_type.as_whnf();
+            let kts_x = match &*l_type_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(l.clone()))),
             };
 
             // Extract the RHS record type
-            let kts_y = match r_type.to_valuef() {
+            let r_type_borrow = r_type.as_whnf();
+            let kts_y = match &*r_type_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(MustCombineRecord(r.clone()))),
             };
@@ -735,8 +721,8 @@ 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>,
+                kts_l: &HashMap<Label, TypedValue>,
+                kts_r: &HashMap<Label, TypedValue>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::intersection_with_key;
 
@@ -747,7 +733,7 @@ fn type_last_layer(
                                kts_l_inner: &TypedValue,
                                kts_r_inner: &TypedValue|
                  -> Result<Typed, TypeError> {
-                    match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) {
+                    match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) {
                         (
                             ValueF::RecordType(kvs_l_inner),
                             ValueF::RecordType(kvs_r_inner),
@@ -760,13 +746,7 @@ fn type_last_layer(
                     }
                 };
 
-                let kts = intersection_with_key(
-                    |k: &Label, l: &TypedValue, r: &TypedValue| {
-                        combine(k, l, r)
-                    },
-                    &kts_l,
-                    &kts_r,
-                );
+                let kts = intersection_with_key(combine, kts_l, kts_r);
 
                 Ok(tck_record_type(
                     ctx,
@@ -776,8 +756,8 @@ fn type_last_layer(
             };
 
             // Extract the Const of the LHS
-            let k_l = match l.get_type()?.to_valuef() {
-                ValueF::Const(k) => k,
+            let k_l = match l.get_type()?.as_const() {
+                Some(k) => k,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         l.clone(),
@@ -786,8 +766,8 @@ fn type_last_layer(
             };
 
             // Extract the Const of the RHS
-            let k_r = match r.get_type()?.to_valuef() {
-                ValueF::Const(k) => k,
+            let k_r = match r.get_type()?.as_const() {
+                Some(k) => k,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
                         r.clone(),
@@ -808,7 +788,8 @@ fn type_last_layer(
             };
 
             // Extract the LHS record type
-            let kts_x = match l.to_valuef() {
+            let borrow_l = l.as_whnf();
+            let kts_x = match &*borrow_l {
                 ValueF::RecordType(kts) => kts,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
@@ -818,7 +799,8 @@ fn type_last_layer(
             };
 
             // Extract the RHS record type
-            let kts_y = match r.to_valuef() {
+            let borrow_r = r.as_whnf();
+            let kts_y = match &*borrow_r {
                 ValueF::RecordType(kts) => kts,
                 _ => {
                     return Err(mkerr(RecordTypeMergeRequiresRecordType(
@@ -833,7 +815,7 @@ fn type_last_layer(
                 .and(Ok(RetTypeOnly(Typed::from_const(k))))
         }
         BinOp(o @ ListAppend, l, r) => {
-            match l.get_type()?.to_valuef() {
+            match &*l.get_type()?.as_whnf() {
                 ValueF::AppliedBuiltin(List, _) => {}
                 _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
             }
@@ -895,56 +877,63 @@ fn type_last_layer(
             Ok(RetTypeOnly(t))
         }
         Merge(record, union, type_annot) => {
-            let handlers = match record.get_type()?.to_valuef() {
+            let record_type = record.get_type()?;
+            let record_borrow = record_type.as_whnf();
+            let handlers = match &*record_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))),
             };
 
-            let variants = match union.get_type()?.to_valuef() {
+            let union_type = union.get_type()?;
+            let union_borrow = union_type.as_whnf();
+            let variants = match &*union_borrow {
                 ValueF::UnionType(kts) => kts,
                 _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))),
             };
 
             let mut inferred_type = None;
-            for (x, handler) in handlers.iter() {
-                let handler_return_type = match variants.get(x) {
-                    // Union alternative with type
-                    Some(Some(variant_type)) => {
-                        let variant_type = variant_type.to_type();
-                        let handler_type = handler.to_type();
-                        let (x, tx, tb) = match &handler_type.to_valuef() {
-                            ValueF::Pi(x, tx, tb) => {
-                                (x.clone(), tx.to_type(), tb.to_type())
+            for (x, handler) in handlers {
+                let handler_return_type =
+                    match variants.get(x) {
+                        // Union alternative with type
+                        Some(Some(variant_type)) => {
+                            let variant_type = variant_type.to_type();
+                            let handler_type = handler.to_type();
+                            let (x, tx, tb) = match &*handler_type.as_whnf() {
+                                ValueF::Pi(x, tx, tb) => {
+                                    (x.clone(), tx.to_type(), tb.to_type())
+                                }
+                                _ => {
+                                    return Err(mkerr(NotAFunction(
+                                        handler_type.clone(),
+                                    )))
+                                }
+                            };
+
+                            if &variant_type != &tx {
+                                return Err(mkerr(TypeMismatch(
+                                    handler_type,
+                                    tx,
+                                    variant_type,
+                                )));
                             }
-                            _ => return Err(mkerr(NotAFunction(handler_type))),
-                        };
-
-                        if &variant_type != &tx {
-                            return Err(mkerr(TypeMismatch(
-                                handler_type,
-                                tx.to_normalized(),
-                                variant_type,
-                            )));
-                        }
 
-                        // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
-                        match tb.over_binder(x) {
-                            Some(x) => x,
-                            None => {
-                                return Err(mkerr(
+                            // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+                            match tb.over_binder(x) {
+                                Some(x) => x,
+                                None => return Err(mkerr(
                                     MergeHandlerReturnTypeMustNotBeDependent,
-                                ))
+                                )),
                             }
                         }
-                    }
-                    // Union alternative without type
-                    Some(None) => handler.to_type(),
-                    None => {
-                        return Err(mkerr(MergeHandlerMissingVariant(
-                            x.clone(),
-                        )))
-                    }
-                };
+                        // Union alternative without type
+                        Some(None) => handler.to_type(),
+                        None => {
+                            return Err(mkerr(MergeHandlerMissingVariant(
+                                x.clone(),
+                            )))
+                        }
+                    };
                 match &inferred_type {
                     None => inferred_type = Some(handler_return_type),
                     Some(t) => {
@@ -974,8 +963,9 @@ fn type_last_layer(
             }
         }
         Projection(record, labels) => {
-            let trecord = record.get_type()?;
-            let kts = match trecord.to_valuef() {
+            let record_type = record.get_type()?;
+            let record_borrow = record_type.as_whnf();
+            let kts = match &*record_borrow {
                 ValueF::RecordType(kts) => kts,
                 _ => return Err(mkerr(ProjectionMustBeRecord)),
             };
@@ -991,7 +981,7 @@ fn type_last_layer(
             Ok(RetTypeOnly(
                 Typed::from_value_and_type(
                     ValueF::RecordType(new_kts).into_value(),
-                    trecord.get_type()?.into_owned(),
+                    record_type.get_type()?.into_owned(),
                 )
                 .to_type(),
             ))
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 70cff46..44e22e4 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()?.to_normalized();
+                    let ty = expr.get_type()?.into_owned().normalize();
                     assert_eq_display!(ty, expected);
                 }
                 Normalization => {
-- 
cgit v1.2.3