summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
authorNadrieril2019-05-09 16:32:30 +0200
committerNadrieril2019-05-09 16:32:30 +0200
commit7538e29275720407ac172bb05cdbc028d95ff921 (patch)
tree79ad968a7ef6e36e5a4e7fc19df281c46ac68f6c /dhall/src/phase
parent2020d41874f7681ba948a40d8e8f8993d651a81c (diff)
Make shift fallible and improve shift ergonomics
Diffstat (limited to '')
-rw-r--r--dhall/src/phase/mod.rs18
-rw-r--r--dhall/src/phase/typecheck.rs13
2 files changed, 20 insertions, 11 deletions
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index db0a2b9..50103a0 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -238,26 +238,26 @@ impl Normalized {
}
impl Shift for Typed {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- match self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
Typed::Value(th, t) => Typed::Value(
- th.shift(delta, var),
- t.as_ref().map(|x| x.shift(delta, var)),
+ th.shift(delta, var)?,
+ t.as_ref().map(|x| Ok(x.shift(delta, var)?)).transpose()?,
),
Typed::Const(c) => Typed::Const(*c),
- }
+ })
}
}
impl Shift for Type {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- Type(Box::new(self.0.shift(delta, var)))
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Type(Box::new(self.0.shift(delta, var)?)))
}
}
impl Shift for Normalized {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- Normalized(self.0.shift(delta, var))
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Normalized(self.0.shift(delta, var)?))
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2c625fb..497a703 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -732,6 +732,7 @@ fn type_last_layer(
)))
}
};
+
ensure_equal!(&variant_type, &tx, {
mkerr(TypeMismatch(
handler_type.to_typed(),
@@ -739,8 +740,16 @@ fn type_last_layer(
variant_type.to_typed(),
))
});
- // TODO: check that x is not free in tb first
- tb.shift(-1, &x.into())
+
+ // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+ match tb.over_binder(x) {
+ Some(x) => x,
+ None => {
+ return Err(mkerr(
+ MergeHandlerReturnTypeMustNotBeDependent,
+ ))
+ }
+ }
}
// Union alternative without type
Some(None) => handler.to_type(ctx)?,