Make shift fallible and improve shift ergonomics

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)?,