summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2019-04-07 22:39:44 +0200
committerNadrieril2019-04-07 22:39:44 +0200
commitcfdc5297d565c80f8362fc4ac31e25e3ebf34e84 (patch)
tree029ecf3221514847dd029d12bca4ce2296dfc3d7 /dhall/src/typecheck.rs
parent605e883696f8861e4b8c00b18ead9b933ac30e7a (diff)
Tweaks
Diffstat (limited to 'dhall/src/typecheck.rs')
-rw-r--r--dhall/src/typecheck.rs3
1 files changed, 2 insertions, 1 deletions
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![];