diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/normalize.rs | 3 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 3 |
2 files changed, 2 insertions, 4 deletions
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![]; |