Ensure normalization respects var names on the nose

2 files changed, 13 insertions, 18 deletions

diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 459eaf1..bf0c626 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -24,7 +24,7 @@ macro_rules! make_closure {
             .into_value_with_type(make_closure!($($ty)*))
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
-    (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+    (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
         let var: AlphaLabel = Label::from(stringify!($var)).into();
         let ty = make_closure!($($ty)*);
         let body = make_closure!($($body)*);
@@ -276,12 +276,12 @@ pub(crate) fn apply_builtin(
                 f.app(list_t.clone())
                     .app({
                         // Move `t` under new variables
-                        let t1 = t.under_binder(Label::from("x"));
-                        let t2 = t1.under_binder(Label::from("xs"));
+                        let t1 = t.under_binder(Label::from("a"));
+                        let t2 = t1.under_binder(Label::from("as"));
                         make_closure!(
-                            λ(x : #t) ->
-                            λ(xs : List #t1) ->
-                            [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
+                            λ(a : #t) ->
+                            λ(as : List #t1) ->
+                            [ var(a, 1, #t2) ] # var(as, 0, List #t2)
                         )
                     })
                     .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
@@ -303,8 +303,8 @@ pub(crate) fn apply_builtin(
             Ret::Value(
                 f.app(optional_t.clone())
                     .app({
-                        let t1 = t.under_binder(Label::from("x"));
-                        make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+                        let t1 = t.under_binder(Label::from("a"));
+                        make_closure!(λ(a: #t) -> Some(var(a, 0, #t1)))
                     })
                     .app(
                         EmptyOptionalLit(t.clone())
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 0163c4d..f1648cf 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -206,11 +206,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             let expr = parse_file_str(&expr_file_path)?
                 .resolve()?
                 .typecheck()?
-                .normalize();
-            let expected = parse_file_str(&expected_file_path)?
-                .resolve()?
-                .typecheck()?
-                .normalize();
+                .normalize()
+                .to_expr();
+            let expected = parse_file_str(&expected_file_path)?.to_expr();
 
             assert_eq_display!(expr, expected);
         }
@@ -220,12 +218,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
                 .typecheck()?
                 .normalize()
                 .to_expr_alpha();
-            let expected = parse_file_str(&expected_file_path)?
-                .resolve()?
-                .typecheck()?
-                .normalize();
+            let expected = parse_file_str(&expected_file_path)?.to_expr();
 
-            assert_eq_display!(expr, expected.to_expr());
+            assert_eq_display!(expr, expected);
         }
     }
     Ok(())