2 files changed, 51 insertions, 36 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c89e147..f2bae80 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -163,7 +163,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
             [_, NEListLit(xs), _, cons, nil] => {
                 let mut v = nil;
                 for x in xs.into_iter().rev() {
-                    v = cons.clone().app(x.normalize_whnf().clone()).app(v);
+                    v = cons.clone().app_thunk(x).app(v);
                 }
                 v
             }
@@ -197,7 +197,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value {
                 nothing
             },
             [_, NEOptionalLit(x), _, just, _] => {
-                just.app(x.normalize_whnf().clone())
+                just.app_thunk(x)
             }
         ),
         NaturalBuild => improved_slice_patterns::match_vec!(args;
@@ -678,43 +678,59 @@ impl Value {
 
     /// Apply to a value
     pub(crate) fn app(self, val: Value) -> Value {
-        match (self, val) {
-            (Value::Lam(x, _, e), val) => {
-                let val = Typed(
-                    Thunk::from_whnf(val),
-                    None,
-                    std::marker::PhantomData,
-                );
+        self.app_thunk(val.into_thunk())
+    }
+
+    /// Apply to a thunk
+    pub(crate) fn app_thunk(self, th: Thunk) -> Value {
+        // If nothing else matches, convert to Expr
+        let fallback = |f: Value, a: Thunk| {
+            Value::Expr(rc(ExprF::App(
+                f.normalize_to_expr(),
+                a.normalize_whnf().normalize_to_expr(),
+            )))
+        };
+
+        match self {
+            Value::Lam(x, _, e) => {
+                let val = Typed(th, None, std::marker::PhantomData);
                 e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
             }
-            (Value::AppliedBuiltin(b, mut args), val) => {
-                args.push(val);
+            Value::AppliedBuiltin(b, mut args) => {
+                args.push(th.normalize_whnf().clone());
                 apply_builtin(b, args)
             }
-            (Value::OptionalSomeClosure(_), val) => {
-                Value::NEOptionalLit(Thunk::from_whnf(val))
-            }
-            (Value::ListConsClosure(t, None), val) => {
-                Value::ListConsClosure(t, Some(Thunk::from_whnf(val)))
+            Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th),
+            Value::ListConsClosure(t, None) => {
+                Value::ListConsClosure(t, Some(th))
             }
-            (Value::ListConsClosure(_, Some(x)), Value::EmptyListLit(_)) => {
-                Value::NEListLit(vec![x])
-            }
-            (Value::ListConsClosure(_, Some(x)), Value::NEListLit(mut xs)) => {
-                xs.insert(0, x);
-                Value::NEListLit(xs)
-            }
-            (Value::NaturalSuccClosure, Value::NaturalLit(n)) => {
-                Value::NaturalLit(n + 1)
+            Value::ListConsClosure(t, Some(x)) => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::EmptyListLit(_) => Value::NEListLit(vec![x]),
+                    Value::NEListLit(xs) => {
+                        let mut xs = xs.clone();
+                        xs.insert(0, x);
+                        Value::NEListLit(xs)
+                    }
+                    _ => {
+                        drop(v);
+                        fallback(Value::ListConsClosure(t, Some(x)), th)
+                    }
+                }
             }
-            (Value::UnionConstructor(l, kts), val) => {
-                Value::UnionLit(l, Thunk::from_whnf(val), kts)
+            Value::NaturalSuccClosure => {
+                let v = th.normalize_whnf();
+                match &*v {
+                    Value::NaturalLit(n) => Value::NaturalLit(n + 1),
+                    _ => {
+                        drop(v);
+                        fallback(Value::NaturalSuccClosure, th)
+                    }
+                }
             }
-            // Can't do anything useful, convert to expr
-            (f, a) => Value::Expr(rc(ExprF::App(
-                f.normalize_to_expr(),
-                a.normalize_to_expr(),
-            ))),
+            Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts),
+            f => fallback(f, th),
         }
     }
 
@@ -1323,8 +1339,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
                 UnionLit(l, v, kts) => match handlers.remove(&l) {
                     Some(h) => {
                         let h = h.normalize_whnf().clone();
-                        let v = v.normalize_whnf().clone();
-                        return h.app(v);
+                        return h.app_thunk(v);
                     }
                     None => UnionLit(l, v, kts),
                 },
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 461f1cc..fb698d0 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -693,7 +693,7 @@ impl TypeIntermediate {
                 );
                 Typed(
                     Value::from_builtin(Builtin::List)
-                        .app(t.clone().normalize_whnf()?)
+                        .app(t.normalize_whnf()?)
                         .into_thunk(),
                     Some(const_to_type(Const::Type)),
                     PhantomData,
@@ -709,7 +709,7 @@ impl TypeIntermediate {
                 );
                 Typed(
                     Value::from_builtin(Builtin::Optional)
-                        .app(t.clone().normalize_whnf()?)
+                        .app(t.normalize_whnf()?)
                         .into_thunk(),
                     Some(const_to_type(Const::Type)),
                     PhantomData,