summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs9
1 files changed, 8 insertions, 1 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a83f175..5880d92 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -677,7 +677,7 @@ pub(crate) fn type_with(
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
ExprKind::Embed(p) => {
- return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+ return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
@@ -692,3 +692,10 @@ pub(crate) fn type_with(
pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
type_with(&TyEnv::new(), e)
}
+
+pub(crate) fn typecheck_with(
+ expr: &Expr<Normalized>,
+ ty: Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+ typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+}