clippy

6 files changed, 118 insertions, 126 deletions

diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index c65d70e..5c569e1 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -299,7 +299,7 @@ impl Subst<Typed> for TypeThunk {
 
 impl std::cmp::PartialEq for Thunk {
     fn eq(&self, other: &Self) -> bool {
-        &*self.as_value() == &*other.as_value()
+        *self.as_value() == *other.as_value()
     }
 }
 impl std::cmp::Eq for Thunk {}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index cff599b..bc8fa34 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -132,7 +132,7 @@ impl Value {
                 rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.into_iter()
+                elts.iter()
                     .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
                     .collect(),
             )),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index e474e44..35bff80 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -101,9 +101,7 @@ impl Shift for () {
 }
 
 impl<T> Subst<T> for () {
-    fn subst_shift(&self, _var: &AlphaVar, _val: &T) -> Self {
-        ()
-    }
+    fn subst_shift(&self, _var: &AlphaVar, _val: &T) -> Self {}
 }
 
 impl std::cmp::PartialEq for AlphaVar {
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 29da609..ea29869 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -12,7 +12,9 @@
     clippy::type_complexity,
     clippy::infallible_destructuring_match,
     clippy::many_single_char_names,
-    clippy::match_wild_err_arm
+    clippy::match_wild_err_arm,
+    clippy::redundant_closure,
+    clippy::ptr_arg
 )]
 
 //! [Dhall][dhall] is a programmable configuration language that provides a non-repetitive
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 2253ae0..be2ba51 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -14,6 +14,7 @@ use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
 pub type InputSubExpr = ResolvedSubExpr;
 pub type OutputSubExpr = NormalizedSubExpr;
 
+#[allow(clippy::cognitive_complexity)]
 pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
     use dhall_syntax::Builtin::*;
     use Value::*;
@@ -206,7 +207,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
         (NaturalBuild, [f, r..]) => match &*f.as_value() {
             // fold/build fusion
             Value::AppliedBuiltin(NaturalFold, args) => {
-                if args.len() >= 1 {
+                if !args.is_empty() {
                     Ok((r, args[0].to_value()))
                 } else {
                     // Do we really need to handle this case ?
@@ -365,10 +366,10 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
 
 // Small helper enum to avoid repetition
 enum Ret<'a> {
-    RetValue(Value),
-    RetThunk(Thunk),
-    RetThunkRef(&'a Thunk),
-    RetExpr(ExprF<Thunk, X>),
+    Value(Value),
+    Thunk(Thunk),
+    ThunkRef(&'a Thunk),
+    Expr(ExprF<Thunk, X>),
 }
 
 fn merge_maps<K, V>(
@@ -402,7 +403,6 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge,
         TextAppend,
     };
-    use Ret::{RetThunkRef, RetValue};
     use Value::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
@@ -410,65 +410,69 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     let x_borrow = x.as_value();
     let y_borrow = y.as_value();
     Some(match (o, &*x_borrow, &*y_borrow) {
-        (BoolAnd, BoolLit(true), _) => RetThunkRef(y),
-        (BoolAnd, _, BoolLit(true)) => RetThunkRef(x),
-        (BoolAnd, BoolLit(false), _) => RetValue(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => RetValue(BoolLit(false)),
-        (BoolAnd, _, _) if x == y => RetThunkRef(x),
-        (BoolOr, BoolLit(true), _) => RetValue(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => RetValue(BoolLit(true)),
-        (BoolOr, BoolLit(false), _) => RetThunkRef(y),
-        (BoolOr, _, BoolLit(false)) => RetThunkRef(x),
-        (BoolOr, _, _) if x == y => RetThunkRef(x),
-        (BoolEQ, BoolLit(true), _) => RetThunkRef(y),
-        (BoolEQ, _, BoolLit(true)) => RetThunkRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => RetValue(BoolLit(true)),
-        (BoolNE, BoolLit(false), _) => RetThunkRef(y),
-        (BoolNE, _, BoolLit(false)) => RetThunkRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => RetValue(BoolLit(false)),
+        (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
+        (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
+        (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)),
+        (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)),
+        (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
+        (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)),
+        (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)),
+        (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
+        (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
+        (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
+        (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
+        (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
+        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)),
+        (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)),
+        (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
+        (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
+        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)),
+        (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)),
 
-        (NaturalPlus, NaturalLit(0), _) => RetThunkRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => RetThunkRef(x),
+        (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
+        (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
         (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            RetValue(NaturalLit(x + y))
+            Ret::Value(NaturalLit(x + y))
         }
-        (NaturalTimes, NaturalLit(0), _) => RetValue(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => RetValue(NaturalLit(0)),
-        (NaturalTimes, NaturalLit(1), _) => RetThunkRef(y),
-        (NaturalTimes, _, NaturalLit(1)) => RetThunkRef(x),
+        (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)),
+        (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)),
+        (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
+        (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
         (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            RetValue(NaturalLit(x * y))
+            Ret::Value(NaturalLit(x * y))
         }
 
-        (ListAppend, EmptyListLit(_), _) => RetThunkRef(y),
-        (ListAppend, _, EmptyListLit(_)) => RetThunkRef(x),
+        (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
         (ListAppend, NEListLit(xs), NEListLit(ys)) => {
-            RetValue(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
+            Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
         }
 
-        (TextAppend, TextLit(x), _) if x.is_empty() => RetThunkRef(y),
-        (TextAppend, _, TextLit(y)) if y.is_empty() => RetThunkRef(x),
-        (TextAppend, TextLit(x), TextLit(y)) => {
-            RetValue(TextLit(squash_textlit(x.iter().chain(y.iter()).cloned())))
-        }
+        (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
+        (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
+        (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit(
+            squash_textlit(x.iter().chain(y.iter()).cloned()),
+        )),
         (TextAppend, TextLit(x), _) => {
             use std::iter::once;
             let y = InterpolatedTextContents::Expr(y.clone());
-            RetValue(TextLit(squash_textlit(x.iter().cloned().chain(once(y)))))
+            Ret::Value(TextLit(squash_textlit(
+                x.iter().cloned().chain(once(y)),
+            )))
         }
         (TextAppend, _, TextLit(y)) => {
             use std::iter::once;
             let x = InterpolatedTextContents::Expr(x.clone());
-            RetValue(TextLit(squash_textlit(once(x).chain(y.iter().cloned()))))
+            Ret::Value(TextLit(squash_textlit(
+                once(x).chain(y.iter().cloned()),
+            )))
         }
 
         (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            RetThunkRef(x)
+            Ret::ThunkRef(x)
         }
         (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            RetThunkRef(y)
+            Ret::ThunkRef(y)
         }
         (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let mut kvs = kvs2.clone();
@@ -476,14 +480,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            RetValue(RecordLit(kvs))
+            Ret::Value(RecordLit(kvs))
         }
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            RetThunkRef(x)
+            Ret::ThunkRef(x)
         }
         (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            RetThunkRef(y)
+            Ret::ThunkRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
@@ -493,14 +497,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                     v2.clone(),
                 ))
             });
-            RetValue(RecordLit(kvs))
+            Ret::Value(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
-            RetThunkRef(x)
+            Ret::ThunkRef(x)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
-            RetThunkRef(y)
+            Ret::ThunkRef(y)
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
@@ -510,7 +514,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
                     v2.to_thunk(),
                 )))
             });
-            RetValue(RecordType(kvs))
+            Ret::Value(RecordType(kvs))
         }
 
         _ => return None,
@@ -518,7 +522,6 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
 }
 
 pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
-    use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue};
     use Value::{
         BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -528,51 +531,53 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
     let ret = match expr {
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => RetThunk(x),
+        ExprF::Annot(x, _) => Ret::Thunk(x),
         ExprF::Lam(x, t, e) => {
-            RetValue(Lam(x.into(), TypeThunk::from_thunk(t), e))
+            Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
         }
-        ExprF::Pi(x, t, e) => RetValue(Pi(
+        ExprF::Pi(x, t, e) => Ret::Value(Pi(
             x.into(),
             TypeThunk::from_thunk(t),
             TypeThunk::from_thunk(e),
         )),
         ExprF::Let(x, _, v, b) => {
             let v = Typed::from_thunk_untyped(v);
-            RetThunk(b.subst_shift(&x.into(), &v))
-        }
-        ExprF::App(v, a) => RetValue(v.app_thunk(a)),
-        ExprF::Builtin(b) => RetValue(Value::from_builtin(b)),
-        ExprF::Const(c) => RetValue(Value::Const(c)),
-        ExprF::BoolLit(b) => RetValue(BoolLit(b)),
-        ExprF::NaturalLit(n) => RetValue(NaturalLit(n)),
-        ExprF::IntegerLit(n) => RetValue(IntegerLit(n)),
-        ExprF::DoubleLit(n) => RetValue(DoubleLit(n)),
+            Ret::Thunk(b.subst_shift(&x.into(), &v))
+        }
+        ExprF::App(v, a) => Ret::Value(v.app_thunk(a)),
+        ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)),
+        ExprF::Const(c) => Ret::Value(Value::Const(c)),
+        ExprF::BoolLit(b) => Ret::Value(BoolLit(b)),
+        ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
+        ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
+        ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
         ExprF::OldOptionalLit(None, t) => {
-            RetValue(EmptyOptionalLit(TypeThunk::from_thunk(t)))
+            Ret::Value(EmptyOptionalLit(TypeThunk::from_thunk(t)))
         }
-        ExprF::OldOptionalLit(Some(e), _) => RetValue(NEOptionalLit(e)),
-        ExprF::SomeLit(e) => RetValue(NEOptionalLit(e)),
+        ExprF::OldOptionalLit(Some(e), _) => Ret::Value(NEOptionalLit(e)),
+        ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
         ExprF::EmptyListLit(t) => {
-            RetValue(EmptyListLit(TypeThunk::from_thunk(t)))
+            Ret::Value(EmptyListLit(TypeThunk::from_thunk(t)))
         }
         ExprF::NEListLit(elts) => {
-            RetValue(NEListLit(elts.into_iter().collect()))
+            Ret::Value(NEListLit(elts.into_iter().collect()))
+        }
+        ExprF::RecordLit(kvs) => {
+            Ret::Value(RecordLit(kvs.into_iter().collect()))
         }
-        ExprF::RecordLit(kvs) => RetValue(RecordLit(kvs.into_iter().collect())),
-        ExprF::RecordType(kts) => RetValue(RecordType(
+        ExprF::RecordType(kts) => Ret::Value(RecordType(
             kts.into_iter()
                 .map(|(k, t)| (k, TypeThunk::from_thunk(t)))
                 .collect(),
         )),
-        ExprF::UnionLit(l, x, kts) => RetValue(UnionLit(
+        ExprF::UnionLit(l, x, kts) => Ret::Value(UnionLit(
             l,
             x,
             kts.into_iter()
                 .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
                 .collect(),
         )),
-        ExprF::UnionType(kts) => RetValue(UnionType(
+        ExprF::UnionType(kts) => Ret::Value(UnionType(
             kts.into_iter()
                 .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
                 .collect(),
@@ -582,28 +587,28 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
             let elts: Vec<_> = squash_textlit(elts.into_iter());
             // Simplify bare interpolation
             if let [Expr(th)] = elts.as_slice() {
-                RetThunk(th.clone())
+                Ret::Thunk(th.clone())
             } else {
-                RetValue(TextLit(elts))
+                Ret::Value(TextLit(elts))
             }
         }
         ExprF::BoolIf(ref b, ref e1, ref e2) => {
             let b_borrow = b.as_value();
             match &*b_borrow {
-                BoolLit(true) => RetThunkRef(e1),
-                BoolLit(false) => RetThunkRef(e2),
+                BoolLit(true) => Ret::ThunkRef(e1),
+                BoolLit(false) => Ret::ThunkRef(e2),
                 _ => {
                     let e1_borrow = e1.as_value();
                     let e2_borrow = e2.as_value();
                     match (&*e1_borrow, &*e2_borrow) {
                         // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => RetThunkRef(b),
-                        _ if e1 == e2 => RetThunkRef(e1),
+                        (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
+                        _ if e1 == e2 => Ret::ThunkRef(e1),
                         _ => {
                             drop(b_borrow);
                             drop(e1_borrow);
                             drop(e2_borrow);
-                            RetExpr(expr)
+                            Ret::Expr(expr)
                         }
                     }
                 }
@@ -611,16 +616,16 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         }
         ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
             Some(ret) => ret,
-            None => RetExpr(expr),
+            None => Ret::Expr(expr),
         },
 
         ExprF::Projection(_, ls) if ls.is_empty() => {
-            RetValue(RecordLit(HashMap::new()))
+            Ret::Value(RecordLit(HashMap::new()))
         }
         ExprF::Projection(ref v, ref ls) => {
             let v_borrow = v.as_value();
             match &*v_borrow {
-                RecordLit(kvs) => RetValue(RecordLit(
+                RecordLit(kvs) => Ret::Value(RecordLit(
                     ls.iter()
                         .filter_map(|l| {
                             kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -629,7 +634,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
                 )),
                 _ => {
                     drop(v_borrow);
-                    RetExpr(expr)
+                    Ret::Expr(expr)
                 }
             }
         }
@@ -637,18 +642,18 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
             let v_borrow = v.as_value();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
-                    Some(r) => RetThunk(r.clone()),
+                    Some(r) => Ret::Thunk(r.clone()),
                     None => {
                         drop(v_borrow);
-                        RetExpr(expr)
+                        Ret::Expr(expr)
                     }
                 },
                 UnionType(kts) => {
-                    RetValue(UnionConstructor(l.clone(), kts.clone()))
+                    Ret::Value(UnionConstructor(l.clone(), kts.clone()))
                 }
                 _ => {
                     drop(v_borrow);
-                    RetExpr(expr)
+                    Ret::Expr(expr)
                 }
             }
         }
@@ -658,34 +663,34 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
             let variant_borrow = variant.as_value();
             match (&*handlers_borrow, &*variant_borrow) {
                 (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
-                    Some(h) => RetThunk(h.clone()),
+                    Some(h) => Ret::Thunk(h.clone()),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
-                        RetExpr(expr)
+                        Ret::Expr(expr)
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => RetValue(h.app_thunk(v.clone())),
+                    Some(h) => Ret::Value(h.app_thunk(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
-                        RetExpr(expr)
+                        Ret::Expr(expr)
                     }
                 },
                 _ => {
                     drop(handlers_borrow);
                     drop(variant_borrow);
-                    RetExpr(expr)
+                    Ret::Expr(expr)
                 }
             }
         }
     };
 
     match ret {
-        RetValue(v) => v,
-        RetThunk(th) => th.to_value(),
-        RetThunkRef(th) => th.to_value(),
-        RetExpr(expr) => Value::PartialExpr(expr),
+        Ret::Value(v) => v,
+        Ret::Thunk(th) => th.to_value(),
+        Ret::ThunkRef(th) => th.to_value(),
+        Ret::Expr(expr) => Value::PartialExpr(expr),
     }
 }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index bb36060..419b2e2 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,5 +1,3 @@
-#![allow(non_snake_case)]
-use std::borrow::Borrow;
 use std::collections::HashMap;
 
 use dhall_proc_macros as dhall;
@@ -17,7 +15,7 @@ use crate::phase::{Normalized, Resolved, Type, Typed};
 
 macro_rules! ensure_equal {
     ($x:expr, $y:expr, $err:expr $(,)*) => {
-        if !prop_equal($x, $y) {
+        if $x.to_value() != $y.to_value() {
             return Err($err);
         }
     };
@@ -42,7 +40,7 @@ fn tck_pi_type(
     use crate::error::TypeMessage::*;
     let ctx2 = ctx.insert_type(&x, tx.clone());
 
-    let kA = match tx.get_type()?.as_const() {
+    let ka = match tx.get_type()?.as_const() {
         Some(k) => k,
         _ => {
             return Err(TypeError::new(
@@ -52,7 +50,7 @@ fn tck_pi_type(
         }
     };
 
-    let kB = match te.get_type()?.as_const() {
+    let kb = match te.get_type()?.as_const() {
         Some(k) => k,
         _ => {
             return Err(TypeError::new(
@@ -62,7 +60,7 @@ fn tck_pi_type(
         }
     };
 
-    let k = match function_check(kA, kB) {
+    let k = match function_check(ka, kb) {
         Ok(k) => k,
         Err(()) => {
             return Err(TypeError::new(
@@ -109,7 +107,7 @@ fn tck_record_type(
                 return Err(TypeError::new(ctx, RecordTypeDuplicateField))
             }
             Entry::Vacant(_) => {
-                entry.or_insert(TypeThunk::from_type(t.clone()))
+                entry.or_insert_with(|| TypeThunk::from_type(t.clone()))
             }
         };
     }
@@ -150,8 +148,9 @@ fn tck_union_type(
             Entry::Occupied(_) => {
                 return Err(TypeError::new(ctx, UnionTypeDuplicateField))
             }
-            Entry::Vacant(_) => entry
-                .or_insert(t.as_ref().map(|t| TypeThunk::from_type(t.clone()))),
+            Entry::Vacant(_) => entry.or_insert_with(|| {
+                t.as_ref().map(|t| TypeThunk::from_type(t.clone()))
+            }),
         };
     }
 
@@ -207,24 +206,12 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-// Equality up to alpha-equivalence (renaming of bound variables)
-fn prop_equal<T, U>(eL0: T, eR0: U) -> bool
-where
-    T: Borrow<Type>,
-    U: Borrow<Type>,
-{
-    eL0.borrow().to_value() == eR0.borrow().to_value()
-}
-
 pub fn type_of_const(c: Const) -> Result<Type, TypeError> {
     match c {
         Const::Type => Ok(Type::from_const(Const::Kind)),
         Const::Kind => Ok(Type::from_const(Const::Sort)),
         Const::Sort => {
-            return Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Sort,
-            ))
+            Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
         }
     }
 }
@@ -728,7 +715,7 @@ fn type_last_layer(
                 }
                 (Some(t), None) => Ok(RetTypeOnly(t)),
                 (None, Some(t)) => Ok(RetTypeOnly(t.to_type())),
-                (None, None) => return Err(mkerr(MergeEmptyNeedsAnnotation)),
+                (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)),
             }
         }
         Projection(record, labels) => {