diff --git a/lib/types.rb b/lib/types.rb
index d5d7acaca707c9b16eb36f5f51fadea1a0244ce6..6dbd9d8928cd03f60db33442c64f691f35ee4016 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -148,6 +148,73 @@ module Dhallish
 		end
 		module_function :resolve
 
+		def unification(a, b, mapping={})
+			assert("a and b must be types") { is_a_type(a) and is_a_type(b) }
+			case a
+			when Type
+				if b.is_a? Type
+					unification(a.metadata, b.metadata, mapping)
+				else
+					nil
+				end
+			when Unresolved
+				if b.is_a? Unresolved
+					if mapping[a.name] == nil
+						mapping[a.name] = b.name
+						mapping
+					elsif mapping[a.name] != mapping[b.name]
+						nil
+					else
+						mapping
+					end
+				else
+					nil
+				end
+			when Function
+				if b.is_a? Function
+					if unification(a.argtype, b.argtype, mapping).nil?
+						nil
+					else
+						arestype = a.restype
+						brestype = b.restype
+						if !a.unres.nil?; arestype = resolve(a.restype, a.unres, Unresolved.new(get_new_sym())) end
+						if !b.unres.nil?; brestype = resolve(b.restype, b.unres, Unresolved.new(get_new_sym())) end
+						unification(arestype, brestype, mapping)
+					end
+				else
+					nil
+				end
+			when Optional
+				if b.is_a? Optional
+					unification(a.type, b.type, mapping)
+				else
+					nil
+				end
+			when List
+				if b.is_a? List
+					unification(a.type, b.type, mapping)
+				else
+					nil
+				end
+			when Record
+				if b.is_a? Record and a.types.keys.length == b.types.keys.length
+					for key in a.types.keys
+						aelm = a.types[key]
+						belm = b.types[key]
+						if belm.nil?; return nil end
+						ret = unification(aelm, belm, mapping)
+						if ret.nil?; return nil end
+					end
+					mapping
+				else
+					nil
+				end
+			else
+				a == b
+			end
+		end
+		module_function :unification
+
 		def not_a_type?(x)
 			if x.is_a? Symbol
 				x != Natural and x != Integer and x != Double and x != Bool and x != Text
diff --git a/lib/utils.rb b/lib/utils.rb
index ce32df88a162f7a420f9e868bf0d299110fda6e5..4670dc38fbbb7dd98d6cd5ccf277bff08c50d8ef 100644
--- a/lib/utils.rb
+++ b/lib/utils.rb
@@ -12,3 +12,9 @@ class DhallError < StandardError
 		super(msg)
 	end
 end
+
+$dhallish_internal_global_counter = 0
+def get_new_sym()
+	$dhallish_internal_global_counter += 1
+	("__newsym_#{$dhallish_internal_global_counter}").to_sym
+end