summaryrefslogtreecommitdiff
path: root/dhall/src/phase/typecheck.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase/typecheck.rs')
-rw-r--r--dhall/src/phase/typecheck.rs11
1 files changed, 4 insertions, 7 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index ecf9793..96ff246 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,7 +2,6 @@ use std::collections::HashMap;
use dhall_syntax::{
rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
- X,
};
use crate::core::context::{NormalizationContext, TypecheckContext};
@@ -214,7 +213,7 @@ macro_rules! make_type {
};
}
-fn type_of_builtin(b: Builtin) -> Expr<X> {
+fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
use dhall_syntax::Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -398,7 +397,7 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: &ExprF<Typed, X>,
+ e: &ExprF<Typed, Normalized>,
) -> Result<Ret, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;
@@ -598,9 +597,7 @@ fn type_last_layer(
}
}
Const(c) => Ok(RetWhole(Typed::from_const(*c))),
- Builtin(b) => {
- Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
- }
+ Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)),
BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
@@ -1016,7 +1013,7 @@ pub fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
pub fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
let expr: SubExpr<_> = e.0;
- let ty: SubExpr<_> = ty.to_expr().absurd();
+ let ty: SubExpr<_> = ty.to_expr();
type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
pub fn skip_typecheck(e: Resolved) -> Typed {