src/main/java/pl/wojciechkarpiel/jhou/ast/Term.java

@@ -3,7 +3,8 @@ package pl.wojciechkarpiel.jhou.ast;
 import pl.wojciechkarpiel.jhou.ast.util.Visitor;
 
 /**
- * term.equals is equality modulo alpha conversion. It does not take into account beta nor eta conversions
+ * term.equals is raw structural equality. λx.x and λy.y are not equal.
+ * For weaker notions of equality (alpha/beta/eta), see the Api.
  */
 public interface Term {
     <T> T visit(Visitor<T> visitor);

src/main/java/pl/wojciechkarpiel/jhou/unifier/tree/WorkWorkNode.java

@@ -1,5 +1,6 @@
 package pl.wojciechkarpiel.jhou.unifier.tree;
 
+import pl.wojciechkarpiel.jhou.ast.Equality;
 import pl.wojciechkarpiel.jhou.ast.Term;
 import pl.wojciechkarpiel.jhou.ast.Variable;
 import pl.wojciechkarpiel.jhou.normalizer.Normalizer;
@@ -136,28 +137,30 @@ public class WorkWorkNode implements Tree {
     private static List<Substitution> deduplicateSort(List<Substitution> input) {
         if (input.isEmpty()) return input;
 
-        Map<Variable, Set<Term>> dedupByVar = new HashMap<>(input.size());
+        // List<Term> and not Set<Term> because of alpha-equality problem
+        Map<Variable, List<Term>> dedupByVar = new HashMap<>(input.size());
         for (Substitution pair_ : input) {
             if (pair_.getSubstitution().size() > 1) throw new RuntimeException();
             if (pair_.getSubstitution().isEmpty()) continue;
             SubstitutionPair pair = pair_.getSubstitution().get(0);
-            Set<Term> s_ = new HashSet<>();
-            Set<Term> s = dedupByVar.putIfAbsent(pair.getVariable(), s_);
+            List<Term> s_ = new ArrayList<>();
+            List<Term> s = dedupByVar.putIfAbsent(pair.getVariable(), s_);
             if (s == null) s = s_;
-            s.add(pair.getTerm());
+            // could be Set.add if not for alpha equality (bruijn would fix the problem of hashcode-equals for alpha)
+            if (s.stream().noneMatch(t -> Equality.alphaEqual(t, pair.getTerm()))) s.add(pair.getTerm());
         }
         if (dedupByVar.isEmpty()) {
             return input;
         }
 
-        List<Pair<Variable, Set<Term>>> least = new ArrayList<>();
-        int minCount = dedupByVar.values().stream().mapToInt(Set::size).min().getAsInt();
+        List<Pair<Variable, List<Term>>> least = new ArrayList<>();
+        int minCount = dedupByVar.values().stream().mapToInt(List::size).min().getAsInt();
         dedupByVar.entrySet().stream().filter(p -> p.getValue().size() == minCount)
                 .forEach(p -> least.add(Pair.of(p.getKey(), p.getValue())));
 
         least.sort(Comparator.comparingInt(o -> o.getLeft().getId().getId()));
 
-        Pair<Variable, Set<Term>> minSized = least.get(0);
+        Pair<Variable, List<Term>> minSized = least.get(0);
         return minSized.getRight().stream()
                 // Sorting here doesn't help the algorithm, it's here to ensure deterministic outputs
                 .sorted(Comparator.comparingInt(Term::hashCode))

src/test/java/pl/wojciechkarpiel/jhou/ast/AbstractionTest.java

@@ -0,0 +1,28 @@
+package pl.wojciechkarpiel.jhou.ast;
+
+import org.junit.jupiter.api.Test;
+import pl.wojciechkarpiel.jhou.ast.type.Type;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static pl.wojciechkarpiel.jhou.Api.abstraction;
+import static pl.wojciechkarpiel.jhou.Api.freshType;
+
+class AbstractionTest {
+
+    @Test
+    void equalsHashcodeContractTest() {
+        Type t = freshType();
+        Term ax = abstraction(t, x -> x);
+        Term ay = abstraction(t, x -> x);
+        assertHashcodeEquals(ax, ay);
+        assertHashcodeEquals(ax, ax);
+        assertHashcodeEquals(ay, ay);
+    }
+
+
+    private void assertHashcodeEquals(Object a, Object b) {
+        if (a.equals(b)) {
+            assertEquals(a.hashCode(), b.hashCode());
+        }
+    }
+}

src/test/java/pl/wojciechkarpiel/jhou/unifier/simplifier/MatcherTest.java

@@ -12,9 +12,9 @@ import pl.wojciechkarpiel.jhou.termHead.BetaEtaNormal;
 import pl.wojciechkarpiel.jhou.termHead.HeadOps;
 import pl.wojciechkarpiel.jhou.testUtil.TestUtil;
 import pl.wojciechkarpiel.jhou.types.TypeCalculator;
-import pl.wojciechkarpiel.jhou.unifier.*;
-import pl.wojciechkarpiel.jhou.unifier.simplifier.result.SimplificationResult;
-import pl.wojciechkarpiel.jhou.util.ListUtil;
+import pl.wojciechkarpiel.jhou.unifier.SolutionIterator;
+import pl.wojciechkarpiel.jhou.unifier.UnificationSettings;
+import pl.wojciechkarpiel.jhou.unifier.Unifier;
 
 import java.util.List;
 import java.util.Optional;
@@ -104,7 +104,6 @@ class MatcherTest {
         Constant c1 = new Constant(Id.uniqueId(), c1t);
         Variable v1 = new Variable(Id.uniqueId(), c1t);
         Variable v2 = new Variable(Id.uniqueId(), c2t);
-        BaseType fint = new BaseType(Id.uniqueId(), "TFIN");
         Variable v = new Variable(Id.uniqueId(), new ArrowType(c1t, new ArrowType(c2t, c2t)));
         Term flexible = new Abstraction(v1, new Abstraction(v2, new Application(new Application(v, c1), c2)));
         Constant c = new Constant(Id.uniqueId(), new ArrowType(c1t, new ArrowType(c2t, c2t)));
@@ -215,7 +214,6 @@ class MatcherTest {
 
         BetaEtaNormal noRight = BetaEtaNormal.normalize(right);
         BetaEtaNormal noLeft = BetaEtaNormal.normalize(left);
-        SimplificationResult q = Simplifier.simplify(new DisagreementSet(ListUtil.of(new DisagreementPair(left, right))));
         List<Term> match = Matcher.possibleSubstitutionTerms(new Matcher.RigidFlexible(noRight, noLeft));
         assertEquals(3, match.size());
         Term imitator = match.get(0);