Remove dead code

8 files changed, 25 insertions, 1187 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 9749c50..8b13789 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,96 +1 @@
-use crate::error::TypeError;
-use crate::semantics::core::value::Value;
-use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Binder};
-use crate::semantics::nze::NzVar;
-// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
-use crate::syntax::{Label, V};
 
-#[derive(Debug, Clone)]
-enum CtxItem {
-    // Variable is bound with given type
-    Kept(Value),
-    // Variable has been replaced by corresponding value
-    Replaced(Value),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct TyCtx {
-    ctx: Vec<(Binder, CtxItem)>,
-}
-
-impl TyCtx {
-    pub fn new() -> Self {
-        TyCtx { ctx: Vec::new() }
-    }
-    fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
-        TyCtx { ctx: vec }
-    }
-    pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
-        let mut vec = self.ctx.clone();
-        vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
-        self.with_vec(vec)
-    }
-    pub fn insert_value(
-        &self,
-        x: &Binder,
-        e: Value,
-    ) -> Result<Self, TypeError> {
-        let mut vec = self.ctx.clone();
-        vec.push((x.clone(), CtxItem::Replaced(e)));
-        Ok(self.with_vec(vec))
-    }
-    pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
-        let mut var = var.clone();
-        let mut shift_delta: isize = 0;
-        let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
-        let found_item = loop {
-            if let Some((label, item)) = rev_ctx.next() {
-                var = match var.over_binder(&label) {
-                    Some(newvar) => newvar,
-                    None => break item,
-                };
-                if let CtxItem::Kept(_) = item {
-                    shift_delta += 1;
-                }
-            } else {
-                // Unbound variable
-                return None;
-            }
-        };
-        let var_idx = rev_ctx
-            .filter(|(_, i)| match i {
-                CtxItem::Kept(_) => true,
-                CtxItem::Replaced(_) => false,
-            })
-            .count();
-
-        let v = match found_item {
-            CtxItem::Kept(t) => Value::from_kind_and_type(
-                ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
-                t.clone(),
-            ),
-            CtxItem::Replaced(v) => v.clone()
-                // .normalize_whnf(&NzEnv::construct(
-                //     self.ctx
-                //         .iter()
-                //         .filter_map(|(_, i)| match i {
-                //             CtxItem::Kept(t) => {
-                //                 Some(NzEnvItem::Kept(t.clone()))
-                //             }
-                //             CtxItem::Replaced(_) => None,
-                //         })
-                //         .collect(),
-                // )),
-        };
-        // Can't fail because delta is positive
-        let v = v.shift(shift_delta, &AlphaVar::default()).unwrap();
-        return Some(v);
-    }
-    // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> {
-    //     self.lookup(&var.normal)
-    // }
-    pub fn new_binder(&self, l: &Label) -> Binder {
-        Binder::new(l.clone())
-    }
-}
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index aa819d2..30c4116 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -68,8 +68,6 @@ pub(crate) enum Closure {
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum ValueKind<Value> {
     /// Closures
-    Lam(Binder, Value, Value),
-    Pi(Binder, Value, Value),
     LamClosure {
         binder: Binder,
         annot: Value,
@@ -133,13 +131,6 @@ impl Value {
     pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value {
         Value::new(v, Unevaled, t, Span::Artificial)
     }
-    pub(crate) fn from_kind_and_type_and_span(
-        v: ValueKind<Value>,
-        t: Value,
-        span: Span,
-    ) -> Value {
-        Value::new(v, Unevaled, t, span)
-    }
     pub(crate) fn from_kind_and_type_whnf(
         v: ValueKind<Value>,
         t: Value,
@@ -155,10 +146,6 @@ impl Value {
     pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
         builtin_to_value_env(b, env)
     }
-    pub(crate) fn with_span(self, span: Span) -> Self {
-        self.as_internal_mut().span = span;
-        self
-    }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.as_whnf() {
@@ -238,10 +225,6 @@ impl Value {
 
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
-            ValueKind::Pi(_, t, e) => {
-                v.check_type(t);
-                e.subst_shift(&AlphaVar::default(), &v)
-            }
             ValueKind::PiClosure { annot, closure, .. } => {
                 v.check_type(annot);
                 closure.apply(v.clone())
@@ -276,9 +259,6 @@ impl Value {
     pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(self.as_internal().shift(delta, var)?.into_value())
     }
-    pub(crate) fn over_binder(&self) -> Option<Self> {
-        self.shift(-1, &AlphaVar::default())
-    }
     pub(crate) fn under_binder(&self) -> Self {
         // Can't fail since delta is positive
         self.shift(1, &AlphaVar::default()).unwrap()
@@ -398,10 +378,6 @@ impl Value {
                     | ValueKind::AppliedBuiltin(..)
                     | ValueKind::UnionConstructor(..)
                     | ValueKind::UnionLit(..) => unreachable!(),
-                    ValueKind::Lam(x, t, e) => {
-                        ExprKind::Lam(x.to_label(), t, e)
-                    }
-                    ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
                     ValueKind::Const(c) => ExprKind::Const(c),
                     ValueKind::BoolLit(b) => ExprKind::BoolLit(b),
                     ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n),
@@ -555,14 +531,6 @@ impl ValueKind<Value> {
             ValueKind::NEOptionalLit(th) => {
                 th.normalize_mut();
             }
-            ValueKind::Lam(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
-            ValueKind::Pi(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
             ValueKind::LamClosure { annot, .. }
             | ValueKind::PiClosure { annot, .. } => {
                 annot.normalize_mut();
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index 61a7d0b..aec66f8 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -72,14 +72,6 @@ where
 {
     use ValueKind::*;
     Ok(match input {
-        Lam(l, t, e) => {
-            let (t, e) = v.visit_binder(l, t, e)?;
-            Lam(l.clone(), t, e)
-        }
-        Pi(l, t, e) => {
-            let (t, e) = v.visit_binder(l, t, e)?;
-            Pi(l.clone(), t, e)
-        }
         LamClosure {
             binder,
             annot,
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 92ba8fd..043840e 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -1,76 +1,8 @@
-#![allow(dead_code)]
 use crate::semantics::core::var::AlphaVar;
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
-use crate::syntax::{Expr, ExprKind, Label, V};
+use crate::syntax::{Label, V};
 
-pub(crate) type Type = NzExpr;
-#[derive(Debug, Clone)]
-pub(crate) struct TypeError;
 pub(crate) type Binder = Label;
 
-// An expression with inferred types at every node and resolved variables.
-#[derive(Debug, Clone)]
-pub(crate) struct TyExpr {
-    kind: Box<TyExprKind>,
-    ty: Option<Type>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
-    Var(AlphaVar),
-    Expr(ExprKind<TyExpr, Normalized>),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct NzExpr {
-    kind: Box<NzExprKind>,
-    ty: Option<Box<Type>>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum NzExprKind {
-    Var {
-        var: NzVar,
-    },
-    Lam {
-        binder: Binder,
-        annot: NzExpr,
-        env: NzEnv,
-        body: TyExpr,
-    },
-    Pi {
-        binder: Binder,
-        annot: NzExpr,
-        env: NzEnv,
-        body: TyExpr,
-    },
-    Expr(ExprKind<NzExpr, Normalized>),
-    // Unevaled {
-    //     env: NzEnv,
-    //     expr: TyExprKind,
-    // },
-}
-
-#[derive(Debug, Clone)]
-enum NzEnvItem {
-    // Variable is bound with given type
-    Kept(Type),
-    // Variable has been replaced by corresponding value
-    Replaced(NzExpr),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct TyEnv {
-    names: NameEnv,
-    items: NzEnv,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
-    items: Vec<NzEnvItem>,
-}
-
 #[derive(Debug, Clone)]
 pub(crate) struct NameEnv {
     names: Vec<Binder>,
@@ -88,54 +20,6 @@ pub(crate) enum NzVar {
     /// Fake fresh variable generated for expression equality checking.
     Fresh(usize),
 }
-// TODO: temporary hopefully
-// impl std::cmp::PartialEq for NzVar {
-//     fn eq(&self, _other: &Self) -> bool {
-//         true
-//     }
-// }
-
-impl TyEnv {
-    pub fn new() -> Self {
-        TyEnv {
-            names: NameEnv::new(),
-            items: NzEnv::new(),
-        }
-    }
-    pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.names.as_quoteenv()
-    }
-    pub fn as_nzenv(&self) -> &NzEnv {
-        &self.items
-    }
-    pub fn as_nameenv(&self) -> &NameEnv {
-        &self.names
-    }
-
-    pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self {
-        TyEnv {
-            names: self.names.insert(x),
-            items: self.items.insert_type(t),
-        }
-    }
-    pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self {
-        TyEnv {
-            names: self.names.insert(x),
-            items: self.items.insert_value(e),
-        }
-    }
-    pub fn lookup_var(&self, var: &V<Binder>) -> Option<TyExpr> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.lookup_val(&var).get_type().unwrap();
-        Some(TyExpr::new(TyExprKind::Var(var), Some(ty)))
-    }
-    pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr {
-        self.items.lookup_val(var)
-    }
-    pub fn size(&self) -> usize {
-        self.names.size()
-    }
-}
 
 impl NameEnv {
     pub fn new() -> Self {
@@ -163,9 +47,9 @@ impl NameEnv {
     pub fn insert_mut(&mut self, x: &Binder) {
         self.names.push(x.clone())
     }
-    pub fn remove_mut(&mut self) {
-        self.names.pop();
-    }
+    // pub fn remove_mut(&mut self) {
+    //     self.names.pop();
+    // }
 
     pub fn unlabel_var(&self, var: &V<Binder>) -> Option<AlphaVar> {
         let V(name, idx) = var;
@@ -178,50 +62,17 @@ impl NameEnv {
             .nth(*idx)?;
         Some(AlphaVar::new(V((), idx)))
     }
-    pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
-        let name = &self.names[self.names.len() - 1 - var.idx()];
-        let idx = self
-            .names
-            .iter()
-            .rev()
-            .take(var.idx())
-            .filter(|n| *n == name)
-            .count();
-        V(name.clone(), idx)
-    }
-    pub fn size(&self) -> usize {
-        self.names.len()
-    }
-}
-
-impl NzEnv {
-    pub fn new() -> Self {
-        NzEnv { items: Vec::new() }
-    }
-
-    pub fn insert_type(&self, t: NzExpr) -> Self {
-        let mut env = self.clone();
-        env.items.push(NzEnvItem::Kept(t));
-        env
-    }
-    pub fn insert_value(&self, e: NzExpr) -> Self {
-        let mut env = self.clone();
-        env.items.push(NzEnvItem::Replaced(e));
-        env
-    }
-    pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr {
-        // TODO: use VarEnv
-        let idx = self.items.len() - 1 - var.idx();
-        match &self.items[idx] {
-            NzEnvItem::Kept(ty) => NzExpr::new(
-                NzExprKind::Var {
-                    var: NzVar::new(idx),
-                },
-                Some(ty.clone()),
-            ),
-            NzEnvItem::Replaced(x) => x.clone(),
-        }
-    }
+    // pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
+    //     let name = &self.names[self.names.len() - 1 - var.idx()];
+    //     let idx = self
+    //         .names
+    //         .iter()
+    //         .rev()
+    //         .take(var.idx())
+    //         .filter(|n| *n == name)
+    //         .count();
+    //     V(name.clone(), idx)
+    // }
 }
 
 // TODO: rename to VarEnv
@@ -229,9 +80,6 @@ impl QuoteEnv {
     pub fn new() -> Self {
         QuoteEnv { size: 0 }
     }
-    pub fn construct(size: usize) -> Self {
-        QuoteEnv { size }
-    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -273,232 +121,3 @@ impl NzVar {
         }
     }
 }
-
-impl TyExpr {
-    pub fn new(kind: TyExprKind, ty: Option<Type>) -> Self {
-        TyExpr {
-            kind: Box::new(kind),
-            ty,
-        }
-    }
-
-    pub fn kind(&self) -> &TyExprKind {
-        self.kind.as_ref()
-    }
-    pub fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t.clone()),
-            None => Err(TypeError),
-        }
-    }
-
-    /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        if opts.alpha {
-            self.to_expr_alpha()
-        } else {
-            self.to_expr_noalpha(&mut NameEnv::new())
-        }
-    }
-    fn to_expr_noalpha(&self, env: &mut NameEnv) -> NormalizedExpr {
-        rc(match self.kind() {
-            TyExprKind::Var(var) => ExprKind::Var(env.label_var(var)),
-            TyExprKind::Expr(e) => e.map_ref_maybe_binder(|l, tye| {
-                if let Some(l) = l {
-                    env.insert_mut(l);
-                }
-                let e = tye.to_expr_noalpha(env);
-                if let Some(_) = l {
-                    env.remove_mut();
-                }
-                e
-            }),
-        })
-    }
-    fn to_expr_alpha(&self) -> NormalizedExpr {
-        rc(match self.kind() {
-            TyExprKind::Var(var) => ExprKind::Var(V("_".into(), var.idx())),
-            TyExprKind::Expr(e) => match e.map_ref(TyExpr::to_expr_alpha) {
-                ExprKind::Lam(_, t, e) => ExprKind::Lam("_".into(), t, e),
-                ExprKind::Pi(_, t, e) => ExprKind::Pi("_".into(), t, e),
-                e => e,
-            },
-        })
-    }
-
-    pub fn normalize_nf(&self, env: &NzEnv) -> NzExpr {
-        let kind = match self.kind() {
-            TyExprKind::Var(var) => return env.lookup_val(var),
-            TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
-                NzExprKind::Lam {
-                    binder: binder.clone(),
-                    annot: annot.normalize_nf(env),
-                    env: env.clone(),
-                    body: body.clone(),
-                }
-            }
-            TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
-                NzExprKind::Pi {
-                    binder: binder.clone(),
-                    annot: annot.normalize_nf(env),
-                    env: env.clone(),
-                    body: body.clone(),
-                }
-            }
-            TyExprKind::Expr(e) => {
-                let e = e.map_ref(|tye| tye.normalize_nf(env));
-                match e {
-                    ExprKind::App(f, arg) => match f.kind() {
-                        NzExprKind::Lam { env, body, .. } => {
-                            return body.normalize_nf(&env.insert_value(arg))
-                        }
-                        _ => NzExprKind::Expr(ExprKind::App(f, arg)),
-                    },
-                    _ => NzExprKind::Expr(e),
-                }
-            }
-        };
-        let ty = self.ty.clone();
-        NzExpr::new(kind, ty)
-    }
-
-    pub fn normalize(&self) -> NzExpr {
-        self.normalize_nf(&NzEnv::new())
-    }
-}
-
-impl NzExpr {
-    pub fn new(kind: NzExprKind, ty: Option<Type>) -> Self {
-        NzExpr {
-            kind: Box::new(kind),
-            ty: ty.map(Box::new),
-        }
-    }
-
-    pub fn kind(&self) -> &NzExprKind {
-        self.kind.as_ref()
-    }
-    pub fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t.as_ref().clone()),
-            None => Err(TypeError),
-        }
-    }
-
-    pub fn quote(&self, qenv: QuoteEnv) -> TyExpr {
-        let ty = self.ty.as_ref().map(|t| (**t).clone());
-        let kind = match self.kind.as_ref() {
-            NzExprKind::Var { var } => TyExprKind::Var(qenv.lookup(var)),
-            NzExprKind::Lam {
-                binder,
-                annot,
-                env,
-                body,
-            } => TyExprKind::Expr(ExprKind::Lam(
-                binder.clone(),
-                annot.quote(qenv),
-                body.normalize_nf(&env.insert_type(annot.clone()))
-                    .quote(qenv.insert()),
-            )),
-            NzExprKind::Pi {
-                binder,
-                annot,
-                env,
-                body,
-            } => TyExprKind::Expr(ExprKind::Pi(
-                binder.clone(),
-                annot.quote(qenv),
-                body.normalize_nf(&env.insert_type(annot.clone()))
-                    .quote(qenv.insert()),
-            )),
-            NzExprKind::Expr(e) => {
-                TyExprKind::Expr(e.map_ref(|nze| nze.quote(qenv)))
-            } // NzExprKind::Unevaled { env, expr } => {
-              //     return TyExpr::new(expr.clone(), ty.clone())
-              //         .normalize_nf(env)
-              //         .quote(qenv)
-              // }
-        };
-        TyExpr::new(kind, ty)
-    }
-    pub fn to_expr(&self) -> NormalizedExpr {
-        self.quote(QuoteEnv::new()).to_expr(ToExprOptions {
-            alpha: false,
-            normalize: false,
-        })
-    }
-}
-
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
-fn type_with(env: &TyEnv, e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
-    match e.as_ref() {
-        ExprKind::Var(var) => match env.lookup_var(&var) {
-            Some(x) => Ok(x),
-            None => Err(TypeError),
-        },
-        ExprKind::Lam(binder, annot, body) => {
-            let annot = type_with(env, annot.clone())?;
-            let annot_nf = annot.normalize_nf(env.as_nzenv());
-            let body = type_with(
-                &env.insert_type(&binder, annot_nf.clone()),
-                body.clone(),
-            )?;
-            let ty = NzExpr::new(
-                NzExprKind::Pi {
-                    binder: binder.clone(),
-                    annot: annot_nf,
-                    env: env.as_nzenv().clone(),
-                    body: body.get_type()?.quote(env.as_quoteenv()),
-                },
-                None, // TODO: function_check
-            );
-            Ok(TyExpr::new(
-                TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
-                Some(ty),
-            ))
-        }
-        ExprKind::Pi(binder, annot, body) => {
-            let annot = type_with(env, annot.clone())?;
-            let annot_nf = annot.normalize_nf(env.as_nzenv());
-            let body = type_with(
-                &env.insert_type(&binder, annot_nf.clone()),
-                body.clone(),
-            )?;
-            Ok(TyExpr::new(
-                TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
-                None, // TODO: function_check
-            ))
-        }
-        ExprKind::App(f, arg) => {
-            let f = type_with(env, f.clone())?;
-            let arg = type_with(env, arg.clone())?;
-            let tf = f.get_type()?;
-            let (_expected_arg_ty, body_env, body_ty) = match tf.kind() {
-                NzExprKind::Pi {
-                    annot, env, body, ..
-                } => (annot, env, body),
-                _ => return Err(TypeError),
-            };
-            // if arg.get_type()? != *expected_arg_ty {
-            //     return Err(TypeError);
-            // }
-
-            let arg_nf = arg.normalize_nf(env.as_nzenv());
-            let ty = body_ty.normalize_nf(&body_env.insert_value(arg_nf));
-
-            Ok(TyExpr::new(
-                TyExprKind::Expr(ExprKind::App(f, arg)),
-                Some(ty),
-            ))
-        }
-        e => Ok(TyExpr::new(
-            TyExprKind::Expr(e.traverse_ref(|e| type_with(env, e.clone()))?),
-            None,
-        )),
-    }
-}
-
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
-    type_with(&TyEnv::new(), e)
-}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index f4e4099..d40456b 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
 use std::collections::HashMap;
 use std::convert::TryInto;
 
@@ -376,9 +375,6 @@ pub(crate) fn apply_builtin(
 pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueKind::Lam(_, _, e) => e
-            .subst_shift(&AlphaVar::default(), &a)
-            .to_whnf_check_type(ty),
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).to_whnf_check_type(ty)
         }
@@ -861,9 +857,6 @@ impl NzEnv {
     pub fn new() -> Self {
         NzEnv { items: Vec::new() }
     }
-    pub fn construct(items: Vec<NzEnvItem>) -> Self {
-        NzEnv { items }
-    }
     pub fn to_alpha_tyenv(&self) -> TyEnv {
         TyEnv::from_nzenv_alpha(self)
     }
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 6de65e8..4392365 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,122 +1,10 @@
-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::phase::normalize::merge_maps;
 use crate::semantics::phase::normalize::NzEnv;
-use crate::semantics::phase::Normalized;
-use crate::semantics::{AlphaVar, Binder, Value, ValueKind};
+use crate::semantics::{Value, ValueKind};
 use crate::syntax;
 use crate::syntax::{
-    Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
-    UnspannedExpr,
+    Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr,
 };
 
-fn tck_pi_type(
-    binder: Binder,
-    tx: Value,
-    te: Value,
-) -> Result<Value, TypeError> {
-    use TypeMessage::*;
-
-    let ka = match tx.get_type()?.as_const() {
-        Some(k) => k,
-        _ => return Err(TypeError::new(InvalidInputType(tx))),
-    };
-
-    let kb = match te.get_type()?.as_const() {
-        Some(k) => k,
-        _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))),
-    };
-
-    let k = function_check(ka, kb);
-
-    Ok(Value::from_kind_and_type(
-        ValueKind::Pi(binder, tx, te),
-        Value::from_const(k),
-    ))
-}
-
-fn tck_record_type(
-    kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
-) -> Result<Value, TypeError> {
-    use std::collections::hash_map::Entry;
-    use TypeMessage::*;
-    let mut new_kts = HashMap::new();
-    // An empty record type has type Type
-    let mut k = Const::Type;
-    for e in kts {
-        let (x, t) = e?;
-        // Construct the union of the contained `Const`s
-        match t.get_type()?.as_const() {
-            Some(k2) => k = max(k, k2),
-            None => return Err(TypeError::new(InvalidFieldType(x, t))),
-        }
-        // Check for duplicated entries
-        let entry = new_kts.entry(x);
-        match &entry {
-            Entry::Occupied(_) => {
-                return Err(TypeError::new(RecordTypeDuplicateField))
-            }
-            Entry::Vacant(_) => entry.or_insert_with(|| t),
-        };
-    }
-
-    Ok(Value::from_kind_and_type(
-        ValueKind::RecordType(new_kts),
-        Value::from_const(k),
-    ))
-}
-
-fn tck_union_type<Iter>(kts: Iter) -> Result<Value, TypeError>
-where
-    Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
-{
-    use std::collections::hash_map::Entry;
-    use TypeMessage::*;
-    let mut new_kts = HashMap::new();
-    // Check that all types are the same const
-    let mut k = None;
-    for e in kts {
-        let (x, t) = e?;
-        if let Some(t) = &t {
-            match (k, t.get_type()?.as_const()) {
-                (None, Some(k2)) => k = Some(k2),
-                (Some(k1), Some(k2)) if k1 == k2 => {}
-                _ => {
-                    return Err(TypeError::new(InvalidFieldType(x, t.clone())))
-                }
-            }
-        }
-        let entry = new_kts.entry(x);
-        match &entry {
-            Entry::Occupied(_) => {
-                return Err(TypeError::new(UnionTypeDuplicateField))
-            }
-            Entry::Vacant(_) => entry.or_insert_with(|| t),
-        };
-    }
-
-    // An empty union type has type Type;
-    // an union type with only unary variants also has type Type
-    let k = k.unwrap_or(Const::Type);
-
-    Ok(Value::from_kind_and_type(
-        ValueKind::UnionType(new_kts),
-        Value::from_const(k),
-    ))
-}
-
-fn function_check(a: Const, b: Const) -> Const {
-    if b == Const::Type {
-        Const::Type
-    } else {
-        max(a, b)
-    }
-}
-
 pub(crate) fn const_to_value(c: Const) -> Value {
     let v = ValueKind::Const(c);
     match c {
@@ -289,511 +177,3 @@ pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
             .normalize_whnf_noenv(),
     )
 }
-
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
-/// Some normalization is done while typechecking, so the returned expression might be partially
-/// normalized as well.
-fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
-    use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
-    let span = e.span();
-
-    match e.as_ref() {
-        Lam(var, annot, body) => {
-            let binder = ctx.new_binder(var);
-            let annot = type_with(ctx, annot.clone())?;
-            annot.normalize_nf();
-            let ctx2 = ctx.insert_type(&binder, annot.clone());
-            let body = type_with(&ctx2, body.clone())?;
-            let body_type = body.get_type()?;
-            Ok(Value::from_kind_and_type(
-                ValueKind::Lam(binder.clone(), annot.clone(), body),
-                tck_pi_type(binder, annot, body_type)?,
-            ))
-        }
-        Pi(x, ta, tb) => {
-            let binder = ctx.new_binder(x);
-            let ta = type_with(ctx, ta.clone())?;
-            let ctx2 = ctx.insert_type(&binder, ta.clone());
-            let tb = type_with(&ctx2, tb.clone())?;
-            tck_pi_type(binder, ta, tb)
-        }
-        Let(x, t, v, e) => {
-            let v = if let Some(t) = t {
-                t.rewrap(Annot(v.clone(), t.clone()))
-            } else {
-                v.clone()
-            };
-
-            let v = type_with(ctx, v)?;
-            let binder = ctx.new_binder(x);
-            let e =
-                type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?;
-            // let e_ty = e.get_type()?;
-            // Ok(Value::from_kind_and_type(
-            //     ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)),
-            //     e_ty,
-            // ))
-            Ok(e)
-        }
-        Embed(p) => Ok(p.clone().into_value()),
-        Var(var) => match ctx.lookup(&var) {
-            Some(typed) => Ok(typed.clone()),
-            None => Err(TypeError::new(TypeMessage::UnboundVariable(span))),
-        },
-        e => {
-            // Typecheck recursively all subexpressions
-            let expr = e.traverse_ref_with_special_handling_of_binders(
-                |e| type_with(ctx, e.clone()),
-                |_, _| unreachable!(),
-            )?;
-            type_last_layer(ctx, expr, span)
-        }
-    }
-}
-
-/// When all sub-expressions have been typed, check the remaining toplevel
-/// layer.
-fn type_last_layer(
-    ctx: &TyCtx,
-    e: ExprKind<Value, Normalized>,
-    span: Span,
-) -> Result<Value, TypeError> {
-    use syntax::BinOp::*;
-    use syntax::Builtin::*;
-    use syntax::Const::Type;
-    let mkerr =
-        |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string())));
-
-    /// Intermediary return type
-    enum Ret {
-        /// Returns the contained value as is
-        RetWhole(Value),
-        /// Returns the input expression `e` with the contained value as its type
-        RetTypeOnly(Value),
-    }
-    use Ret::*;
-
-    let ret = match &e {
-        ExprKind::Import(_) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
-        ExprKind::Lam(_, _, _)
-        | ExprKind::Pi(_, _, _)
-        | ExprKind::Let(_, _, _, _)
-        | ExprKind::Embed(_)
-        | ExprKind::Var(_) => unreachable!(),
-        ExprKind::App(f, a) => {
-            let tf = f.get_type()?;
-            let tf_borrow = tf.as_whnf();
-            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"),
-            }
-        }
-        ExprKind::Annot(x, t) => {
-            if &x.get_type()? != t {
-                return mkerr("AnnotMismatch");
-            }
-            RetWhole(x.clone())
-        }
-        ExprKind::Assert(t) => {
-            match &*t.as_whnf() {
-                ValueKind::Equivalence(x, y) if x == y => {}
-                ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
-                _ => return mkerr("AssertMustTakeEquivalence"),
-            }
-            RetTypeOnly(t.clone())
-        }
-        ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
-                return mkerr("InvalidPredicate");
-            }
-
-            if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-                return mkerr("IfBranchMustBeTerm");
-            }
-
-            if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-                return mkerr("IfBranchMustBeTerm");
-            }
-
-            if y.get_type()? != z.get_type()? {
-                return mkerr("IfBranchMismatch");
-            }
-
-            RetTypeOnly(y.get_type()?)
-        }
-        ExprKind::EmptyListLit(t) => {
-            let arg = match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(
-                    syntax::Builtin::List,
-                    args,
-                    _,
-                    _,
-                ) if args.len() == 1 => args[0].clone(),
-                _ => return mkerr("InvalidListType"),
-            };
-            RetWhole(Value::from_kind_and_type(
-                ValueKind::EmptyListLit(arg),
-                t.clone(),
-            ))
-        }
-        ExprKind::NEListLit(xs) => {
-            let mut iter = xs.iter().enumerate();
-            let (_, x) = iter.next().unwrap();
-            for (_, y) in iter {
-                if x.get_type()? != y.get_type()? {
-                    return mkerr("InvalidListElement");
-                }
-            }
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
-                return mkerr("InvalidListType");
-            }
-
-            RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
-        }
-        ExprKind::SomeLit(x) => {
-            let t = x.get_type()?;
-            if t.get_type()?.as_const() != Some(Const::Type) {
-                return mkerr("InvalidOptionalType");
-            }
-
-            RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
-        }
-        ExprKind::RecordType(kts) => RetWhole(tck_record_type(
-            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        )?),
-        ExprKind::UnionType(kts) => RetWhole(tck_union_type(
-            kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        )?),
-        ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
-            kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
-        )?),
-        ExprKind::Field(r, x) => {
-            match &*r.get_type()?.as_whnf() {
-                ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => RetTypeOnly(tth.clone()),
-                    None => return mkerr("MissingRecordField"),
-                },
-                // TODO: branch here only when r.get_type() is a Const
-                _ => {
-                    match &*r.as_whnf() {
-                        ValueKind::UnionType(kts) => match kts.get(&x) {
-                            // Constructor has type T -> < x: T, ... >
-                            Some(Some(t)) => RetTypeOnly(tck_pi_type(
-                                ctx.new_binder(x),
-                                t.clone(),
-                                r.under_binder(),
-                            )?),
-                            Some(None) => RetTypeOnly(r.clone()),
-                            None => return mkerr("MissingUnionField"),
-                        },
-                        _ => return mkerr("NotARecord"),
-                    }
-                } // _ => mkerr("NotARecord"),
-            }
-        }
-        ExprKind::Const(c) => RetWhole(const_to_value(*c)),
-        ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)),
-        ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
-        ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
-        ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
-        ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
-        ExprKind::TextLit(interpolated) => {
-            let text_type = builtin_to_value(Text);
-            for contents in interpolated.iter() {
-                use InterpolatedTextContents::Expr;
-                if let Expr(x) = contents {
-                    if x.get_type()? != text_type {
-                        return mkerr("InvalidTextInterpolation");
-                    }
-                }
-            }
-            RetTypeOnly(text_type)
-        }
-        ExprKind::BinOp(RightBiasedRecordMerge, l, r) => {
-            let l_type = l.get_type()?;
-            let r_type = r.get_type()?;
-
-            // Extract the LHS record type
-            let l_type_borrow = l_type.as_whnf();
-            let kts_x = match &*l_type_borrow {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("MustCombineRecord"),
-            };
-
-            // Extract the RHS record type
-            let r_type_borrow = r_type.as_whnf();
-            let kts_y = match &*r_type_borrow {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("MustCombineRecord"),
-            };
-
-            // Union the two records, prefering
-            // the values found in the RHS.
-            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
-                Ok(r_t.clone())
-            })?;
-
-            // Construct the final record type from the union
-            RetTypeOnly(tck_record_type(
-                kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
-            )?)
-        }
-        ExprKind::BinOp(RecursiveRecordMerge, l, r) => {
-            RetTypeOnly(type_last_layer(
-                ctx,
-                ExprKind::BinOp(
-                    RecursiveRecordTypeMerge,
-                    l.get_type()?,
-                    r.get_type()?,
-                ),
-                Span::Artificial,
-            )?)
-        }
-        ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => {
-            // Extract the LHS record type
-            let borrow_l = l.as_whnf();
-            let kts_x = match &*borrow_l {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
-            };
-
-            // Extract the RHS record type
-            let borrow_r = r.as_whnf();
-            let kts_y = match &*borrow_r {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
-            };
-
-            // Ensure that the records combine without a type error
-            let kts = merge_maps(
-                kts_x,
-                kts_y,
-                // If the Label exists for both records, then we hit the recursive case.
-                |_, l: &Value, r: &Value| {
-                    type_last_layer(
-                        ctx,
-                        ExprKind::BinOp(
-                            RecursiveRecordTypeMerge,
-                            l.clone(),
-                            r.clone(),
-                        ),
-                        Span::Artificial,
-                    )
-                },
-            )?;
-
-            RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
-        }
-        ExprKind::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");
-            }
-
-            RetTypeOnly(l.get_type()?)
-        }
-        ExprKind::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.get_type()? != r.get_type()? {
-                return mkerr("EquivalenceTypeMismatch");
-            }
-
-            RetWhole(Value::from_kind_and_type(
-                ValueKind::Equivalence(l.clone(), r.clone()),
-                Value::from_const(Type),
-            ))
-        }
-        ExprKind::BinOp(o, l, r) => {
-            let t = builtin_to_value(match o {
-                BoolAnd => Bool,
-                BoolOr => Bool,
-                BoolEQ => Bool,
-                BoolNE => Bool,
-                NaturalPlus => Natural,
-                NaturalTimes => Natural,
-                TextAppend => Text,
-                ListAppend => unreachable!(),
-                RightBiasedRecordMerge => unreachable!(),
-                RecursiveRecordMerge => unreachable!(),
-                RecursiveRecordTypeMerge => unreachable!(),
-                ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
-                Equivalence => unreachable!(),
-            });
-
-            if l.get_type()? != t {
-                return mkerr("BinOpTypeMismatch");
-            }
-
-            if r.get_type()? != t {
-                return mkerr("BinOpTypeMismatch");
-            }
-
-            RetTypeOnly(t)
-        }
-        ExprKind::Merge(record, union, type_annot) => {
-            let record_type = record.get_type()?;
-            let record_borrow = record_type.as_whnf();
-            let handlers = match &*record_borrow {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("Merge1ArgMustBeRecord"),
-            };
-
-            let union_type = union.get_type()?;
-            let union_borrow = union_type.as_whnf();
-            let variants = match &*union_borrow {
-                ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(
-                    syntax::Builtin::Optional,
-                    args,
-                    _,
-                    _,
-                ) if args.len() == 1 => {
-                    let ty = &args[0];
-                    let mut kts = HashMap::new();
-                    kts.insert("None".into(), None);
-                    kts.insert("Some".into(), Some(ty.clone()));
-                    Cow::Owned(kts)
-                }
-                _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
-            };
-
-            let mut inferred_type = None;
-            for (x, handler_type) in handlers {
-                let handler_return_type =
-                    match variants.get(x) {
-                        // Union alternative with type
-                        Some(Some(variant_type)) => {
-                            let handler_type_borrow = handler_type.as_whnf();
-                            let (tx, tb) = match &*handler_type_borrow {
-                                ValueKind::Pi(_, tx, tb) => (tx, tb),
-                                _ => return mkerr("NotAFunction"),
-                            };
-
-                            if variant_type != tx {
-                                return mkerr("TypeMismatch");
-                            }
-
-                            // 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",
-                                ),
-                            }
-                        }
-                        // Union alternative without type
-                        Some(None) => handler_type.clone(),
-                        None => return mkerr("MergeHandlerMissingVariant"),
-                    };
-                match &inferred_type {
-                    None => inferred_type = Some(handler_return_type),
-                    Some(t) => {
-                        if t != &handler_return_type {
-                            return mkerr("MergeHandlerTypeMismatch");
-                        }
-                    }
-                }
-            }
-            for x in variants.keys() {
-                if !handlers.contains_key(x) {
-                    return mkerr("MergeVariantMissingHandler");
-                }
-            }
-
-            match (inferred_type, type_annot.as_ref()) {
-                (Some(t1), Some(t2)) => {
-                    if &t1 != t2 {
-                        return mkerr("MergeAnnotMismatch");
-                    }
-                    RetTypeOnly(t1)
-                }
-                (Some(t), None) => RetTypeOnly(t),
-                (None, Some(t)) => RetTypeOnly(t.clone()),
-                (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
-            }
-        }
-        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
-        ExprKind::Projection(record, labels) => {
-            let record_type = record.get_type()?;
-            let record_type_borrow = record_type.as_whnf();
-            let kts = match &*record_type_borrow {
-                ValueKind::RecordType(kts) => kts,
-                _ => return mkerr("ProjectionMustBeRecord"),
-            };
-
-            let mut new_kts = HashMap::new();
-            for l in labels {
-                match kts.get(l) {
-                    None => return mkerr("ProjectionMissingEntry"),
-                    Some(t) => {
-                        use std::collections::hash_map::Entry;
-                        match new_kts.entry(l.clone()) {
-                            Entry::Occupied(_) => {
-                                return mkerr("ProjectionDuplicateField")
-                            }
-                            Entry::Vacant(e) => e.insert(t.clone()),
-                        }
-                    }
-                };
-            }
-
-            RetTypeOnly(Value::from_kind_and_type(
-                ValueKind::RecordType(new_kts),
-                record_type.get_type()?,
-            ))
-        }
-        ExprKind::ProjectionByExpr(_, _) => {
-            unimplemented!("selection by expression")
-        }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
-    };
-
-    Ok(match ret {
-        RetTypeOnly(typ) => Value::from_kind_and_type_and_span(
-            ValueKind::PartialExpr(e),
-            typ,
-            span,
-        ),
-        RetWhole(v) => v.with_span(span),
-    })
-}
-
-/// `type_of` is the same as `type_with` with an empty context, meaning that the
-/// expression must be closed (i.e. no free variables), otherwise type-checking
-/// will fail.
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
-    type_with(&TyCtx::new(), e)
-}
-
-pub(crate) fn typecheck_with(
-    expr: Expr<Normalized>,
-    ty: Expr<Normalized>,
-) -> Result<Value, TypeError> {
-    typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
-}
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>,