diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml
index 8aef87157..264ae8a9d 100644
--- a/src/stages/typesystem/core.ml
+++ b/src/stages/typesystem/core.ml
@@ -1,68 +1,74 @@
-  type type_variable = string
+type type_variable = (*Type_variable *) string
 
-  let fresh_type_variable : ?name:string -> unit -> type_variable =
-    let id = ref 0 in
-    let inc () = id := !id + 1 in
-    fun ?name () ->
-      inc () ;
-      match name with
-      | None -> "type_variable_" ^ (string_of_int !id)
-      | Some name -> "tv_" ^ name ^ "_" ^ (string_of_int !id)
+(* generate a new type variable and gave it an id *)
+let fresh_type_variable : ?name:string -> unit -> type_variable =
+  let id = ref 0 in
+  let inc () = id := !id + 1 in
+  fun ?name () ->
+    inc () ;
+    match name with
+    | None -> (*Type_variable*) "type_variable_" ^ (string_of_int !id)
+    | Some name -> (*Type_variable*)"tv_" ^ name ^ "_" ^ (string_of_int !id)
 
 
-  type constant_tag =
-    | C_arrow     (* * -> * -> * *)
-    | C_option    (* * -> * *)
-    | C_tuple     (* * … -> * *)
-    | C_record    (* ( label , * ) … -> * *)
-    | C_variant   (* ( label , * ) … -> * *)
-    | C_map       (* * -> * -> * *)
-    | C_big_map       (* * -> * -> * *)
-    | C_list      (* * -> * *)
-    | C_set       (* * -> * *)
-    | C_unit      (* * *)
-    | C_bool      (* * *)
-    | C_string    (* * *)
-    | C_nat       (* * *)
-    | C_tez       (* * *)
-    | C_timestamp (* * *)
-    | C_int       (* * *)
-    | C_address   (* * *)
-    | C_bytes     (* * *)
-    | C_key_hash  (* * *)
-    | C_key       (* * *)
-    | C_signature (* * *)
-    | C_operation (* * *)
-    | C_contract  (* * -> * *)
+(* add information on the type or the kind for operator*)
+type constant_tag =
+  | C_arrow     (* * -> * -> * *) (* isn't this wrong*)
+  | C_option    (* * -> * *)
+  | C_tuple     (* * … -> * *)
+  | C_record    (* ( label , * ) … -> * *)
+  | C_variant   (* ( label , * ) … -> * *)
+  | C_map       (* * -> * -> * *)
+  | C_big_map   (* * -> * -> * *)
+  | C_list      (* * -> * *)
+  | C_set       (* * -> * *)
+  | C_unit      (* * *)
+  | C_bool      (* * *)
+  | C_string    (* * *)
+  | C_nat       (* * *)
+  | C_tez       (* * *)
+  | C_timestamp (* * *)
+  | C_int       (* * *)
+  | C_address   (* * *)
+  | C_bytes     (* * *)
+  | C_key_hash  (* * *)
+  | C_key       (* * *)
+  | C_signature (* * *)
+  | C_operation (* * *)
+  | C_contract  (* * -> * *)
 
-  type label =
-    | L_int of int
-    | L_string of string
+type label =
+  | L_int of int
+  | L_string of string
 
-  type type_value =
-    | P_forall       of p_forall
-    | P_variable     of type_variable
-    | P_constant     of (constant_tag * type_value list)
-    | P_apply        of (type_value * type_value)
+(* Weird stuff; please explain *)
+type type_value =
+  | P_forall       of p_forall
+  | P_variable     of type_variable (* how a value can be a variable? *)
+  | P_constant     of (constant_tag * type_value list)
+  | P_apply        of (type_value * type_value)
 
-  and p_forall = {
-    binder      : type_variable ;
-    constraints : type_constraint list ;
-    body        : type_value
-  }
+and p_forall = {
+  binder      : type_variable ;
+  constraints : type_constraint list ;
+  body        : type_value
+}
 
-  and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *)
-  and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *)
-  and c_const = (type_variable * type_value)
-  and c_equation = (type_value * type_value)
-  and c_typeclass = (type_value list * typeclass)
-  and c_access_label = (type_value * label * type_variable)
+(* Different type of constraint *) (* why isn't this a variant ? *)
+and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *)
+and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *)
+and c_const = (type_variable * type_value)
+and c_equation = (type_value * type_value)
+and c_typeclass = (type_value list * typeclass)
+and c_access_label = (type_value * label * type_variable)
 
-  and type_constraint =
-    (* | C_assignment of (type_variable * type_pattern) *)
-    | C_equation of c_equation (* TVA = TVB *)
-    | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
-    | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *)
-    (* | … *)
+(*What i was saying just before *)
+and type_constraint =
+  (* | C_assignment of (type_variable * type_pattern) *)
+  | C_equation of c_equation (* TVA = TVB *)
+  | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
+  | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *)
+(* | … *)
 
-  and typeclass = type_value list list
+(* is the first list in case on of the type of the type class as a kind *->*->* ? *)
+and typeclass = type_value list list
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 7a1a1ab73..1290f500d 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -3,6 +3,7 @@ open Core
 let pair_map = fun f (x , y) -> (f x , f y)
 
 module Substitution = struct
+  (* Replace Types variables by the infered type *)
 
   module Pattern = struct
 
@@ -14,11 +15,11 @@ module Substitution = struct
 
     let rec rec_yes = true
     and s_environment_element_definition ~v ~expr = function
-        | T.ED_binder -> ok @@ T.ED_binder
-        | T.ED_declaration (val_, free_variables) ->
-          let%bind val_ = s_annotated_expression ~v ~expr  val_ in
-          let%bind free_variables = bind_map_list (s_type_variable ~v ~expr) free_variables in
-          ok @@ T.ED_declaration (val_, free_variables)
+      | T.ED_binder -> ok @@ T.ED_binder
+      | T.ED_declaration (val_, free_variables) ->
+        let%bind val_ = s_annotated_expression ~v ~expr  val_ in
+        let%bind free_variables = bind_map_list (s_type_variable ~v ~expr) free_variables in
+        ok @@ T.ED_declaration (val_, free_variables)
     and s_environment ~v ~expr = fun lst ->
       bind_map_list (fun (type_variable, T.{ type_value; source_environment; definition }) ->
           let _ = type_value in
@@ -47,10 +48,10 @@ module Substitution = struct
     and s_type_variable ~v ~expr : T.name w = fun tvar ->
       let _TODO = ignore (v, expr, tvar) in
       failwith "TODO: subst: unimplemented case s_type_variable"
-      (* if String.equal tvar v then
-       *   expr
-       * else
-       *   ok tvar *)
+    (* if String.equal tvar v then
+     *   expr
+     * else
+     *   ok tvar *)
 
     and s_type_value' ~v ~expr : T.type_value' w = fun _ ->
       let _TODO = (v, expr) in
@@ -114,11 +115,11 @@ module Substitution = struct
       | T.E_record          aemap ->
         let _TODO = aemap in
         failwith "TODO: subst in record"
-        (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
-         *     let key = s_type_variable ~v ~expr key in
-         *     let val_ = s_annotated_expression ~v ~expr val_ in
-         *     ok @@ (key , val_)) aemap in
-         * ok @@ T.E_record aemap *)
+      (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
+       *     let key = s_type_variable ~v ~expr key in
+       *     let val_ = s_annotated_expression ~v ~expr val_ in
+       *     ok @@ (key , val_)) aemap in
+       * ok @@ T.E_record aemap *)
       | T.E_record_accessor (val_, tvar) ->
         let%bind val_ = s_annotated_expression ~v ~expr val_ in
         let%bind tvar = s_type_variable ~v ~expr tvar in
diff --git a/src/stages/typesystem/shorthands.ml b/src/stages/typesystem/shorthands.ml
index c4d794f87..0d772415d 100644
--- a/src/stages/typesystem/shorthands.ml
+++ b/src/stages/typesystem/shorthands.ml
@@ -14,6 +14,7 @@ let forall_tc binder f =
   let (tc, ty) = f (P_variable freshvar) in
   P_forall { binder = freshvar ; constraints = tc ; body = ty }
 
+(* chained forall *)
 let forall2 a b f =
   forall a @@ fun a' ->
   forall b @@ fun b' ->