From 8e4182f26b20b28f60fb0c21b3e08e19314de9a0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 5 May 2019 00:43:41 +0200
Subject: Make Value equality be alpha-equivalence

Closes #66, #65
---
 dhall/src/typecheck.rs | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8137417..2b87bd2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -243,8 +243,7 @@ where
     T: Borrow<Type>,
     U: Borrow<Type>,
 {
-    eL0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
-        == eR0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
+    eL0.borrow().to_value() == eR0.borrow().to_value()
 }
 
 fn const_to_typed(c: Const) -> Typed {
@@ -352,9 +351,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
             forall (nothing: optional) ->
             optional
         ),
-        // TODO: alpha-equivalence in type-inference tests
         OptionalNone => dhall::expr!(
-            forall (A: Type) -> Optional A
+            forall (a: Type) -> Optional a
         ),
     }
 }
@@ -436,7 +434,7 @@ impl TypeIntermediate {
 
                 Typed::from_thunk_and_type(
                     Value::Pi(
-                        x.clone(),
+                        x.clone().into(),
                         TypeThunk::from_type(ta.clone()),
                         TypeThunk::from_type(tb.clone()),
                     )
@@ -823,12 +821,11 @@ fn type_last_layer(
                     match &r.internal_whnf() {
                         Some(Value::UnionType(kts)) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
-                            // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
                             Some(Some(t)) => {
                                 Ok(RetType(
                                     TypeIntermediate::Pi(
                                         ctx.clone(),
-                                        x.clone(),
+                                        "_".into(),
                                         t.to_type(ctx)?,
                                         r.clone(),
                                     )
-- 
cgit v1.2.3