Fix a bunch of bugs and more tck

2 files changed, 45 insertions, 29 deletions

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c8be3a3..a42265d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::tck::typecheck::TyEnv;
 use crate::semantics::Value;
 use crate::syntax::{ExprKind, Label, Span, V};
 
@@ -48,6 +49,15 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         tyexpr_to_expr(self, opts, &mut Vec::new())
     }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        let opts = ToExprOptions {
+            normalize: true,
+            alpha: false,
+        };
+        let env = env.as_nameenv().names();
+        let mut env = env.iter().collect();
+        tyexpr_to_expr(self, opts, &mut env)
+    }
     // TODO: temporary hack
     pub fn to_value(&self) -> Value {
         todo!()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b64d28..4ca5d4d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -275,10 +275,22 @@ fn type_one_layer(
         }
         ExprKind::Annot(x, t) => {
             let t = t.normalize_whnf(env.as_nzenv());
-            if x.get_type()? != t {
-                return mkerr("annot mismatch");
+            let x_ty = x.get_type()?;
+            if x_ty != t {
+                return mkerr(format!(
+                    "annot mismatch: ({} : {}) : {}",
+                    x.to_expr_tyenv(env),
+                    x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+                    t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                ));
+                // return mkerr(format!(
+                //     "annot mismatch: {} != {}",
+                //     x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+                //     t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                // ));
+                // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
-            t
+            x_ty
         }
         ExprKind::App(f, arg) => {
             let tf = f.get_type()?;
@@ -389,35 +401,29 @@ fn type_one_layer(
             let yk = y.get_type()?.as_const().unwrap();
             Value::from_const(max(xk, yk))
         }
-        // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
-        //     match &*l.get_type()?.as_whnf() {
-        //         ValueKind::AppliedBuiltin(List, _, _) => {}
-        //         _ => return mkerr("BinOpTypeMismatch"),
-        //     }
-
-        //     if l.get_type()? != r.get_type()? {
-        //         return mkerr("BinOpTypeMismatch");
-        //     }
+        ExprKind::BinOp(BinOp::ListAppend, l, r) => {
+            let l_ty = l.get_type()?;
+            match &*l_ty.as_whnf() {
+                ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+                _ => return mkerr("BinOpTypeMismatch"),
+            }
 
-        //     l.get_type()?
-        // }
-        // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-        //     if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-        //         return mkerr("EquivalenceArgumentMustBeTerm");
-        //     }
-        //     if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-        //         return mkerr("EquivalenceArgumentMustBeTerm");
-        //     }
+            if l_ty != r.get_type()? {
+                return mkerr("BinOpTypeMismatch");
+            }
 
-        //     if l.get_type()? != r.get_type()? {
-        //         return mkerr("EquivalenceTypeMismatch");
-        //     }
+            l_ty
+        }
+        ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+            if l.get_type()? != r.get_type()? {
+                return mkerr("EquivalenceTypeMismatch");
+            }
+            if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("EquivalenceArgumentsMustBeTerms");
+            }
 
-        //     RetWhole(Value::from_kind_and_type(
-        //         ValueKind::Equivalence(l.clone(), r.clone()),
-        //         Value::from_const(Type),
-        //     ))
-        // }
+            Value::from_const(Const::Type)
+        }
         ExprKind::BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
                 BinOp::BoolAnd