diff options
| -rw-r--r-- | dhall/src/typecheck.rs | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index c518e3d..ffcc453 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -69,6 +69,7 @@ impl<'a> Normalized<'a> { Ok(match self.0.as_ref() { ExprF::Const(c) => Type(TypeInternal::Const(*c)), ExprF::Pi(_, _, _) | ExprF::RecordType(_) => { + // TODO: wasteful type_with(ctx, self.0.embed_absurd())?.normalize_to_type()? } _ => Type(TypeInternal::Expr(Box::new(self))), @@ -295,9 +296,7 @@ impl TypecheckContext { x: &Label, t: Normalized<'static>, ) -> Self { - TypecheckContext( - self.0.insert(x.clone(), EnvItem::Value(t.shift0(1, x))), - ) + TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t))) } pub(crate) fn lookup( &self, @@ -776,16 +775,13 @@ fn type_last_layer( ensure_equal!(a.get_type()?, tx.as_ref(), { mkerr(TypeMismatch(f, tx.into_normalized()?, a)) }); - Ok(RetExpr(Let( - x.clone(), - None, - a.normalize()?.embed(), - tb.into_normalized()?.into_expr().embed_absurd(), - ))) - // Ok(RetType(mktype( - // &ctx.insert_value(&x, a), - // tb.into_normalized()?.into_expr().embed_absurd(), - // )?)) + + let ctx2 = ctx.insert_value(&x, a.normalize()?); + let tb: Typed = tb.into_normalized()?.into(); + // Normalize with the updated context + let tb = Typed(tb.0, tb.1, ctx2, tb.3).normalize(); + // Convert to type with the current context + Ok(RetType(tb.into_type_ctx(&ctx)?)) } Annot(x, t) => { let t = t.normalize_to_type()?; |