diff --git a/README.md b/README.md
index 97b4901188874c718045821c0266b03f2357cca5..d31ce70c61bdb4e6b8b41b77815525d4df324b0a 100644
--- a/README.md
+++ b/README.md
@@ -1,38 +1,38 @@
 # Ruby-Implementation of a Dhall-like Language
 
+If you want to use *Dhall* in production and do not use *ruby*, use the official haskell version linked below.
+
 - Dhall github project: https://github.com/dhall-lang
 - Treetop library's home page: http://cjheath.github.io/treetop/index.html
 
 See `./tests` for an example of dhallish-code that should work. `.dhall`-files show code that
 evaluates equally in `dhall` and `dhallish`. Code samples in `./tests/test.rb` might be dhallish-specific.
-See `./bin/dhallish` for an example on how to use the `Dhallish` module.
+See `./bin/dhallish` or `./tests/test_dhallish_ctx.rb` for an example on how to use the `Dhallish` module.
+
+*Read [the docs](./DOCS.md)!*
 
 ```bash
 # run tests using:
 ruby ./tests/test.rb
 
 # use dhall as a command line tool:
+./bin/dhallish --help
 ./bin/dhallish <<< "1 + 2"
+
+# examples and usage:
+cat ./tests/examples.dhallish
+./bin/dhallish --help
+./bin/dhallish < texts/examples.dhallish
 ```
 
 ### Changes to `dhall-lang`:
 - More Operators: `<`, `>`, `<=`, `>=`, `-`, `/`
 - `==` and `!=` do work on Numbers (`Natural`s, `Integer`s and `Double`s)
+- It is possible to get an Optional from an union
 
 ### Missing Features:
-- [x] Optionals
-- [x] Records
-- [x] Functions
-- [x] Imports
-- [x] `env:...`
-- [ ] Stuff we are not thinking of right now...
-- Unions (not planed)
-
-## TODO
-- [ ] disallow Type Names like `Natural` or `let` as labels
-- [ ] more tests and tests for expected failure
-- [ ] "n-1": currently interpreted as label, but should be a subtraction (sometimes)
-- [ ] Bignums for Integers?
-- [ ] Multi Line strings
-- [ ] quoted labels
-- [ ] MORE UNICODE!
+- `''strings that start with two quotes''`
+
+### Known Bugs:
+- There is a bug in our unification or substitution that only appears in rare cases when the same name for a generic type is used multiple times.
+
diff --git a/lib/stdlib.rb b/lib/stdlib.rb
index cf5b5a72ddb61f12816c303eb76028996df94e91..c0ccf9130e2ea3bf536fa5a21cd6f1b36c1b565e 100644
--- a/lib/stdlib.rb
+++ b/lib/stdlib.rb
@@ -3,13 +3,17 @@ require_relative './utils.rb'
 
 module Dhallish
 
+	# Utility function to create dhallish function types:
+	# Use [:name] to introduce a new unresolved type and write
+	# :name to use it. Look at `fill_context` for examples.
 	def make_fn_type(*args, rettype)
 		if Types::not_a_type?(rettype); rettype = Types::Unresolved.new(rettype) end
 		args.reverse.reduce(rettype) { |rettype, arg|
 			argtype = arg
 			name = nil
 			if arg.is_a? Array
-				argtype, name = arg
+				name = arg[0]
+				argtype = Types::Type.new(Types::Unresolved.new(name))
 			end
 			if Types::not_a_type?(argtype); argtype = Types::Unresolved.new(argtype) end
 			Types::Function.new(argtype, rettype, name)
@@ -74,9 +78,9 @@ module Dhallish
 
 		# Lists:
 		globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
-		types["List"] = make_fn_type([Types::Type.new, :a], Types::Type.new(Types::List.new(Types::Unresolved.new(:a))))
+		types["List"] = make_fn_type([:list_a], Types::Type.new(Types::List.new(Types::Unresolved.new(:list_a))))
 
-		list_length_type = make_fn_type([Types::Type.new(Types::Unresolved.new(:a)), :a], Types::List.new(Types::Unresolved.new(:a)), Types::Natural)
+		list_length_type = make_fn_type([:list_len_a], Types::List.new(Types::Unresolved.new(:list_len_a)), Types::Natural)
 		globalctx["List/length"] = BuiltinFunction.new{ |a|
 			BuiltinFunction.new { |list|
 				list.length
@@ -85,11 +89,11 @@ module Dhallish
 		types["List/length"] = list_length_type
 
 		list_fold_type = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
-			[Types::Type.new(Types::Unresolved.new(:b)), :b],
-			make_fn_type(:a, :b, :b),
-			:b, :b)
+			[:list_fold_a],
+			Types::List.new(Types::Unresolved.new(:list_fold_a)),
+			[:list_fold_b],
+			make_fn_type(:list_fold_a, :list_fold_b, :list_fold_b),
+			:list_fold_b, :list_fold_b)
 		globalctx["List/fold"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				BuiltinFunction.new { |b|
@@ -104,9 +108,9 @@ module Dhallish
 		types["List/fold"] = list_fold_type
 
 		list_head_type = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
-			Types::Optional.new(Types::Unresolved.new(:a)))
+			[:list_head_a],
+			Types::List.new(Types::Unresolved.new(:list_head_a)),
+			Types::Optional.new(Types::Unresolved.new(:list_head_a)))
 		globalctx["List/head"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.first
@@ -115,9 +119,9 @@ module Dhallish
 		types["List/head"] = list_head_type
 
 		list_last_type = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
-			Types::Optional.new(Types::Unresolved.new(:a)))
+			[:list_last_a],
+			Types::List.new(Types::Unresolved.new(:list_last_a)),
+			Types::Optional.new(Types::Unresolved.new(:list_last_a)))
 		globalctx["List/last"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.last
@@ -126,9 +130,9 @@ module Dhallish
 		types["List/last"] = list_last_type
 
 		list_tail_type = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
-			Types::List.new(Types::Unresolved.new(:a)))
+			[:list_tail_a],
+			Types::List.new(Types::Unresolved.new(:list_tail_a)),
+			Types::List.new(Types::Unresolved.new(:list_tail_a)))
 		globalctx["List/tail"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				if list.empty?
@@ -141,19 +145,19 @@ module Dhallish
 		types["List/tail"] = list_tail_type
 
 		types["List/reverse"] = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
-			Types::List.new(Types::Unresolved.new(:a)))
+			[:list_reverse_a],
+			Types::List.new(Types::Unresolved.new(:list_reverse_a)),
+			Types::List.new(Types::Unresolved.new(:list_reverse_a)))
 		globalctx["List/reverse"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list| list.reverse }
 		}
 
 		types["List/build"] = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
+			[:list_build_a],
 			make_fn_type(
-				[Types::Type.new(Types::Unresolved.new(:b)), :b],
-				make_fn_type(:a, :b, :b), :b, :b),
-			Types::List.new(Types::Unresolved.new(:a)))
+				[:list_build_b],
+				make_fn_type(:list_build_a, :list_build_b, :list_build_b), :list_build_b, :list_build_b),
+			Types::List.new(Types::Unresolved.new(:list_build_a)))
 		globalctx["List/build"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |f|
 				cons = BuiltinFunction.new { |x|
@@ -164,11 +168,11 @@ module Dhallish
 		}
 
 		types["List/indexed"] = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::List.new(Types::Unresolved.new(:a)),
+			[:list_indexed_a],
+			Types::List.new(Types::Unresolved.new(:list_indexed_a)),
 			Types::List.new(Types::Record.new({
 				"index" => Types::Natural,
-				"value" => Types::Unresolved.new(:a)})))
+				"value" => Types::Unresolved.new(:list_indexed_a)})))
 		globalctx["List/indexed"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.map.with_index { |val, idx|
@@ -181,14 +185,14 @@ module Dhallish
 		globalctx["Optional"] = BuiltinFunction.new { |a|
 			Types::Optional.new(a)
 		}
-		types["Optional"] = make_fn_type([Types::Type.new, :a], Types::Type.new(Types::Optional.new(Types::Unresolved.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(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			Types::Optional.new(Types::Unresolved.new(:a)),
-			[Types::Type.new(Types::Unresolved.new(:b)), :b],
-			make_fn_type(:a, :b),
-			:b, :b)
+			[:opt_fold_a],
+			Types::Optional.new(Types::Unresolved.new(:opt_fold_a)),
+			[:opt_fold_b],
+			make_fn_type(:opt_fold_a, :opt_fold_b),
+			:opt_fold_b, :opt_fold_b)
 		globalctx["Optional/fold"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |opt|
 				BuiltinFunction.new { |b|
@@ -207,10 +211,10 @@ module Dhallish
 		types["Optional/fold"] = optional_fold_type
 
 		types["Optional/build"] = make_fn_type(
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			make_fn_type([Types::Type.new(Types::Unresolved.new(:b)), :b],
-				make_fn_type(:a, :b), :b, :b),
-			Types::Optional.new(Types::Unresolved.new(:a)))
+			[:opt_build_a],
+			make_fn_type([:opt_build_b],
+				make_fn_type(:opt_build_a, :opt_build_b), :opt_build_b, :opt_build_b),
+			Types::Optional.new(Types::Unresolved.new(:opt_build_a)))
 		globalctx["Optional/build"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |f|
 				just = BuiltinFunction.new { |x| x }
@@ -222,9 +226,9 @@ module Dhallish
 		# Naturals:
 		natural_fold_type = make_fn_type(
 			Types::Natural,
-			[Types::Type.new(Types::Unresolved.new(:a)), :a],
-			make_fn_type(:a, :a),
-			:a, :a)
+			[:nat_fold_a],
+			make_fn_type(:nat_fold_a, :nat_fold_a),
+			:nat_fold_a, :nat_fold_a)
 		globalctx["Natural/fold"] = BuiltinFunction.new { |n|
 			BuiltinFunction.new { |a|
 				BuiltinFunction.new { |succ|
@@ -252,7 +256,7 @@ module Dhallish
 			succ = BuiltinFunction.new { |n| n + 1 }
 			f.call(Types::Natural).call(succ).call(zero)
 		}
-		types["Natural/build"] = make_fn_type(make_fn_type([Types::Type.new(Types::Unresolved.new(:a)), :a], make_fn_type(:a, :a), :a, :a), Types::Natural)
+		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
 	module_function :fill_context