summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-01-30 14:49:17 +0000
committerNadrieril2020-01-30 14:49:17 +0000
commit837298f26e07bb264a6b6f0286cbb811553b0477 (patch)
tree18e29e6500632819c805fe9883989745d2c1f8b4 /dhall/src/semantics/tck
parent25bd09136742403d7f3d6c6143f72e6687f39457 (diff)
Increase encapsulation for Closures
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs10
1 files changed, 5 insertions, 5 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0c5e779..bc1c87f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage};
use crate::semantics::phase::normalize::merge_maps;
use crate::semantics::phase::Normalized;
use crate::semantics::{
- type_of_builtin, Binder, BuiltinClosure, Closure, NzVar, TyEnv, TyExpr,
+ type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
TyExprKind, Type, Value, ValueKind,
};
use crate::syntax::{
@@ -48,7 +48,7 @@ fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
Ok(Value::from_const(function_check(ks, kt)))
}
-fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
+fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
@@ -452,9 +452,9 @@ fn type_one_layer(
return mkerr("MergeHandlerTypeMismatch");
}
- let v = NzVar::fresh();
- // TODO: handle case where variable is used in closure
- closure.apply_var(v)
+ closure.remove_binder().or_else(|()| {
+ mkerr("MergeReturnTypeIsDependent")
+ })?
}
_ => return mkerr("NotAFunction"),
}