diff --git a/generics/generics.js b/generics/generics.js
index 8a4754f..2318d69 100644
--- a/generics/generics.js
+++ b/generics/generics.js
@@ -48,6 +48,75 @@ export const occurring = (type, typeVars) => {
   return new Set();
 }
 
+export const properUnify = eqDict => (
+  {typeVars: formalTypeVars, type: formalType},
+  {typeVars: actualTypeVars, type: actualType},
+) => {
+  if (getEq(eqDict)(formalType)(actualType)) {
+    return {
+      substitutions: new Map(),
+      typeVars: new Set([
+        ...actualTypeVars,
+        // ...formalTypeVars, // <- i don't think we need these?
+      ]),
+      type: actualType,
+    }
+  }
+
+  if (formalTypeVars.has(formalType)) {
+    // formalType is type variable -> substitute it by actualType
+    return {
+      substitutions: new Map([[formalType, actualType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars,
+      ].filter(a => a !== formalType)),
+      type: actualType,
+    }
+  }
+  if (actualTypeVars.has(actualType)) {
+    // same as above, but in opposite direction:
+    // actualType is type variable -> substitute it by formalType
+    return {
+      substitutions: new Map([[actualType, formalType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars,
+      ].filter(a => a !== actualType)),
+      type: formalType,
+    }
+  }
+  
+  // WIP...
+}
+
+const mergeOneWay = (m1, m2) => {
+  const m1copy = new Map(m1);
+  const m2copy = new Map(m2);
+  for (const [key1, val1] of m1copy.entries()) {
+    if (m2copy.has(val1)) {
+      m1copy.set(key1, m2.get(val1));
+      m2copy.delete(val1);
+      return [false, m1copy, m2copy, new Set([val1])];
+    }
+  }
+  return [true, m1copy, m2copy, new Set()]; // stable
+}
+
+export const mergeSubstitutions = (m1, m2) => {
+  let stable = false;
+  let deletedTypeVars = new Set();
+  while (!stable) {
+    let d;
+    // notice we swap m2 and m1, so the rewriting can happen both ways:
+    [stable, m2, m1, d] = mergeOneWay(m1, m2);
+    if (!stable) {
+      deletedTypeVars = deletedTypeVars.union(d);
+    }
+  }
+  return [new Map([...m1, ...m2]), deletedTypeVars];
+}
+
 // Currently very ad-hoc.
 
 // Thanks to Hans for pointing out that this algorithm exactly like "Unification" in Prolog (hence the function name):
@@ -77,6 +146,17 @@ export const unify = (
     };
   }
 
+  if (actualTypeVars.has(actualType)) {
+    // same as above, but in the other direction
+    return {
+      substitutions: new Map([[actualType, formalType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars].filter(a => a !== actualType)),
+      type: formalType,
+    };
+  }
+
   if (formalType.in !== undefined) {
     // function type
     if (actualType.in === undefined) {
@@ -95,13 +175,15 @@ export const unify = (
         }
       }
       // merge substitutions
-      const newSubstitutions = new Map([
-        ...inType.substitutions,
-        ...outType.substitutions,
-      ]);
+      const [newSubstitutions, deletedTypeVars] = mergeSubstitutions(
+        inType.substitutions, outType.substitutions);
+      // const newSubstitutions = new Map([
+      //   ...inType.substitutions,
+      //   ...outType.substitutions,
+      // ]);
       const newTypeVars = new Set([
         ...actualTypeVars,
-        ...formalTypeVars].filter(a => !newSubstitutions.has(a)));
+        ...formalTypeVars].filter(a => !newSubstitutions.has(a) && !deletedTypeVars.has(a)));
       return {
         substitutions: newSubstitutions,
         typeVars: newTypeVars,
diff --git a/generics/generics.test.js b/generics/generics.test.js
index e20634d..182e52b 100644
--- a/generics/generics.test.js
+++ b/generics/generics.test.js
@@ -1,20 +1,21 @@
 import { Bool, Int } from "../primitives/symbols.js";
 import { lsType } from "../structures/list_common.js";
 import { fnType } from "../metacircular.js";
-import { assign, makeGeneric, unify } from "./generics.js";
+import { assign, makeGeneric, mergeSubstitutions, unify } from "./generics.js";
+import { select } from "@inquirer/prompts";
 
 // a -> Int
 const a_to_Int = makeGeneric(a => fnType({in: a, out: Int}));
 // Bool -> Int
 const Bool_to_Int = makeGeneric(() => fnType({in: lsType(Bool), out: Int}));
-// should be: Bool -> Int
+console.log("should be: Bool -> Int")
 console.log(unify(a_to_Int, Bool_to_Int));
 
 // (a -> a) -> b
 const fnType2 = makeGeneric((a,b) => fnType({in: fnType({in: a, out: a}), out: b}));
 // (Bool -> Bool) -> a
 const fnType3 = makeGeneric(a => fnType({in: fnType({in: Bool, out: Bool}), out: a}));
-// should be: (Bool -> Bool) -> a
+console.log("should be: (Bool -> Bool) -> a");
 console.log(unify(fnType2, fnType3));
 
 // (a -> b) -> [a] -> [b]
@@ -26,5 +27,14 @@ const mapFnType = makeGeneric((a,b) =>
 // a -> a
 const idFnType = makeGeneric(a =>
   fnType({in: a, out: a}));
-// should be: [a] -> [a]
+console.log("should be: [a] -> [a]");
 console.log(assign(mapFnType, idFnType));
+
+// (a -> Int) -> [a] -> a
+const weirdFnType = makeGeneric(a =>
+  fnType({
+    in: fnType({in: a, out: Int}),
+    out: fnType({in: lsType(a), out: a}),
+  }));
+console.log("should be: [Int] -> Int");
+console.log(assign(weirdFnType, idFnType));
\ No newline at end of file
diff --git a/typeclasses/eq.js b/typeclasses/eq.js
index e69de29..12efd21 100644
--- a/typeclasses/eq.js
+++ b/typeclasses/eq.js
@@ -0,0 +1,38 @@
+import { makeGeneric } from "../generics/generics";
+import { Type, typedFnType } from "../metacircular";
+import { Bool, Byte, Char, Double, Int } from "../primitives/symbols";
+import { deepEqual } from "../util";
+import { eqDictType } from "./eq_type";
+
+export const getEq = numDict => numDict.eq;
+
+export const ModuleEq = {l:[
+  ...typedFnType(eqDictType, fnType => fnType({in: Type, out: Type})),
+
+  ...typedFnType(getEq, fnType => makeGeneric(a =>
+    fnType({
+      in: eqDictType(a),
+      out: fnType({
+        in: a,
+        out: fnType({
+          in: a,
+          out: Bool,
+        }),
+      }),
+    }))),
+]};
+
+// all our data (and types) are encoded such that we can test equality the same way:
+
+const eq = x => y => deepEqual(x,y);
+
+const EqDict = {eq};
+
+export const EqInstances = new Map([
+  [Int, EqDict],
+  [Bool, EqDict],
+  [Double, EqDict],
+  [Byte, EqDict],
+  [Char, EqDict],
+  [Type, EqDict],
+]);
diff --git a/typeclasses/eq_type.js b/typeclasses/eq_type.js
new file mode 100644
index 0000000..09e5614
--- /dev/null
+++ b/typeclasses/eq_type.js
@@ -0,0 +1,4 @@
+import { DefaultMap } from "../util.js";
+
+const eqDictTypeRegistry = new DefaultMap(a => ({ eqDict: a }));
+export const eqDictType = a => eqDictTypeRegistry.getdefault(a, true);
diff --git a/typeclasses/num.test.js b/typeclasses/num.test.js
index 95c3f19..f05b31a 100644
--- a/typeclasses/num.test.js
+++ b/typeclasses/num.test.js
@@ -2,6 +2,7 @@ import { assign } from "../generics/generics.js";
 import { makeGeneric } from "../generics/generics.js";
 import { fnType } from "../metacircular.js";
 import { Double, Int } from "../primitives/symbols.js";
+import { getMul, NumInstances } from "./num.js";
 import { numDictType } from "./num_type.js";
 
 const square = numDict => x => getMul(numDict)(x)(x);
@@ -21,3 +22,7 @@ console.log(assign(squareFnType, makeGeneric(() => numDictType(Int))));
 // should be: Double -> Double
 console.log(assign(squareFnType, makeGeneric(() => numDictType(Double))));
 
+// to call 'square' we need:
+//   - access to a mapping from types to their typeclass instantiation
+//   - to know that our argument is 'Int'
+console.log(square(NumInstances.get(Int))(42n)); // 1764n