diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000000000000000000000000000000000..6f9fbd81e3457d0dda888a32acfed99c8dfd9e10
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "dhall-lang"]
+	path = dhall-lang
+	url = https://github.com/dhall-lang/dhall-lang.git
diff --git a/dhall-lang b/dhall-lang
new file mode 160000
index 0000000000000000000000000000000000000000..b583925f00ef787e201bb07bed0e6fef0db9463d
--- /dev/null
+++ b/dhall-lang
@@ -0,0 +1 @@
+Subproject commit b583925f00ef787e201bb07bed0e6fef0db9463d
diff --git a/lib/ast.rb b/lib/ast.rb
index e4a5e354a8fb69c41267f117fa776e844f74dedd..8c57919cc0025d343e5fe5114c3eaf8b62c4e154 100644
--- a/lib/ast.rb
+++ b/lib/ast.rb
@@ -636,7 +636,7 @@ module Dhallish
 							new_path = File.dirname src
 						else
 							opath = basedir.path
-							basedir.path = File.join basedir.path,  (@prefix + src)
+							basedir.path = File.join basedir.path, (@prefix + src)
 							src = basedir.to_s
 							basedir.path = File.dirname basedir.path
 							new_path = URI basedir.to_s
@@ -652,6 +652,8 @@ module Dhallish
 						new_path.path = File.dirname new_path.path
 					end
 
+					# STDERR.puts "import src: #{src}"
+
 					file = open(src)
 					text = file.read
 
diff --git a/lib/stdlib.rb b/lib/stdlib.rb
index 48a05057b39ffb91fc4f8d1a62306066559471f1..cd5f24b71aef34e5a3a56d866288eb8697ec99f7 100644
--- a/lib/stdlib.rb
+++ b/lib/stdlib.rb
@@ -21,6 +21,12 @@ module Dhallish
 	end
 	module_function :make_fn_type
 
+	def define(ctx, name, value, type)
+		ctx["<#TYPES#>"][name.to_s] = type
+		ctx["<#VALS#>"][name.to_s] = value
+	end
+	module_function :define
+
 	def fill_context(globalctx, types)
 
 		# Types:
@@ -78,7 +84,7 @@ module Dhallish
 		globalctx["Double/toInteger"] = douToInt
 		types["Double/toInteger"] = Types::Function.new(Types::Double, Types::Integer)
 
-
+=begin
 		# Lists:
 		globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
 		types["List"] = make_fn_type([:list_a], Types::Type.new(Types::List.new(Types::Unresolved.new(:list_a))))
@@ -262,6 +268,191 @@ module Dhallish
 			f.call(Types::Natural).call(succ).call(zero)
 		}
 		types["Natural/build"] = make_fn_type(make_fn_type([:nat_build_a], make_fn_type(:nat_build_a, :nat_build_a), :nat_build_a, :nat_build_a), Types::Natural)
+=end
+
+		# Lists:
+		globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
+		types["List"] = make_fn_type([:a], Types::Type.new(Types::List.new(Types::Unresolved.new(:a))))
+
+		list_length_type = make_fn_type([:a], Types::List.new(Types::Unresolved.new(:a)), Types::Natural)
+		globalctx["List/length"] = BuiltinFunction.new{ |a|
+			BuiltinFunction.new { |list|
+				list.length
+			}
+		}
+		types["List/length"] = list_length_type
+
+		list_fold_type = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			[:b],
+			make_fn_type(:a, :b, :b),
+			:b, :b)
+		globalctx["List/fold"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list|
+				BuiltinFunction.new { |b|
+					BuiltinFunction.new { |f|
+						BuiltinFunction.new { |x|
+							acc = x
+							list.reverse_each { |elm| acc = f.call(elm).call(acc) }
+							acc
+						}
+					}
+				}
+			}
+		}
+		types["List/fold"] = list_fold_type
+
+		list_head_type = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			Types::Optional.new(Types::Unresolved.new(:a)))
+		globalctx["List/head"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list|
+				list.first
+			}
+		}
+		types["List/head"] = list_head_type
+
+		list_last_type = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			Types::Optional.new(Types::Unresolved.new(:a)))
+		globalctx["List/last"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list|
+				list.last
+			}
+		}
+		types["List/last"] = list_last_type
+
+		list_tail_type = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			Types::List.new(Types::Unresolved.new(:a)))
+		globalctx["List/tail"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list|
+				if list.empty?
+					[]
+				else
+					list[1..list.length]
+				end
+			}
+		}
+		types["List/tail"] = list_tail_type
+
+		types["List/reverse"] = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			Types::List.new(Types::Unresolved.new(:a)))
+		globalctx["List/reverse"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list| list.reverse }
+		}
+
+		types["List/build"] = make_fn_type(
+			[:a],
+			make_fn_type(
+				[:b],
+				make_fn_type(:a, :b, :b), :b, :b),
+			Types::List.new(Types::Unresolved.new(:a)))
+		globalctx["List/build"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |f|
+				cons = BuiltinFunction.new { |x|
+					BuiltinFunction.new { |list| [x] + list }
+				}
+				f.call(Types::List.new(a)).call(cons).call([])
+			}
+		}
+
+		types["List/indexed"] = make_fn_type(
+			[:a],
+			Types::List.new(Types::Unresolved.new(:a)),
+			Types::List.new(Types::Record.new({
+				"index" => Types::Natural,
+				"value" => Types::Unresolved.new(:a)})))
+		globalctx["List/indexed"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |list|
+				list.map.with_index { |val, idx|
+					{ "index" => idx, "value" => val }
+				}
+			}
+		}
+
+		# Optionals:
+		globalctx["Optional"] = BuiltinFunction.new { |a|
+			Types::Optional.new(a)
+		}
+		types["Optional"] = make_fn_type([:opt_a], Types::Type.new(Types::Optional.new(Types::Unresolved.new(:opt_a))))
+
+		optional_fold_type = make_fn_type(
+			[:a],
+			Types::Optional.new(Types::Unresolved.new(:a)),
+			[:b],
+			make_fn_type(:a, :b),
+			:b, :b)
+		globalctx["Optional/fold"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |opt|
+				BuiltinFunction.new { |b|
+					BuiltinFunction.new { |f|
+						BuiltinFunction.new { |x|
+							if opt.nil?
+								x
+							else
+								f.call(opt)
+							end
+						}
+					}
+				}
+			}
+		}
+		types["Optional/fold"] = optional_fold_type
+
+		types["Optional/build"] = make_fn_type(
+			[:a],
+			make_fn_type([:b],
+				make_fn_type(:a, :b), :b, :b),
+			Types::Optional.new(Types::Unresolved.new(:a)))
+		globalctx["Optional/build"] = BuiltinFunction.new { |a|
+			BuiltinFunction.new { |f|
+				just = BuiltinFunction.new { |x| x }
+				f.call(Types::Optional.new(a)).call(just).call(nil)
+			}
+		}
+
+
+		# Naturals:
+		natural_fold_type = make_fn_type(
+			Types::Natural,
+			[:a],
+			make_fn_type(:a, :a),
+			:a, :a)
+		globalctx["Natural/fold"] = BuiltinFunction.new { |n|
+			BuiltinFunction.new { |a|
+				BuiltinFunction.new { |succ|
+					BuiltinFunction.new { |zero|
+						res = zero
+						n.times { res = succ.call(res) }
+						res
+					}
+				}
+			}
+		}
+		types["Natural/fold"] = natural_fold_type
+
+		types["Natural/even"] = make_fn_type(Types::Natural, Types::Bool)
+		globalctx["Natural/even"] = BuiltinFunction.new { |n| n % 2 == 0 }
+
+		types["Natural/odd"] = make_fn_type(Types::Natural, Types::Bool)
+		globalctx["Natural/odd"] = BuiltinFunction.new { |n| n % 2 == 1 }
+
+		types["Natural/isZero"] = make_fn_type(Types::Natural, Types::Bool)
+		globalctx["Natural/isZero"] = BuiltinFunction.new { |n| n == 0 }
+
+		globalctx["Natural/build"] = BuiltinFunction.new { |f|
+			zero = 0
+			succ = BuiltinFunction.new { |n| n + 1 }
+			f.call(Types::Natural).call(succ).call(zero)
+		}
+		types["Natural/build"] = make_fn_type(make_fn_type([:a], make_fn_type(:a, :a), :a, :a), Types::Natural)
 
 	end
 	module_function :fill_context
diff --git a/lib/types.rb b/lib/types.rb
index 1e6bbee26f4eacf1214c09402f6369345a34d9c5..b36499edca49bf8bd90578e77dd1d868f8980558 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -23,7 +23,7 @@ module Dhallish
 				end
 			end
 			def to_s()
-				if @metadata.nil? or @metadata.is_a? Unresolved
+				if @metadata.nil?
 					"Type"
 				else
 					"Type(#{@metadata.to_s})"
@@ -149,10 +149,16 @@ module Dhallish
 			end
 		end
 
+		# basically a substitution
 		def resolve(orgtype, name, newtype)
+			puts "resolve[#{name} => #{newtype}]:\t#{orgtype}"
 			case orgtype
 			when Type
-				Type.new(resolve(orgtype.metadata, name, newtype))
+				if !orgtype.metadata.nil?
+					Type.new(resolve(orgtype.metadata, name, newtype))
+				else
+					Type.new(nil)
+				end
 			when Unresolved
 				if name == orgtype.name
 					newtype
@@ -160,17 +166,25 @@ module Dhallish
 					orgtype
 				end
 			when Function
-				if orgtype.restype.nil?
-					Function.new(resolve(orgtype.argtype, name, newtype), nil, orgtype.unres)
-				else
-					restype = orgtype.restype
-					argtype = orgtype.argtype
-					if orgtype.unres.nil? or orgtype.unres != name
-						restype = resolve(orgtype.restype, name, newtype)
-						argtype = resolve(orgtype.argtype, name, newtype)
-					end
-					Function.new(argtype, restype, orgtype.unres)
+				restype = orgtype.restype
+				argtype = orgtype.argtype
+				unres = orgtype.unres
+				if orgtype.unres.nil? or orgtype.unres != name
+					restype = resolve(orgtype.restype, name, newtype)
+					argtype = resolve(orgtype.argtype, name, newtype)
+				elsif !orgtype.unres.nil?
+					assert("debug: #{orgtype}") {
+						argtype == Type.new(Unresolved.new(orgtype.unres))
+					}
+					# TODO: resolve bug?
+					# Bug vielleicht in call node?
+					# `dhalltest.rb`
+					#puts "1--> #{Function.new(argtype, restype, unres)}"
+					#argtype = resolve(orgtype.argtype, name, newtype)
+					#unres = name
+					#puts "2--> #{Function.new(argtype, restype, unres)}"
 				end
+				Function.new(argtype, restype, unres)
 			when Optional
 				Optional.new(resolve(orgtype.type, name, newtype))
 			when List
@@ -180,6 +194,7 @@ module Dhallish
 			when Union
 				Union.new(orgtype.types.map{ |key, val| [key, resolve(val, name, newtype)] }.to_h)
 			else
+				assert("debug: #{orgtype}") { is_a_type?(orgtype) }
 				orgtype
 			end
 		end
@@ -188,82 +203,87 @@ module Dhallish
 		def unification(a, b, mapping={})
 			case a
 			when Type
-				if b.is_a? Type
+				if !b.is_a? Type; return nil end
+				# I think those Kinds dhall has might be important here.
+				# `Type` is actually of type `Kind`?
+				# TODO: There is stuff to be done here i think...
+				if !a.metadata.nil? and !b.metadata.nil?
 					unification(a.metadata, b.metadata, mapping)
+				elsif b.metadata.nil?
+					mapping
 				else
 					nil
 				end
+			when Natural, Integer, Double, Text, Bool
+				if a == b; mapping else nil end
+			when List
+				if !b.is_a? List; return nil end
+				unification(a.type, b.type, mapping)
+			when Optional
+				if !b.is_a? Optional; return nil end
+				unification(a.type, b.type, mapping)
+			when Record
+				if !b.is_a? Record or a.types.length != b.types.length; return nil end
+				for key in a.types.keys
+					afield = a.types[key]
+					bfield = b.types[key]
+					if bfield.nil? or unification(afield, bfield, mapping).nil?
+						return nil
+					end
+				end
+				mapping
+			when Union
+				if !b.is_a? Union or a.types.length != b.types.length; return nil end
+				for key in a.types.keys
+					afield = a.types[key]
+					bfield = b.types[key]
+					if bfield.nil? or unification(afield, bfield, mapping).nil?
+						return nil
+					end
+				end
+				mapping
 			when Unresolved
-				if b.is_a? Unresolved
-					if mapping[a.name] == nil
-						mapping[a.name] = b.name
+				if !b.is_a? Unresolved; return nil end
+				if mapping[a.name] != nil
+					if mapping[a.name] == b.name
 						mapping
-					elsif mapping[a.name] != b.name
-						nil
 					else
-						mapping
+						nil
 					end
 				else
-					nil
+					mapping[a.name] = b.name
+					mapping
 				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)
+				if !b.is_a? Function; return nil end
+				if !a.unres.nil?
+					assert("debug: #{a}") { a.argtype.is_a? Type and a.argtype.metadata == Unresolved.new(a.unres) }
+					if b.unres.nil?; return nil end
+					assert("debug: #{b}") { b.argtype.is_a? Type and b.argtype.metadata == Unresolved.new(b.unres) }
+
+					# TODO: Update mapping?
+					# TODO: keys and values swapped?
+
+					arestype = a.restype
+					brestype = b.restype
+					if mapping.keys.include? a.unres
+						sym = get_new_sym()
+						arestype = resolve(arestype, a.unres, Unresolved.new(sym))
 					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
+					if mapping.values.include? b.unres
+						sym = get_new_sym()
+						brestype = resolve(brestype, b.unres, Unresolved.new(sym))
 					end
-					mapping
+					unification(arestype, brestype, mapping)
 				else
-					nil
-				end
-			when Union
-				if b.is_a? Union 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
+					if !unification(a.argtype, b.argtype, mapping).nil?
+						unification(a.restype, b.restype, mapping)
+					else
+						nil
 					end
-					mapping
-				else
-					nil
 				end
 			else
-				if a == b
-					mapping
-				else
-					nil
-				end
+				raise "New Type? a: #{a.inspect}, b: #{b.inspect}"
 			end
 		end
 		module_function :unification
@@ -307,9 +327,11 @@ module Dhallish
 			"{#{ dhallval.map{ |key, val| "\"#{escape_str(key)}\": #{ to_json(val) }" }.join(", ") }}"
 		when nil
 			"null"
+		when Union
+			to_json(dhallval.init_val)
 		else
 			if Types::is_a_type? dhallval
-				"\"#{dhallval.to_s}\""
+				"\"Dhallish::Type(#{dhallval.to_s})\""
 			else
 				"\"<#{escape_str(dhallval.class.to_s)}##{dhallval.hash.abs.to_s(16)}>\""
 			end
diff --git a/lib/utils.rb b/lib/utils.rb
index b03bd3ae75a5d117a379221e525d0e83a37704e8..300fb1e6152cfcefb74a668769f07d58dcac5a4d 100644
--- a/lib/utils.rb
+++ b/lib/utils.rb
@@ -16,7 +16,7 @@ end
 $dhallish_internal_global_counter = 0
 def get_new_sym()
 	$dhallish_internal_global_counter += 1
-	("__newsym_#{$dhallish_internal_global_counter}").to_sym
+	("__#{$dhallish_internal_global_counter}").to_sym
 end
 
 def escape_str(str)
diff --git a/tests/test.rb b/tests/test.rb
index 6e1205583dde98b1117477db603d1e7d3026867d..c6cc00e66630af777adb3240493b9e4891762e08 100755
--- a/tests/test.rb
+++ b/tests/test.rb
@@ -36,7 +36,7 @@ positive_tests = {
 	"fallback for file import": ["let x = ./foobarfoobar.dhall as Text ? 1 in x", 1],
 	"more type annotation": [ "let f = \\(a: Type) -> \\(l: List a) -> \\(x: a) -> x in (f: forall(b: Type) -> forall(l: List b) -> b -> b) Natural [1, 2, 3] 5", 5 ],
 	"select from union": [ "let union = <a : Natural | b : Text>.a 17 in union.a : Optional Natural", 17 ],
-        "union merge": [ "merge { Left = \\(x: Natural) -> Natural/show x, Right = \\(y: Integer) -> Integer/show y } < Left = 42 | Right : Integer >", "42" ]
+	"union merge": [ "merge { Left = \\(x: Natural) -> Natural/show x, Right = \\(y: Integer) -> Integer/show y } < Left = 42 | Right : Integer >", "42" ]
 }
 
 negative_tests = {
@@ -115,3 +115,12 @@ dhallfiles.each { |file|
 		print_msg(file, true)
 	end
 }
+
+puts "\n=== Testing Typecheck on dhall-lang/Prelude/package.dhall"
+begin
+  Dhallish::evaluate("./" + File.join(File.dirname(__FILE__), "../dhall-lang/Prelude/package.dhall"))
+rescue
+	print_msg("Prelude/package.dhall", false)
+else
+	print_msg("Prelude/package.dhall", true)
+end