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.rs26
1 files changed, 14 insertions, 12 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e3f57c2..20076cd 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -200,20 +200,22 @@ fn type_one_layer(
match scrut_nf.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
- Some(Some(ty)) => Value::from_kind_and_type(
- ValueKind::PiClosure {
- binder: Binder::new(x.clone()),
- annot: ty.clone(),
- closure: Closure::new_constant(
- env.as_nzenv(),
- scrut.clone(),
- ),
- },
- type_of_function(
+ Some(Some(ty)) => {
+ let pi_ty = type_of_function(
ty.get_type()?,
scrut.get_type()?,
- )?,
- ),
+ )?;
+ Value::from_kind_and_type(
+ ValueKind::PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: ty.clone(),
+ closure: Closure::new_constant(
+ scrut_nf,
+ ),
+ },
+ pi_ty,
+ )
+ }
Some(None) => scrut_nf,
None => return mkerr("MissingUnionField"),
},