Make shift fallible and improve shift ergonomics

1 files changed, 11 insertions, 2 deletions

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