diff options
Diffstat (limited to 'dhall/src/semantics/phase/typecheck.rs')
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 1aab736..18e70e4 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> { pub(crate) fn builtin_to_value(b: Builtin) -> Value { Value::from_kind_and_type( ValueKind::from_builtin(b), - typecheck(type_of_builtin(b)).unwrap(), + crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) + .unwrap() + .normalize_whnf_noenv(), ) } @@ -380,17 +382,21 @@ fn type_last_layer( ExprKind::App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (tx, tb) = match &*tf_borrow { - ValueKind::Pi(_, tx, tb) => (tx, tb), + 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"), - }; - if &a.get_type()? != tx { - return mkerr("TypeMismatch"); } - - let ret = tb.subst_shift(&AlphaVar::default(), a); - ret.normalize_nf(); - RetTypeOnly(ret) } ExprKind::Annot(x, t) => { if &x.get_type()? != t { |