From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 10 Feb 2020 19:14:07 +0000 Subject: Remove need for Embed This was an archaic leftover from copying the Haskell datatypes anyway --- dhall/src/semantics/tck/typecheck.rs | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7f02832..4e45637 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -761,21 +761,13 @@ fn type_one_layer( /// `type_with` typechecks an expressio in the provided environment. pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))), + HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } - HirKind::Expr(ExprKind::Embed(p)) => { - let val = p.clone().into_value(); - ( - val.to_tyexpr_noenv().kind().clone(), - Some(val.get_type(&TyEnv::new())?), - ) - // return Ok(p.clone().into_value().to_tyexpr_noenv()) - } HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { -- cgit v1.2.3