Fix a bunch of bugs and more tck

1 files changed, 16 insertions, 10 deletions

diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 1aab736..18e70e4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     Value::from_kind_and_type(
         ValueKind::from_builtin(b),
-        typecheck(type_of_builtin(b)).unwrap(),
+        crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
+            .unwrap()
+            .normalize_whnf_noenv(),
     )
 }
 
@@ -380,17 +382,21 @@ fn type_last_layer(
         ExprKind::App(f, a) => {
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
-            let (tx, tb) = match &*tf_borrow {
-                ValueKind::Pi(_, tx, tb) => (tx, tb),
+            match &*tf_borrow {
+                ValueKind::Pi(_, tx, tb) => {
+                    if &a.get_type()? != tx {
+                        return mkerr("TypeMismatch");
+                    }
+
+                    let ret = tb.subst_shift(&AlphaVar::default(), a);
+                    ret.normalize_nf();
+                    RetTypeOnly(ret)
+                }
+                ValueKind::PiClosure { closure, .. } => {
+                    RetTypeOnly(closure.apply(a.clone()))
+                }
                 _ => return mkerr("NotAFunction"),
-            };
-            if &a.get_type()? != tx {
-                return mkerr("TypeMismatch");
             }
-
-            let ret = tb.subst_shift(&AlphaVar::default(), a);
-            ret.normalize_nf();
-            RetTypeOnly(ret)
         }
         ExprKind::Annot(x, t) => {
             if &x.get_type()? != t {