diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml
index 941104001..138671f6e 100644
--- a/src/passes/4-typer/solver.ml
+++ b/src/passes/4-typer/solver.ml
@@ -4,6 +4,7 @@ module Core = Typesystem.Core
 
 module Wrap = struct
   module I = Ast_simplified
+  module T = Ast_typed
   module O = Core
 
   type constraints = O.type_constraint list
@@ -16,8 +17,8 @@ module Wrap = struct
   (*   let%bind state' = add_type state t in *)
   (*   return expr state' in *)
 
-  let rec type_expression_to_type_value : I.type_expression -> O.type_value = fun te ->
-    match te with
+  let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te ->
+    match te.type_value' with
     | T_tuple types ->
       P_constant (C_tuple, List.map type_expression_to_type_value types)
     | T_sum kvmap ->
@@ -42,16 +43,43 @@ module Wrap = struct
       in
       P_constant (csttag, List.map type_expression_to_type_value args)
 
+
+  let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
+    match te with
+    | T_tuple types ->
+      P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
+    | T_sum kvmap ->
+      P_constant (C_variant, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap)
+    | T_record kvmap ->
+      P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap)
+    | T_function (arg , ret) ->
+      P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ arg ; ret ])
+    | T_variable type_name -> P_variable type_name
+    | T_constant (type_name , args) ->
+      let csttag = Core.(match type_name with
+          | "arrow"  -> C_arrow
+          | "option" -> C_option
+          | "tuple"  -> C_tuple
+          | "map"    -> C_map
+          | "list"   -> C_list
+          | "set"    -> C_set
+          | "unit"   -> C_unit
+          | "bool"   -> C_bool
+          | "string" -> C_string
+          | _        -> failwith "unknown type constructor")
+      in
+      P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
+
   (** TODO *)
   let type_declaration : I.declaration -> constraints = fun td ->
     match td with
     | Declaration_type (name , te) ->
-      let pattern = type_expression_to_type_value te in
+      let pattern = type_expression_to_type_value_copypasted te in
       [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
     | Declaration_constant (name, te, _) ->(
         match te with 
         | Some (exp) ->
-          let pattern = type_expression_to_type_value exp in
+          let pattern = type_expression_to_type_value_copypasted exp in
           [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
         | None -> 
           (** TODO *)
@@ -62,12 +90,12 @@ module Wrap = struct
     let type_name = Core.fresh_type_variable () in
     [] , type_name
 
-  let variable : I.name -> I.type_expression -> (constraints * O.type_variable) = fun _name expr ->
+  let variable : I.name -> T.type_value -> (constraints * O.type_variable) = fun _name expr ->
     let pattern = type_expression_to_type_value expr in
     let type_name = Core.fresh_type_variable () in
     [C_equation (P_variable (type_name) , pattern)] , type_name
 
-  let literal : I.type_expression -> (constraints * O.type_variable) = fun t ->
+  let literal : T.type_value -> (constraints * O.type_variable) = fun t ->
     let pattern = type_expression_to_type_value t in
     let type_name = Core.fresh_type_variable () in
     [C_equation (P_variable (type_name) , pattern)] , type_name
@@ -85,7 +113,7 @@ module Wrap = struct
    *)
 
   let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys ->
-    let patterns = List.map type_expression_to_type_value tys in
+    let patterns = List.map type_expression_to_type_value_copypasted tys in
     let pattern = O.(P_constant (C_tuple , patterns)) in
     let type_name = Core.fresh_type_variable () in
     [C_equation (P_variable (type_name) , pattern)] , type_name
@@ -129,8 +157,8 @@ module Wrap = struct
     fun ~base ~key ->
       let key_type = Core.fresh_type_variable () in
       let element_type = Core.fresh_type_variable () in
-      let base' = type_expression_to_type_value base in
-      let key' = type_expression_to_type_value key in
+      let base' = type_expression_to_type_value_copypasted base in
+      let key' = type_expression_to_type_value_copypasted key in
       let base_expected = mk_map_type key_type element_type in
       let expr_type = Core.fresh_type_variable () in
       O.[C_equation (base' , base_expected);
@@ -140,9 +168,9 @@ module Wrap = struct
   let constructor
     : I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable)
     = fun t_arg c_arg sum ->
-      let t_arg = type_expression_to_type_value t_arg in
-      let c_arg = type_expression_to_type_value c_arg in
-      let sum = type_expression_to_type_value sum in
+      let t_arg = type_expression_to_type_value_copypasted t_arg in
+      let c_arg = type_expression_to_type_value_copypasted c_arg in
+      let sum = type_expression_to_type_value_copypasted sum in
       let whole_expr = Core.fresh_type_variable () in
       [
         C_equation (P_variable (whole_expr) , sum) ;
@@ -150,7 +178,7 @@ module Wrap = struct
       ] , whole_expr
 
   let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields ->
-    let record_type = type_expression_to_type_value (I.t_record fields) in
+    let record_type = type_expression_to_type_value_copypasted (I.t_record fields) in
     let whole_expr = Core.fresh_type_variable () in
     [C_equation (P_variable whole_expr , record_type)] , whole_expr
 
@@ -158,7 +186,7 @@ module Wrap = struct
     fun ctor element_tys ->
       let elttype = O.P_variable (Core.fresh_type_variable ()) in
       let aux elt =
-        let elt' = type_expression_to_type_value elt
+        let elt' = type_expression_to_type_value_copypasted elt
         in O.C_equation (elttype , elt') in
       let equations = List.map aux element_tys in
       let whole_expr = Core.fresh_type_variable () in
@@ -174,10 +202,10 @@ module Wrap = struct
       let k_type = O.P_variable (Core.fresh_type_variable ()) in
       let v_type = O.P_variable (Core.fresh_type_variable ()) in
       let aux_k (k , _v) =
-        let k' = type_expression_to_type_value k in
+        let k' = type_expression_to_type_value_copypasted k in
         O.C_equation (k_type , k') in
       let aux_v (_k , v) =
-        let v' = type_expression_to_type_value v in
+        let v' = type_expression_to_type_value_copypasted v in
         O.C_equation (v_type , v') in
       let equations_k = List.map aux_k kv_tys in
       let equations_v = List.map aux_v kv_tys in
@@ -189,16 +217,16 @@ module Wrap = struct
   let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun f arg ->
       let whole_expr = Core.fresh_type_variable () in
-      let f'   = type_expression_to_type_value f in
-      let arg' = type_expression_to_type_value arg in
+      let f'   = type_expression_to_type_value_copypasted f in
+      let arg' = type_expression_to_type_value_copypasted arg in
       O.[
         C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
       ] , whole_expr
 
   let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun ds ind ->
-      let ds'  = type_expression_to_type_value ds in
-      let ind' = type_expression_to_type_value ind in
+      let ds'  = type_expression_to_type_value_copypasted ds in
+      let ind' = type_expression_to_type_value_copypasted ind in
       let whole_expr = Core.fresh_type_variable () in
       let v = Core.fresh_type_variable () in
       O.[
@@ -208,8 +236,8 @@ module Wrap = struct
 
   let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun a b ->
-      let a' = type_expression_to_type_value a in
-      let b' = type_expression_to_type_value b in
+      let a' = type_expression_to_type_value_copypasted a in
+      let b' = type_expression_to_type_value_copypasted b in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (a' , P_constant (C_unit , [])) ;
@@ -218,8 +246,8 @@ module Wrap = struct
 
   let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun expr body ->
-      let expr' = type_expression_to_type_value expr in
-      let body' = type_expression_to_type_value body in
+      let expr' = type_expression_to_type_value_copypasted expr in
+      let body' = type_expression_to_type_value_copypasted body in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (expr'                 , P_constant (C_bool , [])) ;
@@ -229,11 +257,11 @@ module Wrap = struct
 
   let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) =
     fun rhs rhs_tv_opt result ->
-      let rhs'        = type_expression_to_type_value rhs in
-      let result'     = type_expression_to_type_value result in
+      let rhs'        = type_expression_to_type_value_copypasted rhs in
+      let result'     = type_expression_to_type_value_copypasted result in
       let rhs_tv_opt' = match rhs_tv_opt with
           None -> []
-        | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
+        | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value_copypasted annot)] in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (result' , P_variable whole_expr)
@@ -241,8 +269,8 @@ module Wrap = struct
 
   let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun v e ->
-      let v' = type_expression_to_type_value v in
-      let e' = type_expression_to_type_value e in
+      let v' = type_expression_to_type_value_copypasted v in
+      let e' = type_expression_to_type_value_copypasted e in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (v' , e') ;
@@ -251,8 +279,8 @@ module Wrap = struct
 
   let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
     fun e annot ->
-      let e' = type_expression_to_type_value e in
-      let annot' = type_expression_to_type_value annot in
+      let e' = type_expression_to_type_value_copypasted e in
+      let annot' = type_expression_to_type_value_copypasted annot in
       let whole_expr = Core.fresh_type_variable () in
       O.[
         C_equation (e' , annot') ;
@@ -262,7 +290,7 @@ module Wrap = struct
   let matching : I.type_expression list -> (constraints * O.type_variable) =
     fun es ->
       let whole_expr = Core.fresh_type_variable () in
-      let type_values = (List.map type_expression_to_type_value es) in
+      let type_values = (List.map type_expression_to_type_value_copypasted es) in
       let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values
       in cs, whole_expr
 
@@ -280,12 +308,12 @@ module Wrap = struct
       let unification_body = Core.fresh_type_variable () in
       let arg'  = match arg with
           None -> []
-        | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in
+        | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value_copypasted arg)] in
       let body'  = match body with
           None -> []
-        | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
+        | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value_copypasted body)]
       in O.[
-          C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
+          C_equation (type_expression_to_type_value_copypasted fresh , P_variable unification_arg) ;
           C_equation (P_variable whole_expr ,
                       P_constant (C_arrow , [P_variable unification_arg ;
                                              P_variable unification_body]))
diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index d32263ba8..70ad57305 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -420,17 +420,17 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
      to actually perform the recursive calls *)
 
   (* Basic *)
-  | E_failwith expr -> (
-      let%bind (expr', state') = type_expression e state expr in
-      let (constraints , expr_type) = Wrap.failwith_ () in
-      let expr'' = e_failwith expr' in
-      return expr''  state' constraints expr_type
-    )
+  (* | E_failwith expr -> (
+   *     let%bind (expr', state') = type_expression e state expr in
+   *     let (constraints , expr_type) = Wrap.failwith_ () in
+   *     let expr'' = e_failwith expr' in
+   *     return expr''  state' constraints expr_type
+   *   ) *)
   | E_variable name -> (
-      let%bind tv' =
+      let%bind (tv' : Environment.element) =
         trace_option (unbound_variable e name ae.location)
         @@ Environment.get_opt name e in
-      let (constraints , expr_type) = Wrap.variable name tv'.type_expression in
+      let (constraints , expr_type) = Wrap.variable name tv'.type_value in
       let expr' = e_variable name in
       return expr' state constraints expr_type
     )
@@ -449,8 +449,8 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
   | E_literal (Literal_nat n) -> (
       return_wrapped (e_nat n) state @@ Wrap.literal (t_nat ())
     )
-  | E_literal (Literal_tez t) -> (
-      return_wrapped (e_tez t) state @@ Wrap.literal (t_tez ())
+  | E_literal (Literal_mutez t) -> (
+      return_wrapped (e_mutez t) state @@ Wrap.literal (t_mutez ())
     )
   | E_literal (Literal_address a) -> (
       return_wrapped (e_address a) state @@ Wrap.literal (t_address ())
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index db7fe394a..a3eca7837 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -28,6 +28,11 @@ them. please report this to the developers." in
     let content () = name in
     error title content
 
+  let no_type_variable name =
+    let title () = "type variables can't be transpiled" in
+    let content () = name in
+    error title content
+
   let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l)
 
   let unsupported_pattern_matching kind location =
@@ -102,6 +107,7 @@ open Errors
 
 let rec transpile_type (t:AST.type_value) : type_value result =
   match t.type_value' with
+  | T_variable name -> fail @@ no_type_variable name
   | T_constant ("bool", []) -> ok (T_base Base_bool)
   | T_constant ("int", []) -> ok (T_base Base_int)
   | T_constant ("nat", []) -> ok (T_base Base_nat)
diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml
index 78c41cca8..fb5a7c97b 100644
--- a/src/passes/6-transpiler/untranspiler.ml
+++ b/src/passes/6-transpiler/untranspiler.ml
@@ -203,3 +203,4 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
       let m' = map_of_kv_list lst in
       return (E_record m')
   | T_function _ -> fail @@ bad_untranspile "function" v
+  | T_variable v -> return (E_variable v)
diff --git a/src/passes/operators/helpers.ml b/src/passes/operators/helpers.ml
index b588605f2..46ffc302b 100644
--- a/src/passes/operators/helpers.ml
+++ b/src/passes/operators/helpers.ml
@@ -113,7 +113,7 @@ module Typer = struct
       List.exists (eq_2 (a , b)) [
         t_int () ;
         t_nat () ;
-        t_tez () ;
+        t_mutez () ;
         t_string () ;
         t_bytes () ;
         t_address () ;
diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml
index 5eb1dfb91..27584f065 100644
--- a/src/passes/operators/operators.ml
+++ b/src/passes/operators/operators.ml
@@ -297,8 +297,8 @@ module Typer = struct
     then ok @@ t_int () else
     if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ()))
     then ok @@ t_timestamp () else
-    if (eq_2 (a , b) (t_tez ()))
-    then ok @@ t_tez () else
+    if (eq_2 (a , b) (t_mutez ()))
+    then ok @@ t_mutez () else
       fail (simple_error "Typing substraction, bad parameters.")
 
   let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
@@ -428,16 +428,16 @@ module Typer = struct
 
   let unit = constant "UNIT" @@ t_unit ()
 
-  let amount = constant "AMOUNT" @@ t_tez ()
+  let amount = constant "AMOUNT" @@ t_mutez ()
 
-  let balance = constant "BALANCE" @@ t_tez ()
+  let balance = constant "BALANCE" @@ t_mutez ()
 
   let address = constant "ADDRESS" @@ t_address ()
 
   let now = constant "NOW" @@ t_timestamp ()
 
   let transaction = typer_3 "CALL" @@ fun param amount contract ->
-    let%bind () = assert_t_tez amount in
+    let%bind () = assert_t_mutez amount in
     let%bind contract_param = get_t_contract contract in
     let%bind () = assert_type_value_eq (param , contract_param) in
     ok @@ t_operation ()
@@ -447,7 +447,7 @@ module Typer = struct
     let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in
     let%bind () = assert_eq_1 spendable (t_bool ()) in
     let%bind () = assert_eq_1 delegatable (t_bool ()) in
-    let%bind () = assert_t_tez init_balance in
+    let%bind () = assert_t_mutez init_balance in
     let%bind (arg , res) = get_t_function code in
     let%bind (_param , storage) = get_t_pair arg in
     let%bind (storage' , op_lst) = get_t_pair res in
@@ -485,8 +485,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if (eq_1 a (t_nat ()) && eq_1 b (t_tez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_tez ()))
-    then ok @@ t_tez () else
+    if (eq_1 a (t_nat ()) && eq_1 b (t_mutez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_mutez ()))
+    then ok @@ t_mutez () else
       simple_fail "Multiplying with wrong types"
 
   let div = typer_2 "DIV" @@ fun a b ->
@@ -494,8 +494,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if eq_1 a (t_tez ()) && eq_1 b (t_nat ())
-    then ok @@ t_tez () else
+    if eq_1 a (t_mutez ()) && eq_1 b (t_nat ())
+    then ok @@ t_mutez () else
       simple_fail "Dividing with wrong types"
 
   let mod_ = typer_2 "MOD" @@ fun a b ->
@@ -508,8 +508,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if eq_2 (a , b) (t_tez ())
-    then ok @@ t_tez () else
+    if eq_2 (a , b) (t_mutez ())
+    then ok @@ t_mutez () else
     if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
     then ok @@ t_int () else
     if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ()))
diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml
index fb8923ea9..d77334e87 100644
--- a/src/stages/ast_typed/PP.ml
+++ b/src/stages/ast_typed/PP.ml
@@ -14,6 +14,7 @@ let rec type_value' ppf (tv':type_value') : unit =
   | T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
   | T_constant (c, []) -> fprintf ppf "%s" c
   | T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
+  | T_variable name -> fprintf ppf "%s" name
 
 and type_value ppf (tv:type_value) : unit =
   type_value' ppf tv.type_value'
diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml
index d9dcebb73..a4909851c 100644
--- a/src/stages/ast_typed/combinators.ml
+++ b/src/stages/ast_typed/combinators.ml
@@ -21,11 +21,12 @@ let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
 let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
 let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
 let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
-let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s
+let t_mutez ?s () : type_value = make_t (T_constant ("tez", [])) s
 let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) s
 let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
 let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
 let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
+let t_variable t ?s () : type_value = make_t (T_variable t) s
 let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
 let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s
 let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
@@ -82,7 +83,7 @@ let get_t_unit (t:type_value) : unit result = match t.type_value' with
   | T_constant ("unit", []) -> ok ()
   | _ -> simple_fail "not a unit"
 
-let get_t_tez (t:type_value) : unit result = match t.type_value' with
+let get_t_mutez (t:type_value) : unit result = match t.type_value' with
   | T_constant ("tez", []) -> ok ()
   | _ -> simple_fail "not a tez"
 
@@ -179,7 +180,7 @@ let assert_t_map = fun t ->
 let is_t_map = Function.compose to_bool get_t_map
 let is_t_big_map = Function.compose to_bool get_t_big_map
 
-let assert_t_tez : type_value -> unit result = get_t_tez
+let assert_t_mutez : type_value -> unit result = get_t_mutez
 let assert_t_key = get_t_key
 let assert_t_signature = get_t_signature
 let assert_t_key_hash = get_t_key_hash
@@ -235,6 +236,8 @@ let e_nat n : expression = E_literal (Literal_nat n)
 let e_mutez n : expression = E_literal (Literal_mutez n)
 let e_bool b : expression = E_literal (Literal_bool b)
 let e_string s : expression = E_literal (Literal_string s)
+let e_bytes s : expression = E_literal (Literal_bytes s)
+let e_timestamp s : expression = E_literal (Literal_timestamp s)
 let e_address s : expression = E_literal (Literal_address s)
 let e_operation s : expression = E_literal (Literal_operation s)
 let e_lambda l : expression = E_lambda l
@@ -247,7 +250,7 @@ let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
 let e_a_unit = make_a_e e_unit (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
 let e_a_nat n = make_a_e (e_nat n) (t_nat ())
-let e_a_mutez n = make_a_e (e_mutez n) (t_tez ())
+let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ())
 let e_a_bool b = make_a_e (e_bool b) (t_bool ())
 let e_a_string s = make_a_e (e_string s) (t_string ())
 let e_a_address s = make_a_e (e_address s) (t_address ())
diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml
index 5ba66b4ea..723ba3100 100644
--- a/src/stages/ast_typed/misc.ml
+++ b/src/stages/ast_typed/misc.ml
@@ -346,6 +346,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ = assert_type_value_eq (result, result') in
       ok ()
   | T_function _, _ -> fail @@ different_kinds a b
+  | T_variable x, T_variable y -> let _ = x == y in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding"
+  | T_variable _, _ -> fail @@ different_kinds a b
 
 (* No information about what made it fail *)
 let type_value_eq ab = Trace.to_bool @@ assert_type_value_eq ab
diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml
index d0b8ee2bb..b60632a0d 100644
--- a/src/stages/ast_typed/types.ml
+++ b/src/stages/ast_typed/types.ml
@@ -56,6 +56,7 @@ and type_value' =
   | T_sum of tv_map
   | T_record of tv_map
   | T_constant of type_name * tv list
+  | T_variable of type_name
   | T_function of (tv * tv)
 
 and type_value = {