diff --git a/eyg/bin/run-tests.js b/eyg/bin/run-tests.js
index 8abe37a84..d80e5c384 100644
--- a/eyg/bin/run-tests.js
+++ b/eyg/bin/run-tests.js
@@ -11,7 +11,7 @@ async function main() {
   let failures = 0;
 
   for await (let entry of await opendir(dir)) {
-    if (!entry.name.endsWith("test.js")) continue;
+    if (!entry.name.endsWith("terms_test.js")) continue;
     let path = "../" + dir + entry.name;
     process.stdout.write("\nlanguage/" + entry.name.slice(0, -3) + ":\n  ");
     let module = await import(path);
diff --git a/eyg/src/eyg/ast/editor.gleam b/eyg/src/eyg/ast/editor.gleam
index e37b3e827..ba42e8307 100644
--- a/eyg/src/eyg/ast/editor.gleam
+++ b/eyg/src/eyg/ast/editor.gleam
@@ -1603,6 +1603,9 @@ pub fn get_element(tree: e.Expression(a, b), position) -> Element(a, b) {
       let [#(_, child), .._] = list.drop(fields, i)
       get_element(child, rest)
     }
+    // TODO need to get out the union tag
+    #(_, e.Tagged(_tag, value)), [1, ..rest] -> get_element(value, rest)
+
     #(_, e.Let(pattern, _, _)), [0, ..rest] -> get_pattern(pattern, rest, tree)
     #(_, e.Let(_, value, _)), [1, ..rest] -> get_element(value, rest)
     #(_, e.Let(_, _, then)), [2, ..rest] -> get_element(then, rest)
diff --git a/eyg/src/eyg/ast/expression.gleam b/eyg/src/eyg/ast/expression.gleam
index ee35a34c8..26c5fe337 100644
--- a/eyg/src/eyg/ast/expression.gleam
+++ b/eyg/src/eyg/ast/expression.gleam
@@ -57,10 +57,9 @@ pub fn example(config, hole) {
   }
 }
 
-fn tagged(name, value) {
-  function(p.Row([#(name, "then")]), call(variable("then"), value))
-}
-
+// fn tagged(name, value) {
+//   function(p.Row([#(name, "then")]), call(variable("then"), value))
+// }
 pub fn lift_type(_config, hole) {
   case hole {
     t.Function(from, _to) -> {
@@ -154,6 +153,7 @@ pub type Node(m, g) {
   Binary(value: String)
   Tuple(elements: List(Expression(m, g)))
   Row(fields: List(#(String, Expression(m, g))))
+  Tagged(tag: String, value: Expression(m, g))
   Variable(label: String)
   Let(pattern: Pattern, value: Expression(m, g), then: Expression(m, g))
   Function(pattern: Pattern, body: Expression(m, g))
@@ -192,3 +192,15 @@ pub fn tuple_(elements) {
 pub fn variable(label) {
   #(dynamic.from(Nil), Variable(label))
 }
+
+pub fn row(fields) {
+  #(dynamic.from(Nil), Row(fields))
+}
+
+pub fn tagged(tag, value) {
+  #(dynamic.from(Nil), Tagged(tag, value))
+}
+
+pub fn hole() {
+  #(dynamic.from(Nil), Hole)
+}
diff --git a/eyg/src/eyg/inference.gleam b/eyg/src/eyg/inference.gleam
new file mode 100644
index 000000000..73996877a
--- /dev/null
+++ b/eyg/src/eyg/inference.gleam
@@ -0,0 +1,497 @@
+import gleam/io
+import gleam/int
+import gleam/option.{None, Some}
+import gleam/string
+import gleam/list
+import gleam/pair
+import eyg/ast/expression as e
+import eyg/ast/pattern as p
+import eyg/typer/monotype as t
+import eyg/typer
+
+pub fn do_unify(
+  pair: #(t.Monotype(n), t.Monotype(n)),
+  state: State(n),
+) -> Result(State(n), typer.Reason(n)) {
+  let #(t1, t2) = pair
+  case t1, t2 {
+    t.Unbound(i), t.Unbound(j) if i == j -> Ok(state)
+    t.Unbound(i), _ ->
+      case list.key_find(state.substitutions, i) {
+        Ok(t1) -> do_unify(#(t1, t2), state)
+        Error(Nil) -> Ok(add_substitution(i, t2, state))
+      }
+    _, t.Unbound(j) ->
+      case list.key_find(state.substitutions, j) {
+        Ok(t2) -> do_unify(#(t1, t2), state)
+        Error(Nil) -> Ok(add_substitution(j, t1, state))
+      }
+    t.Native(n1), t.Native(n2) if n1 == n2 -> Ok(state)
+    t.Binary, t.Binary -> Ok(state)
+    t.Tuple(e1), t.Tuple(e2) ->
+      case list.zip(e1, e2) {
+        Ok(pairs) -> list.try_fold(pairs, state, do_unify)
+        Error(#(c1, c2)) -> Error(typer.IncorrectArity(c1, c2))
+      }
+    // Is the type only ever Row. I think not it's Record Record and Union Union
+    // TODO t.Record(r1)
+    t.Row(row1, extra1), t.Row(row2, extra2) | t.Union(row1, extra1), t.Union(
+      row2,
+      extra2,
+    ) -> {
+      let #(unmatched1, unmatched2, shared) = typer.group_shared(row1, row2)
+      let #(i, state) = fresh(state)
+      try state = case unmatched2, extra1 {
+        [], _ -> Ok(state)
+        only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(i)), state))
+        only, None -> Error(typer.UnexpectedFields(only))
+      }
+      try state = case unmatched1, extra2 {
+        [], _ -> Ok(state)
+        only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(i)), state))
+        only, None -> Error(typer.MissingFields(only))
+      }
+      list.try_fold(shared, state, do_unify)
+    }
+    t.Function(from1, to1), t.Function(from2, to2) -> {
+      try state = do_unify(#(from1, from2), state)
+      do_unify(#(to1, to2), state)
+    }
+    _, _ -> Error(typer.UnmatchedTypes(t1, t2))
+  }
+}
+
+fn add_substitution(i, type_, state: State(n)) -> State(n) {
+  // These checks arrive too late end up with reursive type only existing in first recursion
+  // We assume i doesn't occur in substitutions
+  // let check =
+  //   list.contains(free_in_type(do_resolve(type_, substitutions, [])), i)
+  // let type_ = case check {
+  //   True -> {
+  //     io.debug("============")
+  //     io.debug(i)
+  //     io.debug(type_)
+  //     t.Recursive(i, type_)
+  //   }
+  //   False -> type_
+  // }
+  let substitutions = [#(i, type_), ..state.substitutions]
+  State(..state, substitutions: substitutions)
+}
+
+fn unify(t1, t2, state: State(n)) {
+  // let State(substitutions: s, ..) = state
+  // try s = do_unify(#(t1, t2), s)
+  // //   TODO add errors here
+  // Ok(State(..state, substitutions: s))
+  do_unify(#(t1, t2), state)
+}
+
+// relies on type having been resolved
+fn do_free_in_type(type_, set) {
+  case type_ {
+    t.Unbound(i) -> push_new(i, set)
+    t.Native(_) | t.Binary -> set
+    t.Tuple(elements) -> list.fold(elements, set, do_free_in_type)
+    t.Row(rows, rest) | t.Union(rows, rest) -> do_free_in_row(rows, rest, set)
+    t.Recursive(i, type_) -> {
+      let inner = do_free_in_type(type_, set)
+      difference(inner, [i])
+    }
+    t.Function(from, to) -> {
+      let set = do_free_in_type(from, set)
+      do_free_in_type(to, set)
+    }
+  }
+}
+
+fn do_free_in_row(rows, rest, set) {
+  let set =
+    list.fold(
+      rows,
+      set,
+      fn(row, set) {
+        let #(_name, type_) = row
+        do_free_in_type(type_, set)
+      },
+    )
+  case rest {
+    None -> set
+    // Already resolved
+    Some(i) -> push_new(i, set)
+  }
+}
+
+pub fn free_in_type(t) {
+  do_free_in_type(t, [])
+}
+
+pub fn do_free_in_polytype(poly, substitutions) {
+  let #(quantifiers, mono) = poly
+  let mono = resolve(mono, substitutions)
+  difference(free_in_type(mono), quantifiers)
+}
+
+pub fn do_free_in_env(env, substitutions, set) {
+  case env {
+    [] -> set
+    [#(_, polytype), ..env] -> {
+      let set = union(do_free_in_polytype(polytype, substitutions), set)
+      do_free_in_env(env, substitutions, set)
+    }
+  }
+}
+
+pub fn free_in_env(env, substitutions) {
+  do_free_in_env(env, substitutions, [])
+}
+
+// TODO smart filter or stateful env
+// |> list.filter(fn(i) { is_not_free_in_env(i, substitutions, env) })
+//   Hmm have Native(Letter) in the type and list of strings in the parameters
+// can't be new numbers
+// Dont need to be named can just use initial i's discovered
+pub fn generalise(mono, substitutions, env) {
+  let mono = resolve(mono, substitutions)
+  let type_params =
+    difference(free_in_type(mono), free_in_env(env, substitutions))
+  #(type_params, mono)
+}
+
+// Need to handle having recursive type on it's own. i.e. i needs to be in Recursive(i, inner)
+pub fn instantiate(poly, state) {
+  let #(forall, mono) = poly
+  let #(substitutions, state) =
+    list.map_state(
+      forall,
+      state,
+      fn(i, state) {
+        // TODO with zip
+        let #(tj, state) = fresh(state)
+        #(#(i, tj), state)
+      },
+    )
+  let t = do_resolve(mono, substitutions, [])
+  #(t, state)
+}
+
+pub fn print(t, state) {
+  let type_ = resolve(t, state)
+  let #(rendered, _) = to_string(type_, [])
+  rendered
+}
+
+pub fn to_string(t, used) {
+  // Having structural types would allow replacing integer variables with letter variables easily in a substitution
+  // a function to list variable types would allow a simple substitution
+  // A lot easier to debug if not using used as part of this
+  case t {
+    t.Unbound(i) -> {
+      let used = push_new(i, used)
+      assert Ok(index) = index(used, i)
+      #(int.to_string(index), used)
+    }
+    t.Recursive(i, t) -> {
+      let used = push_new(i, used)
+      let #(inner, used) = to_string(t, used)
+      assert Ok(index) = index(used, i)
+      let rendered = string.join(["μ", int.to_string(index), ".", inner])
+      #(rendered, used)
+    }
+    t.Tuple(elements) -> {
+      let #(rendered, used) = list.map_state(elements, used, to_string)
+      let rendered =
+        string.join(["(", string.join(list.intersperse(rendered, ", ")), ")"])
+      #(rendered, used)
+    }
+    // TODO used first fn used variable names
+    t.Union(_, _) -> #("UNION", used)
+    t.Binary -> #("Binary", used)
+    t.Function(from, to) -> {
+      let #(from, used) = to_string(from, used)
+      let #(to, used) = to_string(to, used)
+      let rendered = string.join([from, " -> ", to])
+      #(rendered, used)
+    }
+  }
+}
+
+pub fn do_resolve(type_, substitutions: List(#(Int, t.Monotype(n))), recuring) {
+  case type_ {
+    t.Unbound(i) ->
+      case list.find(recuring, i) {
+        Ok(_) -> type_
+        Error(Nil) ->
+          case list.key_find(substitutions, i) {
+            Ok(t.Unbound(j)) if i == j -> type_
+            Error(Nil) -> type_
+            Ok(sub) -> {
+              let inner = do_resolve(sub, substitutions, [i, ..recuring])
+              let recursive = list.contains(free_in_type(inner), i)
+              case recursive {
+                False -> inner
+                True -> t.Recursive(i, inner)
+              }
+            }
+          }
+      }
+    // This needs to exist as might already have been called by generalize
+    t.Recursive(i, sub) -> {
+      let inner = do_resolve(sub, substitutions, [i, ..recuring])
+      t.Recursive(i, inner)
+    }
+    t.Binary -> t.Binary
+    t.Tuple(elements) -> {
+      let elements = list.map(elements, do_resolve(_, substitutions, recuring))
+      t.Tuple(elements)
+    }
+    t.Row(fields, rest) -> {
+      let resolved_fields =
+        list.map(
+          fields,
+          fn(field) {
+            let #(name, type_) = field
+            #(name, do_resolve(type_, substitutions, recuring))
+          },
+        )
+      case rest {
+        None -> t.Row(resolved_fields, None)
+        Some(i) -> {
+          type_
+          case do_resolve(t.Unbound(i), substitutions, recuring) {
+            t.Unbound(j) -> t.Row(resolved_fields, Some(j))
+            t.Row(inner, rest) ->
+              t.Row(list.append(resolved_fields, inner), rest)
+          }
+        }
+      }
+    }
+    t.Union(variants, rest) -> {
+      let resolved_variants =
+        // TODO map_value would help or a resolve_named unify_named etc probably also sensible
+        list.map(
+          variants,
+          fn(variant) {
+            let #(name, type_) = variant
+            #(name, do_resolve(type_, substitutions, recuring))
+          },
+        )
+      case rest {
+        None -> t.Union(resolved_variants, None)
+        Some(i) -> {
+          type_
+          case do_resolve(t.Unbound(i), substitutions, recuring) {
+            t.Unbound(j) -> t.Union(resolved_variants, Some(j))
+            t.Union(inner, rest) ->
+              t.Union(list.append(resolved_variants, inner), rest)
+          }
+        }
+      }
+    }
+    t.Function(from, to) -> {
+      let from = do_resolve(from, substitutions, recuring)
+      let to = do_resolve(to, substitutions, recuring)
+      t.Function(from, to)
+    }
+  }
+}
+
+pub fn resolve(t, state) {
+  let State(substitutions: substitutions, ..) = state
+  do_resolve(t, substitutions, [])
+}
+
+pub type State(n) {
+  State(//   definetly not this
+    // native_to_string: fn(n) -> String,
+    next_unbound: Int, substitutions: List(#(Int, t.Monotype(n))))
+}
+
+fn fresh(state) {
+  let State(next_unbound: i, ..) = state
+  #(t.Unbound(i), State(..state, next_unbound: i + 1))
+}
+
+pub fn infer(untyped, expected) {
+  let state = State(0, [])
+  let scope = []
+  do_infer(untyped, expected, state, scope)
+}
+
+// return just substitutions
+fn do_infer(untyped, expected, state, scope) {
+  let #(_, expression) = untyped
+  case expression {
+    e.Binary(value) ->
+      case unify(expected, t.Binary, state) {
+        Ok(state) -> #(#(Ok(expected), e.Binary(value)), state)
+        Error(reason) -> #(#(Error(reason), e.Binary(value)), state)
+      }
+    e.Tuple(elements) -> {
+      let #(with_type, state) =
+        list.map_state(
+          elements,
+          state,
+          fn(e, state) {
+            let #(u, state) = fresh(state)
+            #(#(e, u), state)
+          },
+        )
+      let #(t, state) = case unify(
+        expected,
+        t.Tuple(list.map(with_type, pair.second)),
+        state,
+      ) {
+        Ok(state) -> #(Ok(expected), state)
+        Error(reason) -> #(Error(reason), state)
+      }
+      let #(elements, state) =
+        list.map_state(
+          with_type,
+          state,
+          fn(with_type, state) {
+            let #(element, expected) = with_type
+            do_infer(element, expected, state, scope)
+          },
+        )
+      #(#(t, e.Tuple(elements)), state)
+    }
+    e.Row(fields) -> {
+      // This approach fails because the fresh type is not available later
+      // let #(fields, state) = list.map_state(fields, state, fn(field, state) {
+      //   let #(name, untyped) = field
+      //   let #(type_, state) = fresh(state)
+      //   let #(typed, state) = do_infer(untyped, type_, state, scope)
+      //   #(#(name, typed), state)
+      // })
+      // let field_types = list.map(fields, fn(field) {
+      //   let #(name, typed) = field
+      //   let #(Ok(type_), _tree) = typed
+      //   #(name, type_)
+      // })
+      // let given = t.Row(field_types, None)
+      // #(#(Ok(t.Tuple([])), e.Binary("")), state)
+      let #(pairs, state) =
+        list.map_state(
+          fields,
+          state,
+          fn(field, state) {
+            let #(name, untyped) = field
+            let #(expected, state) = fresh(state)
+            let row_type = #(name, expected)
+            let #(typed, state) = do_infer(untyped, expected, state, scope)
+            let typed_row = #(name, typed)
+            #(#(row_type, typed_row), state)
+          },
+        )
+      let #(row_types, typed_rows) = list.unzip(pairs)
+      let given = t.Row(row_types, None)
+      let #(t, state) = case unify(expected, given, state) {
+        Ok(state) -> #(Ok(expected), state)
+        Error(reason) -> #(Error(reason), state)
+      }
+      #(#(t, e.Row(typed_rows)), state)
+    }
+    e.Tagged(tag, value) -> {
+      let #(i, state) = fresh(state)
+      let #(t.Unbound(j), state) = fresh(state)
+      let given = t.Union([#(tag, i)], Some(j))
+      let #(t, state) = case unify(expected, given, state) {
+        Ok(state) -> #(Ok(expected), state)
+        Error(reason) -> #(Error(reason), state)
+      }
+      let #(typed, state) = do_infer(value, i, state, scope)
+      #(#(t, e.Tagged(tag, typed)), state)
+    }
+
+    e.Function(p.Variable(label), body) -> {
+      let #(arg, state) = fresh(state)
+      let #(return, state) = fresh(state)
+      let #(t, state) = case unify(expected, t.Function(arg, return), state) {
+        Ok(state) -> #(Ok(expected), state)
+        Error(reason) -> #(Error(reason), state)
+      }
+      let #(body, state) =
+        do_infer(body, return, state, [#(label, #([], arg)), ..scope])
+      #(#(t, e.Function(p.Variable(label), body)), state)
+    }
+    e.Call(func, with) -> {
+      let #(arg, state) = fresh(state)
+      let #(func, state) =
+        do_infer(func, t.Function(arg, expected), state, scope)
+      let #(with, state) = do_infer(with, arg, state, scope)
+      #(#(Ok(expected), e.Call(func, with)), state)
+    }
+
+    e.Let(p.Variable(label), value, then) -> {
+      let #(u, state) = fresh(state)
+      //   TODO haandle self case or variable renaming
+      let value_scope = [#(label, #([], u)), ..scope]
+      let #(value, state) = do_infer(value, u, state, value_scope)
+      let polytype = generalise(u, state, scope)
+      let #(then, state) =
+        do_infer(then, expected, state, [#(label, polytype), ..scope])
+      #(#(Ok(expected), e.Let(p.Variable(label), value, then)), state)
+    }
+    e.Variable(label) ->
+      case list.key_find(scope, label) {
+        Ok(polytype) -> {
+          let #(monotype, state) = instantiate(polytype, state)
+          case unify(expected, monotype, state) {
+            Ok(state) -> #(#(Ok(expected), e.Variable(label)), state)
+            Error(reason) -> #(#(Error(reason), e.Variable(label)), state)
+          }
+        }
+        Error(Nil) -> #(
+          #(Error(typer.UnknownVariable(label)), e.Variable(label)),
+          state,
+        )
+      }
+  }
+}
+
+// Set
+fn push_new(item: a, set: List(a)) -> List(a) {
+  case list.find(set, item) {
+    Ok(_) -> set
+    Error(Nil) -> [item, ..set]
+  }
+}
+
+fn difference(items: List(a), excluded: List(a)) -> List(a) {
+  do_difference(items, excluded, [])
+}
+
+fn do_difference(items, excluded, accumulator) {
+  case items {
+    [] -> list.reverse(accumulator)
+    [next, ..items] ->
+      case list.find(excluded, next) {
+        Ok(_) -> do_difference(items, excluded, accumulator)
+        Error(_) -> push_new(next, accumulator)
+      }
+  }
+}
+
+fn union(new: List(a), existing: List(a)) -> List(a) {
+  case new {
+    [] -> existing
+    [next, ..new] -> {
+      let existing = push_new(next, existing)
+      union(new, existing)
+    }
+  }
+}
+
+fn do_index(list, term, count) {
+  case list {
+    [] -> Error(Nil)
+    [item, .._] if item == term -> Ok(count)
+    [_, ..list] -> do_index(list, term, count + 1)
+  }
+}
+
+// set index start from back
+fn index(list, term) {
+  do_index(list.reverse(list), term, 0)
+}
diff --git a/eyg/src/eyg/typer.gleam b/eyg/src/eyg/typer.gleam
index 493802327..4e00af1a2 100644
--- a/eyg/src/eyg/typer.gleam
+++ b/eyg/src/eyg/typer.gleam
@@ -18,7 +18,7 @@ pub type Reason(n) {
   UnknownVariable(label: String)
   UnmatchedTypes(expected: t.Monotype(n), given: t.Monotype(n))
   MissingFields(expected: List(#(String, t.Monotype(n))))
-  UnexpectedFields(expected: List(#(String, t.Monotype(n))))
+  UnexpectedFields(unexpected: List(#(String, t.Monotype(n))))
   UnableToProvide(expected: t.Monotype(n), generator: e.Generator)
 }
 
@@ -168,7 +168,7 @@ pub fn next_unbound(typer) {
 }
 
 // monotype function??
-// This will need the checker/unification/constraints data structure as it uses subsitutions and updates the next var value
+// This will need the checker/unification/constraints data structure as it uses substitutions and updates the next var value
 // next unbound inside mono can be integer and unbound(i) outside
 pub fn unify(expected, given, state) {
   // Pass as tuple to make reduce functions easier to implement
@@ -178,68 +178,67 @@ pub fn unify(expected, given, state) {
   let expected = t.resolve(expected, substitutions)
   let given = t.resolve(given, substitutions)
 
-  case occurs_in(expected, given) || occurs_in(given, expected) {
-    True -> Ok(typer)
-    False ->
-      case expected, given {
-        t.Native(e), t.Native(g) if e == g -> Ok(typer)
-        t.Native(_), t.Native(_) ->
-          // The typer is passed because some constrains should end up in typer i.e. if some values in Tuple are Ok
-          Error(#(UnmatchedTypes(expected, given), typer))
-        t.Binary, t.Binary -> Ok(typer)
-        t.Tuple(expected), t.Tuple(given) ->
-          case list.zip(expected, given) {
-            Error(#(expected, given)) ->
-              Error(#(IncorrectArity(expected, given), typer))
-            Ok(pairs) ->
-              list.try_fold(
-                pairs,
-                typer,
-                fn(pair, typer) {
-                  let #(expected, given) = pair
-                  unify(expected, given, #(typer, scope))
-                },
-              )
-          }
-        t.Unbound(i), any -> Ok(add_substitution(i, any, typer))
-        any, t.Unbound(i) -> Ok(add_substitution(i, any, typer))
-        t.Row(expected, expected_extra), t.Row(given, given_extra) -> {
-          let #(expected, given, shared) = group_shared(expected, given)
-          let #(x, typer) = next_unbound(typer)
-          try typer = case given, expected_extra {
-            [], _ -> Ok(typer)
-            only, Some(i) ->
-              Ok(add_substitution(i, t.Row(only, Some(x)), typer))
-            only, None -> Error(#(UnexpectedFields(only), typer))
-          }
-          try typer = case expected, given_extra {
-            [], _ -> Ok(typer)
-            only, Some(i) ->
-              Ok(add_substitution(i, t.Row(only, Some(x)), typer))
-            only, None -> Error(#(MissingFields(only), typer))
-          }
+  // case occurs_in(expected, given) || occurs_in(given, expected) {
+  //   // True -> todo("handle_occurs")
+  //   _ ->
+  case expected, given {
+    t.Native(e), t.Native(g) if e == g -> Ok(typer)
+    t.Native(_), t.Native(_) ->
+      // The typer is passed because some constrains should end up in typer i.e. if some values in Tuple are Ok
+      Error(#(UnmatchedTypes(expected, given), typer))
+    t.Binary, t.Binary -> Ok(typer)
+    t.Tuple(expected), t.Tuple(given) ->
+      case list.zip(expected, given) {
+        Error(#(expected, given)) ->
+          Error(#(IncorrectArity(expected, given), typer))
+        Ok(pairs) ->
           list.try_fold(
-            shared,
+            pairs,
             typer,
             fn(pair, typer) {
               let #(expected, given) = pair
               unify(expected, given, #(typer, scope))
             },
           )
-        }
-        t.Function(expected_from, expected_return), t.Function(
-          given_from,
-          given_return,
-        ) -> {
-          try x = unify(expected_from, given_from, state)
-          unify(expected_return, given_return, #(x, scope))
-        }
-        expected, given -> Error(#(UnmatchedTypes(expected, given), typer))
       }
+    t.Unbound(i), any -> Ok(add_substitution(i, any, typer))
+    any, t.Unbound(i) -> Ok(add_substitution(i, any, typer))
+    t.Row(expected, expected_extra), t.Row(given, given_extra) -> {
+      let #(expected, given, shared) = group_shared(expected, given)
+      let #(x, typer) = next_unbound(typer)
+      try typer = case given, expected_extra {
+        [], _ -> Ok(typer)
+        only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(x)), typer))
+        only, None -> Error(#(UnexpectedFields(only), typer))
+      }
+      try typer = case expected, given_extra {
+        [], _ -> Ok(typer)
+        only, Some(i) -> Ok(add_substitution(i, t.Row(only, Some(x)), typer))
+        only, None -> Error(#(MissingFields(only), typer))
+      }
+      list.try_fold(
+        shared,
+        typer,
+        fn(pair, typer) {
+          let #(expected, given) = pair
+          unify(expected, given, #(typer, scope))
+        },
+      )
+    }
+    t.Function(expected_from, expected_return), t.Function(
+      given_from,
+      given_return,
+    ) -> {
+      try x = unify(expected_from, given_from, state)
+      unify(expected_return, given_return, #(x, scope))
+    }
+    expected, given -> Error(#(UnmatchedTypes(expected, given), typer))
   }
+  // }
 }
 
-fn group_shared(left, right) {
+// TODO test in list
+pub fn group_shared(left, right) {
   do_group_shared(left, right, [], [])
 }
 
diff --git a/eyg/src/eyg/typer/monotype.gleam b/eyg/src/eyg/typer/monotype.gleam
index cf044696b..f0799cf08 100644
--- a/eyg/src/eyg/typer/monotype.gleam
+++ b/eyg/src/eyg/typer/monotype.gleam
@@ -8,9 +8,12 @@ pub type Monotype(n) {
   Native(n)
   Binary
   Tuple(elements: List(Monotype(n)))
+  // TODO rename Record
   Row(fields: List(#(String, Monotype(n))), extra: Option(Int))
+  Union(variants: List(#(String, Monotype(n))), extra: Option(Int))
   Function(from: Monotype(n), to: Monotype(n))
   Unbound(i: Int)
+  Recursive(i: Int, type_: Monotype(n))
 }
 
 fn row_to_string(row, native_to_string) {
@@ -114,6 +117,7 @@ pub fn literal(monotype) {
 
 fn do_occurs_in(i, b) {
   case b {
+    Recursive(j, inner) -> do_occurs_in(i, inner)
     Unbound(j) if i == j -> True
     Unbound(_) -> False
     Native(_) -> False
@@ -142,15 +146,22 @@ fn occurs_in(a, b) {
 
 pub fn resolve(type_, substitutions) {
   case type_ {
+    Recursive(i, inner) -> Recursive(i, inner)
     Unbound(i) ->
       case list.key_find(substitutions, i) {
         Ok(Unbound(j)) if i == j -> type_
         Error(Nil) -> type_
-        Ok(substitution) -> {
-          let False = occurs_in(Unbound(i), substitution)
-          resolve(substitution, substitutions)
-        }
+        Ok(substitution) ->
+          case occurs_in(Unbound(i), substitution) {
+            False -> resolve(substitution, substitutions)
+            True -> {
+              io.debug("====================")
+              io.debug(substitution)
+              Recursive(i, substitution)
+            }
+          }
       }
+    // let False = 
     Native(name) -> Native(name)
     Binary -> Binary
     Tuple(elements) -> {
diff --git a/eyg/src/eyg/typer/polytype.gleam b/eyg/src/eyg/typer/polytype.gleam
index 857e10fd5..a662c88a8 100644
--- a/eyg/src/eyg/typer/polytype.gleam
+++ b/eyg/src/eyg/typer/polytype.gleam
@@ -51,6 +51,11 @@ pub fn replace_variable(monotype, x, y) {
         True -> t.Unbound(y)
         False -> t.Unbound(i)
       }
+    t.Recursive(i, inner) ->
+      case i == x {
+        True -> t.Recursive(y, inner)
+        False -> t.Recursive(i, inner)
+      }
   }
 }
 
@@ -116,6 +121,7 @@ fn free_variables_in_monotype(monotype) {
     t.Function(from, to) ->
       union(free_variables_in_monotype(from), free_variables_in_monotype(to))
     t.Unbound(i) -> [i]
+    t.Recursive(_, inner) -> free_variables_in_monotype(inner)
   }
 }
 
diff --git a/eyg/src/gleam/list.gleam b/eyg/src/gleam/list.gleam
index 970ee68d1..93f0c9f7c 100644
--- a/eyg/src/gleam/list.gleam
+++ b/eyg/src/gleam/list.gleam
@@ -10,6 +10,34 @@ pub fn find(list: List(a), search: a) -> Result(a, Nil) {
   }
 }
 
+pub fn contains(list: List(a), search: a) -> Bool {
+  case find(list, search) {
+    Ok(_) -> True
+    Error(Nil) -> False
+  }
+}
+
+fn do_unzip(input, xs, ys) {
+  case input {
+    [] -> #(reverse(xs), reverse(ys))
+    [#(x, y), ..rest] -> do_unzip(rest, [x, ..xs], [y, ..ys])
+  }
+}
+
+/// Takes a single list of 2-element tuples and returns two lists.
+///
+/// ## Examples
+///
+///    > unzip([#(1, 2), #(3, 4)])
+///    #([1, 3], [2, 4])
+///
+///    > unzip([])
+///    #([], [])
+///
+pub fn unzip(input: List(#(a, b))) -> #(List(a), List(b)) {
+  do_unzip(input, [], [])
+}
+
 /// Finds the first element in a given list for which the given function returns
 /// True.
 ///
diff --git a/eyg/test/eyg/functions_test.gleam b/eyg/test/eyg/functions_test.gleam
index f9650317d..beed21a6d 100644
--- a/eyg/test/eyg/functions_test.gleam
+++ b/eyg/test/eyg/functions_test.gleam
@@ -9,27 +9,6 @@ import eyg/typer/monotype as t
 import eyg/typer/monotype.{resolve}
 import eyg/typer/polytype
 
-pub fn type_bound_function_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let untyped = ast.function(p.Tuple([]), ast.binary(""))
-  let #(typed, typer) = infer(untyped, t.Unbound(-1), #(typer, scope))
-  let typer.Typer(substitutions: substitutions, ..) = typer
-  let Ok(type_) = get_type(typed)
-  let t.Function(t.Tuple([]), t.Binary) = resolve(type_, substitutions)
-}
-
-pub fn generic_function_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let untyped = ast.function(p.Variable("x"), ast.variable("x"))
-  let #(typed, typer) = infer(untyped, t.Unbound(-1), #(typer, scope))
-  let typer.Typer(substitutions: substitutions, ..) = typer
-  let Ok(type_) = get_type(typed)
-  let t.Function(t.Unbound(a), t.Unbound(b)) = resolve(type_, substitutions)
-  let True = a == b
-}
-
 pub fn call_function_test() {
   let typer = init(fn(_) { todo })
   let scope = typer.root_scope([])
diff --git a/eyg/test/eyg/patterns_test.gleam b/eyg/test/eyg/patterns_test.gleam
index 342acb94e..323c5b169 100644
--- a/eyg/test/eyg/patterns_test.gleam
+++ b/eyg/test/eyg/patterns_test.gleam
@@ -9,107 +9,6 @@ import eyg/typer/monotype as t
 import eyg/typer/polytype
 import platform/browser
 
-// This is proablbly better called assignment tests, unless it grows too big and patterns should be separate
-pub fn variable_of_expected_type_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope =
-    typer.Scope(
-      variables: [#("foo", polytype.Polytype([], t.Tuple([])))],
-      path: [],
-    )
-  let untyped = ast.variable("foo")
-  assert #(typed, _typer) = infer(untyped, t.Tuple([]), #(typer, scope))
-  assert Ok(t.Tuple([])) = get_type(typed)
-}
-
-pub fn variable_of_unexpected_type_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([])))])
-  let state = #(typer, scope)
-  let untyped = ast.variable("foo")
-  assert #(typed, _typer) = infer(untyped, t.Binary, state)
-  assert Error(reason) = get_type(typed)
-  assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
-}
-
-pub fn missing_variable_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.variable("foo")
-  let #(typed, _state) = infer(untyped, t.Binary, state)
-  let Error(reason) = get_type(typed)
-  assert typer.UnknownVariable("foo") = reason
-}
-
-// assignment
-pub fn expected_assignment_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped =
-    ast.let_(pattern.Variable("foo"), ast.tuple_([]), ast.variable("foo"))
-  let #(typed, _typer) = infer(untyped, t.Tuple([]), state)
-  assert Ok(t.Tuple([])) = get_type(typed)
-}
-
-pub fn unexpected_then_type_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped =
-    ast.let_(pattern.Variable("foo"), ast.binary("wrong"), ast.variable("foo"))
-  let #(typed, _typer) = infer(untyped, t.Tuple([]), state)
-  //   Should the error be on the inner
-  assert Ok(t.Tuple([])) = get_type(typed)
-  assert #(_context, expression.Let(_pattern, _value, then)) = typed
-  assert Error(reason) = get_type(then)
-  assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
-}
-
-pub fn matched_expected_tuple_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope =
-    typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([t.Binary])))])
-  let state = #(typer, scope)
-  let untyped =
-    ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a"))
-  let #(typed, typer) = infer(untyped, t.Binary, state)
-  let Ok(t.Binary) = get_type(typed)
-  assert #(_context, expression.Let(_pattern, value, _then)) = typed
-  let typer.Typer(substitutions: substitutions, ..) = typer
-  let Ok(type_) = get_type(value)
-  let t.Tuple([t.Binary]) = t.resolve(type_, substitutions)
-}
-
-pub fn expected_a_tuple_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Binary))])
-  let state = #(typer, scope)
-
-  let untyped =
-    ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a"))
-  let #(typed, _state) = infer(untyped, t.Binary, state)
-  let Ok(t.Binary) = get_type(typed)
-  assert #(_context, expression.Let(_pattern, value, _then)) = typed
-  let Error(reason) = get_type(value)
-  let typer.UnmatchedTypes(t.Tuple([_]), t.Binary) = reason
-}
-
-pub fn unexpected_tuple_size_test() {
-  let typer = typer.init(browser.native_to_string)
-  let scope = typer.root_scope([#("foo", polytype.Polytype([], t.Tuple([])))])
-  let state = #(typer, scope)
-
-  let untyped =
-    ast.let_(pattern.Tuple(["a"]), ast.variable("foo"), ast.variable("a"))
-  let #(typed, _state) = infer(untyped, t.Binary, state)
-  let Ok(t.Binary) = get_type(typed)
-  assert #(_context, expression.Let(_pattern, value, _then)) = typed
-  let Error(reason) = get_type(value)
-  let typer.IncorrectArity(1, 0) = reason
-}
-
 pub fn matched_expected_row_test() {
   let scope =
     typer.root_scope([
diff --git a/eyg/test/eyg/terms_test.gleam b/eyg/test/eyg/terms_test.gleam
index 42f3d9461..5184a57d8 100644
--- a/eyg/test/eyg/terms_test.gleam
+++ b/eyg/test/eyg/terms_test.gleam
@@ -1,113 +1,475 @@
 import gleam/io
-import gleam/option.{None}
+import gleam/list
+import gleam/option.{None, Some}
 import eyg
 import eyg/ast
-import eyg/ast/expression
-import eyg/typer.{get_type, infer, init}
+import eyg/ast/editor
+import eyg/ast/expression.{
+  binary, call, function, hole, let_, row, tagged, tuple_, variable,
+}
+import eyg/typer
+import eyg/ast/expression as e
 import eyg/typer/monotype as t
+import eyg/ast/pattern as p
 import eyg/typer/polytype
+import eyg/inference
 
-pub fn expected_binary_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.binary("Hello")
-  let #(typed, _typer) = infer(untyped, t.Binary, state)
-  assert Ok(t.Binary) = get_type(typed)
-}
-
-pub fn unexpected_binary_error_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.binary("Hello")
-  let #(typed, _typer) = infer(untyped, t.Tuple([]), state)
-  assert Error(reason) = get_type(typed)
-  assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
+// builder pattern for adding variables in test where this would be helpful
+// pub fn infer(untyped, type_) {
+//   let native_to_string = fn(_: Nil) { "" }
+//   let variables = [#("equal", typer.equal_fn())]
+//   let checker = typer.init(native_to_string)
+//   let scope = typer.root_scope(variables)
+//   let state = #(checker, scope)
+//   // TODO replace all variables
+//   //
+//   // sdo
+//   typer.infer(untyped, type_, state)
+// }
+fn infer(untyped, type_) {
+  inference.infer(untyped, type_)
 }
 
-pub fn expected_empty_tuple_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.tuple_([])
-  let #(typed, _typer) = infer(untyped, t.Tuple([]), state)
-  assert Ok(t.Tuple([])) = get_type(typed)
+fn unbound() {
+  t.Unbound(-1)
 }
 
-pub fn expected_non_empty_tuple_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.tuple_([ast.tuple_([])])
-  let #(typed, _typer) = infer(untyped, t.Tuple([t.Tuple([])]), state)
-  assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed)
+fn get_type(typed, checker) {
+  let #(typed, tree) = typed
+  case typed {
+    Ok(type_) -> {
+      let resolved = inference.resolve(type_, checker)
+      Ok(resolved)
+    }
+    Error(typer.UnmatchedTypes(expected, given)) -> {
+      let expected = inference.resolve(expected, checker)
+      let given = inference.resolve(given, checker)
+      Error(typer.UnmatchedTypes(expected, given))
+    }
+    Error(reason) -> Error(reason)
+  }
+}
+
+// TODO move to AST
+fn get_expression(tree, path) {
+  let editor.Expression(expression) = editor.get_element(tree, path)
+  Ok(expression)
+}
+
+pub fn binary_expression_test() {
+  let source = binary("Hello")
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(t.Binary) = get_type(typed, checker)
+
+  let #(typed, checker) = infer(source, t.Binary)
+  assert Ok(t.Binary) = get_type(typed, checker)
+
+  let #(typed, checker) = infer(source, t.Tuple([]))
+  assert Error(reason) = get_type(typed, checker)
+  assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
 }
 
-pub fn unexpected_tuple_size_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.tuple_([ast.binary("not needed")])
-  let #(typed, _typer) = infer(untyped, t.Tuple([]), state)
-  assert Error(reason) = get_type(typed)
+pub fn tuple_expression_test() {
+  let source = tuple_([binary("Hello")])
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([t.Binary]) = type_
+  let #(typed, checker) = infer(source, t.Tuple([unbound()]))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([t.Binary]) = type_
+  let #(typed, checker) = infer(source, t.Tuple([t.Binary]))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([t.Binary]) = type_
+  let #(typed, checker) = infer(source, t.Tuple([]))
+  assert Error(reason) = get_type(typed, checker)
   assert typer.IncorrectArity(0, 1) = reason
+  let #(typed, checker) = infer(source, t.Tuple([t.Tuple([])]))
+  // Type is correct here only internally is there a failure
+  assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed, checker)
+  assert Ok(element) = get_expression(typed, [0])
+  assert Error(reason) = get_type(element, checker)
+  assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
+}
+
+pub fn pair_test() {
+  let source = tuple_([binary("Hello"), tuple_([])])
+  let tx = t.Unbound(-1)
+  let ty = t.Unbound(-2)
+  let #(typed, checker) = infer(source, t.Tuple([tx, ty]))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([t.Binary, t.Tuple([])]) = type_
+  // could check tx/ty bound properly
+  let #(typed, checker) = infer(source, t.Tuple([tx, tx]))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([t.Binary, t.Binary]) = type_
+  assert Ok(element) = get_expression(typed, [1])
+  assert Error(reason) = get_type(element, checker)
+  assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
 }
 
-pub fn unexpected_tuple_element_type_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.tuple_([ast.binary("Yo")])
-  let #(typed, _typer) = infer(untyped, t.Tuple([t.Tuple([])]), state)
-  assert Ok(t.Tuple([t.Tuple([])])) = get_type(typed)
-  assert #(_context, expression.Tuple([child])) = typed
-  assert Error(reason) = get_type(child)
+pub fn row_expression_test() {
+  // TODO order when row is called
+  let source = row([#("foo", binary("Hello"))])
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Row([#("foo", t.Binary)], None) = type_
+  let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], None))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Row([#("foo", t.Binary)], None) = type_
+  // TODO row with some
+  let #(typed, checker) =
+    infer(source, t.Row([#("foo", t.Binary), #("bar", t.Binary)], None))
+  assert Error(reason) = get_type(typed, checker)
+  assert typer.MissingFields([#("bar", t.Binary)]) = reason
+  let #(typed, checker) = infer(source, t.Row([], None))
+  assert Error(reason) = get_type(typed, checker)
+  // assert typer.UnexpectedFields([#("foo", t.Binary)]) = reason
+  // TODO move up
+  let #(typed, checker) = infer(source, t.Row([#("foo", t.Tuple([]))], None))
+  // TODO think which one I want most.
+  // assert Ok(type_) = get_type(typed, checker)
+  // assert t.Row([#("foo", t.Tuple([]))], None) = type_
+  // assert Ok(element) = get_expression(typed, [0, 1])
+  // assert Error(reason) = get_type(element, checker)
+  // assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
+  // ----- up to previous todo
+  // T.Row(head, option(more_row))
+  // Means no such thing as an empty record. Good because tuple is unit
+  let #(typed, checker) = infer(source, t.Row([#("foo", t.Binary)], Some(-1)))
+  assert Ok(type_) = get_type(typed, checker)
+  // TODO should resolve to none
+  // assert t.Row([#("foo", t.Binary)], None) = type_
+}
+
+pub fn tag_test() {
+  let source = tagged("Some", tuple_([]))
+
+  // Unbound
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Union([#("Some", t.Tuple([]))], Some(_)) = type_
+
+  // Part of Option
+  let #(typed, checker) =
+    infer(
+      source,
+      t.Union([#("Some", t.Tuple([])), #("None", t.Tuple([]))], None),
+    )
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Union([#("Some", t.Tuple([])), #("None", t.Tuple([]))], None) = type_
+  io.debug(inference.print(type_, checker))
+
+  // Mismatched type
+  let #(typed, checker) =
+    infer(source, t.Union([#("Some", t.Binary), #("None", t.Tuple([]))], None))
+  assert Ok(type_) = get_type(typed, checker)
+  // TODO expected option of A or A
+  assert Ok(element) = get_expression(typed, [1])
+  assert Error(reason) = get_type(element, checker)
+  assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
+  // assert t.Union([#("Some", t.Tuple([]))], Some(_)) = type_
+  // wrong variant
+  // union Foo
+  let #(typed, checker) = infer(source, t.Union([#("Foo", t.Tuple([]))], None))
+  assert Error(reason) = get_type(typed, checker)
+  assert typer.UnexpectedFields(a) = reason
+  io.debug(a)
+  // io.debug(b)
+}
+
+// // TODO tag test
+// // TODO patterns
+pub fn var_expression_test() {
+  let source = variable("x")
+  let #(typed, checker) = infer(source, unbound())
+  assert Error(reason) = get_type(typed, checker)
+  // TODO check we're on the lowest unbound integer
+  assert typer.UnknownVariable("x") = reason
+}
+
+pub fn function_test() {
+  let source = function(p.Variable(""), binary(""))
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Unbound(_), t.Binary) = type_
+  let #(typed, checker) = infer(source, t.Function(unbound(), t.Unbound(-2)))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Unbound(_), t.Binary) = type_
+  let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Tuple([]), t.Binary) = type_
+  let #(typed, checker) = infer(source, t.Function(unbound(), unbound()))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Binary, t.Binary) = type_
+  let #(typed, checker) = infer(source, t.Binary)
+  assert Error(reason) = get_type(typed, checker)
+  // assert typer.UnmatchedTypes(t.Binary, t.Function(t.Unbound(_), t.Tuple([]))) =
+  //   reason
+  // TODO move up
+  let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Tuple([])))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Tuple([]), t.Tuple([])) = type_
+  assert Ok(body) = get_expression(typed, [1])
+  assert Error(reason) = get_type(body, checker)
   assert typer.UnmatchedTypes(t.Tuple([]), t.Binary) = reason
 }
 
-pub fn expected_row_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.row([#("foo", ast.tuple_([]))])
-  let #(typed, _typer) =
-    infer(untyped, t.Row([#("foo", t.Tuple([]))], None), state)
-  assert Ok(t.Row([#("foo", t.Tuple([]))], None)) = get_type(typed)
-}
-
-pub fn unexpected_fields_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.row([#("foo", ast.tuple_([]))])
-  let #(typed, _typer) = infer(untyped, t.Row([], None), state)
-  assert Error(reason) = get_type(typed)
-  assert typer.UnexpectedFields([#("foo", x)]) = reason
-  // x is unbound but we probably have better info
-}
-
-pub fn missing_fields_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.row([])
-  let #(typed, _typer) =
-    infer(untyped, t.Row([#("foo", t.Tuple([]))], None), state)
-  assert Error(reason) = get_type(typed)
-  assert typer.MissingFields([#("foo", x)]) = reason
-  // I think we might only need the name not type, BUT why throw away info
-}
-
-pub fn unexpected_field_type_test() {
-  let typer = init(fn(_) { todo })
-  let scope = typer.root_scope([])
-  let state = #(typer, scope)
-  let untyped = ast.row([#("foo", ast.tuple_([]))])
-  let #(typed, _typer) =
-    infer(untyped, t.Row([#("foo", t.Binary)], None), state)
-  assert Ok(t.Row([#("foo", t.Binary)], None)) = get_type(typed)
-  assert #(_context, expression.Row([#("foo", child)])) = typed
-  assert Error(reason) = get_type(child)
+pub fn id_function_test() {
+  let source = function(p.Variable("x"), variable("x"))
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Unbound(i), t.Unbound(j)) = type_
+  assert True = i == j
+  let #(typed, checker) = infer(source, t.Function(unbound(), t.Binary))
+  assert Ok(type_) = get_type(typed, checker)
+  // TODO check unbound is now binary
+  assert t.Function(t.Binary, t.Binary) = type_
+  let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Binary))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Function(t.Tuple([]), t.Binary) = type_
+  assert Ok(body) = get_expression(typed, [1])
+  assert Error(reason) = get_type(body, checker)
+  assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
+  // Not this is saying that the variable is wrong some how
+}
+
+// // equal bin bin
+// // equal bin tuple still returns true
+// TODO patterns in arguments
+// pub fn call_function_test() {
+//   let func = function(p.Tuple([]), binary(""))
+//   let source = call(func, tuple_([]))
+//   let #(typed, checker) = infer(source, unbound())
+//   assert Ok(type_) = get_type(typed, checker)
+//   assert t.Binary = type_
+//   let #(typed, checker) = infer(source, t.Binary)
+//   assert Ok(type_) = get_type(typed, checker)
+//   assert t.Binary = type_
+//   // Error is internal
+//   // let #(typed, checker) = infer(source, t.Tuple([]))
+//   // assert Error(reason) = get_type(typed, checker)
+//   // assert typer.UnmatchedTypes(t.Tuple([]), t.Tuple([])) = reason
+// }
+pub fn call_generic_function_test() {
+  let func = function(p.Variable("x"), variable("x"))
+  let source = call(func, tuple_([]))
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([]) = type_
+  let #(typed, checker) = infer(source, t.Tuple([]))
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Tuple([]) = type_
+  // error in generic pushed to arguments
+  let #(typed, checker) = infer(source, t.Binary)
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Binary = type_
+  assert Ok(body) = get_expression(typed, [1])
+  assert Error(reason) = get_type(body, checker)
   assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
 }
+
+pub fn call_not_a_function_test() {
+  let source = call(binary("no a func"), tuple_([]))
+  let #(typed, checker) = infer(source, t.Binary)
+  assert Ok(type_) = get_type(typed, checker)
+  assert t.Binary = type_
+  assert Ok(body) = get_expression(typed, [0])
+  assert Error(reason) = get_type(body, checker)
+  assert typer.UnmatchedTypes(expected, t.Binary) = reason
+  // TODO resolve expected
+  // assert t.Function(t.Tuple([]), t.Binary) = expected
+}
+
+// pub fn hole_expression_test() {
+//   let source = hole()
+//   let #(typed, checker) = infer(source, unbound())
+//   assert Ok(type_) = get_type(typed, checker)
+//   // TODO check we're on the lowest unbound integer
+//   assert t.Unbound(_) = type_
+//   let #(typed, checker) = infer(source, t.Binary)
+//   assert Ok(type_) = get_type(typed, checker)
+//   assert t.Binary = type_
+// }
+// // patterns
+// pub fn tuple_pattern_test() {
+//   let source = function(p.Tuple(["x"]), variable("x"))
+//   let #(typed, checker) = infer(source, unbound())
+//   assert Ok(t.Function(from, _)) = get_type(typed, checker)
+//   assert t.Tuple([t.Unbound(_)]) = from
+//   let #(typed, checker) =
+//     infer(source, t.Function(t.Tuple([unbound()]), t.Unbound(-2)))
+//   assert Ok(t.Function(from, _)) = get_type(typed, checker)
+//   assert t.Tuple([t.Unbound(_)]) = from
+//   let #(typed, checker) =
+//     infer(source, t.Function(t.Tuple([t.Binary]), t.Unbound(-2)))
+//   assert Ok(t.Function(from, _)) = get_type(typed, checker)
+//   assert t.Tuple([t.Binary]) = from
+//   // wrong arity
+//   let #(typed, checker) = infer(source, t.Function(t.Tuple([]), t.Unbound(-2)))
+//   assert Error(reason) = get_type(typed, checker)
+//   // TODO need to return the function error
+//   assert typer.IncorrectArity(0, 1) = reason
+//   // wrong bound type
+//   let #(typed, checker) =
+//     infer(source, t.Function(t.Tuple([t.Binary]), t.Tuple([])))
+//   // Should this be an inside error or not
+//   // assert Error(reason) = get_type(typed, checker)
+//   // // TODO need to return the function error
+//   // assert typer.UnmatchedTypes(t.Binary, t.Tuple([])) = reason
+// }
+// // let
+// pub fn row_pattern_test() {
+//   let source = function(p.Row([#("foo", "x")]), variable("x"))
+//   // todo
+// }
+// // TODO expanding row type test
+// // test reusing id
+// // pub fn recursive_tuple_test() {
+// //   let source =
+// //     let_(
+// //       p.Variable("f"),
+// //       function(
+// //         p.Tuple([]),
+// //         tuple_([binary("x"), call(variable("f"), tuple_([]))]),
+// //       ),
+// //       variable("f"),
+// //     )
+// //   let #(typed, checker) = infer(source, unbound())
+// //   assert Ok(t.Function(from, to)) = get_type(typed, checker)
+// //   assert t.Tuple([]) = from
+// //   // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to
+// //   // typer.get_type(typed)
+// //   // |> io.debug
+// //   list.map(checker.substitutions, io.debug)
+// //   // io.debug(mu)
+// //   // io.debug("----")
+// //   let [x, .._] = checker.substitutions
+// //   let #(-1, t.Function(_, t.Tuple(elements))) = x
+// //   io.debug(elements)
+// //   let [_, t.Recursive(mu, inner)] = elements
+// //   io.debug("loow ")
+// //   io.debug(mu)
+// //   io.debug(inner)
+// //   let t.Tuple([_, t.Unbound(x)]) = inner
+// //   io.debug(x)
+// // }
+// fn my_infer(untyped, goal) {
+//   do_my_infer(untyped, goal, [])
+// }
+// // Do this as alg J
+// fn do_my_infer(untyped, goal, env) {
+//   let #(_, untyped) = untyped
+//   io.debug(untyped)
+//   case untyped {
+//     e.Let(p.Variable(f), #(_, e.Function(p.Variable(x), body)), then) -> {
+//       let p = t.Unbound(1)
+//       let r = t.Unbound(2)
+//       let env = [#(f, t.Function(p, r)), #(x, p), ..env]
+//       do_my_infer(body, r, env)
+//     }
+//     e.Tuple([e1, e2]) -> {
+//       // unify goal tuple(tnext 1)
+//       let t1 = t.Unbound(3)
+//       let t2 = t.Unbound(4)
+//       io.debug("goal")
+//       io.debug(goal)
+//       do_my_infer(e1, t1, env)
+//       do_my_infer(e2, t2, env)
+//     }
+//     e.Binary(_) -> {
+//       io.debug("is binary")
+//       io.debug(goal)
+//       #(1, 1)
+//     }
+//     e.Call(e1, e2) -> {
+//       io.debug(goal)
+//       io.debug(e1)
+//       io.debug(e2)
+//       // 0 = 1 -> 2
+//       // 1 = Tuple([]) Null
+//       // 2 = Tuple(3, 4)
+//       // 3 = Binary
+//       // 4 = 1 -> 2.1
+//       // 2 = Tuple(Binary, 2)
+//       // rA(Binary, A)
+//       // rA[Nil | Cons (B, A)]
+//       // reverse: rA[Nil | Cons (B, A)] -> rA[Nil | Cons (B, A)]
+//       // map: rA[Nil | Cons (B, A)] -> (B, C) -> rD[Nil | Cons (C, D)]
+//       // map: List(B) -> (B -> C) -> List(C)
+//       todo("in call")
+//     }
+//     e.Variable(label) -> {
+//       let t = list.key_find(env, label)
+//       io.debug(t)
+//       todo
+//     }
+//   }
+//   // #(1, 1)
+// }
+pub fn recursive_loop_test() {
+  let source =
+    let_(
+      p.Variable("f"),
+      function(
+        p.Variable("x"),
+        let_(p.Variable("tmp"), binary(""), call(variable("f"), variable("x"))),
+      ),
+      variable("f"),
+    )
+  let #(typed, checker) = infer(source, unbound())
+  assert Ok(t.Function(t.Unbound(i), t.Unbound(j))) = get_type(typed, checker)
+  assert True = i != j
+  // TODO x = i and f = i -> j internally but not poly
+  // assert Ok(body) = get_expression(typed, [1])
+  // assert Ok(t.Function(t.Unbound(i), t.Unbound(j))) = get_type(body, checker)
+  // TODO ----
+  // id called polymorphically internally FAil
+  // id called polymorphically externally Success
+}
+
+// TODO let x = x Test
+pub fn my_recursive_tuple_test() {
+  let source =
+    let_(
+      p.Variable("f"),
+      function(
+        p.Variable("x"),
+        tuple_([binary("hello"), call(variable("f"), tuple_([]))]),
+      ),
+      variable("f"),
+    )
+  let #(typed, checker) = infer(source, unbound())
+
+  // io.debug("-=-------------------")
+  // io.debug(typed)
+  // list.map(
+  //   checker.substitutions,
+  //   fn(s) {
+  //     let #(k, t) = s
+  //     io.debug(k)
+  //     // io.debug(t.to_string(t, fn(_) { "OOO" }))
+  //     io.debug(inference.to_string(t, []))
+  //   },
+  // )
+  let Ok(type_) = get_type(typed, checker)
+  let "() -> μ0.(Binary, 0)" = inference.print(type_, checker)
+  // inference.print(t.Unbound(4), checker)
+  // |> io.debug
+  // assert Ok(t.Function(from, to)) = get_type(typed, checker)
+  // assert t.Tuple([]) = from
+  // // assert t.Tuple([t.Binary, t.Unbound(mu)]) = to
+  // // typer.get_type(typed)
+  // // |> io.debug
+  // list.map(checker.substitutions, io.debug)
+  // // io.debug(mu)
+  // // io.debug("----")
+  // let [x, .._] = checker.substitutions
+  // let #(-1, t.Function(_, t.Tuple(elements))) = x
+  // io.debug(elements)
+  // let [_, t.Recursive(mu, inner)] = elements
+  // io.debug("loow ")
+  // io.debug(mu)
+  // io.debug(inner)
+  // let t.Tuple([_, t.Unbound(x)]) = inner
+  // io.debug(x)
+}