diff --git a/patch/gleam/bit_array.patch.gleam b/patch/gleam/bit_array.patch.gleam
index 8ac8737..f8d2b31 100644
--- a/patch/gleam/bit_array.patch.gleam
+++ b/patch/gleam/bit_array.patch.gleam
@@ -7,7 +7,7 @@ fn unsafe_to_string(a: BitArray) -> String {
 }
 
 @external(c, "", "gleam_bit_array_from_string")
-fn from_string(x: String) -> BitArray
+pub fn from_string(x: String) -> BitArray
 
 fn is_utf8_loop(bits: BitArray) -> Bool {
   case bits {
diff --git a/patch/gleam/io.patch.gleam b/patch/gleam/io.patch.gleam
index 8c2d702..511dda4 100644
--- a/patch/gleam/io.patch.gleam
+++ b/patch/gleam/io.patch.gleam
@@ -27,7 +27,7 @@ pub fn println(string: String) -> Nil {
     do_print("\n")
 }
 
-fn println_error(string: String) -> Nil {
+pub fn println_error(string: String) -> Nil {
   do_print_error(string)
   do_print_error("\n")
 }
diff --git a/patch/gleam/string.patch.gleam b/patch/gleam/string.patch.gleam
index 3a34be1..3bdfae1 100644
--- a/patch/gleam/string.patch.gleam
+++ b/patch/gleam/string.patch.gleam
@@ -74,7 +74,7 @@ fn append_pairs(strings: List(String)) {
 fn unsafe_int_to_utf_codepoint(a: Int) -> UtfCodepoint
 
 @external(c, "", "gleam_string_from_utf_codepoints")
-fn from_utf_codepoints(utf_codepoints: List(UtfCodepoint)) -> String
+pub fn from_utf_codepoints(utf_codepoints: List(UtfCodepoint)) -> String
 
 @external(c, "", "gleam_string_do_to_utf_codepoints")
 fn do_to_utf_codepoints(string: String) -> List(UtfCodepoint)
diff --git a/src/gig/compiler.gleam b/src/gig/compiler.gleam
index 8a7d195..e287970 100644
--- a/src/gig/compiler.gleam
+++ b/src/gig/compiler.gleam
@@ -107,14 +107,17 @@ pub fn compile(gleam_file_name: String, options: CompileOptions) {
   // process the prelude
   let assert Ok(source_text) = read_source(sources, "gleam")
   let assert Ok(prelude) = glance.module(source_text)
-  let typed = typed_ast.new_context()
-  let assert Ok(typed) =
-    typed_ast.infer_module(typed, prelude, "gleam", source_text)
+  let assert Ok(typed) = typed_ast.infer_module(dict.new(), prelude, "gleam")
 
   // parse and typecheck input (recursively)
-  let #(typed, _done) = infer_file(sources, typed, ["gleam"], module_id)
+  let typed =
+    infer_file(
+      sources,
+      dict.from_list([#("gleam", #(typed, typed_ast.interface(typed)))]),
+      module_id,
+    )
 
-  let core = core.lower_context(typed)
+  let core = core.lower_modules(dict.map_values(typed, fn(_, p) { p.0 }))
 
   case options.headers {
     True -> generate_headers_only(core, sources)
@@ -123,7 +126,7 @@ pub fn compile(gleam_file_name: String, options: CompileOptions) {
 }
 
 fn generate_headers_only(
-  core: core.Context,
+  core: core.Module,
   sources: dict.Dict(String, String),
 ) -> String {
   headers.module_headers(core)
@@ -150,7 +153,7 @@ fn generate_headers_only(
 }
 
 fn compile_to_binary(
-  core: core.Context,
+  core: core.Module,
   sources: dict.Dict(String, String),
   module_id: String,
   target_path: String,
@@ -277,12 +280,9 @@ fn offset_to_line_col(text: String, offset: Int) {
 
 fn infer_file(
   sources: dict.Dict(String, String),
-  c: typed_ast.Context,
-  done: List(String),
+  modules: dict.Dict(String, #(typed_ast.Module, typed_ast.ModuleInterface)),
   module_id: String,
-) -> #(typed_ast.Context, List(String)) {
-  // add module to "done" list
-  let done = [module_id, ..done]
+) -> dict.Dict(String, #(typed_ast.Module, typed_ast.ModuleInterface)) {
   let assert Ok(source) = dict.get(sources, module_id)
 
   io.println("Parse " <> source)
@@ -300,20 +300,26 @@ fn infer_file(
   }
 
   // infer imports
-  let #(c, done) =
-    list.fold(module.imports, #(c, done), fn(acc, i) {
-      let #(c, done) = acc
+  let modules =
+    list.fold(module.imports, modules, fn(modules, i) {
       let module_id = i.definition.module
-      case list.contains(done, module_id) {
-        True -> #(c, done)
-        False -> infer_file(sources, c, done, module_id)
+      case dict.has_key(modules, module_id) {
+        True -> modules
+        False -> infer_file(sources, modules, module_id)
       }
     })
 
   // infer this file
   io.println("Check " <> source)
-  case typed_ast.infer_module(c, module, module_id, source_text) {
-    Ok(c) -> #(c, done)
+  case
+    typed_ast.infer_module(
+      dict.map_values(modules, fn(_, p) { p.1 }),
+      module,
+      module_id,
+    )
+  {
+    Ok(module) ->
+      dict.insert(modules, module_id, #(module, typed_ast.interface(module)))
     Error(err) ->
       panic as error(source_text, err.location, typed_ast.inspect_error(err))
   }
diff --git a/src/gig/core.gleam b/src/gig/core.gleam
index 285d746..e8ce7c8 100644
--- a/src/gig/core.gleam
+++ b/src/gig/core.gleam
@@ -14,14 +14,17 @@ import gleam/option.{None, Some}
 
 pub const builtin = t.builtin
 
+pub type TypeVarId =
+  t.TypeVarId
+
 pub type Type {
   NamedType(id: String, parameters: List(Type))
   FunctionType(parameters: List(Type), return: Type)
-  Unbound(id: Int)
+  Unbound(id: TypeVarId)
 }
 
 pub type Poly {
-  Poly(vars: List(Int), typ: Type)
+  Poly(vars: List(TypeVarId), typ: Type)
 }
 
 pub type Parameter {
@@ -85,23 +88,32 @@ pub type External {
   )
 }
 
-pub type Context {
-  Context(
+pub type Module {
+  Module(
     types: List(CustomType),
     functions: List(Function),
     externals: List(External),
   )
 }
 
-pub fn lower_context(c: t.Context) {
-  let acc = Context(types: [], functions: [], externals: [])
-  dict.values(c.modules)
+type Context {
+  Context(
+    module: String,
+    definition: String,
+    // TODO: should only need module interfaces.
+    modules: dict.Dict(String, t.Module),
+  )
+}
+
+pub fn lower_modules(modules: dict.Dict(String, t.Module)) {
+  let acc = Module(types: [], functions: [], externals: [])
+  dict.values(modules)
   |> list.sort(fn(a, b) { string.compare(a.name, b.name) })
-  |> list.fold(acc, fn(acc, module) { lower_module(c, acc, module) })
+  |> list.fold(acc, fn(acc, module) { lower_module(acc, modules, module) })
 }
 
-fn lower_module(c: t.Context, acc: Context, module: t.Module) {
-  let c = t.Context(..c, current_module: module.name)
+fn lower_module(acc: Module, modules, module: t.Module) {
+  let c = Context(module: module.name, definition: "", modules:)
 
   // TODO detect what tuples are actually used
   let acc =
@@ -115,7 +127,7 @@ fn lower_module(c: t.Context, acc: Context, module: t.Module) {
         [] -> acc
         _ -> {
           let custom = lower_custom_type(c, custom.definition)
-          Context(..acc, types: [custom, ..acc.types])
+          Module(..acc, types: [custom, ..acc.types])
         }
       }
     })
@@ -134,7 +146,7 @@ fn lower_module(c: t.Context, acc: Context, module: t.Module) {
       let external =
         list.find(attrs, fn(x) {
           case x {
-            t.Attribute("external", [t.LocalVariable(_, "c"), ..]) -> True
+            t.Attribute("external", [t.NameAttributeArgument("c"), ..]) -> True
             _ -> False
           }
         })
@@ -144,18 +156,18 @@ fn lower_module(c: t.Context, acc: Context, module: t.Module) {
           let assert t.Attribute(
             _,
             [
-              t.LocalVariable(_, "c"),
-              t.String(_, _src),
-              t.String(_, external_name),
+              t.NameAttributeArgument("c"),
+              t.StringAttributeArgument(_src),
+              t.StringAttributeArgument(external_name),
             ],
           ) = external
           let fun = fun.definition
-          let typ = map_poly(c, fun.typ)
-          let module = c.current_module
+          let typ = map_poly(fun.typ)
+          let module = c.module
           let name = fun.name
           let internal_name = get_id(module, name)
           let builtin = list.any(attrs, fn(x) { x.name == "builtin" })
-          let parameters = list.map(fun.parameters, lower_parameter(c, _))
+          let parameters = list.map(fun.parameters, lower_parameter)
           let fun =
             External(
               typ:,
@@ -165,32 +177,32 @@ fn lower_module(c: t.Context, acc: Context, module: t.Module) {
               module:,
               builtin:,
             )
-          Context(..acc, externals: [fun, ..acc.externals])
+          Module(..acc, externals: [fun, ..acc.externals])
         }
         Error(_) -> {
           let fun = lower_function(c, fun)
-          Context(..acc, functions: [fun, ..acc.functions])
+          Module(..acc, functions: [fun, ..acc.functions])
         }
       }
     })
   acc
 }
 
-fn lower_custom_type(c: t.Context, custom: t.CustomType) {
-  let typ = map_poly(c, custom.typ)
-  let module = c.current_module
+fn lower_custom_type(c: Context, custom: t.CustomType) {
+  let typ = map_poly(custom.typ)
+  let module = c.module
   let name = custom.name
   let id = get_id(module, name)
   let variants =
     list.map(custom.variants, fn(variant) {
-      let typ = map_poly(c, variant.typ)
+      let typ = map_poly(variant.typ)
       let fields =
         list.index_map(variant.fields, fn(field, i) {
           let name = case field.label {
             Some(label) -> label
             None -> gen_names.get_field_name("", i)
           }
-          Parameter(map_type(c, field.item.typ), name)
+          Parameter(map_type(field.item.typ), name)
         })
       let id = get_id(module, variant.name)
       Variant(typ, id, variant.name, fields)
@@ -198,14 +210,14 @@ fn lower_custom_type(c: t.Context, custom: t.CustomType) {
   CustomType(typ, id, name, variants)
 }
 
-fn lower_function(c: t.Context, def: t.Definition(t.FunctionDefinition)) {
-  let c = t.Context(..c, current_definition: def.definition.name)
+fn lower_function(c: Context, def: t.Definition(t.FunctionDefinition)) {
+  let c = Context(..c, definition: def.definition.name)
   let function = def.definition
-  let typ = map_poly(c, function.typ)
-  let module = c.current_module
+  let typ = map_poly(function.typ)
+  let module = c.module
   let name = function.name
   let id = get_id(module, name)
-  let parameters = list.map(function.parameters, lower_parameter(c, _))
+  let parameters = list.map(function.parameters, lower_parameter)
   let body = lower_body(c, function.body)
   let taken = list.map(parameters, fn(param) { param.name })
   let #(_, _, body) = unshadow(taken, 1, body)
@@ -213,8 +225,8 @@ fn lower_function(c: t.Context, def: t.Definition(t.FunctionDefinition)) {
   Function(typ:, id:, parameters:, body:)
 }
 
-fn lower_parameter(c: t.Context, parameter: t.FunctionParameter) {
-  let typ = map_type(c, parameter.typ)
+fn lower_parameter(parameter: t.FunctionParameter) {
+  let typ = map_type(parameter.typ)
   let name = case parameter.name {
     t.Named(name) -> name
     t.Discarded(name) -> "_" <> name
@@ -223,7 +235,7 @@ fn lower_parameter(c: t.Context, parameter: t.FunctionParameter) {
 }
 
 pub fn register_variant_functions(
-  c: Context,
+  c: Module,
   module_name: String,
   variant: Variant,
 ) {
@@ -239,10 +251,10 @@ pub fn register_variant_functions(
       module: module_name,
       builtin: True,
     )
-  Context(..c, externals: [fun, ..c.externals])
+  Module(..c, externals: [fun, ..c.externals])
 }
 
-fn lower_body(c: t.Context, body: List(t.Statement)) {
+fn lower_body(c: Context, body: List(t.Statement)) {
   case body {
     [] -> lower_expression(c, t.Todo(t.nil_type, None))
     [statement] ->
@@ -287,7 +299,7 @@ fn lower_body(c: t.Context, body: List(t.Statement)) {
           let value = lower_expression(c, value)
           let body = lower_body(c, body)
 
-          let bindings = lower_pattern_bindings(c, pattern, subject)
+          let bindings = lower_pattern_bindings(pattern, subject)
           let body =
             list.fold(bindings, body, fn(body, binding) {
               let #(name, subject) = binding
@@ -315,7 +327,7 @@ fn lower_body(c: t.Context, body: List(t.Statement)) {
 }
 
 fn check_assertions(
-  c: t.Context,
+  c: Context,
   pattern: t.Pattern,
   subject: t.Expression,
   value: Exp,
@@ -384,9 +396,9 @@ fn parse_bitstring_segment_expression(
       }
     })
     |> result.unwrap(case value {
-      t.Int(typ, value) -> IntMode
-      t.Float(typ, value) -> FloatMode
-      t.String(typ, value) -> Utf8Mode
+      t.Int(..) -> IntMode
+      t.Float(..) -> FloatMode
+      t.String(..) -> Utf8Mode
       _ -> IntMode
     })
 
@@ -468,9 +480,9 @@ fn parse_bitstring_segment_pattern(
       }
     })
     |> result.unwrap(case value {
-      t.PatternInt(typ, value) -> IntMode
-      t.PatternFloat(typ, value) -> FloatMode
-      t.PatternString(typ, value) -> Utf8Mode
+      t.PatternInt(..) -> IntMode
+      t.PatternFloat(..) -> FloatMode
+      t.PatternString(..) -> Utf8Mode
       _ -> IntMode
     })
 
@@ -845,7 +857,6 @@ fn index_bit_array(
 }
 
 fn lower_pattern_bindings(
-  c: t.Context,
   pattern: t.Pattern,
   subject: t.Expression,
 ) -> List(#(String, t.Expression)) {
@@ -854,11 +865,11 @@ fn lower_pattern_bindings(
     t.PatternFloat(..) -> []
     t.PatternString(..) -> []
     t.PatternDiscard(..) -> []
-    t.PatternVariable(typ, name) -> [#(name, subject)]
-    t.PatternTuple(typ, elems) -> {
+    t.PatternVariable(name:, ..) -> [#(name, subject)]
+    t.PatternTuple(elems:, ..) -> {
       list.index_map(elems, fn(elem, i) {
         let subject = t.TupleIndex(elem.typ, subject, i)
-        lower_pattern_bindings(c, elem, subject)
+        lower_pattern_bindings(elem, subject)
       })
       |> list.flatten
     }
@@ -875,13 +886,13 @@ fn lower_pattern_bindings(
           let a = [t.Field(Some("item"), x), t.Field(Some("next"), rest)]
           t.PatternConstructor(typ, t.builtin, "Cons", a, a, True, False)
         })
-      lower_pattern_bindings(c, list, subject)
+      lower_pattern_bindings(list, subject)
     }
-    t.PatternAssignment(typ, pattern, name) -> {
-      let pattern = lower_pattern_bindings(c, pattern, subject)
+    t.PatternAssignment(pattern:, name:, ..) -> {
+      let pattern = lower_pattern_bindings(pattern, subject)
       [#(name, subject), ..pattern]
     }
-    t.PatternConcatenate(typ, prefix, prefix_name, suffix_name) -> {
+    t.PatternConcatenate(prefix:, prefix_name:, suffix_name:, ..) -> {
       let prefix_binding = case prefix_name {
         Some(t.Named(name)) -> [#(name, t.String(t.string_type, prefix))]
         _ -> []
@@ -910,10 +921,10 @@ fn lower_pattern_bindings(
 
       list.append(prefix_binding, suffix_binding)
     }
-    t.PatternBitString(typ, segs) -> {
+    t.PatternBitString(segments:, ..) -> {
       // TODO total size not used? can we remove the calculation?
       let #(total_size, segs) =
-        list.fold(segs, #(t.Int(t.int_type, "0"), []), fn(acc, seg) {
+        list.fold(segments, #(t.Int(t.int_type, "0"), []), fn(acc, seg) {
           let #(offset, bindings) = acc
           let #(pattern, options) = seg
 
@@ -921,21 +932,13 @@ fn lower_pattern_bindings(
             index_bit_array(options, subject, offset, pattern)
 
           let offset = t.BinaryOperator(t.int_type, g.AddInt, offset, size)
-          let new_binding = lower_pattern_bindings(c, pattern, inner_subject)
+          let new_binding = lower_pattern_bindings(pattern, inner_subject)
           #(offset, list.append(bindings, new_binding))
         })
       segs
       |> list.reverse()
     }
-    t.PatternConstructor(
-      typ,
-      module,
-      constructor,
-      arguments,
-      ordered_arguments,
-      _,
-      _,
-    ) -> {
+    t.PatternConstructor(module:, constructor:, ordered_arguments:, ..) -> {
       let elems = ordered_arguments
       list.index_map(elems, fn(elem, index) {
         let label = option.unwrap(elem.label, "")
@@ -948,7 +951,7 @@ fn lower_pattern_bindings(
             label,
             index,
           )
-        lower_pattern_bindings(c, elem.item, subject)
+        lower_pattern_bindings(elem.item, subject)
       })
       |> list.flatten
     }
@@ -1011,7 +1014,7 @@ fn add_exp(first: Exp, second: Exp) {
 }
 
 fn lower_pattern_match(
-  c: t.Context,
+  c: Context,
   pattern: t.Pattern,
   subject: t.Expression,
 ) -> Exp {
@@ -1165,8 +1168,8 @@ fn lower_pattern_match(
           let assert NamedType(custom, _) = subject.typ
           let assert Ok(mod) = dict.get(c.modules, module)
           let assert Ok(t.Definition(_, custom)) =
-            list.find(mod.custom_types, fn(c) {
-              get_id(module, c.definition.name) == custom
+            list.find(mod.custom_types, fn(custom_type) {
+              get_id(module, custom_type.definition.name) == custom
             })
           let variant = get_id(module, constructor)
 
@@ -1182,14 +1185,14 @@ fn lower_pattern_match(
   }
 }
 
-fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
+fn lower_expression(c: Context, exp: t.Expression) -> Exp {
   case exp {
-    t.Int(typ, value) -> Literal(map_type(c, typ), Int(value))
-    t.Float(typ, value) -> Literal(map_type(c, typ), Float(value))
-    t.String(typ, value) -> Literal(map_type(c, typ), String(value))
-    t.LocalVariable(typ, name) -> Local(map_type(c, typ), name)
+    t.Int(typ, value) -> Literal(map_type(typ), Int(value))
+    t.Float(typ, value) -> Literal(map_type(typ), Float(value))
+    t.String(typ, value) -> Literal(map_type(typ), String(value))
+    t.LocalVariable(typ, name) -> Local(map_type(typ), name)
     t.Function(typ, module, name, _labels) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
 
       case module, name {
         // convert these to literals
@@ -1201,47 +1204,54 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
         }
       }
     }
-    t.Constant(value:, ..) -> {
+    t.Constant(module:, name:, ..) -> {
+      // TODO: in order for lowering to not require implementation details of
+      // other modules, inlining must happen later
+      let assert Ok(mod) = dict.get(c.modules, module)
+      let assert Ok(constant) =
+        list.find(mod.constants, fn(constant) {
+          constant.definition.name == name
+        })
       // inline the constant
-      lower_expression(c, value)
+      lower_expression(c, constant.definition.value)
     }
     t.NegateInt(typ, value) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let value = lower_expression(c, value)
       let fun = Global(FunctionType([typ], typ), "negate_int")
       Call(typ, fun, [value])
     }
     t.NegateBool(typ, value) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let value = lower_expression(c, value)
       let fun = Global(FunctionType([typ], typ), "negate_bool")
       Call(typ, fun, [value])
     }
     t.Block(_typ, statements) -> lower_body(c, statements)
     t.Panic(typ, value) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let value = case value {
         Some(value) -> lower_expression(c, value)
         None -> {
           let message = "panic: " <> current_location(c)
-          Literal(map_type(c, t.string_type), String(message))
+          Literal(map_type(t.string_type), String(message))
         }
       }
       Panic(typ, value)
     }
     t.Todo(typ, value) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let value = case value {
         Some(value) -> lower_expression(c, value)
         None -> {
           let message = "todo: " <> current_location(c)
-          Literal(map_type(c, t.string_type), String(message))
+          Literal(map_type(t.string_type), String(message))
         }
       }
       Panic(typ, value)
     }
     t.Tuple(typ, elements) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let elements = list.map(elements, lower_expression(c, _))
       let element_types = list.map(elements, fn(e) { e.typ })
       let len = int.to_string(list.length(elements))
@@ -1249,7 +1259,7 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       Call(typ, fun, elements)
     }
     t.List(typ, elements, rest) -> {
-      let list_typ = map_type(c, typ)
+      let list_typ = map_type(typ)
       let rest = case rest {
         Some(rest) -> lower_expression(c, rest)
         None -> Global(list_typ, "Empty")
@@ -1264,8 +1274,8 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       })
     }
     t.Fn(typ, parameters, _return, body) -> {
-      let typ = map_type(c, typ)
-      let parameters = list.map(parameters, lower_parameter(c, _))
+      let typ = map_type(typ)
+      let parameters = list.map(parameters, lower_parameter)
       let body = lower_body(c, body)
       Fn(typ, parameters, body)
     }
@@ -1289,7 +1299,7 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
             }
           }
         })
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let record = lower_expression(c, record)
       let field_types = list.map(fields, fn(x) { x.typ })
       let constructor_typ = FunctionType(field_types, typ)
@@ -1298,7 +1308,7 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       Let(body.typ, subject_name, record, body)
     }
     t.FieldAccess(typ, container, module, variant, _label, index) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let container = lower_expression(c, container)
       let assert NamedType(custom, _) = container.typ
       let assert Ok(module) = dict.get(c.modules, module)
@@ -1314,19 +1324,19 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       Op(typ, FieldAccess(variant.name, field), [container])
     }
     t.Call(typ, function, args) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let function = lower_expression(c, function)
       let arguments = list.map(args, lower_expression(c, _))
       Call(typ, function, arguments)
     }
     t.TupleIndex(typ, tuple, index) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let tuple = lower_expression(c, tuple)
       Op(typ, FieldAccess("#", gen_names.get_field_name("", index)), [tuple])
     }
     t.FnCapture(..) -> todo
     t.BitString(typ, segs) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
 
       let segs =
         list.map(segs, fn(seg) {
@@ -1440,9 +1450,9 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       Let(body.typ, "total_size", total_size, body)
     }
     t.Case(typ, subjects, clauses) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let message = String("No matching clause in " <> current_location(c))
-      let else_body = Panic(typ, Literal(map_type(c, t.string_type), message))
+      let else_body = Panic(typ, Literal(map_type(t.string_type), message))
 
       // Create bindings for each subject
       let subject_vars =
@@ -1465,7 +1475,7 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
               list.flat_map(sub_pats, fn(pair) {
                 let #(#(name, exp, _), pattern) = pair
                 let sub = t.LocalVariable(exp.typ, name)
-                lower_pattern_bindings(c, pattern, sub)
+                lower_pattern_bindings(pattern, sub)
               })
 
             // Create pattern matching conditions
@@ -1528,7 +1538,7 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
       lower_expression(c, not_eq)
     }
     t.BinaryOperator(typ, name, left, right) -> {
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let left = lower_expression(c, left)
       let right = lower_expression(c, right)
       let function_name = case name {
@@ -1563,15 +1573,15 @@ fn lower_expression(c: t.Context, exp: t.Expression) -> Exp {
     t.Echo(typ:, value:) -> {
       let assert Some(value) = value
       let value = lower_expression(c, value)
-      let typ = map_type(c, typ)
+      let typ = map_type(typ)
       let print_typ = FunctionType([value.typ], value.typ)
       Call(typ, Global(print_typ, "echo_"), [value])
     }
   }
 }
 
-fn current_location(c: t.Context) {
-  c.current_module <> "." <> c.current_definition
+fn current_location(c: Context) {
+  c.module <> "." <> c.definition
 }
 
 fn replace_var(replace: String, with: Exp, in: Exp) -> Exp {
@@ -1627,13 +1637,13 @@ fn replace_var(replace: String, with: Exp, in: Exp) -> Exp {
   }
 }
 
-fn map_poly(c: t.Context, typ: t.Poly) {
-  Poly(typ.vars, map_type(c, typ.typ))
+fn map_poly(typ: t.Poly) {
+  Poly(typ.vars, map_type(typ.typ))
 }
 
-fn register_tuple(c: Context, size: Int) {
+fn register_tuple(c: Module, size: Int) {
   let id = gen_names.get_tuple_id(size)
-  let vars = listx.sane_range(size)
+  let vars = list.map(listx.sane_range(size), t.TypeVarId)
   let element_types = list.map(vars, fn(i) { Unbound(i) })
   let custom_typ = Poly(vars, NamedType(id, element_types))
   let constructor_typ = Poly(vars, FunctionType(element_types, custom_typ.typ))
@@ -1646,31 +1656,27 @@ fn register_tuple(c: Context, size: Int) {
   let variant = Variant(constructor_typ, id, "#", element_fields)
   let custom = CustomType(custom_typ, id, "#", [variant])
 
-  let c = Context(..c, types: [custom, ..c.types])
+  let c = Module(..c, types: [custom, ..c.types])
   register_variant_functions(c, t.builtin, variant)
 }
 
-fn map_type(c: t.Context, typ: t.Type) {
+fn map_type(typ: t.Type) {
   case typ {
-    t.NamedType(name:, module:, parameters:) -> {
-      let parameters = list.map(parameters, map_type(c, _))
+    t.NamedType(module:, name:, parameters:) -> {
+      let parameters = list.map(parameters, map_type)
       NamedType(get_id(module, name), parameters)
     }
     t.FunctionType(parameters, return) -> {
-      let parameters = list.map(parameters, map_type(c, _))
-      let return = map_type(c, return)
+      let parameters = list.map(parameters, map_type)
+      let return = map_type(return)
       FunctionType(parameters, return)
     }
     t.TupleType(elements) -> {
-      let parameters = list.map(elements, map_type(c, _))
+      let parameters = list.map(elements, map_type)
       NamedType(gen_names.get_tuple_id(list.length(elements)), parameters)
     }
     t.VariableType(ref) -> {
-      let assert Ok(x) = dict.get(c.type_vars, ref)
-      case x {
-        t.Bound(x) -> map_type(c, x)
-        t.Unbound(x) -> Unbound(x)
-      }
+      Unbound(ref)
     }
   }
 }
diff --git a/src/gig/headers.gleam b/src/gig/headers.gleam
index 8f75be8..62a54ff 100644
--- a/src/gig/headers.gleam
+++ b/src/gig/headers.gleam
@@ -6,7 +6,7 @@ import gleam/dict
 import gleam/list
 import gleam/string
 
-pub fn module_headers(c: core.Context) {
+pub fn module_headers(c: core.Module) {
   c.externals
   |> list.filter(fn(x) { !x.builtin })
   |> list.group(fn(x) { x.module })
diff --git a/src/gig/mono.gleam b/src/gig/mono.gleam
index 85fa9b3..39e21ed 100644
--- a/src/gig/mono.gleam
+++ b/src/gig/mono.gleam
@@ -87,7 +87,7 @@ pub type Exp {
   Panic(typ: Type, value: Exp)
 }
 
-pub fn init_context(in: t.Context) -> Context {
+pub fn init_context(in: t.Module) -> Context {
   let in_types =
     list.fold(in.types, dict.new(), fn(d, i) { dict.insert(d, i.id, i) })
   let in_functions =
@@ -111,7 +111,7 @@ pub fn init_context(in: t.Context) -> Context {
   )
 }
 
-pub fn run(in: t.Context, main_name: String) {
+pub fn run(in: t.Module, main_name: String) {
   let c = init_context(in)
 
   let main = case dict.get(c.in_functions, main_name) {
@@ -137,7 +137,7 @@ pub fn run(in: t.Context, main_name: String) {
   #(c, main_name)
 }
 
-pub fn sub_type(sub: List(#(Int, Type)), typ: t.Type) -> Type {
+pub fn sub_type(sub: List(#(t.TypeVarId, Type)), typ: t.Type) -> Type {
   case typ {
     t.Unbound(id) ->
       case list.find(sub, fn(sub) { sub.0 == id }) {
@@ -150,7 +150,11 @@ pub fn sub_type(sub: List(#(Int, Type)), typ: t.Type) -> Type {
   }
 }
 
-fn unify_poly(c: Context, poly: t.Poly, mono: Type) -> List(#(Int, Type)) {
+fn unify_poly(
+  c: Context,
+  poly: t.Poly,
+  mono: Type,
+) -> List(#(t.TypeVarId, Type)) {
   let sub = unify_type(c, poly.typ, mono)
   list.map(poly.vars, fn(x) {
     case list.find(sub, fn(s) { s.0 == x }) {
@@ -162,7 +166,11 @@ fn unify_poly(c: Context, poly: t.Poly, mono: Type) -> List(#(Int, Type)) {
   })
 }
 
-fn unify_type(c: Context, poly: t.Type, mono: Type) -> List(#(Int, Type)) {
+fn unify_type(
+  c: Context,
+  poly: t.Type,
+  mono: Type,
+) -> List(#(t.TypeVarId, Type)) {
   case poly, mono {
     t.Unbound(id), _ -> [#(id, mono)]
     t.NamedType(a, aa), NamedType(b, ba) ->
@@ -194,7 +202,7 @@ pub fn type_name(typ: Type) -> String {
   }
 }
 
-fn get_type_string(sub: List(#(Int, Type))) {
+fn get_type_string(sub: List(#(t.TypeVarId, Type))) {
   // TODO only include typed that are actually used
   // e.g. variant that only uses part of the params
   // e.g. phantom type
@@ -410,7 +418,7 @@ fn instantiate_builtin(c: Context, fun_name: String, mono: Type) -> Context {
 
 fn typed_to_mono_exp(
   c: Context,
-  sub: List(#(Int, Type)),
+  sub: List(#(t.TypeVarId, Type)),
   e: t.Exp,
 ) -> #(Context, Exp) {
   let c = instantiate_type(c, sub_type(sub, e.typ))
diff --git a/src/gig/typed_ast.gleam b/src/gig/typed_ast.gleam
index 645dcbe..e6aa366 100644
--- a/src/gig/typed_ast.gleam
+++ b/src/gig/typed_ast.gleam
@@ -1,6 +1,7 @@
 import gig/call_graph
 import gig/graph
 import glance.{Span} as g
+import gleam/order
 import listx
 
 import gleam/dict.{type Dict}
@@ -12,28 +13,27 @@ import gleam/string
 
 pub const builtin = "gleam"
 
-pub const nil_type = NamedType("Nil", builtin, [])
+pub const nil_type = NamedType(builtin, "Nil", [])
 
-pub const bool_type = NamedType("Bool", builtin, [])
+pub const bool_type = NamedType(builtin, "Bool", [])
 
-pub const int_type = NamedType("Int", builtin, [])
+pub const int_type = NamedType(builtin, "Int", [])
 
-pub const codepoint_type = NamedType("UtfCodepoint", builtin, [])
+pub const codepoint_type = NamedType(builtin, "UtfCodepoint", [])
 
-pub const float_type = NamedType("Float", builtin, [])
+pub const float_type = NamedType(builtin, "Float", [])
 
-pub const string_type = NamedType("String", builtin, [])
+pub const string_type = NamedType(builtin, "String", [])
 
-pub const bit_array_type = NamedType("BitArray", builtin, [])
+pub const bit_array_type = NamedType(builtin, "BitArray", [])
 
-pub type Ref {
-  Ref(id: Int)
+pub type TypeVarId {
+  TypeVarId(id: Int)
 }
 
-// TODO do we need unbound? what if unbound is just a missing key in the map
 pub type TypeVar {
   Bound(Type)
-  Unbound(id: Int)
+  Unbound
 }
 
 pub type Definition(definition) {
@@ -41,7 +41,12 @@ pub type Definition(definition) {
 }
 
 pub type Attribute {
-  Attribute(name: String, arguments: List(Expression))
+  Attribute(name: String, arguments: List(AttributeArgument))
+}
+
+pub type AttributeArgument {
+  NameAttributeArgument(name: String)
+  StringAttributeArgument(value: String)
 }
 
 // TODO it would probably be good to parameterise the Type
@@ -50,11 +55,6 @@ pub type Attribute {
 pub type Module {
   Module(
     name: String,
-    // TODO move these into context instead of module?
-    // TODO put more info into the envs
-    module_env: Dict(String, String),
-    type_env: Dict(String, #(Poly, List(Variant))),
-    value_env: Dict(String, ResolvedGlobal),
     imports: List(Definition(Import)),
     custom_types: List(Definition(CustomType)),
     type_aliases: List(Definition(TypeAlias)),
@@ -63,6 +63,18 @@ pub type Module {
   )
 }
 
+/// The interface to a module without its implementation
+pub type ModuleInterface {
+  ModuleInterface(
+    name: String,
+    imports: List(String),
+    custom_types: List(CustomType),
+    type_aliases: List(TypeAlias),
+    constants: List(ConstantDeclaration),
+    functions: List(FunctionDeclaration),
+  )
+}
+
 pub type FunctionDefinition {
   FunctionDefinition(
     typ: Poly,
@@ -75,6 +87,16 @@ pub type FunctionDefinition {
   )
 }
 
+/// Declaration of a function for the ModuleInterface
+pub type FunctionDeclaration {
+  FunctionDeclaration(
+    typ: Poly,
+    name: String,
+    parameters: List(FunctionParameter),
+    return: Option(Annotation),
+  )
+}
+
 pub type Span =
   g.Span
 
@@ -141,7 +163,7 @@ pub type Expression {
     name: String,
     labels: List(Option(String)),
   )
-  Constant(typ: Type, module: String, name: String, value: Expression)
+  Constant(typ: Type, module: String, name: String)
   NegateInt(typ: Type, value: Expression)
   NegateBool(typ: Type, value: Expression)
   Block(typ: Type, statements: List(Statement))
@@ -255,6 +277,7 @@ pub type Import {
 
 pub type ConstantDefinition {
   ConstantDefinition(
+    typ: Poly,
     name: String,
     publicity: Publicity,
     annotation: Option(Annotation),
@@ -262,6 +285,11 @@ pub type ConstantDefinition {
   )
 }
 
+/// Declaration of a constant for the ModuleInterface
+pub type ConstantDeclaration {
+  ConstantDeclaration(typ: Poly, name: String, annotation: Option(Annotation))
+}
+
 pub type UnqualifiedImport {
   UnqualifiedImport(name: String, alias: Option(String))
 }
@@ -301,23 +329,21 @@ pub type Field(t) {
 }
 
 pub type Type {
-  // TODO change to module, name
-  NamedType(name: String, module: String, parameters: List(Type))
+  NamedType(module: String, name: String, parameters: List(Type))
   TupleType(elements: List(Type))
   FunctionType(parameters: List(Type), return: Type)
-  VariableType(ref: Ref)
+  VariableType(ref: TypeVarId)
 }
 
 pub type Poly {
-  // TODO should vars be List(TypeVarRef) ??
-  Poly(vars: List(Int), typ: Type)
+  Poly(vars: List(TypeVarId), typ: Type)
 }
 
 pub type Annotation {
   NamedAnno(
     typ: Type,
-    name: String,
     module: Option(String),
+    name: String,
     parameters: List(Annotation),
   )
   TupleAnno(typ: Type, elements: List(Annotation))
@@ -343,22 +369,24 @@ pub type Error {
   IncompatibleTypes(location: Location, type_a: Type, type_b: Type)
   RecursiveTypeError(location: Location)
   BitPatternSegmentTypeOverSpecified(location: Location)
+  InvalidAttributeArgument(location: Location)
 }
 
-pub type QualifiedName {
-  QualifiedName(module: String, name: String)
+pub type QName {
+  QName(module: String, name: String)
 }
 
 pub type Context {
   Context(
-    module_source: String,
-    current_module: String,
     current_definition: String,
     current_span: Span,
-    type_vars: Dict(Ref, TypeVar),
-    modules: Dict(String, Module),
+    type_vars: Dict(TypeVarId, TypeVar),
+    module: Module,
     type_uid: Int,
     temp_uid: Int,
+    module_aliases: Dict(String, String),
+    type_env: Dict(QName, #(Poly, List(Variant))),
+    value_env: Dict(QName, ResolvedGlobal),
   )
 }
 
@@ -368,92 +396,66 @@ pub type LocalEnv =
 pub type TypeEnv =
   Dict(String, Type)
 
-pub fn new_context() -> Context {
-  Context(
-    module_source: "",
-    current_module: "",
-    current_definition: "",
-    current_span: Span(0, 0),
-    type_vars: dict.new(),
-    modules: dict.new(),
-    type_uid: 0,
-    temp_uid: 0,
-  )
-}
-
+/// Run type inference on a `glance.Module`.
+/// Interfaces of all modules this module imports must be provided.
 pub fn infer_module(
-  c: Context,
+  modules: Dict(String, ModuleInterface),
   module: g.Module,
   module_name: String,
-  module_source: String,
-) -> Result(Context, Error) {
-  let modules =
-    dict.insert(
-      c.modules,
-      module_name,
-      Module(
-        name: module_name,
-        module_env: dict.new(),
-        type_env: dict.new(),
-        value_env: dict.new(),
-        imports: [],
-        custom_types: [],
-        type_aliases: [],
-        constants: [],
-        functions: [],
-      ),
+) -> Result(Module, Error) {
+  let c =
+    list.fold(
+      dict.values(modules),
+      new_context(module_name),
+      add_module_interface,
     )
 
-  let c = Context(..c, modules:, current_module: module_name, module_source:)
-
   // handle module imports
   use c <- result.try(
     list.try_fold(module.imports, c, fn(c, imp) {
-      try_update_module(c, fn(module) {
-        let imp = imp.definition
-        let module_id = imp.module
-
-        let module_env = case imp.alias {
-          Some(alias) ->
-            case alias {
-              g.Named(alias) -> dict.insert(module.module_env, alias, module_id)
-              g.Discarded(_) -> module.module_env
-            }
-          None -> {
-            // assert: imported name is a non-empty string
-            let assert Ok(alias) = list.last(string.split(module_id, "/"))
-            dict.insert(module.module_env, alias, module_id)
+      let imp = imp.definition
+      let module_id = imp.module
+
+      let module_aliases = case imp.alias {
+        Some(alias) ->
+          case alias {
+            g.Named(alias) -> dict.insert(c.module_aliases, alias, module_id)
+            g.Discarded(_) -> c.module_aliases
           }
+        None -> {
+          // assert: imported name is a non-empty string
+          let assert Ok(alias) = list.last(string.split(module_id, "/"))
+          dict.insert(c.module_aliases, alias, module_id)
         }
+      }
 
-        use type_env <- result.try(
-          list.try_fold(imp.unqualified_types, module.type_env, fn(acc, imp) {
-            use #(_, poly, variants) <- result.map(resolve_global_type_name(
-              c,
-              module_id,
-              imp.name,
-            ))
-            let alias = case imp.alias {
-              Some(alias) -> alias
-              None -> imp.name
-            }
-            dict.insert(acc, alias, #(poly, variants))
-          }),
-        )
+      use type_env <- result.try(
+        list.try_fold(imp.unqualified_types, c.type_env, fn(acc, imp) {
+          use #(_, poly, variants) <- result.map(resolve_global_type_name(
+            c,
+            module_id,
+            imp.name,
+          ))
+          let alias = case imp.alias {
+            Some(alias) -> alias
+            None -> imp.name
+          }
+          dict.insert(acc, QName(c.module.name, alias), #(poly, variants))
+        }),
+      )
 
-        use value_env <- result.map(
-          list.try_fold(imp.unqualified_values, module.value_env, fn(acc, imp) {
-            use value <- result.map(resolve_global_name(c, module_id, imp.name))
-            let alias = case imp.alias {
-              Some(alias) -> alias
-              None -> imp.name
-            }
-            dict.insert(acc, alias, value)
-          }),
-        )
+      use value_env <- result.map(
+        list.try_fold(imp.unqualified_values, c.value_env, fn(acc, imp) {
+          use value <- result.map(resolve_global_name(c, module_id, imp.name))
+          let alias = case imp.alias {
+            Some(alias) -> alias
+            None -> imp.name
+          }
+          dict.insert(acc, QName(c.module.name, alias), value)
+        }),
+      )
 
-        Module(..module, module_env:, type_env:, value_env:)
-      })
+      Context(..c, module_aliases:, type_env:, value_env:)
     }),
   )
 
@@ -472,7 +474,7 @@ pub fn infer_module(
         })
       let parameters = list.reverse(parameters)
       let param_types = list.map(parameters, fn(x) { x.1 })
-      let typ = NamedType(custom.name, c.current_module, param_types)
+      let typ = NamedType(c.module.name, custom.name, param_types)
       let typ = generalise(c, typ)
 
       register_type(c, def.definition.name, typ, [])
@@ -498,7 +500,7 @@ pub fn infer_module(
       // update the placeholder type
       use #(_, placeholder, _) <- result.try(resolve_global_type_name(
         c,
-        c.current_module,
+        c.module.name,
         alias.name,
       ))
       use c <- result.map(unify(c, alias.aliased.typ, placeholder.typ))
@@ -536,10 +538,10 @@ pub fn infer_module(
       // reconstruct the type parameters
       use #(_, poly, _) <- result.try(resolve_global_type_name(
         c,
-        c.current_module,
+        c.module.name,
         custom.name,
       ))
-      let param_types = list.map(poly.vars, fn(x) { VariableType(Ref(x)) })
+      let param_types = list.map(poly.vars, fn(x) { VariableType(x) })
       let parameters = list.zip(custom.parameters, param_types)
 
       // infer the custom type including variants
@@ -601,7 +603,7 @@ pub fn infer_module(
       let c = Context(..c, current_span: def.definition.location)
 
       let poly = generalise(c, constant.value.typ)
-      let c = register_constant(c, constant.name, poly, constant.value)
+      let c = register_constant(c, constant.name, poly)
       use attrs <- result.map(infer_attributes(c, def.attributes))
       let def = Definition(attrs, constant)
       update_module(c, fn(mod) {
@@ -616,56 +618,135 @@ pub fn infer_module(
     call_graph.function_graph(module)
     |> graph.strongly_connected_components()
 
-  list.try_fold(rec_groups, c, fn(c, group) {
-    // find the function definitions by name
-    use group <- result.try(
-      list.try_map(group, fn(fun_name) {
-        list.find(module.functions, fn(f) { f.definition.name == fun_name })
-        |> result.replace_error(UnresolvedFunction(location(c), fun_name))
-      }),
-    )
-
-    // infer types for the group
-    use #(c, group) <- result.try(
-      list.try_fold(group, #(c, []), fn(acc, def) {
-        let #(c, group) = acc
-        let c = Context(..c, current_definition: def.definition.name)
-        let c = Context(..c, current_span: def.definition.location)
-
-        // infer function
-        use #(c, fun) <- result.try(infer_function(c, def.definition))
-        use attrs <- result.map(infer_attributes(c, def.attributes))
-        let def = Definition(attrs, fun)
+  use c <- result.map(
+    list.try_fold(rec_groups, c, fn(c, group) {
+      // find the function definitions by name
+      use group <- result.try(
+        list.try_map(group, fn(fun_name) {
+          list.find(module.functions, fn(f) { f.definition.name == fun_name })
+          |> result.replace_error(UnresolvedFunction(location(c), fun_name))
+        }),
+      )
 
-        #(c, [def, ..group])
-      }),
-    )
+      // infer types for the group
+      use #(c, group) <- result.try(
+        list.try_fold(group, #(c, []), fn(acc, def) {
+          let #(c, group) = acc
+          let c = Context(..c, current_definition: def.definition.name)
+          let c = Context(..c, current_span: def.definition.location)
 
-    // generalise
-    list.try_fold(group, c, fn(c, def) {
-      let fun = def.definition
+          // infer function
+          use #(c, fun) <- result.try(infer_function(c, def.definition))
+          use attrs <- result.map(infer_attributes(c, def.attributes))
+          let def = Definition(attrs, fun)
 
-      // unify placeholder type
-      use placeholder <- result.try(resolve_global_name(
-        c,
-        c.current_module,
-        fun.name,
-      ))
-      use c <- result.map(unify(c, placeholder.typ.typ, fun.typ.typ))
+          #(c, [def, ..group])
+        }),
+      )
 
       // generalise
-      let typ = generalise(c, fun.typ.typ)
-      let fun = FunctionDefinition(..fun, typ:)
-      let def = Definition(..def, definition: fun)
+      list.try_fold(group, c, fn(c, def) {
+        let fun = def.definition
 
-      // update context
-      let labels = list.map(fun.parameters, fn(f) { f.label })
-      let c = register_function(c, fun.name, fun.typ, labels)
-      update_module(c, fn(mod) {
-        Module(..mod, functions: [def, ..mod.functions])
+        // unify placeholder type
+        use placeholder <- result.try(resolve_global_name(
+          c,
+          c.module.name,
+          fun.name,
+        ))
+        use c <- result.map(unify(c, placeholder.typ.typ, fun.typ.typ))
+
+        // generalise
+        let typ = generalise(c, fun.typ.typ)
+        let fun = FunctionDefinition(..fun, typ:)
+        let def = Definition(..def, definition: fun)
+
+        // update context
+        let labels = list.map(fun.parameters, fn(f) { f.label })
+        let c = register_function(c, fun.name, fun.typ, labels)
+        update_module(c, fn(mod) {
+          Module(..mod, functions: [def, ..mod.functions])
+        })
       })
+    }),
+  )
+
+  // Fully resolve all type references
+  let mod = c.module
+  let type_aliases =
+    list.map(
+      mod.type_aliases,
+      map_definition(_, fn(type_alias) {
+        TypeAlias(..type_alias, typ: substitute_poly(c, type_alias.typ))
+      }),
+    )
+  let custom_types =
+    list.map(mod.custom_types, map_definition(_, substitute_custom_type(c, _)))
+  let constants =
+    list.map(
+      mod.constants,
+      map_definition(_, fn(constant) {
+        ConstantDefinition(
+          ..constant,
+          typ: substitute_poly(c, constant.typ),
+          value: substitute_expression(c, constant.value),
+        )
+      }),
+    )
+  let functions =
+    list.map(mod.functions, map_definition(_, substitute_function(c, _)))
+  Module(..mod, type_aliases:, custom_types:, constants:, functions:)
+}
+
+pub fn interface(module: Module) -> ModuleInterface {
+  ModuleInterface(
+    name: module.name,
+    imports: list.map(module.imports, fn(i) { i.definition.module }),
+    custom_types: list.map(module.custom_types, fn(t) { t.definition }),
+    type_aliases: list.map(module.type_aliases, fn(t) { t.definition }),
+    constants: list.filter(module.constants, fn(c) {
+      c.definition.publicity == Public
     })
-  })
+      |> list.map(fn(c) {
+        ConstantDeclaration(
+          typ: c.definition.typ,
+          name: c.definition.name,
+          annotation: c.definition.annotation,
+        )
+      }),
+    functions: list.filter(module.functions, fn(f) {
+      f.definition.publicity == Public
+    })
+      |> list.map(fn(f) {
+        FunctionDeclaration(
+          typ: f.definition.typ,
+          name: f.definition.name,
+          parameters: f.definition.parameters,
+          return: f.definition.return,
+        )
+      }),
+  )
+}
+
+fn new_context(module_name: String) -> Context {
+  Context(
+    current_definition: "",
+    current_span: Span(0, 0),
+    type_vars: dict.new(),
+    module: Module(
+      name: module_name,
+      imports: [],
+      custom_types: [],
+      type_aliases: [],
+      constants: [],
+      functions: [],
+    ),
+    type_uid: 0,
+    temp_uid: 1,
+    module_aliases: dict.new(),
+    type_env: dict.new(),
+    value_env: dict.new(),
+  )
 }
 
 /// Returns a human-readable string description of the error.
@@ -708,36 +789,26 @@ pub fn inspect_error(error: Error) {
       <> string.inspect(type_b)
     RecursiveTypeError(..) ->
       "Encountered a cyclical dependency between type variables"
-    BitPatternSegmentTypeOverSpecified(_) ->
+    BitPatternSegmentTypeOverSpecified(..) ->
       "Bit pattern segment type set multiple times"
+    InvalidAttributeArgument(..) ->
+      "Unexpected expression for attribute argument (only variable or string are allowed)"
   }
 }
 
 fn generalise(c: Context, typ: Type) {
   let tvs =
     list.unique(find_tvs(c, typ))
-    |> list.sort(int.compare)
+    |> list.sort(type_var_id_compare)
   Poly(tvs, typ)
 }
 
-fn get_current_module(c: Context) -> Module {
-  // assert: the current module exists
-  let assert Ok(module) = dict.get(c.modules, c.current_module)
-  module
+fn type_var_id_compare(a: TypeVarId, b: TypeVarId) -> order.Order {
+  int.compare(a.id, b.id)
 }
 
 fn update_module(c: Context, fun: fn(Module) -> Module) {
-  let module = get_current_module(c)
-  let module = fun(module)
-  let modules = dict.insert(c.modules, c.current_module, module)
-  Context(..c, modules:)
-}
-
-fn try_update_module(c: Context, fun: fn(Module) -> Result(Module, Error)) {
-  let module = get_current_module(c)
-  use module <- result.map(fun(module))
-  let modules = dict.insert(c.modules, c.current_module, module)
-  Context(..c, modules:)
+  Context(..c, module: fun(c.module))
 }
 
 fn register_function(
@@ -746,32 +817,23 @@ fn register_function(
   typ: Poly,
   labels: List(Option(String)),
 ) -> Context {
-  update_module(c, fn(module) {
-    let value_env =
-      dict.insert(
-        module.value_env,
-        name,
-        FunctionGlobal(c.current_module, name, typ, labels),
-      )
-    Module(..module, value_env:)
-  })
+  let value_env =
+    dict.insert(
+      c.value_env,
+      QName(c.module.name, name),
+      FunctionGlobal(c.module.name, name, typ, labels),
+    )
+  Context(..c, value_env:)
 }
 
-fn register_constant(
-  c: Context,
-  name: String,
-  typ: Poly,
-  value: Expression,
-) -> Context {
-  update_module(c, fn(module) {
-    let value_env =
-      dict.insert(
-        module.value_env,
-        name,
-        ConstantGlobal(c.current_module, name, typ, value),
-      )
-    Module(..module, value_env:)
-  })
+fn register_constant(c: Context, name: String, typ: Poly) -> Context {
+  let value_env =
+    dict.insert(
+      c.value_env,
+      QName(c.module.name, name),
+      ConstantGlobal(c.module.name, name, typ),
+    )
+  Context(..c, value_env:)
 }
 
 fn register_type(
@@ -780,35 +842,30 @@ fn register_type(
   typ: Poly,
   variants: List(Variant),
 ) -> Context {
-  update_module(c, fn(module) {
-    let type_env = dict.insert(module.type_env, name, #(typ, variants))
-    Module(..module, type_env:)
-  })
+  let type_env =
+    dict.insert(c.type_env, QName(c.module.name, name), #(typ, variants))
+  Context(..c, type_env:)
 }
 
 fn infer_attributes(c: Context, attrs: List(g.Attribute)) {
-  let attr_env =
-    dict.new()
-    |> dict.insert("c", nil_type)
-    |> dict.insert("erlang", nil_type)
-    |> dict.insert("javascript", nil_type)
-
-  use #(_, attrs) <- result.map(
-    list.try_fold(attrs, #(c, []), fn(acc, attr) {
-      let #(c, attrs) = acc
-      use #(c, exprs) <- result.map(
-        list.try_fold(attr.arguments, #(c, []), fn(acc, attr) {
-          let #(c, exprs) = acc
-          use #(c, expr) <- result.map(infer_expression(c, attr_env, attr))
-          #(c, [expr, ..exprs])
-        }),
-      )
-      let exprs = list.reverse(exprs)
-      let attr = Attribute(attr.name, exprs)
-      #(c, [attr, ..attrs])
-    }),
-  )
-  list.reverse(attrs)
+  list.try_map(attrs, fn(attr) {
+    use args <- result.map(
+      list.try_map(attr.arguments, map_attribute_argument(c, _)),
+    )
+    Attribute(attr.name, args)
+  })
+}
+
+fn map_attribute_argument(
+  c: Context,
+  expr: g.Expression,
+) -> Result(AttributeArgument, Error) {
+  let c = Context(..c, current_span: expr.location)
+  case expr {
+    g.String(value:, ..) -> Ok(StringAttributeArgument(value))
+    g.Variable(name:, ..) -> Ok(NameAttributeArgument(name))
+    _ -> Error(InvalidAttributeArgument(location(c)))
+  }
 }
 
 fn infer_constant(
@@ -830,7 +887,10 @@ fn infer_constant(
     None -> Ok(#(c, None))
   })
 
-  let constant = ConstantDefinition(con.name, publicity, annotation, value)
+  let poly = generalise(c, value.typ)
+
+  let constant =
+    ConstantDefinition(poly, con.name, publicity, annotation, value)
 
   #(c, constant)
 }
@@ -915,9 +975,8 @@ fn infer_alias_type(
       let n = dict.insert(n, name, typ)
       // assert: new_type_var_ref always returns a VariableType
       let assert VariableType(ref) = typ
-      #(c, n, [ref.id, ..args])
+      #(c, n, [ref, ..args])
     })
-
   let args = list.reverse(args)
 
   use #(c, aliased) <- result.map(do_infer_annotation(
@@ -941,7 +1000,7 @@ fn infer_custom_type(
   // create a type variable for each parameter
   // these will be used when a field references a type parameter
   let param_types = list.map(parameters, fn(x) { x.1 })
-  let module = c.current_module
+  let module = c.module.name
   let name = custom.name
   let typ = NamedType(module:, name:, parameters: param_types)
 
@@ -1130,9 +1189,7 @@ fn do_infer_annotation(
         |> result.map(dict.from_list),
       )
       let typ = do_instantiate(c, mapping, poly.typ)
-
-      // let typ = NamedType(name, module, list.map(params, fn(x) { x.typ }))
-      #(c, NamedAnno(typ, name, anno_module, params))
+      #(c, NamedAnno(typ, anno_module, name, params))
     }
     g.TupleType(_, elements) -> {
       use #(c, elements) <- result.map(
@@ -1173,6 +1230,63 @@ fn do_infer_annotation(
   }
 }
 
+fn add_module_interface(c: Context, m: ModuleInterface) -> Context {
+  let value_env =
+    list.fold(m.constants, c.value_env, fn(value_env, constant) {
+      dict.insert(
+        value_env,
+        QName(m.name, constant.name),
+        ConstantGlobal(m.name, constant.name, constant.typ),
+      )
+    })
+  let value_env =
+    list.fold(m.functions, value_env, fn(value_env, function) {
+      dict.insert(
+        value_env,
+        QName(m.name, function.name),
+        FunctionGlobal(
+          m.name,
+          function.name,
+          function.typ,
+          list.map(function.parameters, fn(f) { f.label }),
+        ),
+      )
+    })
+  let value_env =
+    list.flat_map(m.custom_types, fn(custom_type) { custom_type.variants })
+    |> list.fold(value_env, fn(value_env, variant) {
+      dict.insert(
+        value_env,
+        QName(m.name, variant.name),
+        FunctionGlobal(
+          m.name,
+          variant.name,
+          variant.typ,
+          list.map(variant.fields, fn(f) { f.label }),
+        ),
+      )
+    })
+
+  let type_env =
+    list.fold(m.custom_types, c.type_env, fn(type_env, custom_type) {
+      dict.insert(type_env, QName(m.name, custom_type.name), #(
+        custom_type.typ,
+        custom_type.variants,
+      ))
+    })
+
+  let type_env =
+    list.fold(m.type_aliases, type_env, fn(type_env, type_alias) {
+      dict.insert(
+        type_env,
+        QName(m.name, type_alias.name),
+        #(type_alias.typ, []),
+      )
+    })
+
+  Context(..c, value_env:, type_env:)
+}
+
 pub type ResolvedGlobal {
   FunctionGlobal(
     module: String,
@@ -1180,7 +1294,7 @@ pub type ResolvedGlobal {
     typ: Poly,
     labels: List(Option(String)),
   )
-  ConstantGlobal(module: String, name: String, typ: Poly, value: Expression)
+  ConstantGlobal(module: String, name: String, typ: Poly)
 }
 
 type ResolvedVariable {
@@ -1207,7 +1321,7 @@ fn resolve_unqualified_global(
   name: String,
 ) -> Result(ResolvedGlobal, Error) {
   // try global env
-  resolve_global_name(c, c.current_module, name)
+  resolve_global_name(c, c.module.name, name)
   |> result.try_recover(fn(_) {
     // try prelude
     resolve_global_name(c, builtin, name)
@@ -1217,7 +1331,7 @@ fn resolve_unqualified_global(
 /// Resolve a global from a possibly aliased module
 fn resolve_aliased_global(
   c: Context,
-  name: QualifiedName,
+  name: QName,
 ) -> Result(ResolvedGlobal, Error) {
   resolve_module(c, name.module)
   |> result.try(resolve_global_name(c, _, name.name))
@@ -1229,8 +1343,7 @@ pub fn resolve_global_name(
   module_name: String,
   name: String,
 ) -> Result(ResolvedGlobal, Error) {
-  use module <- result.try(get_module(c, module_name))
-  dict.get(module.value_env, name)
+  dict.get(c.value_env, QName(module_name, name))
   |> result.replace_error(UnresolvedGlobal(location(c), name))
 }
 
@@ -1239,21 +1352,21 @@ fn resolve_type_name(
   c: Context,
   mod: Option(String),
   name: String,
-) -> Result(#(QualifiedName, Poly, List(Variant)), Error) {
+) -> Result(#(QName, Poly, List(Variant)), Error) {
   case mod {
     Some(mod) -> resolve_aliased_type_name(c, mod, name)
     None ->
-      resolve_global_type_name(c, c.current_module, name)
+      resolve_global_type_name(c, c.module.name, name)
       |> result.try_recover(fn(_) { resolve_global_type_name(c, builtin, name) })
   }
 }
 
-/// Resolve a type name from a possibly aliased module 
+/// Resolve a type name from a possibly aliased module
 fn resolve_aliased_type_name(
   c: Context,
   module: String,
   name: String,
-) -> Result(#(QualifiedName, Poly, List(Variant)), Error) {
+) -> Result(#(QName, Poly, List(Variant)), Error) {
   resolve_module(c, module)
   |> result.try(resolve_global_type_name(c, _, name))
 }
@@ -1263,35 +1376,26 @@ pub fn resolve_global_type_name(
   c: Context,
   module_name: String,
   name: String,
-) -> Result(#(QualifiedName, Poly, List(Variant)), Error) {
-  use module <- result.try(get_module(c, module_name))
-  use #(typ, variants) <- result.map(
-    dict.get(module.type_env, name)
-    |> result.replace_error(UnresolvedType(
-      location(c),
-      module_name <> "." <> name,
-    )),
-  )
-  #(QualifiedName(module_name, name), typ, variants)
+) -> Result(#(QName, Poly, List(Variant)), Error) {
+  dict.get(c.type_env, QName(module_name, name))
+  |> result.replace_error(UnresolvedType(
+    location(c),
+    module_name <> "." <> name,
+  ))
+  |> result.map(fn(t) { #(QName(module_name, name), t.0, t.1) })
 }
 
 /// Resolve a qualified or unqualified contructor name
 fn resolve_constructor_name(c: Context, mod: Option(String), name: String) {
   case mod {
-    Some(mod) -> resolve_aliased_global(c, QualifiedName(mod, name))
+    Some(mod) -> resolve_aliased_global(c, QName(mod, name))
     None -> resolve_unqualified_global(c, name)
   }
 }
 
 /// Resolve a module alias to its fully qualified name
 fn resolve_module(c: Context, module_name: String) -> Result(String, Error) {
-  dict.get(get_current_module(c).module_env, module_name)
-  |> result.replace_error(UnresolvedModule(location(c), module_name))
-}
-
-/// Get a module by its fully qualified name
-fn get_module(c: Context, module_name: String) -> Result(Module, Error) {
-  dict.get(c.modules, module_name)
+  dict.get(c.module_aliases, module_name)
   |> result.replace_error(UnresolvedModule(location(c), module_name))
 }
 
@@ -1301,8 +1405,8 @@ fn new_temp_var(c: Context) -> #(Context, String) {
 }
 
 fn new_type_var_ref(c: Context) {
-  let ref = Ref(c.type_uid)
-  let type_vars = dict.insert(c.type_vars, ref, Unbound(c.type_uid))
+  let ref = TypeVarId(c.type_uid)
+  let type_vars = dict.insert(c.type_vars, ref, Unbound)
   let typ = VariableType(ref)
   #(Context(..c, type_vars: type_vars, type_uid: c.type_uid + 1), typ)
 }
@@ -1362,7 +1466,7 @@ fn infer_pattern(
       )
 
       // Create the list type
-      let typ = NamedType("List", builtin, [elem_type])
+      let typ = NamedType(builtin, "List", [elem_type])
 
       // Handle the tail pattern if present
       use #(c, n, tail) <- result.map(case tail {
@@ -1779,9 +1883,9 @@ fn infer_expression(
               let #(c, typ) = instantiate(c, typ)
               Ok(#(c, Function(typ, module, name, labels)))
             }
-            ConstantGlobal(module, name, typ, value) -> {
+            ConstantGlobal(module, name, typ) -> {
               let #(c, typ) = instantiate(c, typ)
-              Ok(#(c, Constant(typ, module, name, value)))
+              Ok(#(c, Constant(typ, module, name)))
             }
           }
         Ok(ResolvedLocal(name, typ)) -> {
@@ -1875,7 +1979,7 @@ fn infer_expression(
 
       // Create a type variable for the element type
       let #(c, elem_type) = new_type_var_ref(c)
-      let typ = NamedType("List", builtin, [elem_type])
+      let typ = NamedType(builtin, "List", [elem_type])
 
       // Unify all element types
       use c <- result.try(
@@ -1981,16 +2085,20 @@ fn infer_expression(
 
         // field access must be on a named type
         let value_typ = case resolve_type(c, value.typ) {
-          NamedType(type_name, module, _) -> Ok(#(type_name, module))
+          NamedType(module, type_name, _) -> Ok(#(type_name, module))
           _ -> Error(InvalidFieldAccess(location(c)))
         }
         use #(type_name, module) <- result.try(value_typ)
 
         // find the custom type definition
-        use custom <- result.try(resolve_custom_type(c, module, type_name))
+        use #(typ, variants) <- result.try(resolve_custom_type(
+          c,
+          module,
+          type_name,
+        ))
 
         // access only works with one variant
-        let variant = case custom.definition.variants {
+        let variant = case variants {
           // TODO proper implementation checking all variants
           [variant, ..] -> Ok(variant)
           _ -> Error(InvalidFieldAccess(location(c)))
@@ -2006,8 +2114,8 @@ fn infer_expression(
         use #(field, index) <- result.try(field)
 
         // create a getter function type
-        let getter = FunctionType([custom.definition.typ.typ], field.item.typ)
-        let getter = Poly(custom.definition.typ.vars, getter)
+        let getter = FunctionType([typ.typ], field.item.typ)
+        let getter = Poly(typ.vars, getter)
         let #(c, getter) = instantiate(c, getter)
 
         // unify the getter as if we're calling it on the value
@@ -2022,16 +2130,16 @@ fn infer_expression(
           // try a module access instead
           case container {
             g.Variable(_, module) -> {
-              case resolve_aliased_global(c, QualifiedName(module, label)) {
+              case resolve_aliased_global(c, QName(module, label)) {
                 Ok(FunctionGlobal(module, name, poly, labels)) -> {
                   let #(c, typ) = instantiate(c, poly)
                   Ok(#(c, Function(typ, module, name, labels)))
                 }
-                Ok(ConstantGlobal(module, name, poly, value)) -> {
+                Ok(ConstantGlobal(module, name, poly)) -> {
                   let #(c, typ) = instantiate(c, poly)
-                  Ok(#(c, Constant(typ, module, name, value)))
+                  Ok(#(c, Constant(typ, module, name)))
                 }
-                Error(_) -> Error(e)
+                Error(e) -> Error(e)
               }
             }
             _ -> Error(e)
@@ -2365,8 +2473,7 @@ fn infer_expression(
 }
 
 fn resolve_custom_type(c: Context, module: String, type_name: String) {
-  use mod <- result.try(get_module(c, module))
-  list.find(mod.custom_types, fn(x) { x.definition.name == type_name })
+  dict.get(c.type_env, QName(module, type_name))
   |> result.replace_error(UnresolvedType(location(c), type_name))
 }
 
@@ -2445,15 +2552,15 @@ fn infer_fn(
 }
 
 type PolyEnv =
-  Dict(Int, Type)
+  Dict(TypeVarId, Type)
 
-fn get_type_var(c: Context, var: Ref) {
+fn get_type_var(c: Context, var: TypeVarId) {
   // assert: this function is only called for previously created type variables
-  let assert Ok(x) = dict.get(c.type_vars, var)
+  let assert Ok(x) = dict.get(c.type_vars, var) as string.inspect(var)
   x
 }
 
-fn set_type_var(c: Context, var: Ref, bind: TypeVar) {
+fn set_type_var(c: Context, var: TypeVarId, bind: TypeVar) {
   Context(..c, type_vars: dict.insert(c.type_vars, var, bind))
 }
 
@@ -2469,12 +2576,12 @@ fn instantiate(c: Context, poly: Poly) -> #(Context, Type) {
   #(c, typ)
 }
 
-fn find_tvs(c: Context, t: Type) -> List(Int) {
+fn find_tvs(c: Context, t: Type) -> List(TypeVarId) {
   case t {
     VariableType(ref) ->
       case get_type_var(c, ref) {
         Bound(x) -> find_tvs(c, x)
-        Unbound(x) -> [x]
+        Unbound -> [ref]
       }
     NamedType(_, _, args) -> list.flat_map(args, find_tvs(c, _))
     FunctionType(args, ret) -> list.flat_map([ret, ..args], find_tvs(c, _))
@@ -2485,16 +2592,20 @@ fn find_tvs(c: Context, t: Type) -> List(Int) {
 fn do_instantiate(c: Context, n: PolyEnv, typ: Type) -> Type {
   case typ {
     VariableType(ref) ->
-      case get_type_var(c, ref) {
-        Bound(x) -> do_instantiate(c, n, x)
-        Unbound(x) ->
-          case dict.get(n, x) {
-            Ok(r) -> r
-            Error(_) -> typ
+      case dict.get(n, ref) {
+        Ok(r) -> r
+        Error(_) ->
+          case get_type_var(c, ref) {
+            Bound(x) -> do_instantiate(c, n, x)
+            Unbound -> typ
           }
       }
-    NamedType(name, module, args) ->
-      NamedType(name, module, list.map(args, do_instantiate(c, n, _)))
+    NamedType(module:, name:, parameters:) ->
+      NamedType(
+        module:,
+        name:,
+        parameters: list.map(parameters, do_instantiate(c, n, _)),
+      )
     FunctionType(args, ret) ->
       FunctionType(
         list.map(args, do_instantiate(c, n, _)),
@@ -2513,9 +2624,7 @@ fn unify(c: Context, a: Type, b: Type) -> Result(Context, Error) {
       case a == b {
         True -> Ok(c)
         False -> {
-          // assert: since a resolves to VariableType(ref), ref is Unbound
-          let assert Unbound(aid) = get_type_var(c, ref)
-          let #(c, occurs) = occurs(c, aid, b)
+          let #(c, occurs) = occurs(c, ref, b)
           case occurs {
             True -> Error(RecursiveTypeError(location(c)))
             False -> Ok(set_type_var(c, ref, Bound(b)))
@@ -2523,7 +2632,7 @@ fn unify(c: Context, a: Type, b: Type) -> Result(Context, Error) {
         }
       }
     a, VariableType(_) -> unify(c, b, a)
-    NamedType(aname, amodule, _), NamedType(bname, bmodule, _)
+    NamedType(amodule, aname, _), NamedType(bmodule, bname, _)
       if aname != bname || amodule != bmodule
     -> Error(IncompatibleTypes(location(c), a, b))
     NamedType(_, _, aargs), NamedType(_, _, bargs) ->
@@ -2553,15 +2662,15 @@ fn unify_arguments(
   list.try_fold(args, c, fn(c, x) { unify(c, x.0, x.1) })
 }
 
-fn occurs(c: Context, id: Int, in: Type) -> #(Context, Bool) {
+fn occurs(c: Context, id: TypeVarId, in: Type) -> #(Context, Bool) {
   case in {
     VariableType(ref) ->
       case get_type_var(c, ref) {
         Bound(t) -> occurs(c, id, t)
-        Unbound(i) -> {
+        Unbound -> {
           // TODO not sure if this "set" is needed
-          let c = set_type_var(c, ref, Unbound(i))
-          #(c, id == i)
+          let c = set_type_var(c, ref, Unbound)
+          #(c, id == ref)
         }
       }
     NamedType(_, _, args) ->
@@ -2600,26 +2709,382 @@ pub fn resolve_type(c: Context, typ: Type) -> Type {
   }
 }
 
-pub fn resolve_type_deep(c: Context, typ: Type) {
+fn substitute_custom_type(c: Context, custom_type: CustomType) {
+  CustomType(
+    ..custom_type,
+    typ: substitute_poly(c, custom_type.typ),
+    variants: list.map(custom_type.variants, fn(variant) {
+      Variant(
+        ..variant,
+        typ: substitute_poly(c, variant.typ),
+        fields: list.map(
+          variant.fields,
+          map_field(_, substitute_annotation(c, _)),
+        ),
+      )
+    }),
+  )
+}
+
+fn substitute_function(c: Context, function: FunctionDefinition) {
+  FunctionDefinition(
+    ..function,
+    typ: substitute_poly(c, function.typ),
+    parameters: list.map(function.parameters, substitute_function_parameter(
+      c,
+      _,
+    )),
+    body: list.map(function.body, substitute_statement(c, _)),
+    return: option.map(function.return, substitute_annotation(c, _)),
+  )
+}
+
+fn substitute_function_parameter(
+  c: Context,
+  param: FunctionParameter,
+) -> FunctionParameter {
+  FunctionParameter(
+    ..param,
+    typ: substitute_type(c, param.typ),
+    annotation: option.map(param.annotation, substitute_annotation(c, _)),
+  )
+}
+
+fn substitute_statement(c: Context, statement: Statement) -> Statement {
+  case statement {
+    Use(typ:, patterns:, function:) ->
+      Use(
+        typ: substitute_type(c, typ),
+        patterns: list.map(patterns, substitute_pattern(c, _)),
+        function: substitute_expression(c, function),
+      )
+    Assignment(typ:, kind:, pattern:, annotation:, value:) ->
+      Assignment(
+        typ: substitute_type(c, typ),
+        kind:,
+        pattern: substitute_pattern(c, pattern),
+        annotation: option.map(annotation, substitute_annotation(c, _)),
+        value: substitute_expression(c, value),
+      )
+    Assert(typ:, expression:, message:) ->
+      Assert(
+        typ: substitute_type(c, typ),
+        expression: substitute_expression(c, expression),
+        message: option.map(message, substitute_expression(c, _)),
+      )
+    Expression(typ:, expression:) ->
+      Expression(
+        typ: substitute_type(c, typ),
+        expression: substitute_expression(c, expression),
+      )
+  }
+}
+
+fn substitute_expression(c: Context, expr: Expression) -> Expression {
+  // TODO: do we need to substitute type annotations?
+  case expr {
+    Int(..) -> expr
+    Float(..) -> expr
+    String(..) -> expr
+    LocalVariable(typ:, name:) ->
+      LocalVariable(typ: substitute_type(c, typ), name:)
+    Function(typ:, module:, name:, labels:) ->
+      Function(typ: substitute_type(c, typ), module:, name:, labels:)
+    Constant(typ:, module:, name:) ->
+      Constant(typ: substitute_type(c, typ), module:, name:)
+    NegateInt(typ:, value:) ->
+      NegateInt(
+        typ: substitute_type(c, typ),
+        value: substitute_expression(c, value),
+      )
+    NegateBool(typ:, value:) ->
+      NegateBool(
+        typ: substitute_type(c, typ),
+        value: substitute_expression(c, value),
+      )
+    Block(typ:, statements:) ->
+      Block(
+        typ: substitute_type(c, typ),
+        statements: list.map(statements, substitute_statement(c, _)),
+      )
+    Panic(typ:, value:) ->
+      Panic(
+        typ: substitute_type(c, typ),
+        value: option.map(value, substitute_expression(c, _)),
+      )
+    Todo(typ:, value:) ->
+      Todo(
+        typ: substitute_type(c, typ),
+        value: option.map(value, substitute_expression(c, _)),
+      )
+    Echo(typ:, value:) ->
+      Echo(
+        typ: substitute_type(c, typ),
+        value: option.map(value, substitute_expression(c, _)),
+      )
+    Tuple(typ:, elements:) ->
+      Tuple(
+        typ: substitute_type(c, typ),
+        elements: list.map(elements, substitute_expression(c, _)),
+      )
+    List(typ:, elements:, rest:) ->
+      List(
+        typ: substitute_type(c, typ),
+        elements: list.map(elements, substitute_expression(c, _)),
+        rest: option.map(rest, substitute_expression(c, _)),
+      )
+    Fn(typ:, parameters:, return:, body:) ->
+      Fn(
+        typ: substitute_type(c, typ),
+        parameters: list.map(parameters, substitute_function_parameter(c, _)),
+        return: option.map(return, substitute_annotation(c, _)),
+        body: list.map(body, substitute_statement(c, _)),
+      )
+    RecordUpdate(
+      typ:,
+      module:,
+      resolved_module:,
+      constructor:,
+      record:,
+      fields:,
+      ordered_fields:,
+    ) ->
+      RecordUpdate(
+        typ: substitute_type(c, typ),
+        module:,
+        resolved_module:,
+        constructor:,
+        record: substitute_expression(c, record),
+        fields: list.map(fields, fn(field) {
+          let #(name, expr) = field
+          #(name, substitute_expression(c, expr))
+        }),
+        ordered_fields: list.map(ordered_fields, fn(field) {
+          result.map(field, map_field(_, substitute_expression(c, _)))
+          |> result.map_error(substitute_type(c, _))
+        }),
+      )
+    FieldAccess(typ:, container:, module:, variant:, label:, index:) ->
+      FieldAccess(
+        typ: substitute_type(c, typ),
+        container: substitute_expression(c, container),
+        module:,
+        variant:,
+        label:,
+        index:,
+      )
+    Call(typ:, function:, ordered_arguments:) ->
+      Call(
+        typ: substitute_type(c, typ),
+        function: substitute_expression(c, function),
+        ordered_arguments: list.map(ordered_arguments, substitute_expression(
+          c,
+          _,
+        )),
+      )
+    TupleIndex(typ:, tuple:, index:) ->
+      TupleIndex(
+        typ: substitute_type(c, typ),
+        tuple: substitute_expression(c, tuple),
+        index:,
+      )
+    FnCapture(typ:, label:, function:, arguments_before:, arguments_after:) ->
+      FnCapture(
+        typ: substitute_type(c, typ),
+        label:,
+        function: substitute_expression(c, function),
+        arguments_before: list.map(
+          arguments_before,
+          map_field(_, substitute_expression(c, _)),
+        ),
+        arguments_after: list.map(
+          arguments_after,
+          map_field(_, substitute_expression(c, _)),
+        ),
+      )
+    BitString(typ:, segments:) ->
+      BitString(
+        typ: substitute_type(c, typ),
+        segments: list.map(segments, fn(segment) {
+          let #(expr, options) = segment
+          #(
+            substitute_expression(c, expr),
+            list.map(
+              options,
+              map_bit_string_segment_option(_, substitute_expression(c, _)),
+            ),
+          )
+        }),
+      )
+    Case(typ:, subjects:, clauses:) ->
+      Case(
+        typ: substitute_type(c, typ),
+        subjects: list.map(subjects, substitute_expression(c, _)),
+        clauses: list.map(clauses, substitute_clause(c, _)),
+      )
+    BinaryOperator(typ:, name:, left:, right:) ->
+      BinaryOperator(
+        typ: substitute_type(c, typ),
+        name:,
+        left: substitute_expression(c, left),
+        right: substitute_expression(c, right),
+      )
+  }
+}
+
+fn substitute_clause(c: Context, clause: Clause) -> Clause {
+  Clause(
+    patterns: list.map(clause.patterns, fn(alternative) {
+      list.map(alternative, substitute_pattern(c, _))
+    }),
+    guard: option.map(clause.guard, substitute_expression(c, _)),
+    body: substitute_expression(c, clause.body),
+  )
+}
+
+fn substitute_pattern(c: Context, pattern: Pattern) -> Pattern {
+  case pattern {
+    PatternInt(..) -> pattern
+    PatternFloat(..) -> pattern
+    PatternString(..) -> pattern
+    PatternDiscard(typ:, name:) ->
+      PatternDiscard(typ: substitute_type(c, typ), name:)
+    PatternVariable(typ:, name:) ->
+      PatternVariable(typ: substitute_type(c, typ), name:)
+    PatternTuple(typ:, elems:) ->
+      PatternTuple(
+        typ: substitute_type(c, typ),
+        elems: list.map(elems, substitute_pattern(c, _)),
+      )
+    PatternList(typ:, elements:, tail:) ->
+      PatternList(
+        typ: substitute_type(c, typ),
+        elements: list.map(elements, substitute_pattern(c, _)),
+        tail: option.map(tail, substitute_pattern(c, _)),
+      )
+    PatternAssignment(typ:, pattern:, name:) ->
+      PatternAssignment(
+        typ: substitute_type(c, typ),
+        pattern: substitute_pattern(c, pattern),
+        name:,
+      )
+    PatternConcatenate(typ:, prefix:, prefix_name:, suffix_name:) ->
+      PatternConcatenate(
+        typ: substitute_type(c, typ),
+        prefix:,
+        prefix_name:,
+        suffix_name:,
+      )
+    PatternBitString(typ:, segments:) ->
+      PatternBitString(
+        typ: substitute_type(c, typ),
+        segments: list.map(segments, fn(segment) {
+          let #(pattern, options) = segment
+          #(
+            substitute_pattern(c, pattern),
+            list.map(
+              options,
+              map_bit_string_segment_option(_, substitute_pattern(c, _)),
+            ),
+          )
+        }),
+      )
+    PatternConstructor(
+      typ:,
+      module:,
+      constructor:,
+      arguments:,
+      ordered_arguments:,
+      with_module:,
+      with_spread:,
+    ) ->
+      PatternConstructor(
+        typ: substitute_type(c, typ),
+        module:,
+        constructor:,
+        arguments: list.map(arguments, map_field(_, substitute_pattern(c, _))),
+        ordered_arguments: list.map(
+          ordered_arguments,
+          map_field(_, substitute_pattern(c, _)),
+        ),
+        with_module:,
+        with_spread:,
+      )
+  }
+}
+
+fn substitute_poly(c: Context, poly: Poly) {
+  Poly(poly.vars, substitute_type(c, poly.typ))
+}
+
+fn substitute_type(c: Context, typ: Type) {
   case typ {
-    VariableType(x) -> {
-      case get_type_var(c, x) {
-        Bound(x) -> resolve_type_deep(c, x)
-        Unbound(..) -> typ
+    NamedType(module:, name:, parameters:) -> {
+      let parameters = list.map(parameters, substitute_type(c, _))
+      NamedType(module:, name:, parameters:)
+    }
+    FunctionType(parameters, return) -> {
+      let parameters = list.map(parameters, substitute_type(c, _))
+      let return = substitute_type(c, return)
+      FunctionType(parameters:, return:)
+    }
+    TupleType(elements) -> {
+      let elements = list.map(elements, substitute_type(c, _))
+      TupleType(elements:)
+    }
+    VariableType(ref) -> {
+      case get_type_var(c, ref) {
+        Bound(x) -> substitute_type(c, x)
+        Unbound -> VariableType(ref)
       }
     }
-    NamedType(name, mod, args) ->
-      NamedType(name, mod, list.map(args, resolve_type_deep(c, _)))
-    FunctionType(args, ret) ->
-      FunctionType(
-        list.map(args, resolve_type_deep(c, _)),
-        resolve_type_deep(c, ret),
+  }
+}
+
+fn substitute_annotation(c: Context, anno: Annotation) -> Annotation {
+  case anno {
+    NamedAnno(typ:, module:, name:, parameters:) ->
+      NamedAnno(
+        typ: substitute_type(c, typ),
+        module:,
+        name:,
+        parameters: list.map(parameters, substitute_annotation(c, _)),
       )
-    TupleType(elements) ->
-      TupleType(list.map(elements, resolve_type_deep(c, _)))
+    TupleAnno(typ:, elements:) ->
+      TupleAnno(
+        typ: substitute_type(c, typ),
+        elements: list.map(elements, substitute_annotation(c, _)),
+      )
+    FunctionAnno(typ:, parameters:, return:) ->
+      FunctionAnno(
+        typ: substitute_type(c, typ),
+        parameters: list.map(parameters, substitute_annotation(c, _)),
+        return: substitute_annotation(c, return),
+      )
+    VariableAnno(typ:, name:) ->
+      VariableAnno(typ: substitute_type(c, typ), name:)
+    HoleAnno(typ:, name:) -> HoleAnno(substitute_type(c, typ), name:)
   }
 }
 
+fn map_field(field: Field(a), func: fn(a) -> b) -> Field(b) {
+  Field(..field, item: func(field.item))
+}
+
+fn map_definition(def: Definition(a), func: fn(a) -> b) -> Definition(b) {
+  Definition(..def, definition: func(def.definition))
+}
+
 fn location(c: Context) {
-  Location(c.current_module, c.current_definition, c.current_span)
+  Location(c.module.name, c.current_definition, c.current_span)
+}
+
+fn map_bit_string_segment_option(
+  option: BitStringSegmentOption(a),
+  func: fn(a) -> a,
+) -> BitStringSegmentOption(a) {
+  case option {
+    SizeValueOption(expr) -> SizeValueOption(func(expr))
+    _ -> option
+  }
 }