Remove dead code

2 files changed, 8 insertions, 27 deletions

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index e4108ad..abb6fa8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
@@ -58,10 +57,6 @@ impl TyExpr {
         let mut env = env.iter().collect();
         tyexpr_to_expr(self, opts, &mut env)
     }
-    // TODO: temporary hack
-    pub fn to_value(&self) -> Value {
-        todo!()
-    }
 
     pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
         normalize_tyexpr_whnf(self, env)
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index abb36e1..99eb31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,12 +1,8 @@
-#![allow(dead_code)]
-#![allow(unreachable_code)]
-#![allow(unused_imports)]
 use std::borrow::Cow;
 use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
 use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
 use crate::semantics::phase::normalize::{merge_maps, NzEnv};
 use crate::semantics::phase::typecheck::{
@@ -14,12 +10,12 @@ use crate::semantics::phase::typecheck::{
 };
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+    Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
-    Span, UnspannedExpr, V,
+    Span, V,
 };
 
 #[derive(Debug, Clone)]
@@ -111,6 +107,8 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
 fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
@@ -503,20 +501,6 @@ fn type_one_layer(
                     Some(Some(variant_type)) => {
                         let handler_type_borrow = handler_type.as_whnf();
                         match &*handler_type_borrow {
-                            ValueKind::Pi(_, tx, tb) => {
-                                if variant_type != tx {
-                                    return mkerr("MergeHandlerTypeMismatch");
-                                }
-
-                                // Extract `tb` from under the binder. Fails if the variable was used
-                                // in `tb`.
-                                match tb.over_binder() {
-                                    Some(x) => x,
-                                    None => return mkerr(
-                                        "MergeHandlerReturnTypeMustNotBeDependent",
-                                    ),
-                                }
-                            }
                             ValueKind::PiClosure { closure, annot, .. } => {
                                 if variant_type != annot {
                                     // return mkerr("MergeHandlerTypeMismatch");
@@ -609,8 +593,7 @@ fn type_one_layer(
     })
 }
 
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
+/// `type_with` typechecks an expressio in the provided environment.
 pub(crate) fn type_with(
     env: &TyEnv,
     expr: &Expr<Normalized>,
@@ -689,10 +672,13 @@ pub(crate) fn type_with(
     Ok(TyExpr::new(tyekind, ty, expr.span()))
 }
 
+/// Typecheck an expression and return the expression annotated with types if type-checking
+/// succeeded, or an error if type-checking failed.
 pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
     type_with(&TyEnv::new(), e)
 }
 
+/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(
     expr: &Expr<Normalized>,
     ty: Expr<Normalized>,