From cfdc5297d565c80f8362fc4ac31e25e3ebf34e84 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 22:39:44 +0200
Subject: Tweaks

---
 dhall/src/normalize.rs | 3 ---
 dhall/src/typecheck.rs | 3 ++-
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c07d3cb..ac730a9 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -267,9 +267,6 @@ where
             Done(NaturalLit(x * y))
         }
         BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
-        BinOp(ListAppend, EmptyListLit(t), EmptyListLit(_)) => {
-            Done(EmptyListLit(SubExpr::clone(t)))
-        }
         BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
         BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
         BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index babfad0..04c042b 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -144,7 +144,7 @@ fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
     vl == vr
 }
 
-// Takes normalized expressions as input
+// Equality up to alpha-equivalence (renaming of bound variables)
 fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
     use dhall_core::ExprF::*;
     fn go<S, T>(
@@ -202,6 +202,7 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
         }
     }
     match (&eL0.0, &eR0.0) {
+        // Note: Untyped != Untyped, to avoid soundness issues
         (TypeInternal::Untyped, TypeInternal::Untyped) => false,
         (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
             let mut ctx = vec![];
-- 
cgit v1.2.3