Remove most TyExpr from normalization

3 files changed, 9 insertions, 21 deletions

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index b3e7895..af955f4 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    pub fn new() -> Self {
-        VarEnv { size: 0 }
-    }
+    // pub fn new() -> Self {
+    //     VarEnv { size: 0 }
+    // }
     pub fn size(&self) -> usize {
         self.size
     }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index fa578c0..29099c5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{
-    rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
-};
-use crate::syntax::{ExprKind, Span, V};
+use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
+use crate::syntax::{ExprKind, Span};
 use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -56,13 +54,10 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         self.to_hir().to_expr(opts)
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_hir().to_expr_tyenv(env)
-    }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.clone())
+        Value::new_thunk(env, self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 810e483..5b233f8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -266,17 +266,10 @@ fn type_one_layer(
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return span_err(&format!(
-                    "annot mismatch: ({} : {}) : {}",
-                    x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                    t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
+                    "annot mismatch: {} != {}",
+                    x_ty.to_expr_tyenv(env),
+                    t.to_expr_tyenv(env)
                 ));
-                // return span_err(format!(
-                //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                //     t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
-                // ));
-                // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
             x_ty
         }