diff options
| author | Nadrieril | 2020-01-30 22:08:57 +0000 |
|---|---|---|
| committer | Nadrieril | 2020-01-30 22:08:57 +0000 |
| commit | 70af1a47bce9e6c8282d6e53cf82aeda9aab10de (patch) | |
| tree | 50ea14fd5c4c6c5f8d27f4cadb00310460590309 /dhall/src/semantics/tck | |
| parent | 4e2bb03bcf6355d49216c6886bf03e5aeaad16cc (diff) | |
Tweak ConstantClosure
Diffstat (limited to 'dhall/src/semantics/tck')
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 26 |
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"), }, |