From 611d4ced3a5ffca8b9765971001995a216dbbb54 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 24 Dec 2019 21:21:10 +0000
Subject: Ensure the output of type inference matches the spec variable names

---
 dhall/src/semantics/phase/typecheck.rs | 14 +++++++-------
 dhall/src/tests.rs                     |  4 ++--
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 97502d4..e9836e8 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -288,7 +288,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
             optional
         ),
         OptionalNone => make_type!(
-            forall (a: Type) -> Optional a
+            forall (A: Type) -> Optional A
         ),
     })
 }
@@ -503,9 +503,9 @@ fn type_last_layer(
                                 RetTypeOnly(
                                     tck_pi_type(
                                         ctx,
-                                        "_".into(),
+                                        x.clone(),
                                         t.clone(),
-                                        r.under_binder(Label::from("_")),
+                                        r.under_binder(x),
                                     )?
                                 )
                             },
@@ -764,12 +764,12 @@ fn type_last_layer(
                 }
             }
 
-            match (inferred_type, type_annot) {
-                (Some(ref t1), Some(t2)) => {
-                    if t1 != t2 {
+            match (inferred_type, type_annot.as_ref()) {
+                (Some(t1), Some(t2)) => {
+                    if &t1 != t2 {
                         return mkerr(MergeAnnotMismatch);
                     }
-                    RetTypeOnly(t2.clone())
+                    RetTypeOnly(t1)
                 }
                 (Some(t), None) => RetTypeOnly(t),
                 (None, Some(t)) => RetTypeOnly(t.clone()),
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index d73c2d4..7a3a540 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -160,11 +160,11 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
         TypeInferenceSuccess(expr_file_path, expected_file_path) => {
             let expr =
                 parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
-            let ty = expr.get_type()?.normalize();
+            let ty = expr.get_type()?.normalize_to_expr();
             let expected = parse_file_str(&expected_file_path)?
                 .resolve()?
                 .typecheck()?
-                .normalize();
+                .normalize_to_expr();
             assert_eq_display!(ty, expected);
         }
         TypeInferenceFailure(file_path) => {
-- 
cgit v1.2.3