diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml
index 124ef3fb3..c2b26dc9a 100644
--- a/src/bin/expect_tests/contract_tests.ml
+++ b/src/bin/expect_tests/contract_tests.ml
@@ -1084,7 +1084,7 @@ let%expect_test _ =
 let%expect_test _ =
   run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ;
   [%expect {|
-ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n                let rhs#723 = #P in\n                let p = rhs#723.0 in\n                let s = rhs#723.1 in\n                ( LIST_EMPTY() : (type_operator: list(operation)) , store ) ,\n                NONE() : (type_operator: option(key_hash)) ,\n                300000000mutez ,\n                \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
+ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n                let rhs#727 = #P in\n                let p = rhs#727.0 in\n                let s = rhs#727.1 in\n                ( LIST_EMPTY() : (type_operator: list(operation)) , store ) ,\n                NONE() : (type_operator: option(key_hash)) ,\n                300000000mutez ,\n                \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
 
 
  If you're not sure how to fix this error, you can
@@ -1097,7 +1097,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8,
 
   run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ;
   [%expect {|
-ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n                let rhs#726 = #P in\n                let p = rhs#726.0 in\n                let s = rhs#726.1 in\n                ( LIST_EMPTY() : (type_operator: list(operation)) , a ) ,\n                NONE() : (type_operator: option(key_hash)) ,\n                300000000mutez ,\n                1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
+ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n                let rhs#730 = #P in\n                let p = rhs#730.0 in\n                let s = rhs#730.1 in\n                ( LIST_EMPTY() : (type_operator: list(operation)) , a ) ,\n                NONE() : (type_operator: option(key_hash)) ,\n                300000000mutez ,\n                1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
 
 
  If you're not sure how to fix this error, you can
diff --git a/src/bin/expect_tests/michelson_or_tests.ml b/src/bin/expect_tests/michelson_or_tests.ml
index d1e8b7c85..2bf4c6475 100644
--- a/src/bin/expect_tests/michelson_or_tests.ml
+++ b/src/bin/expect_tests/michelson_or_tests.ml
@@ -17,7 +17,7 @@ let%expect_test _ =
   run_ligo_good [ "compile-contract" ; contract "michelson_or_tree.mligo" ; "main" ] ;
   [%expect {|
     { parameter unit ;
-      storage (or int (or int nat)) ;
+      storage (or (int %three) (or %four (int %one) (nat %two))) ;
       code { PUSH int 1 ;
              LEFT nat ;
              RIGHT int ;
diff --git a/src/bin/expect_tests/michelson_pair_test.ml b/src/bin/expect_tests/michelson_pair_test.ml
new file mode 100644
index 000000000..1b77033e6
--- /dev/null
+++ b/src/bin/expect_tests/michelson_pair_test.ml
@@ -0,0 +1,46 @@
+open Cli_expect
+
+let contract basename =
+  "../../test/contracts/" ^ basename
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; contract "michelson_pair_tree.ligo" ; "main" ] ;
+  [%expect {|
+    { parameter unit ;
+      storage (pair (string %three) (pair %four (int %one) (nat %two))) ;
+      code { PUSH nat 2 ;
+             PUSH int 1 ;
+             PAIR ;
+             PUSH string "foo" ;
+             PAIR ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP } } } |}]
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; contract "michelson_pair_tree.mligo" ; "main" ] ;
+  [%expect {|
+    { parameter unit ;
+      storage (pair (int %three) (pair %four (int %one) (nat %two))) ;
+      code { PUSH nat 2 ;
+             PUSH int 1 ;
+             PAIR ;
+             PUSH int 3 ;
+             PAIR ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP } } } |}]
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; contract "michelson_pair_tree.religo" ; "main" ] ;
+  [%expect {|
+    { parameter unit ;
+      storage (pair (int %three) (pair %four (int %one) (nat %two))) ;
+      code { PUSH nat 2 ;
+             PUSH int 1 ;
+             PAIR ;
+             PUSH int 3 ;
+             PAIR ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP } } } |}]
\ No newline at end of file
diff --git a/src/bin/expect_tests/syntax_error_tests.ml b/src/bin/expect_tests/syntax_error_tests.ml
index 2f591ab00..0968c1d5b 100644
--- a/src/bin/expect_tests/syntax_error_tests.ml
+++ b/src/bin/expect_tests/syntax_error_tests.ml
@@ -4,7 +4,7 @@ let%expect_test _ =
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_syntax.ligo" ; "main" ] ;
   [%expect {|
     ligo: : Parse error in file "error_syntax.ligo", line 1, characters 16-17 at "-", after "bar":
-          15: <syntax error> {}
+          16: <syntax error> {}
 
 
      If you're not sure how to fix this error, you can
diff --git a/src/main/compile/of_typed.ml b/src/main/compile/of_typed.ml
index 43b2216fe..8bcbfd882 100644
--- a/src/main/compile/of_typed.ml
+++ b/src/main/compile/of_typed.ml
@@ -15,8 +15,8 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
   | T_arrow {type1=args} -> (
       match args.type_content with
       | T_record m when LMap.cardinal m = 2 -> (
-        let param_exp = LMap.find (Label "0") m in
-        let storage_exp = LMap.find (Label "1") m in
+        let {field_type=param_exp;_} = LMap.find (Label "0") m in
+        let {field_type=storage_exp;_} = LMap.find (Label "1") m in
           match c with
           | Check_parameter -> assert_type_expression_eq (param_exp,   param.type_expression)
           | Check_storage   -> assert_type_expression_eq (storage_exp, param.type_expression)
diff --git a/src/passes/1-parser/cameligo/AST.ml b/src/passes/1-parser/cameligo/AST.ml
index c558eb72d..df94dc783 100644
--- a/src/passes/1-parser/cameligo/AST.ml
+++ b/src/passes/1-parser/cameligo/AST.ml
@@ -166,6 +166,7 @@ and type_expr =
 | TFun    of (type_expr * arrow * type_expr) reg
 | TPar    of type_expr par reg
 | TVar    of variable
+| TStringLiteral of Lexer.lexeme reg
 
 and cartesian = (type_expr, times) nsepseq reg
 
@@ -407,6 +408,7 @@ let type_expr_to_region = function
 | TApp {region; _}
 | TFun {region; _}
 | TPar {region; _}
+| TStringLiteral {region; _}
 | TVar {region; _} -> region
 
 let list_pattern_to_region = function
diff --git a/src/passes/1-parser/cameligo/Parser.mly b/src/passes/1-parser/cameligo/Parser.mly
index 950423005..12352480d 100644
--- a/src/passes/1-parser/cameligo/Parser.mly
+++ b/src/passes/1-parser/cameligo/Parser.mly
@@ -149,6 +149,7 @@ cartesian:
 core_type:
   type_name      { TVar $1 }
 | par(type_expr) { TPar $1 }
+| "<string>"     { TStringLiteral $1 }
 | module_name "." type_name {
     let module_name = $1.value in
     let type_name   = $3.value in
diff --git a/src/passes/1-parser/cameligo/ParserLog.ml b/src/passes/1-parser/cameligo/ParserLog.ml
index 4791ff6dc..6ebe07c73 100644
--- a/src/passes/1-parser/cameligo/ParserLog.ml
+++ b/src/passes/1-parser/cameligo/ParserLog.ml
@@ -156,6 +156,7 @@ and print_type_expr state = function
 | TPar par        -> print_type_par state par
 | TVar var        -> print_var state var
 | TFun t          -> print_fun_type state t
+| TStringLiteral s -> print_string state s
 
 and print_fun_type state {value; _} =
   let domain, arrow, range = value in
@@ -1124,6 +1125,9 @@ and pp_type_expr state = function
  | TVar v ->
     pp_node  state "TVar";
     pp_ident (state#pad 1 0) v
+ | TStringLiteral s ->
+    pp_node   state "String";
+    pp_string (state#pad 1 0) s
 
 and pp_type_tuple state {value; _} =
   let components     = Utils.nsepseq_to_list value.inside in
diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml
index 0c26f87cd..fa22a7b25 100644
--- a/src/passes/1-parser/pascaligo/AST.ml
+++ b/src/passes/1-parser/pascaligo/AST.ml
@@ -185,6 +185,7 @@ and type_expr =
 | TFun    of (type_expr * arrow * type_expr) reg
 | TPar    of type_expr par reg
 | TVar    of variable
+| TStringLiteral of Lexer.lexeme reg
 
 and cartesian = (type_expr, times) nsepseq reg
 
@@ -658,6 +659,7 @@ let type_expr_to_region = function
 | TApp    {region; _}
 | TFun    {region; _}
 | TPar    {region; _}
+| TStringLiteral {region; _}
 | TVar    {region; _} -> region
 
 let rec expr_to_region = function
diff --git a/src/passes/1-parser/pascaligo/Parser.mly b/src/passes/1-parser/pascaligo/Parser.mly
index 1c31f92cd..21d9420b7 100644
--- a/src/passes/1-parser/pascaligo/Parser.mly
+++ b/src/passes/1-parser/pascaligo/Parser.mly
@@ -161,6 +161,7 @@ cartesian:
 
 core_type:
   type_name      { TVar $1 }
+| "<string>"     { TStringLiteral $1 }
 | par(type_expr) { TPar $1 }
 | type_name type_tuple {
     let region = cover $1.region $2.region
diff --git a/src/passes/1-parser/pascaligo/ParserLog.ml b/src/passes/1-parser/pascaligo/ParserLog.ml
index 0467d7a61..6347b07f7 100644
--- a/src/passes/1-parser/pascaligo/ParserLog.ml
+++ b/src/passes/1-parser/pascaligo/ParserLog.ml
@@ -153,6 +153,7 @@ and print_type_expr state = function
 | TFun    type_fun    -> print_type_fun    state type_fun
 | TPar    par_type    -> print_par_type    state par_type
 | TVar    type_var    -> print_var         state type_var
+| TStringLiteral s -> print_string state s
 
 and print_cartesian state {value; _} =
   print_nsepseq state "*" print_type_expr value
@@ -940,6 +941,9 @@ and pp_type_expr state = function
                     field_decl.value in
     let fields = Utils.nsepseq_to_list value.ne_elements in
     List.iteri (List.length fields |> apply) fields
+| TStringLiteral s ->
+  pp_node   state "String";
+  pp_string (state#pad 1 0) s
 
 and pp_cartesian state {value; _} =
   let apply len rank =
diff --git a/src/passes/1-parser/reasonligo/Parser.mly b/src/passes/1-parser/reasonligo/Parser.mly
index e8dea1820..7a1c02ada 100644
--- a/src/passes/1-parser/reasonligo/Parser.mly
+++ b/src/passes/1-parser/reasonligo/Parser.mly
@@ -206,6 +206,7 @@ type_args:
 
 core_type:
   type_name      { TVar $1 }
+| "<string>"     { TStringLiteral $1 }
 | par(fun_type)  { TPar $1 }
 | module_name "." type_name {
     let module_name = $1.value in
diff --git a/src/passes/10-transpiler/transpiler.ml b/src/passes/10-transpiler/transpiler.ml
index 7168af974..f1a764953 100644
--- a/src/passes/10-transpiler/transpiler.ml
+++ b/src/passes/10-transpiler/transpiler.ml
@@ -258,10 +258,6 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
       ok (T_big_map kv')
   | T_operator (TC_map_or_big_map _) ->
       fail @@ corner_case ~loc:"transpiler" "TC_map_or_big_map should have been resolved before transpilation"
-  | T_operator (TC_michelson_or {l;r}) ->
-      let%bind l' = transpile_type l in
-      let%bind r' = transpile_type r in
-      ok (T_or ((None,l'),(None,r')))
   | T_operator (TC_list t) ->
       let%bind t' = transpile_type t in
       ok (T_list t')
@@ -276,9 +272,7 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
       let%bind result' = transpile_type result in
       ok (T_function (param', result'))
     )
-  (* TODO hmm *)
-  | T_sum m ->
-      let is_michelson_or = Ast_typed.Helpers.is_michelson_or m in
+  | T_sum m when Ast_typed.Helpers.is_michelson_or m ->
       let node = Append_tree.of_list @@ kv_list_of_cmap m in
       let aux a b : type_value annotated result =
         let%bind a = a in
@@ -286,14 +280,35 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
         ok (None, T_or (a, b))
       in
       let%bind m' = Append_tree.fold_ne
-                      (fun (Ast_typed.Types.Constructor ann, a) ->
-                        let%bind a = transpile_type a in
-                        ok ((
-                          if is_michelson_or then 
-                            None 
-                          else 
-                            Some (String.uncapitalize_ascii ann)), 
-                          a))
+                      (fun (_, ({ctor_type ; michelson_annotation}: AST.ctor_content)) ->
+                        let%bind a = transpile_type ctor_type in
+                        ok (michelson_annotation, a) )
+                      aux node in
+      ok @@ snd m'
+  | T_sum m ->
+      let node = Append_tree.of_list @@ kv_list_of_cmap m in
+      let aux a b : type_value annotated result =
+        let%bind a = a in
+        let%bind b = b in
+        ok (None, T_or (a, b))
+      in
+      let%bind m' = Append_tree.fold_ne
+                      (fun (Ast_typed.Types.Constructor ann, ({ctor_type ; _}: AST.ctor_content)) ->
+                        let%bind a = transpile_type ctor_type in
+                        ok (Some (String.uncapitalize_ascii ann), a))
+                      aux node in
+      ok @@ snd m'
+  | T_record m when Ast_typed.Helpers.is_michelson_pair m ->
+      let node = Append_tree.of_list @@ Ast_typed.Helpers.tuple_of_record m in
+      let aux a b : type_value annotated result =
+        let%bind a = a in
+        let%bind b = b in
+        ok (None, T_pair (a, b))
+      in
+      let%bind m' = Append_tree.fold_ne
+                      (fun (_, ({field_type ; michelson_annotation} : AST.field_content)) ->
+                        let%bind a = transpile_type field_type in
+                        ok (michelson_annotation, a) )
                       aux node in
       ok @@ snd m'
   | T_record m ->
@@ -311,8 +326,8 @@ let rec transpile_type (t:AST.type_expression) : type_value result =
         ok (None, T_pair (a, b))
       in
       let%bind m' = Append_tree.fold_ne
-                      (fun (Ast_typed.Types.Label ann, a) ->
-                        let%bind a = transpile_type a in                        
+                      (fun (Ast_typed.Types.Label ann, ({field_type;_}: AST.field_content)) ->
+                        let%bind a = transpile_type field_type in
                         ok ((if is_tuple_lmap then 
                               None 
                             else 
@@ -368,7 +383,8 @@ and transpile_environment_element_type : AST.environment_element -> type_value r
 
 and tree_of_sum : AST.type_expression -> (AST.constructor' * AST.type_expression) Append_tree.t result = fun t ->
   let%bind map_tv = get_t_sum t in
-  ok @@ Append_tree.of_list @@ kv_list_of_cmap map_tv
+  let kt_list = List.map (fun (k,({ctor_type;_}:AST.ctor_content)) -> (k,ctor_type)) (kv_list_of_cmap map_tv) in
+  ok @@ Append_tree.of_list kt_list
 
 and transpile_annotated_expression (ae:AST.expression) : expression result =
   let%bind tv = transpile_type ae.type_expression in
@@ -445,7 +461,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
       let%bind ty_lmap =
         trace_strong (corner_case ~loc:__LOC__ "not a record") @@
         get_t_record (get_type_expression record) in
-      let%bind ty'_lmap = Ast_typed.Helpers.bind_map_lmap transpile_type ty_lmap in
+      let%bind ty'_lmap = Ast_typed.Helpers.bind_map_lmap_t transpile_type ty_lmap in
       let%bind path =
         trace_strong (corner_case ~loc:__LOC__ "record access") @@
         record_access_to_lr ty' ty'_lmap path in
@@ -462,7 +478,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
       let%bind ty_lmap =
         trace_strong (corner_case ~loc:__LOC__ "not a record") @@
         get_t_record (get_type_expression record) in
-      let%bind ty'_lmap = Ast_typed.Helpers.bind_map_lmap transpile_type ty_lmap in
+      let%bind ty'_lmap = Ast_typed.Helpers.bind_map_lmap_t transpile_type ty_lmap in
       let%bind path = 
         trace_strong (corner_case ~loc:__LOC__ "record access") @@
         record_access_to_lr ty' ty'_lmap path in
diff --git a/src/passes/10-transpiler/untranspiler.ml b/src/passes/10-transpiler/untranspiler.ml
index a2c2f79d9..bf59c6a81 100644
--- a/src/passes/10-transpiler/untranspiler.ml
+++ b/src/passes/10-transpiler/untranspiler.ml
@@ -185,18 +185,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
         bind_fold_right_list aux init big_map'
       )
     | TC_map_or_big_map _ -> fail @@ corner_case ~loc:"untranspiler" "TC_map_or_big_map t should not be present in mini-c"
-    | TC_michelson_or {l=l_ty; r=r_ty} -> (
-        let%bind v' = bind_map_or (get_left , get_right) v in
-        ( match v' with
-          | D_left l  ->
-            let%bind l' = untranspile l l_ty in
-            return @@ E_constructor { constructor = Constructor "M_left" ; element = l' }
-          | D_right r ->
-            let%bind r' = untranspile r r_ty in
-            return @@ E_constructor { constructor = Constructor "M_right" ; element = r' }
-          | _ -> fail (wrong_mini_c_value "michelson_or" v)
-        )
-      )
     | TC_list ty -> (
         let%bind lst =
           trace_strong (wrong_mini_c_value "list" v) @@
@@ -232,7 +220,7 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
       fail @@ bad_untranspile "contract" v
   )
   | T_sum m ->
-      let lst = kv_list_of_cmap m in
+      let lst = List.map (fun (k,{ctor_type;_}) -> (k,ctor_type)) @@ kv_list_of_cmap m in
       let%bind node = match Append_tree.of_list lst with
         | Empty -> fail @@ corner_case ~loc:__LOC__ "empty sum type"
         | Full t -> ok t
@@ -243,7 +231,7 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
       let%bind sub = untranspile v tv in
       return (E_constructor {constructor=Constructor name;element=sub})
   | T_record m ->
-      let lst = Ast_typed.Helpers.kv_list_of_record_or_tuple m in
+      let lst = List.map (fun (k,{field_type;_}) -> (k,field_type)) @@ Ast_typed.Helpers.kv_list_of_record_or_tuple m in
       let%bind node = match Append_tree.of_list lst with
         | Empty -> fail @@ corner_case ~loc:__LOC__ "empty record"
         | Full t -> ok t in
diff --git a/src/passes/2-concrete_to_imperative/cameligo.ml b/src/passes/2-concrete_to_imperative/cameligo.ml
index 933909e65..1bf3b3ffe 100644
--- a/src/passes/2-concrete_to_imperative/cameligo.ml
+++ b/src/passes/2-concrete_to_imperative/cameligo.ml
@@ -160,6 +160,10 @@ open Operators.Concrete_to_imperative.Cameligo
 
 let r_split = Location.r_split
 
+let get_t_string_singleton_opt = function
+  | Raw.TStringLiteral s -> Some (String.(sub s.value 1 ((length s.value)-2)))
+  | _ -> None
+
 let rec pattern_to_var : Raw.pattern -> _ = fun p ->
   match p with
   | Raw.PPar p -> pattern_to_var p.value.inside
@@ -236,12 +240,44 @@ and compile_type_expression : Raw.type_expr -> type_expression result = fun te -
   | TApp x -> (
       let (x,loc) = r_split x in
       let (name, tuple) = x in
-      let lst = npseq_to_list tuple.value.inside in
-      let%bind lst' = bind_map_list compile_type_expression lst in
-      let%bind cst =
-        trace (unknown_predefined_type name) @@
-        type_operators name.value in
-      t_operator ~loc cst lst'
+      ( match name.value with
+        | "michelson_or" -> 
+          let lst = npseq_to_list tuple.value.inside in
+          (match lst with
+          | [a ; b ; c ; d ] -> (
+            let%bind b' =
+              trace_option (simple_error "second argument of michelson_or must be a string singleton") @@
+                get_t_string_singleton_opt b in
+            let%bind d' =
+              trace_option (simple_error "fourth argument of michelson_or must be a string singleton") @@
+                get_t_string_singleton_opt d in
+            let%bind a' = compile_type_expression a in
+            let%bind c' = compile_type_expression c in
+            ok @@ t_michelson_or ~loc a' b' c' d'
+            )
+          | _ -> simple_fail "michelson_or does not have the right number of argument")
+        | "michelson_pair" ->
+          let lst = npseq_to_list tuple.value.inside in
+          (match lst with
+          | [a ; b ; c ; d ] -> (
+            let%bind b' =
+              trace_option (simple_error "second argument of michelson_pair must be a string singleton") @@
+                get_t_string_singleton_opt b in
+            let%bind d' =
+              trace_option (simple_error "fourth argument of michelson_pair must be a string singleton") @@
+                get_t_string_singleton_opt d in
+            let%bind a' = compile_type_expression a in
+            let%bind c' = compile_type_expression c in
+            ok @@ t_michelson_pair ~loc a' b' c' d'
+            )
+          | _ -> simple_fail "michelson_pair does not have the right number of argument")
+        | _ ->
+          let lst = npseq_to_list tuple.value.inside in
+          let%bind lst' = bind_map_list compile_type_expression lst in
+          let%bind cst =
+          trace (unknown_predefined_type name) @@
+          type_operators name.value in
+          t_operator ~loc cst lst' )
     )
   | TProd p -> (
       let%bind tpl = compile_list_type_expression  @@ npseq_to_list p.value in
@@ -274,6 +310,7 @@ and compile_type_expression : Raw.type_expr -> type_expression result = fun te -
         @@ npseq_to_list s in
       let m = List.fold_left (fun m (x, y) -> CMap.add (Constructor x) y m) CMap.empty lst in
       ok @@ make_t ~loc @@ T_sum m
+  | TStringLiteral _s -> simple_fail "we don't support singleton string type"
 
 and compile_list_type_expression (lst:Raw.type_expr list) : type_expression result =
   match lst with
diff --git a/src/passes/2-concrete_to_imperative/pascaligo.ml b/src/passes/2-concrete_to_imperative/pascaligo.ml
index e7a99ec7d..be855993f 100644
--- a/src/passes/2-concrete_to_imperative/pascaligo.ml
+++ b/src/passes/2-concrete_to_imperative/pascaligo.ml
@@ -142,6 +142,10 @@ let return_statement expr = ok @@ fun expr'_opt ->
   | None -> ok @@ expr
   | Some expr' -> ok @@ e_sequence expr expr'
 
+let get_t_string_singleton_opt = function
+  | Raw.TStringLiteral s -> Some (String.(sub s.value 1 ((length s.value)-2)))
+  | _ -> None
+
 
 let rec compile_type_expression (t:Raw.type_expr) : type_expression result =
   match t with
@@ -162,13 +166,45 @@ let rec compile_type_expression (t:Raw.type_expr) : type_expression result =
   | TApp x ->
       let (x, loc) = r_split x in
       let (name, tuple) = x in
-      let lst = npseq_to_list tuple.value.inside in
-      let%bind lst =
-        bind_list @@ List.map compile_type_expression lst in (** TODO: fix constant and operator*)
-      let%bind cst =
-        trace (unknown_predefined_type name) @@
-        type_operators name.value in
-      t_operator ~loc cst lst
+      (match name.value with
+        | "michelson_or" -> 
+          let lst = npseq_to_list tuple.value.inside in
+          (match lst with
+          | [a ; b ; c ; d ] -> (
+            let%bind b' =
+              trace_option (simple_error "second argument of michelson_or must be a string singleton") @@
+                get_t_string_singleton_opt b in
+            let%bind d' =
+              trace_option (simple_error "fourth argument of michelson_or must be a string singleton") @@
+                get_t_string_singleton_opt d in
+            let%bind a' = compile_type_expression a in
+            let%bind c' = compile_type_expression c in
+            ok @@ t_michelson_or ~loc a' b' c' d'
+            )
+          | _ -> simple_fail "michelson_or does not have the right number of argument")
+        | "michelson_pair" ->
+          let lst = npseq_to_list tuple.value.inside in
+          (match lst with
+          | [a ; b ; c ; d ] -> (
+            let%bind b' =
+              trace_option (simple_error "second argument of michelson_pair must be a string singleton") @@
+                get_t_string_singleton_opt b in
+            let%bind d' =
+              trace_option (simple_error "fourth argument of michelson_pair must be a string singleton") @@
+                get_t_string_singleton_opt d in
+            let%bind a' = compile_type_expression a in
+            let%bind c' = compile_type_expression c in
+            ok @@ t_michelson_pair ~loc a' b' c' d'
+            )
+          | _ -> simple_fail "michelson_pair does not have the right number of argument")
+        | _ ->
+          let lst = npseq_to_list tuple.value.inside in
+          let%bind lst =
+            bind_list @@ List.map compile_type_expression lst in (** TODO: fix constant and operator*)
+          let%bind cst =
+            trace (unknown_predefined_type name) @@
+            type_operators name.value in
+          t_operator ~loc cst lst)
   | TProd p ->
       let%bind tpl = compile_list_type_expression
     @@ npseq_to_list p.value in
@@ -203,6 +239,7 @@ let rec compile_type_expression (t:Raw.type_expr) : type_expression result =
         @@ npseq_to_list s in
       let m = List.fold_left (fun m (x, y) -> CMap.add (Constructor x) y m) CMap.empty lst in
       ok @@ make_t ~loc @@ T_sum m
+  | TStringLiteral _s -> simple_fail "we don't support singleton string type"
 
 and compile_list_type_expression (lst:Raw.type_expr list) : type_expression result =
   match lst with
diff --git a/src/passes/3-self_ast_imperative/michelson_or.ml b/src/passes/3-self_ast_imperative/michelson_or.ml
deleted file mode 100644
index b8adb0fe8..000000000
--- a/src/passes/3-self_ast_imperative/michelson_or.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-open Ast_imperative
-open Trace
-
-let peephole_type_expression : type_expression -> type_expression result = fun e ->
-  let return type_content = ok { type_content; location=e.location } in
-  match e.type_content with
-  | T_operator (TC_michelson_or (l_ty,r_ty)) ->
-    return @@ T_sum (CMap.of_list [ (Constructor "M_left", l_ty) ; (Constructor "M_right", r_ty) ])
-  | e -> return e
diff --git a/src/passes/3-self_ast_imperative/self_ast_imperative.ml b/src/passes/3-self_ast_imperative/self_ast_imperative.ml
index 5b02d6a49..b0270ebd0 100644
--- a/src/passes/3-self_ast_imperative/self_ast_imperative.ml
+++ b/src/passes/3-self_ast_imperative/self_ast_imperative.ml
@@ -7,7 +7,6 @@ let all_expression_mapper = [
 ]
 let all_type_expression_mapper = [
   Entrypoints_length_limit.peephole_type_expression ;
-  Michelson_or.peephole_type_expression ;
 ]
 
 let all_exp = List.map (fun el -> Helpers.Expression el) all_expression_mapper
diff --git a/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml b/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml
index 527c6ee5b..75f8906fb 100644
--- a/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml
+++ b/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml
@@ -3,6 +3,15 @@ module O = Ast_sugar
 open Trace
 
 module Errors = struct
+  let corner_case loc =
+    let title () = "corner case" in
+    let message () = Format.asprintf "corner case, please report to developers\n" in
+    let data = [
+      ("location",
+      fun () -> Format.asprintf  "%s" loc)
+    ] in
+    error ~data title message
+
   let bad_collection expr =
     let title () = "" in
     let message () = Format.asprintf "\nCannot loop over this collection : %a\n" I.PP.expression expr in
@@ -110,7 +119,8 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
       let%bind sum = 
         bind_map_list (fun (k,v) ->
           let%bind v = compile_type_expression v in
-          ok @@ (k,v)
+          let content : O.ctor_content = {ctor_type = v ; michelson_annotation = None} in
+          ok @@ (k,content)
         ) sum
       in
       return @@ O.T_sum (O.CMap.of_list sum)
@@ -119,7 +129,8 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
       let%bind record = 
         bind_map_list (fun (k,v) ->
           let%bind v = compile_type_expression v in
-          ok @@ (k,v)
+          let content : O.field_content = {field_type = v ; michelson_annotation = None} in
+          ok @@ (k,content)
         ) record
       in
       return @@ O.T_record (O.LMap.of_list record)
@@ -132,6 +143,20 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
       return @@ T_arrow {type1;type2}
     | I.T_variable type_variable -> return @@ T_variable type_variable 
     | I.T_constant type_constant -> return @@ T_constant type_constant
+    | I.T_operator (TC_michelson_or (l,l_ann,r,r_ann)) ->
+      let%bind (l,r) = bind_map_pair compile_type_expression (l,r) in
+      let sum : (O.constructor' * O.ctor_content) list = [
+        (O.Constructor "M_left" , {ctor_type = l ; michelson_annotation = Some l_ann}); 
+        (O.Constructor "M_right", {ctor_type = r ; michelson_annotation = Some r_ann}); ]
+      in
+      return @@ O.T_sum (O.CMap.of_list sum)
+    | I.T_operator (TC_michelson_pair (l,l_ann,r,r_ann)) ->
+      let%bind (l,r) = bind_map_pair compile_type_expression (l,r) in
+      let sum : (O.label * O.field_content) list = [
+        (O.Label "0" , {field_type = l ; michelson_annotation = Some l_ann}); 
+        (O.Label "1", {field_type = r ; michelson_annotation = Some r_ann}); ]
+      in
+      return @@ O.T_record (O.LMap.of_list sum)
     | I.T_operator type_operator ->
       let%bind type_operator = compile_type_operator type_operator in
       return @@ T_operator type_operator
@@ -157,12 +182,10 @@ and compile_type_operator : I.type_operator -> O.type_operator result =
     | TC_big_map (k,v) ->
       let%bind (k,v) = bind_map_pair compile_type_expression (k,v) in
       ok @@ O.TC_big_map (k,v)
-    | TC_michelson_or (l,r) ->
-      let%bind (l,r) = bind_map_pair compile_type_expression (l,r) in
-      ok @@ O.TC_michelson_or (l,r)
     | TC_arrow (i,o) ->
       let%bind (i,o) = bind_map_pair compile_type_expression (i,o) in
       ok @@ O.TC_arrow (i,o)
+    | TC_michelson_or _ | TC_michelson_pair _ -> fail @@ Errors.corner_case __LOC__
 
 let rec compile_expression : I.expression -> O.expression result =
   fun e ->
@@ -558,10 +581,12 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
   let return te = ok @@ I.make_t te in
   match te.type_content with
     | O.T_sum sum -> 
+      (* This type sum could be a michelson_or as well, we could use is_michelson_or *)
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let%bind v = uncompile_type_expression v in
+          let {ctor_type;_} : O.ctor_content = v in
+          let%bind v = uncompile_type_expression ctor_type in
           ok @@ (k,v)
         ) sum
       in
@@ -570,7 +595,8 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let%bind v = uncompile_type_expression v in
+          let {field_type;_} : O.field_content = v in
+          let%bind v = uncompile_type_expression field_type in
           ok @@ (k,v)
         ) record
       in
@@ -609,9 +635,6 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result =
     | TC_big_map (k,v) ->
       let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in
       ok @@ I.TC_big_map (k,v)
-    | TC_michelson_or (l,r) ->
-      let%bind (l,r) = bind_map_pair uncompile_type_expression (l,r) in
-      ok @@ I.TC_michelson_or (l,r)
     | TC_arrow (i,o) ->
       let%bind (i,o) = bind_map_pair uncompile_type_expression (i,o) in
       ok @@ I.TC_arrow (i,o)
diff --git a/src/passes/5-self_ast_sugar/helpers.ml b/src/passes/5-self_ast_sugar/helpers.ml
index 856cb680a..0d3b353b7 100644
--- a/src/passes/5-self_ast_sugar/helpers.ml
+++ b/src/passes/5-self_ast_sugar/helpers.ml
@@ -2,6 +2,20 @@ open Ast_sugar
 open Trace
 open Stage_common.Helpers
 
+let bind_map_cmap f map = bind_cmap (
+  CMap.map 
+    (fun ({ctor_type;_} as ctor) -> 
+      let%bind ctor' = f ctor_type in
+      ok {ctor with ctor_type = ctor'}) 
+    map)
+
+let bind_map_lmap_t f map = bind_lmap (
+  LMap.map 
+    (fun ({field_type;_} as field) -> 
+      let%bind field' = f field_type in
+      ok {field with field_type = field'}) 
+    map)
+
 type 'a folder = 'a -> expression -> 'a result
 let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f init e ->
   let self = fold_expression f in 
@@ -227,7 +241,7 @@ and map_type_expression : ty_exp_mapper -> type_expression -> type_expression re
     let%bind temap' = bind_map_cmap self temap in
     return @@ (T_sum temap')
   | T_record temap ->
-    let%bind temap' = bind_map_lmap self temap in
+    let%bind temap' = bind_map_lmap_t self temap in
     return @@ (T_record temap')
   | T_tuple telst ->
     let%bind telst' = bind_map_list self telst in
diff --git a/src/passes/6-sugar_to_core/sugar_to_core.ml b/src/passes/6-sugar_to_core/sugar_to_core.ml
index e13cdfda1..ce1af8ae2 100644
--- a/src/passes/6-sugar_to_core/sugar_to_core.ml
+++ b/src/passes/6-sugar_to_core/sugar_to_core.ml
@@ -10,8 +10,10 @@ let rec idle_type_expression : I.type_expression -> O.type_expression result =
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let%bind v = idle_type_expression v in
-          ok @@ (k,v)
+          let {ctor_type ; michelson_annotation} : I.ctor_content = v in
+          let%bind ctor_type = idle_type_expression ctor_type in
+          let v' : O.ctor_content = {ctor_type ; michelson_annotation} in
+          ok @@ (k,v')
         ) sum
       in
       return @@ O.T_sum (O.CMap.of_list sum)
@@ -19,15 +21,17 @@ let rec idle_type_expression : I.type_expression -> O.type_expression result =
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let%bind v = idle_type_expression v in
-          ok @@ (k,v)
+          let {field_type ; michelson_annotation} : I.field_content = v in
+          let%bind field_type = idle_type_expression field_type in
+          let v' : O.field_content = {field_type ; field_annotation=michelson_annotation} in
+          ok @@ (k,v')
         ) record
       in
       return @@ O.T_record (O.LMap.of_list record)
     | I.T_tuple tuple ->
       let aux (i,acc) el = 
         let%bind el = idle_type_expression el in
-        ok @@ (i+1,(O.Label (string_of_int i), el)::acc) in
+        ok @@ (i+1,(O.Label (string_of_int i), ({field_type=el;field_annotation=None}:O.field_content))::acc) in
       let%bind (_, lst ) = bind_fold_list aux (0,[]) tuple in
       let record = O.LMap.of_list lst in
       return @@ O.T_record record
@@ -62,9 +66,6 @@ and idle_type_operator : I.type_operator -> O.type_operator result =
     | TC_big_map (k,v) ->
       let%bind (k,v) = bind_map_pair idle_type_expression (k,v) in
       ok @@ O.TC_big_map (k,v)
-    | TC_michelson_or (l,r) ->
-      let%bind (l,r) = bind_map_pair idle_type_expression (l,r) in
-      ok @@ O.TC_michelson_or (l,r)
     | TC_arrow (i,o) ->
       let%bind (i,o) = bind_map_pair idle_type_expression (i,o) in
       ok @@ O.TC_arrow (i,o)
@@ -244,8 +245,10 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let%bind v = uncompile_type_expression v in
-          ok @@ (k,v)
+          let {ctor_type;michelson_annotation} : O.ctor_content = v in
+          let%bind ctor_type = uncompile_type_expression ctor_type in
+          let v' : I.ctor_content = {ctor_type;michelson_annotation} in
+          ok @@ (k,v')
         ) sum
       in
       return @@ I.T_sum (O.CMap.of_list sum)
@@ -253,8 +256,10 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let%bind v = uncompile_type_expression v in
-          ok @@ (k,v)
+          let {field_type;field_annotation} : O.field_content = v in
+          let%bind field_type = uncompile_type_expression field_type in
+          let v' : I.field_content = {field_type;michelson_annotation=field_annotation} in
+          ok @@ (k,v')
         ) record
       in
       return @@ I.T_record (O.LMap.of_list record)
@@ -290,9 +295,6 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result =
       let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in
       ok @@ I.TC_big_map (k,v)
     | TC_map_or_big_map _ -> failwith "TC_map_or_big_map shouldn't be uncompiled"
-    | TC_michelson_or (l,r) ->
-      let%bind (l,r) = bind_map_pair uncompile_type_expression (l,r) in
-      ok @@ I.TC_michelson_or (l,r)
     | TC_arrow (i,o) ->
       let%bind (i,o) = bind_map_pair uncompile_type_expression (i,o) in
       ok @@ I.TC_arrow (i,o)
diff --git a/src/passes/7-self_ast_core/helpers.ml b/src/passes/7-self_ast_core/helpers.ml
new file mode 100644
index 000000000..e76e4f064
--- /dev/null
+++ b/src/passes/7-self_ast_core/helpers.ml
@@ -0,0 +1,313 @@
+open Ast_core
+open Trace
+open Stage_common.Helpers
+
+include Stage_common.PP
+include Stage_common.Types.Ast_generic_type(Ast_core_parameter)
+
+let bind_map_cmap f map = bind_cmap (
+  CMap.map 
+    (fun ({ctor_type;_} as ctor) -> 
+      let%bind ctor' = f ctor_type in
+      ok {ctor with ctor_type = ctor'}) 
+    map)
+
+let bind_map_lmap_t f map = bind_lmap (
+  LMap.map 
+    (fun ({field_type;_} as field) -> 
+      let%bind field' = f field_type in
+      ok {field with field_type = field'}) 
+    map)
+
+type 'a folder = 'a -> expression -> 'a result
+let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f init e ->
+  let self = fold_expression f in 
+  let%bind init' = f init e in
+  match e.expression_content with
+  | E_literal _ | E_variable _ -> ok init'
+  | E_constant {arguments=lst} -> (
+    let%bind res = bind_fold_list self init' lst in
+    ok res
+  )
+  | E_application {lamb;args} -> (
+      let ab = (lamb,args) in
+      let%bind res = bind_fold_pair self init' ab in
+      ok res
+    )
+  | E_lambda { binder = _ ; input_type = _ ; output_type = _ ; result = e }
+  | E_ascription {anno_expr=e; _} | E_constructor {element=e} -> (
+      let%bind res = self init' e in
+      ok res
+    )
+  | E_matching {matchee=e; cases} -> (
+      let%bind res = self init' e in
+      let%bind res = fold_cases f res cases in
+      ok res
+    )
+  | E_record m -> (
+    let aux init'' _ expr =
+      let%bind res = fold_expression self init'' expr in
+      ok res
+    in
+    let%bind res = bind_fold_lmap aux (ok init') m in
+    ok res
+  )
+  | E_record_update {record;update} -> (
+    let%bind res = self init' record in
+    let%bind res = fold_expression self res update in
+    ok res 
+  )
+  | E_record_accessor {record} -> (
+     let%bind res = self init' record in
+     ok res
+    )
+  | E_let_in { let_binder = _ ; rhs ; let_result } -> (
+      let%bind res = self init' rhs in
+      let%bind res = self res let_result in
+      ok res
+    )
+  | E_recursive { lambda={result=e;_}; _} ->
+      let%bind res = self init' e in
+      ok res
+
+and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m ->
+  match m with
+  | Match_bool { match_true ; match_false } -> (
+      let%bind res = fold_expression f init match_true in
+      let%bind res = fold_expression f res match_false in
+      ok res
+    )
+  | Match_list { match_nil ; match_cons = (_ , _ , cons, _) } -> (
+      let%bind res = fold_expression f init match_nil in
+      let%bind res = fold_expression f res cons in
+      ok res
+    )
+  | Match_option { match_none ; match_some = (_ , some, _) } -> (
+      let%bind res = fold_expression f init match_none in
+      let%bind res = fold_expression f res some in
+      ok res
+    )
+  | Match_tuple ((_ , e), _) -> (
+      let%bind res = fold_expression f init e in
+      ok res
+    )
+  | Match_variant (lst, _) -> (
+      let aux init' ((_ , _) , e) =
+        let%bind res' = fold_expression f init' e in
+        ok res' in
+      let%bind res = bind_fold_list aux init lst in
+      ok res
+    )
+
+type exp_mapper = expression -> expression result
+type ty_exp_mapper = type_expression -> type_expression result
+type abs_mapper =
+  | Expression of exp_mapper
+  | Type_expression of ty_exp_mapper 
+let rec map_expression : exp_mapper -> expression -> expression result = fun f e ->
+  let self = map_expression f in
+  let%bind e' = f e in
+  let return expression_content = ok { e' with expression_content } in
+  match e'.expression_content with
+  | E_ascription ascr -> (
+      let%bind e' = self ascr.anno_expr in
+      return @@ E_ascription {ascr with anno_expr=e'}
+    )
+  | E_matching {matchee=e;cases} -> (
+      let%bind e' = self e in
+      let%bind cases' = map_cases f cases in
+      return @@ E_matching {matchee=e';cases=cases'}
+    )
+  | E_record_accessor acc -> (
+      let%bind e' = self acc.record in
+      return @@ E_record_accessor {acc with record = e'}
+    )
+  | E_record m -> (
+    let%bind m' = bind_map_lmap self m in
+    return @@ E_record m'
+  )
+  | E_record_update {record; path; update} -> (
+    let%bind record = self record in
+    let%bind update = self update in
+    return @@ E_record_update {record;path;update}
+  )
+  | E_constructor c -> (
+      let%bind e' = self c.element in
+      return @@ E_constructor {c with element = e'}
+  )
+  | E_application {lamb;args} -> (
+      let ab = (lamb,args) in
+      let%bind (lamb,args) = bind_map_pair self ab in
+      return @@ E_application {lamb;args}
+    )
+  | E_let_in { let_binder ; rhs ; let_result; inline } -> (
+      let%bind rhs = self rhs in
+      let%bind let_result = self let_result in
+      return @@ E_let_in { let_binder ; rhs ; let_result; inline }
+    )
+  | E_lambda { binder ; input_type ; output_type ; result } -> (
+      let%bind result = self result in
+      return @@ E_lambda { binder ; input_type ; output_type ; result }
+    )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind result = self lambda.result in
+      let lambda = {lambda with result} in
+      return @@ E_recursive { fun_name; fun_type; lambda}
+  | E_constant c -> (
+      let%bind args = bind_map_list self c.arguments in
+      return @@ E_constant {c with arguments=args}
+    )
+  | E_literal _ | E_variable _ as e' -> return e'
+
+and map_type_expression : ty_exp_mapper -> type_expression -> type_expression result = fun f ({type_content ; location ; type_meta} as te) ->
+  let self = map_type_expression f in
+  let%bind te' = f te in
+  let return type_content = ok { type_content; location ; type_meta } in
+  match type_content with
+  | T_sum temap ->
+    let%bind temap' = bind_map_cmap self temap in
+    return @@ (T_sum temap')
+  | T_record temap ->
+    let%bind temap' = bind_map_lmap_t self temap in
+    return @@ (T_record temap')
+  | T_arrow {type1 ; type2} ->
+    let%bind type1' = self type1 in
+    let%bind type2' = self type2 in
+    return @@ (T_arrow {type1=type1' ; type2=type2'})
+  | T_operator _
+  | T_variable _ | T_constant _ -> ok te'
+
+and map_cases : exp_mapper -> matching_expr -> matching_expr result = fun f m ->
+  match m with
+  | Match_bool { match_true ; match_false } -> (
+      let%bind match_true = map_expression f match_true in
+      let%bind match_false = map_expression f match_false in
+      ok @@ Match_bool { match_true ; match_false }
+    )
+  | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> (
+      let%bind match_nil = map_expression f match_nil in
+      let%bind cons = map_expression f cons in
+      ok @@ Match_list { match_nil ; match_cons = (hd , tl , cons, ()) }
+    )
+  | Match_option { match_none ; match_some = (name , some, _) } -> (
+      let%bind match_none = map_expression f match_none in
+      let%bind some = map_expression f some in
+      ok @@ Match_option { match_none ; match_some = (name , some, ()) }
+    )
+  | Match_tuple ((names , e), _) -> (
+      let%bind e' = map_expression f e in
+      ok @@ Match_tuple ((names , e'), [])
+    )
+  | Match_variant (lst, _) -> (
+      let aux ((a , b) , e) =
+        let%bind e' = map_expression f e in
+        ok ((a , b) , e')
+      in
+      let%bind lst' = bind_map_list aux lst in
+      ok @@ Match_variant (lst', ())
+    )
+
+and map_program : abs_mapper -> program -> program result = fun m p ->
+  let aux = fun (x : declaration) ->
+    match x,m with
+    | (Declaration_constant (t , o , i, e), Expression m') -> (
+        let%bind e' = map_expression m' e in
+        ok (Declaration_constant (t , o , i, e'))
+      )
+    | (Declaration_type (tv,te), Type_expression m') -> (
+        let%bind te' = map_type_expression m' te in
+        ok (Declaration_type (tv, te'))
+      )
+    | decl,_ -> ok decl
+  (* | Declaration_type of (type_variable * type_expression) *)
+  in
+  bind_map_list (bind_map_location aux) p
+
+type 'a fold_mapper = 'a -> expression -> (bool * 'a * expression) result
+let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expression) result = fun f a e ->
+  let self = fold_map_expression f in
+  let%bind (continue, init',e') = f a e in
+  if (not continue) then ok(init',e')
+  else
+  let return expression_content = { e' with expression_content } in
+  match e'.expression_content with
+  | E_ascription ascr -> (
+      let%bind (res,e') = self init' ascr.anno_expr in
+      ok (res, return @@ E_ascription {ascr with anno_expr=e'})
+    )
+  | E_matching {matchee=e;cases} -> (
+      let%bind (res, e') = self init' e in
+      let%bind (res,cases') = fold_map_cases f res cases in
+      ok (res, return @@ E_matching {matchee=e';cases=cases'})
+    )
+  | E_record_accessor acc -> (
+      let%bind (res, e') = self init' acc.record in
+      ok (res, return @@ E_record_accessor {acc with record = e'})
+    )
+  | E_record m -> (
+    let%bind (res, lst') = bind_fold_map_list (fun res (k,e) -> let%bind (res,e) = self res e in ok (res,(k,e))) init' (LMap.to_kv_list m) in
+    let m' = LMap.of_list lst' in
+    ok (res, return @@ E_record m')
+  )
+  | E_record_update {record; path; update} -> (
+    let%bind (res, record) = self init' record in
+    let%bind (res, update) = self res update in
+    ok (res, return @@ E_record_update {record;path;update})
+  )
+  | E_constructor c -> (
+      let%bind (res,e') = self init' c.element in
+      ok (res, return @@ E_constructor {c with element = e'})
+  )
+  | E_application {lamb;args} -> (
+      let ab = (lamb,args) in
+      let%bind (res,(a,b)) = bind_fold_map_pair self init' ab in
+      ok (res, return @@ E_application {lamb=a;args=b})
+    )
+  | E_let_in { let_binder ; rhs ; let_result; inline } -> (
+      let%bind (res,rhs) = self init' rhs in
+      let%bind (res,let_result) = self res let_result in
+      ok (res, return @@ E_let_in { let_binder ; rhs ; let_result ; inline })
+    )
+  | E_lambda { binder ; input_type ; output_type ; result } -> (
+      let%bind (res,result) = self init' result in
+      ok ( res, return @@ E_lambda { binder ; input_type ; output_type ; result })
+    )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind (res, result) = self init' lambda.result in
+      let lambda = {lambda with result} in
+      ok ( res, return @@ E_recursive { fun_name; fun_type; lambda})
+  | E_constant c -> (
+      let%bind (res,args) = bind_fold_map_list self init' c.arguments in
+      ok (res, return @@ E_constant {c with arguments=args})
+    )
+  | E_literal _ | E_variable _ as e' -> ok (init', return e')
+
+and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m ->
+  match m with
+  | Match_bool { match_true ; match_false } -> (
+      let%bind (init, match_true) = fold_map_expression f init match_true in
+      let%bind (init, match_false) = fold_map_expression f init match_false in
+      ok @@ (init, Match_bool { match_true ; match_false })
+    )
+  | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> (
+      let%bind (init, match_nil) = fold_map_expression f init match_nil in
+      let%bind (init, cons) = fold_map_expression f init cons in
+      ok @@ (init, Match_list { match_nil ; match_cons = (hd , tl , cons, ()) })
+    )
+  | Match_option { match_none ; match_some = (name , some, _) } -> (
+      let%bind (init, match_none) = fold_map_expression f init match_none in
+      let%bind (init, some) = fold_map_expression f init some in
+      ok @@ (init, Match_option { match_none ; match_some = (name , some, ()) })
+    )
+  | Match_tuple ((names , e), _) -> (
+      let%bind (init, e') = fold_map_expression f init e in
+      ok @@ (init, Match_tuple ((names , e'), []))
+    )
+  | Match_variant (lst, _) -> (
+      let aux init ((a , b) , e) =
+        let%bind (init,e') = fold_map_expression f init e in
+        ok (init, ((a , b) , e'))
+      in
+      let%bind (init,lst') = bind_fold_map_list aux init lst in
+      ok @@ (init, Match_variant (lst', ()))
+    )  
diff --git a/src/passes/7-self_ast_core/self_ast_core.ml b/src/passes/7-self_ast_core/self_ast_core.ml
new file mode 100644
index 000000000..56a41f46f
--- /dev/null
+++ b/src/passes/7-self_ast_core/self_ast_core.ml
@@ -0,0 +1,24 @@
+open Trace
+
+let all_expression_mapper = [
+]
+let all_type_expression_mapper = [
+]
+
+let all_exp = List.map (fun el -> Helpers.Expression el) all_expression_mapper
+let all_ty = List.map (fun el -> Helpers.Type_expression el) all_type_expression_mapper
+
+let all_program =
+  let all_p = List.map Helpers.map_program all_exp in
+  let all_p2 = List.map Helpers.map_program all_ty in
+  bind_chain (List.append all_p all_p2)
+
+let all_expression =
+  let all_p = List.map Helpers.map_expression all_expression_mapper in
+  bind_chain all_p
+
+let map_expression = Helpers.map_expression
+
+let fold_expression = Helpers.fold_expression
+
+let fold_map_expression = Helpers.fold_map_expression
diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml
index 78520eb20..abecd4ef7 100644
--- a/src/passes/8-typer-new/PP.ml
+++ b/src/passes/8-typer-new/PP.ml
@@ -11,7 +11,6 @@ let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
       | Solver.Core.C_variant      -> failwith "variant"
       | Solver.Core.C_map          -> "map"
       | Solver.Core.C_big_map      -> "big_map"
-      | Solver.Core.C_michelson_or -> "michelson_or"
       | Solver.Core.C_list         -> "list"
       | Solver.Core.C_set          -> "set"
       | Solver.Core.C_unit         -> "unit"
diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml
index d7bbd220e..ce2ba87d8 100644
--- a/src/passes/8-typer-new/solver.ml
+++ b/src/passes/8-typer-new/solver.ml
@@ -387,97 +387,93 @@ let compare_simple_c_constant = function
   | C_arrow -> (function
       (* N/A -> 1 *)
       | C_arrow -> 0
-      | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_option -> (function
       | C_arrow -> 1
       | C_option -> 0
-      | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_record -> (function
       | C_arrow | C_option  -> 1
       | C_record -> 0
-      | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_variant -> (function
       | C_arrow | C_option  | C_record -> 1
       | C_variant -> 0
-      | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_map -> (function
       | C_arrow | C_option  | C_record | C_variant -> 1
       | C_map -> 0
-      | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
+      | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_big_map -> (function
       | C_arrow | C_option  | C_record | C_variant | C_map -> 1
       | C_big_map -> 0
-      | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
-  | C_michelson_or -> (function
-      | C_arrow | C_option  | C_record | C_variant | C_map | C_big_map -> 1
-      | C_michelson_or -> 0
       | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_list -> (function
-      | C_arrow | C_option  | C_record | C_variant | C_map | C_big_map | C_michelson_or -> 1
+      | C_arrow | C_option  | C_record | C_variant | C_map | C_big_map -> 1
       | C_list -> 0
       | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_set -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1
       | C_set -> 0
       | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_unit -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
       | C_unit -> 0
       | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_bool -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
       | C_bool -> 0
       | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_string -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1
       | C_string -> 0
       | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_nat -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1
       | C_nat -> 0
       | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_mutez -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1
       | C_mutez -> 0
       | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_timestamp -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1
       | C_timestamp -> 0
       | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_int -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1
       | C_int -> 0
       | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_address -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
       | C_address -> 0
       | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_bytes -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
       | C_bytes -> 0
       | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_key_hash -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
       | C_key_hash -> 0
       | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_key -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
       | C_key -> 0
       | C_signature | C_operation | C_contract | C_chain_id -> -1)
   | C_signature -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
       | C_signature -> 0
       | C_operation | C_contract | C_chain_id -> -1)
   | C_operation -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
       | C_operation -> 0
       | C_contract | C_chain_id -> -1)
   | C_contract -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
       | C_contract -> 0
       | C_chain_id -> -1)
   | C_chain_id -> (function
-      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_michelson_or | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
+      | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
       | C_chain_id -> 0
       (* N/A -> -1 *)
     )
@@ -493,7 +489,6 @@ let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag ->
       | Core.C_variant   -> failwith "variant"
       | Core.C_map       -> "map"
       | Core.C_big_map   -> "big_map"
-      | Core.C_michelson_or -> "michelson_or"
       | Core.C_list      -> "list"
       | Core.C_set       -> "set"
       | Core.C_unit      -> "unit"
diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml
index b8f875e7e..71ec621c2 100644
--- a/src/passes/8-typer-new/typer.ml
+++ b/src/passes/8-typer-new/typer.ml
@@ -138,16 +138,18 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
   | T_sum m ->
     let aux k v prev =
       let%bind prev' = prev in
-      let%bind v' = evaluate_type e v in
-      ok @@ O.CMap.add (convert_constructor' k) v' prev'
+      let {ctor_type ; michelson_annotation} : I.ctor_content = v in
+      let%bind ctor_type = evaluate_type e ctor_type in
+      ok @@ O.CMap.add (convert_constructor' k) ({ctor_type ; michelson_annotation}:O.ctor_content) prev'
     in
     let%bind m = I.CMap.fold aux m (ok O.CMap.empty) in
     return (T_sum m)
   | T_record m ->
     let aux k v prev =
       let%bind prev' = prev in
-      let%bind v' = evaluate_type e v in
-      ok @@ O.LMap.add (convert_label k) v' prev'
+      let {field_type ; field_annotation} : I.field_content = v in
+      let%bind field_type = evaluate_type e field_type in
+      ok @@ O.LMap.add (convert_label k) ({field_type ; michelson_annotation=field_annotation}:O.field_content) prev'
     in
     let%bind m = I.LMap.fold aux m (ok O.LMap.empty) in
     return (T_record m)
@@ -181,10 +183,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
             let%bind k = evaluate_type e k in
             let%bind v = evaluate_type e v in
             ok @@ O.TC_map_or_big_map {k;v}
-        | TC_michelson_or (l,r) ->
-            let%bind l = evaluate_type e l in 
-            let%bind r = evaluate_type e r in 
-            ok @@ O.TC_michelson_or {l;r} 
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ O.TC_contract c
@@ -314,7 +312,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
       ok (O.LMap.add (convert_label k) expr' acc , state')
     in
     let%bind (m' , state') = Stage_common.Helpers.bind_fold_lmap aux (ok (O.LMap.empty , state)) m in
-    let wrapped = Wrap.record (O.LMap.map get_type_expression m') in
+    let wrapped = Wrap.record (O.LMap.map (fun e -> ({field_type = get_type_expression e ; michelson_annotation = None}: O.field_content)) m') in
     return_wrapped (E_record m') state' wrapped
   | E_record_update {record; path; update} ->
     let%bind (record, state) = type_expression e state record in
@@ -326,7 +324,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
       | T_record record -> (
           let field_op = O.LMap.find_opt path record in
           match field_op with
-          | Some tv -> ok (record,tv)
+          | Some {field_type=tv;_} -> ok (record,tv)
           | None -> failwith @@ Format.asprintf "field %a is not part of record" O.PP.label path
       )
       | _ -> failwith "Update an expression which is not a record"
diff --git a/src/passes/8-typer-new/untyper.ml b/src/passes/8-typer-new/untyper.ml
index 0f0803f8e..f082bd072 100644
--- a/src/passes/8-typer-new/untyper.ml
+++ b/src/passes/8-typer-new/untyper.ml
@@ -149,16 +149,18 @@ let rec untype_type_expression (t:O.type_expression) : (I.type_expression) resul
   (* TODO: or should we use t.core if present? *)
   let%bind t = match t.type_content with
   | O.T_sum x ->
-    let aux k v acc =
+    let aux k ({ctor_type ; michelson_annotation} : O.ctor_content) acc =
       let%bind acc = acc in
-      let%bind v' = untype_type_expression v in
+      let%bind ctor_type = untype_type_expression ctor_type in
+      let v' : I.ctor_content = {ctor_type ; michelson_annotation} in 
       ok @@ I.CMap.add (unconvert_constructor' k) v' acc in
     let%bind x' = O.CMap.fold aux x (ok I.CMap.empty) in
     ok @@ I.T_sum x'
   | O.T_record x ->
-    let aux k v acc =
+    let aux k ({field_type ; michelson_annotation} : O.field_content) acc =
       let%bind acc = acc in
-      let%bind v' = untype_type_expression v in
+      let%bind field_type = untype_type_expression field_type in
+      let v' = ({field_type ; field_annotation=michelson_annotation} : I.field_content) in
       ok @@ I.LMap.add (unconvert_label k) v' acc in
     let%bind x' = O.LMap.fold aux x (ok I.LMap.empty) in
     ok @@ I.T_record x'
@@ -192,10 +194,6 @@ let rec untype_type_expression (t:O.type_expression) : (I.type_expression) resul
          let%bind k = untype_type_expression k in
          let%bind v = untype_type_expression v in
          ok @@ I.TC_map_or_big_map (k,v)
-      | O.TC_michelson_or {l;r} ->     
-         let%bind l = untype_type_expression l in
-         let%bind r = untype_type_expression r in
-         ok @@ I.TC_michelson_or (l,r)
       | O.TC_arrow { type1=arg ; type2=ret } ->
          let%bind arg' = untype_type_expression arg in
          let%bind ret' = untype_type_expression ret in
diff --git a/src/passes/8-typer-new/wrap.ml b/src/passes/8-typer-new/wrap.ml
index 55e7c3257..f51a38140 100644
--- a/src/passes/8-typer-new/wrap.ml
+++ b/src/passes/8-typer-new/wrap.ml
@@ -34,10 +34,12 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
   match te.type_content with
   | T_sum kvmap ->
      let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
-     P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
+     let tlist = List.map (fun ({ctor_type;_}:T.ctor_content) -> ctor_type) (T.CMap.to_list kvmap) in
+     P_constant (C_variant, List.map type_expression_to_type_value tlist)
   | T_record kvmap ->
      let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
-     P_constant (C_record, T.LMap.to_list @@ T.LMap.map type_expression_to_type_value kvmap)
+     let tlist = List.map (fun ({field_type;_}:T.field_content) -> field_type) (T.LMap.to_list kvmap) in
+     P_constant (C_record, List.map type_expression_to_type_value tlist)
   | T_arrow {type1;type2} ->
      P_constant (C_arrow, List.map type_expression_to_type_value [ type1 ; type2 ])
 
@@ -69,7 +71,6 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
                                 | TC_map { k ; v }           -> (C_map, [k;v])
                                 | TC_big_map { k ; v }       -> (C_big_map, [k;v])
                                 | TC_map_or_big_map { k ; v } -> (C_map, [k;v])
-                                | TC_michelson_or { l; r } -> (C_michelson_or, [l;r])
                                 | TC_arrow { type1 ; type2 } -> (C_arrow, [ type1 ; type2 ])
                                 | TC_list l                  -> (C_list, [l])
                                 | TC_contract c              -> (C_contract, [c])
@@ -81,10 +82,12 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
   match te.type_content with
   | T_sum kvmap ->
      let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
-     P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
+     let tlist = List.map (fun ({ctor_type;_}:I.ctor_content) -> ctor_type) (I.CMap.to_list kvmap) in
+     P_constant (C_variant, List.map type_expression_to_type_value_copypasted tlist)
   | T_record kvmap ->
      let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
-     P_constant (C_record, I.LMap.to_list @@ I.LMap.map type_expression_to_type_value_copypasted kvmap)
+     let tlist = List.map (fun ({field_type;_}:I.field_content) -> field_type) (I.LMap.to_list kvmap) in
+     P_constant (C_record, List.map type_expression_to_type_value_copypasted tlist)
   | T_arrow {type1;type2} ->
      P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ type1 ; type2 ])
   | T_variable type_name -> P_variable (type_name) (* eird stuff*)
@@ -104,7 +107,6 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
                                 | TC_map  ( k , v )      -> (C_map    , [k;v])
                                 | TC_big_map  ( k , v )  -> (C_big_map, [k;v])
                                 | TC_map_or_big_map ( k , v) -> (C_map, [k;v])
-                                | TC_michelson_or ( k , v ) -> (C_michelson_or, [k;v])
                                 | TC_contract c          -> (C_contract, [c])
                                 | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
                           )
@@ -184,7 +186,7 @@ let constructor
     C_equation (t_arg , c_arg)
   ] , whole_expr
 
-let record : T.type_expression T.label_map -> (constraints * T.type_variable) = fun fields ->
+let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields ->
   let record_type = type_expression_to_type_value (T.t_record fields ()) in
   let whole_expr = Core.fresh_type_variable () in
   [C_equation (P_variable whole_expr , record_type)] , whole_expr
diff --git a/src/passes/8-typer-old/typer.ml b/src/passes/8-typer-old/typer.ml
index 976459200..7d2a70d8e 100644
--- a/src/passes/8-typer-old/typer.ml
+++ b/src/passes/8-typer-old/typer.ml
@@ -596,23 +596,25 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
       let%bind type2 = evaluate_type e type2 in
       return (T_arrow {type1;type2})
   | T_sum m ->
-      let aux k v prev =
+      let aux k ({ctor_type;michelson_annotation} : I.ctor_content) prev =
         let%bind prev' = prev in
-        let%bind v' = evaluate_type e v in
+        let%bind ctor_type = evaluate_type e ctor_type in
         let%bind () = match Environment.get_constructor k e with
           | Some _ ->
             if I.CMap.mem (Constructor "M_left") m || I.CMap.mem (Constructor "M_right") m then
               ok ()
             else fail (redundant_constructor e k)
           | None -> ok () in
+        let v' : O.ctor_content = {ctor_type;michelson_annotation} in
         ok @@ O.CMap.add (convert_constructor' k) v' prev'
       in
       let%bind m = I.CMap.fold aux m (ok O.CMap.empty) in
       return (T_sum m)
   | T_record m ->
-      let aux k v prev =
+      let aux k ({field_type;field_annotation}: I.field_content) prev =
         let%bind prev' = prev in
-        let%bind v' = evaluate_type e v in
+        let%bind field_type = evaluate_type e field_type in
+        let v' = ({field_type;michelson_annotation=field_annotation} : O.field_content) in
         ok @@ O.LMap.add (convert_label k) v' prev'
       in
       let%bind m = I.LMap.fold aux m (ok O.LMap.empty) in
@@ -647,10 +649,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
             let%bind k = evaluate_type e k in 
             let%bind v = evaluate_type e v in 
             ok @@ O.TC_map_or_big_map {k;v}
-        | TC_michelson_or (l,r) ->
-            let%bind l = evaluate_type e l in 
-            let%bind r = evaluate_type e r in 
-            ok @@ O.TC_michelson_or {l;r}
         | TC_arrow ( arg , ret ) ->
             let%bind arg' = evaluate_type e arg in
             let%bind ret' = evaluate_type e ret in
@@ -727,7 +725,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
             let%bind r_tv = get_t_record prev.type_expression in
             let%bind tv =
               generic_try (bad_record_access property ae prev.type_expression ae.location)
-              @@ (fun () -> O.LMap.find (convert_label property) r_tv) in
+              @@ (fun () -> let ({field_type;_} : O.field_content) = O.LMap.find (convert_label property) r_tv in field_type) in
             let location = ae.location in
             ok @@ make_e ~location (E_record_accessor {record=prev; path=convert_label property}) tv e
       in
@@ -744,8 +742,8 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     let%bind expr' = type_expression' e element in
     ( match t.type_content with
       | T_sum c ->
-        let ct = O.CMap.find (O.Constructor s) c in
-        let%bind _assert = O.assert_type_expression_eq (expr'.type_expression, ct) in
+        let {ctor_type ; _} : O.ctor_content = O.CMap.find (O.Constructor s) c in
+        let%bind _assert = O.assert_type_expression_eq (expr'.type_expression, ctor_type) in
         return (E_constructor {constructor = Constructor s; element=expr'}) t
       | _ -> simple_fail "ll" 
     )
@@ -774,7 +772,8 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
         ok (O.LMap.add (convert_label k) expr' prev)
       in
       let%bind m' = Stage_common.Helpers.bind_fold_lmap aux (ok O.LMap.empty) m in
-      return (E_record m') (t_record (O.LMap.map get_type_expression m') ())
+      let lmap = O.LMap.map (fun e -> ({field_type = get_type_expression e; michelson_annotation = None}:O.field_content)) m' in
+      return (E_record m') (t_record lmap ())
   | E_record_update {record; path; update} ->
     let path = convert_label path in
     let%bind record = type_expression' e record in
@@ -785,7 +784,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       | T_record record -> (
           let field_op = O.LMap.find_opt path record in
           match field_op with
-          | Some tv -> ok (tv)
+          | Some {field_type;_} -> ok field_type
           | None -> failwith @@ Format.asprintf "field %a is not part of record %a" Ast_typed.PP.label path O.PP.type_expression wrapped
       )
       | _ -> failwith "Update an expression which is not a record"
diff --git a/src/passes/9-self_ast_typed/contract_passes.ml b/src/passes/9-self_ast_typed/contract_passes.ml
index d3877bd39..a98d466e8 100644
--- a/src/passes/9-self_ast_typed/contract_passes.ml
+++ b/src/passes/9-self_ast_typed/contract_passes.ml
@@ -62,8 +62,10 @@ let self_typing : contract_pass_data -> expression -> (bool * contract_pass_data
       | E_literal (Literal_string ep) -> check_entrypoint_annotation_format ep entrypoint_exp
       | _ -> fail @@ Errors.entrypoint_annotation_not_literal entrypoint_exp.location in
     let%bind entrypoint_t = match dat.contract_type.parameter.type_content with
-      | T_sum cmap -> trace_option (Errors.unmatched_entrypoint entrypoint_exp.location)
-                      @@ CMap.find_opt (Constructor entrypoint) cmap
+      | T_sum cmap ->
+        let%bind {ctor_type;_} = trace_option (Errors.unmatched_entrypoint entrypoint_exp.location) @@
+          CMap.find_opt (Constructor entrypoint) cmap in
+        ok ctor_type
       | t -> ok {dat.contract_type.parameter with type_content = t} in
     let%bind () =
       trace_strong (bad_self_err ()) @@
diff --git a/src/passes/9-self_ast_typed/no_nested_big_map.ml b/src/passes/9-self_ast_typed/no_nested_big_map.ml
index f90a9b203..710f1b3e4 100644
--- a/src/passes/9-self_ast_typed/no_nested_big_map.ml
+++ b/src/passes/9-self_ast_typed/no_nested_big_map.ml
@@ -39,17 +39,13 @@ let rec check_no_nested_bigmap is_in_bigmap e =
     let%bind _ = check_no_nested_bigmap false type1 in
     let%bind _ = check_no_nested_bigmap false type2 in
     ok ()
-  | T_operator (TC_michelson_or {l; r}) -> 
-    let%bind _ = check_no_nested_bigmap false l in
-    let%bind _ = check_no_nested_bigmap false r in
-    ok ()
   | T_sum s -> 
-    let es = CMap.to_list s in
+    let es = List.map (fun {ctor_type;_} -> ctor_type) (CMap.to_list s) in
     let%bind _ = bind_map_list (fun l -> check_no_nested_bigmap is_in_bigmap l) es in
     ok ()
   | T_record elm -> 
     let es = LMap.to_list elm in
-    let%bind _ = bind_map_list (fun l -> check_no_nested_bigmap is_in_bigmap l) es in
+    let%bind _ = bind_map_list (fun {field_type;_} -> check_no_nested_bigmap is_in_bigmap field_type) es in
     ok ()
   | T_arrow { type1; type2 } -> 
     let%bind _ = check_no_nested_bigmap false type1 in    
diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml
index 1cf4407ae..0400a3606 100644
--- a/src/passes/operators/operators.ml
+++ b/src/passes/operators/operators.ml
@@ -59,7 +59,7 @@ module Concrete_to_imperative = struct
     | "set"          -> ok @@ TC_set unit_expr
     | "map"          -> ok @@ TC_map (unit_expr,unit_expr)
     | "big_map"      -> ok @@ TC_big_map (unit_expr,unit_expr)
-    | "michelson_or" -> ok @@ TC_michelson_or (unit_expr,unit_expr)
+    | "michelson_or" -> ok @@ TC_michelson_or (unit_expr,"",unit_expr,"")
     | "contract"     -> ok @@ TC_contract unit_expr
     | _              -> simple_fail @@ "Not a built-in type (" ^ s ^ ")."
 
diff --git a/src/stages/1-ast_imperative/PP.ml b/src/stages/1-ast_imperative/PP.ml
index 4d735677b..0b9827d4a 100644
--- a/src/stages/1-ast_imperative/PP.ml
+++ b/src/stages/1-ast_imperative/PP.ml
@@ -5,6 +5,20 @@ open PP_helpers
 
 include Stage_common.PP
 
+let cmap_sep value sep ppf m =
+  let lst = CMap.to_kv_list m in
+  let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" constructor k value v in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
+let cmap_sep_d x = cmap_sep x (tag " ,@ ")
+
+let record_sep value sep ppf (m : 'a label_map) =
+  let lst = LMap.to_kv_list m in
+  let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" label k value v in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
 let expression_variable ppf (ev : expression_variable) : unit =
   fprintf ppf "%a" Var.pp ev
 
@@ -39,7 +53,8 @@ and type_operator :
     | TC_set te -> Format.asprintf "set(%a)" f te
     | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
     | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
-    | TC_michelson_or (l, r) -> Format.asprintf "Michelson_or (%a,%a)" f l f r
+    | TC_michelson_or (l,_, r,_) -> Format.asprintf "Michelson_or (%a,%a)" f l f r
+    | TC_michelson_pair (l,_, r,_) -> Format.asprintf "Michelson_pair (%a,%a)" f l f r
     | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v
     | TC_contract te  -> Format.asprintf "Contract (%a)" f te
   in
diff --git a/src/stages/1-ast_imperative/combinators.ml b/src/stages/1-ast_imperative/combinators.ml
index c8b8be570..a7bb20945 100644
--- a/src/stages/1-ast_imperative/combinators.ml
+++ b/src/stages/1-ast_imperative/combinators.ml
@@ -59,9 +59,10 @@ let t_sum ?loc m : type_expression =
 let t_function ?loc type1 type2  : type_expression = make_t ?loc @@ T_arrow {type1; type2}
 let t_map ?loc key value         : type_expression = make_t ?loc @@ T_operator (TC_map (key, value))
 let t_big_map ?loc key value     : type_expression = make_t ?loc @@ T_operator (TC_big_map (key , value))
-let t_michelson_or ?loc l r      : type_expression = make_t ?loc @@ T_operator (TC_michelson_or (l , r))
 let t_set ?loc key               : type_expression = make_t ?loc @@ T_operator (TC_set key)
 let t_contract ?loc contract     : type_expression = make_t ?loc @@ T_operator (TC_contract contract)
+let t_michelson_or ?loc l l_ann r r_ann : type_expression = make_t ?loc @@ T_operator (TC_michelson_or (l, l_ann, r, r_ann))
+let t_michelson_pair ?loc l l_ann r r_ann : type_expression = make_t ?loc @@ T_operator (TC_michelson_pair (l, l_ann, r, r_ann))
 
 (* TODO find a better way than using list*)
 let t_operator ?loc op lst: type_expression result =
@@ -71,7 +72,7 @@ let t_operator ?loc op lst: type_expression result =
   | TC_option _      , [t] -> ok @@ t_option ?loc t
   | TC_map (_,_)     , [kt;vt] -> ok @@ t_map ?loc kt vt
   | TC_big_map (_,_) , [kt;vt] -> ok @@ t_big_map ?loc kt vt
-  | TC_michelson_or (_,_) , [l;r] -> ok @@ t_michelson_or ?loc l r
+  | TC_michelson_or (_,l_ann,_,r_ann) , [l;r] -> ok @@ t_michelson_or ?loc l l_ann r r_ann
   | TC_contract _    , [t] -> ok @@ t_contract t
   | _ , _ -> fail @@ bad_type_operator op
 
diff --git a/src/stages/1-ast_imperative/combinators.mli b/src/stages/1-ast_imperative/combinators.mli
index 1d582184f..50105895a 100644
--- a/src/stages/1-ast_imperative/combinators.mli
+++ b/src/stages/1-ast_imperative/combinators.mli
@@ -42,6 +42,10 @@ val ez_t_sum : ?loc:Location.t -> ( string * type_expression ) list -> type_expr
 
 val t_function : ?loc:Location.t -> type_expression -> type_expression -> type_expression
 val t_map      : ?loc:Location.t -> type_expression -> type_expression -> type_expression
+val t_michelson_or : ?loc:Location.t -> type_expression -> michelson_prct_annotation ->
+  type_expression -> michelson_prct_annotation -> type_expression
+val t_michelson_pair : ?loc:Location.t -> type_expression -> michelson_prct_annotation ->
+  type_expression -> michelson_prct_annotation -> type_expression
 
 val t_operator : ?loc:Location.t -> type_operator -> type_expression list -> type_expression result
 val t_set      : ?loc:Location.t -> type_expression -> type_expression
diff --git a/src/stages/1-ast_imperative/types.ml b/src/stages/1-ast_imperative/types.ml
index f334a370e..49909998e 100644
--- a/src/stages/1-ast_imperative/types.ml
+++ b/src/stages/1-ast_imperative/types.ml
@@ -15,6 +15,8 @@ type type_content =
 
 and arrow = {type1: type_expression; type2: type_expression}
 
+and michelson_prct_annotation = string
+
 and type_operator =
   | TC_contract of type_expression
   | TC_option of type_expression
@@ -22,8 +24,9 @@ and type_operator =
   | TC_set of type_expression
   | TC_map of type_expression * type_expression
   | TC_big_map of type_expression * type_expression
-  | TC_michelson_or of type_expression * type_expression
   | TC_arrow of type_expression * type_expression
+  | TC_michelson_or of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation
+  | TC_michelson_pair of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation
 
 and type_expression = {type_content: type_content; location: Location.t}
 
diff --git a/src/stages/2-ast_sugar/PP.ml b/src/stages/2-ast_sugar/PP.ml
index 419cbb724..22f726ff6 100644
--- a/src/stages/2-ast_sugar/PP.ml
+++ b/src/stages/2-ast_sugar/PP.ml
@@ -4,6 +4,22 @@ open Format
 open PP_helpers
 
 include Stage_common.PP
+include Stage_common.PP.Ast_PP_type(Ast_sugar_parameter)
+
+let cmap_sep value sep ppf m =
+  let lst = CMap.to_kv_list m in
+  let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, {ctor_type;_}) = fprintf ppf "@[<h>%a -> %a@]" constructor k value ctor_type in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
+let cmap_sep_d x = cmap_sep x (tag " ,@ ")
+
+let record_sep_t value sep ppf (m : 'a label_map) =
+  let lst = LMap.to_kv_list m in
+  let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, {field_type;_}) = fprintf ppf "@[<h>%a -> %a@]" label k value field_type in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
 
 let expression_variable ppf (ev : expression_variable) : unit =
   fprintf ppf "%a" Var.pp ev
@@ -15,8 +31,8 @@ let rec type_expression' :
     -> unit =
   fun f ppf te ->
   match te.type_content with
-  | T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
-  | T_record m -> fprintf ppf "{%a}" (record_sep f (const ";")) m
+  | T_sum m -> fprintf ppf "@[<hv 4>sum[%a]@]" (cmap_sep_d f) m
+  | T_record m -> fprintf ppf "{%a}" (record_sep_t f (const ";")) m
   | T_tuple  t -> fprintf ppf "(%a)" (list_sep_d f) t
   | T_arrow  a -> fprintf ppf "%a -> %a" f a.type1 f a.type2
   | T_variable tv -> type_variable ppf tv
@@ -35,7 +51,6 @@ and type_operator : (formatter -> type_expression -> unit) -> formatter -> type_
     | TC_set te -> Format.asprintf "set(%a)" f te
     | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
     | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
-    | TC_michelson_or (l, r) -> Format.asprintf "Michelson_or (%a,%a)" f l f r
     | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v
     | TC_contract te  -> Format.asprintf "Contract (%a)" f te
   in
@@ -57,7 +72,7 @@ and expression_content ppf (ec : expression_content) =
       fprintf ppf "%a(%a)" constant c.cons_name (list_sep_d expression)
         c.arguments
   | E_record m ->
-      fprintf ppf "{%a}" (record_sep expression (const ";")) m
+      fprintf ppf "{%a}" (record_sep_expr expression (const ";")) m
   | E_record_accessor ra ->
       fprintf ppf "%a.%a" expression ra.record label ra.path
   | E_record_update {record; path; update} ->
diff --git a/src/stages/2-ast_sugar/combinators.ml b/src/stages/2-ast_sugar/combinators.ml
index dad7106d3..99f4072b5 100644
--- a/src/stages/2-ast_sugar/combinators.ml
+++ b/src/stages/2-ast_sugar/combinators.ml
@@ -51,10 +51,12 @@ let t_record ?loc m  : type_expression =
   let lst = Map.String.to_kv_list m in
   t_record_ez ?loc lst
 
-let t_pair ?loc (a , b) : type_expression = t_record_ez ?loc [("0",a) ; ("1",b)]
+let t_pair ?loc (a , b) : type_expression = t_record_ez ?loc [
+  ("0",{field_type=a;michelson_annotation=None}) ;
+  ("1",{field_type=b;michelson_annotation=None})]
 let t_tuple ?loc lst    : type_expression = t_record_ez ?loc (tuple_to_record lst)
 
-let ez_t_sum ?loc (lst:(string * type_expression) list) : type_expression =
+let ez_t_sum ?loc (lst:((string * ctor_content) list)) : type_expression =
   let aux prev (k, v) = CMap.add (Constructor k) v prev in
   let map = List.fold_left aux CMap.empty lst in
   make_t ?loc @@ T_sum map
diff --git a/src/stages/2-ast_sugar/combinators.mli b/src/stages/2-ast_sugar/combinators.mli
index ca4605e4e..c91279fa9 100644
--- a/src/stages/2-ast_sugar/combinators.mli
+++ b/src/stages/2-ast_sugar/combinators.mli
@@ -32,13 +32,13 @@ val t_variable  : ?loc:Location.t -> string -> type_expression
 val t_record    : te_map -> type_expression
 *)
 val t_pair   : ?loc:Location.t -> ( type_expression * type_expression ) -> type_expression
-val t_tuple  : ?loc:Location.t -> type_expression list -> type_expression
+val t_tuple  : ?loc:Location.t -> field_content list -> type_expression
 
-val t_record    : ?loc:Location.t -> type_expression Map.String.t -> type_expression
-val t_record_ez : ?loc:Location.t -> (string * type_expression) list -> type_expression
+val t_record    : ?loc:Location.t -> field_content Map.String.t -> type_expression
+val t_record_ez : ?loc:Location.t -> (string * field_content) list -> type_expression
 
-val t_sum    : ?loc:Location.t -> type_expression Map.String.t -> type_expression
-val ez_t_sum : ?loc:Location.t -> ( string * type_expression ) list -> type_expression
+val t_sum    : ?loc:Location.t -> ctor_content Map.String.t -> type_expression
+val ez_t_sum : ?loc:Location.t -> ( string * ctor_content ) list -> type_expression
 
 val t_function : ?loc:Location.t -> type_expression -> type_expression -> type_expression
 val t_map      : ?loc:Location.t -> type_expression -> type_expression -> type_expression
diff --git a/src/stages/2-ast_sugar/types.ml b/src/stages/2-ast_sugar/types.ml
index 47c11d68f..18295b7a5 100644
--- a/src/stages/2-ast_sugar/types.ml
+++ b/src/stages/2-ast_sugar/types.ml
@@ -4,9 +4,13 @@ module Location = Simple_utils.Location
 
 include Stage_common.Types
 
+module Ast_sugar_parameter = struct
+  type type_meta = unit
+end
+
 type type_content =
-  | T_sum of type_expression constructor_map
-  | T_record of type_expression label_map
+  | T_sum of ctor_content constructor_map
+  | T_record of field_content label_map
   | T_tuple  of type_expression list
   | T_arrow of arrow
   | T_variable of type_variable
@@ -15,13 +19,16 @@ type type_content =
 
 and arrow = {type1: type_expression; type2: type_expression}
 
+and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option}
+
+and field_content = {field_type : type_expression ; michelson_annotation : string option}
+
 and type_operator =
   | TC_contract of type_expression
   | TC_option of type_expression
   | TC_list of type_expression
   | TC_set of type_expression
   | TC_map of type_expression * type_expression
-  | TC_michelson_or of type_expression * type_expression
   | TC_big_map of type_expression * type_expression
   | TC_arrow of type_expression * type_expression
 
diff --git a/src/stages/3-ast_core/combinators.ml b/src/stages/3-ast_core/combinators.ml
index 2308cb5b3..aff739d8a 100644
--- a/src/stages/3-ast_core/combinators.ml
+++ b/src/stages/3-ast_core/combinators.ml
@@ -54,7 +54,7 @@ let t_record ?loc m  : type_expression =
 let t_pair ?loc (a , b) : type_expression = t_record_ez ?loc [("0",a) ; ("1",b)]
 let t_tuple ?loc lst    : type_expression = t_record_ez ?loc (tuple_to_record lst)
 
-let ez_t_sum ?loc (lst:(string * type_expression) list) : type_expression =
+let ez_t_sum ?loc (lst:(string * ctor_content) list) : type_expression =
   let aux prev (k, v) = CMap.add (Constructor k) v prev in
   let map = List.fold_left aux CMap.empty lst in
   make_t ?loc @@ T_sum map
diff --git a/src/stages/3-ast_core/combinators.mli b/src/stages/3-ast_core/combinators.mli
index 7320af576..9a857b0f7 100644
--- a/src/stages/3-ast_core/combinators.mli
+++ b/src/stages/3-ast_core/combinators.mli
@@ -31,14 +31,14 @@ val t_variable  : ?loc:Location.t -> string -> type_expression
 (*
 val t_record    : te_map -> type_expression
 *)
-val t_pair   : ?loc:Location.t -> ( type_expression * type_expression ) -> type_expression
-val t_tuple  : ?loc:Location.t -> type_expression list -> type_expression
+val t_pair   : ?loc:Location.t -> ( field_content * field_content ) -> type_expression
+val t_tuple  : ?loc:Location.t -> field_content list -> type_expression
 
-val t_record    : ?loc:Location.t -> type_expression Map.String.t -> type_expression
-val t_record_ez : ?loc:Location.t -> (string * type_expression) list -> type_expression
+val t_record    : ?loc:Location.t -> field_content Map.String.t -> type_expression
+val t_record_ez : ?loc:Location.t -> (string * field_content) list -> type_expression
 
-val t_sum    : ?loc:Location.t -> type_expression Map.String.t -> type_expression
-val ez_t_sum : ?loc:Location.t -> ( string * type_expression ) list -> type_expression
+val t_sum    : ?loc:Location.t -> Types.ctor_content Map.String.t -> type_expression
+val ez_t_sum : ?loc:Location.t -> ( string * Types.ctor_content ) list -> type_expression
 
 val t_function : ?loc:Location.t -> type_expression -> type_expression -> type_expression
 val t_map      : ?loc:Location.t -> type_expression -> type_expression -> type_expression
diff --git a/src/stages/3-ast_core/types.ml b/src/stages/3-ast_core/types.ml
index 6c9637ac4..e925c5f3b 100644
--- a/src/stages/3-ast_core/types.ml
+++ b/src/stages/3-ast_core/types.ml
@@ -8,8 +8,6 @@ end
 
 include Stage_common.Types
 
-(*include Ast_generic_type(Ast_core_parameter)
-*)
 include Ast_generic_type (Ast_core_parameter)
 
 type inline = bool 
diff --git a/src/stages/4-ast_typed/PP.ml b/src/stages/4-ast_typed/PP.ml
index a5cf4c7f1..25905b310 100644
--- a/src/stages/4-ast_typed/PP.ml
+++ b/src/stages/4-ast_typed/PP.ml
@@ -15,8 +15,7 @@ let label ppf (l:label) : unit =
   let Label l = l in fprintf ppf "%s" l
 
 let cmap_sep value sep ppf m =
-  let lst = CMap.to_kv_list m in
-  let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
+  let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) m in
   let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" constructor k value v in
   fprintf ppf "%a" (list_sep new_pp sep) lst
 
@@ -32,6 +31,18 @@ let tuple_sep value sep ppf m =
   let new_pp ppf (_, v) = fprintf ppf "%a" value v in
   fprintf ppf "%a" (list_sep new_pp sep) lst
 
+let record_sep_t value sep ppf (m : 'a label_map) =
+  let lst = LMap.to_kv_list m in
+  let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, {field_type;_}) = fprintf ppf "@[<h>%a -> %a@]" label k value field_type in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
+let tuple_sep_t value sep ppf m =
+  assert (Helpers.is_tuple_lmap m);
+  let lst = Helpers.tuple_of_record m in
+  let new_pp ppf (_, {field_type;_}) = fprintf ppf "%a" value field_type in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
 (* Prints records which only contain the consecutive fields
    0..(cardinal-1) as tuples *)
 let tuple_or_record_sep value format_record sep_record format_tuple sep_tuple ppf m =
@@ -39,11 +50,16 @@ let tuple_or_record_sep value format_record sep_record format_tuple sep_tuple pp
     fprintf ppf format_tuple (tuple_sep value (tag sep_tuple)) m
   else
     fprintf ppf format_record (record_sep value (tag sep_record)) m
+let tuple_or_record_sep_t value format_record sep_record format_tuple sep_tuple ppf m =
+  if Helpers.is_tuple_lmap m then
+    fprintf ppf format_tuple (tuple_sep_t value (tag sep_tuple)) m
+  else
+    fprintf ppf format_record (record_sep_t value (tag sep_record)) m
 
 let list_sep_d x = list_sep x (tag " ,@ ")
 let cmap_sep_d x = cmap_sep x (tag " ,@ ")
 let tuple_or_record_sep_expr value = tuple_or_record_sep value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " ,@ "
-let tuple_or_record_sep_type value = tuple_or_record_sep value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " *@ "
+let tuple_or_record_sep_type value = tuple_or_record_sep_t value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " *@ "
 
 let constant ppf : constant' -> unit = function
   | C_INT                   -> fprintf ppf "INT"
@@ -210,7 +226,7 @@ let rec type_expression' :
           -> unit =
   fun f ppf te ->
   match te.type_content with
-  | T_sum m -> fprintf ppf "@[<hv 4>sum[%a]@]" (cmap_sep_d f) m
+  | T_sum m -> fprintf ppf "@[<hv 4>sum[%a]@]" (cmap_sep_d f) (List.map (fun (c,{ctor_type;_}) -> (c,ctor_type)) (CMap.to_kv_list m))
   | T_record m -> fprintf ppf "%a" (tuple_or_record_sep_type f) m
   | T_arrow a -> fprintf ppf "%a -> %a" f a.type1 f a.type2
   | T_variable tv -> type_variable ppf tv
@@ -234,7 +250,6 @@ and type_operator :
     | TC_map {k; v} -> Format.asprintf "Map (%a,%a)" f k f v
     | TC_big_map {k; v} -> Format.asprintf "Big Map (%a,%a)" f k f v
     | TC_map_or_big_map {k; v} -> Format.asprintf "Map Or Big Map (%a,%a)" f k f v
-    | TC_michelson_or {l; r} -> Format.asprintf "michelson_or (%a,%a)" f l f r
     | TC_arrow {type1; type2} -> Format.asprintf "arrow (%a,%a)" f type1 f type2
     | TC_contract te  -> Format.asprintf "Contract (%a)" f te
   in
diff --git a/src/stages/4-ast_typed/combinators.ml b/src/stages/4-ast_typed/combinators.ml
index 6bfac897f..54a6e6b22 100644
--- a/src/stages/4-ast_typed/combinators.ml
+++ b/src/stages/4-ast_typed/combinators.ml
@@ -54,20 +54,20 @@ let t_contract t ?loc ?s () : type_expression = make_t ?loc (T_operator (TC_cont
 
 let t_record m ?loc ?s () : type_expression = make_t ?loc (T_record m) s
 let make_t_ez_record ?loc (lst:(string * type_expression) list) : type_expression =
-  let lst = List.map (fun (x,y) -> (Label x, y) ) lst in
+  let lst = List.map (fun (x,y) -> (Label x, {field_type=y;michelson_annotation=None}) ) lst in
   let map = LMap.of_list lst in
   make_t ?loc (T_record map) None
 let ez_t_record lst ?loc ?s () : type_expression =
   let m = LMap.of_list lst in
   t_record m ?loc ?s ()
-let t_pair a b ?loc ?s ()   : type_expression = ez_t_record [(Label "0",a) ; (Label "1",b)] ?loc ?s ()
+let t_pair a b ?loc ?s ()   : type_expression = ez_t_record [(Label "0",{field_type=a;michelson_annotation=None}) ; (Label "1",{field_type=b;michelson_annotation=None})] ?loc ?s ()
 
 let t_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map { k ; v })) s
 let t_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_big_map { k ; v })) s
 let t_map_or_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map_or_big_map { k ; v })) s
 
 let t_sum m ?loc ?s () : type_expression = make_t ?loc (T_sum m) s
-let make_t_ez_sum ?loc (lst:(constructor' * type_expression) list) : type_expression =
+let make_t_ez_sum ?loc (lst:(constructor' * ctor_content) list) : type_expression =
   let aux prev (k, v) = CMap.add k v prev in
   let map = List.fold_left aux CMap.empty lst in
   make_t ?loc (T_sum map) None
@@ -150,7 +150,9 @@ let tuple_of_record (m: _ LMap.t) =
     let opt = LMap.find_opt (Label (string_of_int i)) m in
     Option.bind (fun opt -> Some (opt,i+1)) opt
   in
-  Base.Sequence.to_list @@ Base.Sequence.unfold ~init:0 ~f:aux
+  let l = Base.Sequence.to_list @@ Base.Sequence.unfold ~init:0 ~f:aux in
+  List.map (fun {field_type;_} -> field_type) l
+
 
 let get_t_tuple (t:type_expression) : type_expression list result = match t.type_content with
   | T_record lst -> ok @@ tuple_of_record lst
@@ -178,13 +180,14 @@ let get_t_function_full (t:type_expression) : (type_expression * type_expression
     | _ -> ([],t)
   in
   let (input,output) = aux 0 t in
+  let input = List.map (fun (l,t) -> (l,{field_type = t ; michelson_annotation = None})) input in
   ok @@ (t_record (LMap.of_list input) (),output) 
 
-let get_t_sum (t:type_expression) : type_expression constructor_map result = match t.type_content with
+let get_t_sum (t:type_expression) : ctor_content constructor_map result = match t.type_content with
   | T_sum m -> ok m
   | _ -> fail @@ Errors.not_a_x_type "sum" t ()
 
-let get_t_record (t:type_expression) : type_expression label_map result = match t.type_content with
+let get_t_record (t:type_expression) : field_content label_map result = match t.type_content with
   | T_record m -> ok m
   | _ -> fail @@ Errors.not_a_x_type "record" t ()
 
@@ -306,14 +309,20 @@ let e_a_mutez n = make_e (e_mutez n) (t_mutez ())
 let e_a_bool b = make_e (e_bool b) (t_bool ())
 let e_a_string s = make_e (e_string s) (t_string ())
 let e_a_address s = make_e (e_address s) (t_address ())
-let e_a_pair a b = make_e (e_pair a b) (t_pair a.type_expression b.type_expression ())
+let e_a_pair a b = make_e (e_pair a b)
+  (t_pair a.type_expression b.type_expression () )
 let e_a_some s = make_e (e_some s) (t_option s.type_expression ())
 let e_a_lambda l in_ty out_ty = make_e (e_lambda l) (t_function in_ty out_ty ())
 let e_a_none t = make_e (e_none ()) (t_option t ())
-let e_a_record r = make_e (e_record r) (t_record (LMap.map get_type_expression r) ())
+let e_a_record r = make_e (e_record r) (t_record
+  (LMap.map
+    (fun t ->
+      let field_type = get_type_expression t in
+      {field_type ; michelson_annotation=None} )
+    r ) () )
 let e_a_application a b = make_e (e_application a b) (get_type_expression b)
 let e_a_variable v ty = make_e (e_variable v) ty
-let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_expression) r) ())
+let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, {field_type = y.type_expression ; michelson_annotation = None}) r) ())
 let e_a_let_in binder expr body attributes = make_e (e_let_in binder expr body attributes) (get_type_expression body)
 
 
diff --git a/src/stages/4-ast_typed/combinators.mli b/src/stages/4-ast_typed/combinators.mli
index ffcad19f8..9c7523e9e 100644
--- a/src/stages/4-ast_typed/combinators.mli
+++ b/src/stages/4-ast_typed/combinators.mli
@@ -25,15 +25,15 @@ val t_option : type_expression -> ?loc:Location.t -> ?s:S.type_expression -> uni
 val t_pair : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val t_list  : type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val t_variable : type_variable -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
-val t_record : type_expression label_map -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
+val t_record : te_lmap -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val make_t_ez_record : ?loc:Location.t -> (string* type_expression) list -> type_expression 
-val ez_t_record : ( label * type_expression ) list -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression 
+val ez_t_record : ( label * field_content ) list -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression 
 
 val t_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression
 val t_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression
 val t_map_or_big_map : ?loc:Location.t -> type_expression -> type_expression ->  ?s:S.type_expression -> unit -> type_expression
-val t_sum : type_expression constructor_map -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
-val make_t_ez_sum : ?loc:Location.t -> ( constructor' * type_expression ) list -> type_expression
+val t_sum : Types.te_cmap -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
+val make_t_ez_sum : ?loc:Location.t -> ( constructor' * ctor_content ) list -> type_expression
 val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val get_type_expression : expression -> type_expression
@@ -64,8 +64,8 @@ val get_t_tuple : type_expression -> type_expression list result
 val get_t_pair : type_expression -> ( type_expression * type_expression ) result
 val get_t_function : type_expression -> ( type_expression * type_expression ) result
 val get_t_function_full : type_expression -> ( type_expression * type_expression ) result
-val get_t_sum : type_expression -> type_expression constructor_map result
-val get_t_record : type_expression -> type_expression label_map result
+val get_t_sum : type_expression -> ctor_content constructor_map result
+val get_t_record : type_expression -> field_content label_map result
 val get_t_map : type_expression -> ( type_expression * type_expression ) result
 val get_t_big_map : type_expression -> ( type_expression * type_expression ) result
 val get_t_map_key : type_expression -> type_expression result
diff --git a/src/stages/4-ast_typed/combinators_environment.ml b/src/stages/4-ast_typed/combinators_environment.ml
index 5d9ecddb6..5fcb358fa 100644
--- a/src/stages/4-ast_typed/combinators_environment.ml
+++ b/src/stages/4-ast_typed/combinators_environment.ml
@@ -21,5 +21,5 @@ open Environment
 
 let env_sum_type ?(env = full_empty)
     ?(type_name = Var.of_name "a_sum_type")
-    (lst : (constructor' * type_expression) list) =
+    (lst : (constructor' * ctor_content) list) =
   add_type type_name (make_t_ez_sum lst) env
diff --git a/src/stages/4-ast_typed/combinators_environment.mli b/src/stages/4-ast_typed/combinators_environment.mli
index 830ac7ee2..783b1d6a6 100644
--- a/src/stages/4-ast_typed/combinators_environment.mli
+++ b/src/stages/4-ast_typed/combinators_environment.mli
@@ -16,4 +16,4 @@ val e_a_empty_record : expression label_map -> expression
 val ez_e_a_empty_record : ( label * expression ) list -> expression
 val e_a_empty_lambda : lambda -> type_expression -> type_expression -> expression
 
-val env_sum_type : ?env:full_environment -> ?type_name:type_variable -> (constructor' * type_expression) list ->  full_environment
+val env_sum_type : ?env:full_environment -> ?type_name:type_variable -> (constructor' * ctor_content) list ->  full_environment
diff --git a/src/stages/4-ast_typed/environment.ml b/src/stages/4-ast_typed/environment.ml
index 2f83a978b..d1bc6dc73 100644
--- a/src/stages/4-ast_typed/environment.ml
+++ b/src/stages/4-ast_typed/environment.ml
@@ -51,7 +51,7 @@ let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expr
       match type_.type_content with
       | T_sum m ->
         (match CMap.find_opt (convert_constructor' k) m with
-           Some km -> Some (km , type_)
+           Some {ctor_type ; _} -> Some (ctor_type , type_)
          | None -> None)
       | _ -> None
     in
diff --git a/src/stages/4-ast_typed/helpers.ml b/src/stages/4-ast_typed/helpers.ml
index c7dff6989..4aa1a374b 100644
--- a/src/stages/4-ast_typed/helpers.ml
+++ b/src/stages/4-ast_typed/helpers.ml
@@ -9,7 +9,6 @@ let map_type_operator f = function
   | TC_map {k ; v} -> TC_map { k = f k ; v = f v }
   | TC_big_map {k ; v}-> TC_big_map { k = f k ; v = f v }
   | TC_map_or_big_map { k ; v }-> TC_map_or_big_map { k = f k ; v = f v }
-  | TC_michelson_or { l ; r } -> TC_michelson_or { l = f l ; r = f r }
   | TC_arrow {type1 ; type2} -> TC_arrow { type1 = f type1 ; type2 = f type2 }
 
 let bind_map_type_operator f = function
@@ -20,7 +19,6 @@ let bind_map_type_operator f = function
   | TC_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_map {k ; v}
   | TC_big_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_big_map {k ; v}
   | TC_map_or_big_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_map_or_big_map {k ; v}
-  | TC_michelson_or {l ; r}-> let%bind l = f l in let%bind r = f r in ok @@ TC_michelson_or {l ; r}
   | TC_arrow {type1 ; type2}-> let%bind type1 = f type1 in let%bind type2 = f type2 in ok @@ TC_arrow {type1 ; type2}
 
 let type_operator_name = function
@@ -31,7 +29,6 @@ let type_operator_name = function
   | TC_map      _ -> "TC_map"
   | TC_big_map  _ -> "TC_big_map"
   | TC_map_or_big_map _ -> "TC_map_or_big_map"
-  | TC_michelson_or   _ -> "TC_michelson_or"
   | TC_arrow    _ -> "TC_arrow"
 
 let type_expression'_of_string = function
@@ -71,7 +68,6 @@ let string_of_type_operator = function
   | TC_map            { k ; v }         -> "TC_map"      , [k ; v]
   | TC_big_map        { k ; v }         -> "TC_big_map"  , [k ; v]
   | TC_map_or_big_map { k ; v }         -> "TC_map_or_big_map"  , [k ; v]
-  | TC_michelson_or   { l ; r }         -> "TC_michelson_or"    , [l ; r]
   | TC_arrow          { type1 ; type2 } -> "TC_arrow"    , [type1 ; type2]
 
 let string_of_type_constant = function
@@ -124,6 +120,11 @@ let bind_fold_lmap f init (lmap:_ LMap.t) =
   LMap.fold aux lmap init
 
 let bind_map_lmap f map = bind_lmap (LMap.map f map)
+let bind_map_lmap_t f map = bind_lmap (
+  LMap.map 
+    (fun ({field_type;_}) -> 
+      f field_type)
+    map)
 let bind_map_cmap f map = bind_cmap (CMap.map f map)
 let bind_map_lmapi f map = bind_lmap (LMap.mapi f map)
 let bind_map_cmapi f map = bind_cmap (CMap.mapi f map)
@@ -141,7 +142,7 @@ let is_tuple_lmap m =
 let get_pair m =
   let open Trace in
   match (LMap.find_opt (Label "0") m , LMap.find_opt (Label "1") m) with
-  | Some e1, Some e2 -> ok (e1,e2)
+  | Some {field_type=e1;_}, Some {field_type=e2;_} -> ok (e1,e2)
   | _ -> simple_fail "not a pair"
 
 let tuple_of_record (m: _ LMap.t) =
@@ -168,4 +169,13 @@ let kv_list_of_record_or_tuple (m: _ LMap.t) =
 let is_michelson_or (t: _ constructor_map) =
   CMap.cardinal t = 2 && 
   (CMap.mem (Constructor "M_left") t) &&
-  (CMap.mem (Constructor "M_right") t)
\ No newline at end of file
+  (CMap.mem (Constructor "M_right") t)
+
+let is_michelson_pair (t: _ label_map) =
+  let l = LMap.to_list t in
+  List.fold_left
+    (fun prev {field_type=_;michelson_annotation} -> match michelson_annotation with
+      | Some _ -> true
+      | None -> prev)
+    false 
+    l
diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml
index 152c462dc..8612f2ece 100644
--- a/src/stages/4-ast_typed/misc.ml
+++ b/src/stages/4-ast_typed/misc.ml
@@ -342,9 +342,8 @@ let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) :
       | (TC_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
       | (TC_big_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_big_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
         -> ok @@ ([ka;va] ,[kb;vb]) 
-      | TC_michelson_or {l=la;r=ra}, TC_michelson_or {l=lb;r=rb} -> ok @@ ([la;ra] , [lb;rb])
-      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _| TC_michelson_or _ ),
-        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _| TC_michelson_or _ )
+      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _ ),
+        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _ )
         -> fail @@ different_operators opa opb
       in
       if List.length lsta <> List.length lstb then
@@ -357,7 +356,7 @@ let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) :
   | T_sum sa, T_sum sb -> (
       let sa' = CMap.to_kv_list sa in
       let sb' = CMap.to_kv_list sb in
-      let aux ((ka, va), (kb, vb)) =
+      let aux ((ka, {ctor_type=va;_}), (kb, {ctor_type=vb;_})) =
         let%bind _ =
           Assert.assert_true ~msg:"different keys in sum types"
           @@ (ka = kb) in
@@ -378,7 +377,7 @@ let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) :
       let sort_lmap r' = List.sort (fun (Label a,_) (Label b,_) -> String.compare a b) r' in
       let ra' = sort_lmap @@ LMap.to_kv_list ra in
       let rb' = sort_lmap @@ LMap.to_kv_list rb in
-      let aux ((ka, va), (kb, vb)) =
+      let aux ((ka, {field_type=va;_}), (kb, {field_type=vb;_})) =
         let%bind _ =
           trace (different_types "records" a b) @@
           let Label ka = ka in
diff --git a/src/stages/4-ast_typed/types.ml b/src/stages/4-ast_typed/types.ml
index 6ded1c8a0..a25734369 100644
--- a/src/stages/4-ast_typed/types.ml
+++ b/src/stages/4-ast_typed/types.ml
@@ -19,8 +19,8 @@ type type_constant =
     | TC_timestamp
     | TC_void
 
-type te_cmap = type_expression constructor_map
-and te_lmap = type_expression label_map
+type te_cmap = ctor_content constructor_map
+and te_lmap = field_content label_map
 and type_meta = ast_core_type_expression option
 
 and type_content =
@@ -36,6 +36,18 @@ and arrow = {
     type2: type_expression;
   }
 
+and annot_option = string option
+
+and ctor_content = {
+    ctor_type : type_expression;
+    michelson_annotation : annot_option;
+}
+
+and field_content = {
+    field_type : type_expression;
+    michelson_annotation : annot_option;
+}
+
 and type_map_args = {
     k : type_expression;
     v : type_expression;
@@ -54,7 +66,6 @@ and type_operator =
   | TC_map of type_map_args
   | TC_big_map of type_map_args
   | TC_map_or_big_map of type_map_args
-  | TC_michelson_or of michelson_or_args
   | TC_arrow of arrow
 
 
diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml
index 3b1e2441e..2d784057d 100644
--- a/src/stages/common/PP.ml
+++ b/src/stages/common/PP.ml
@@ -8,36 +8,8 @@ let constructor ppf (c:constructor') : unit =
 let label ppf (l:label) : unit =
   let Label l = l in fprintf ppf "%s" l
 
-let cmap_sep value sep ppf m =
-  let lst = CMap.to_kv_list m in
-  let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
-  let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" constructor k value v in
-  fprintf ppf "%a" (list_sep new_pp sep) lst
-
-let record_sep value sep ppf (m : 'a label_map) =
-  let lst = LMap.to_kv_list m in
-  let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
-  let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" label k value v in
-  fprintf ppf "%a" (list_sep new_pp sep) lst
-
-let tuple_sep value sep ppf m =
-  assert (Helpers.is_tuple_lmap m);
-  let lst = Helpers.tuple_of_record m in
-  let new_pp ppf (_, v) = fprintf ppf "%a" value v in
-  fprintf ppf "%a" (list_sep new_pp sep) lst
-
-(* Prints records which only contain the consecutive fields
-   0..(cardinal-1) as tuples *)
-let tuple_or_record_sep value format_record sep_record format_tuple sep_tuple ppf m =
-  if Helpers.is_tuple_lmap m then
-    fprintf ppf format_tuple (tuple_sep value (tag sep_tuple)) m
-  else
-    fprintf ppf format_record (record_sep value (tag sep_record)) m
 
 let list_sep_d x = list_sep x (tag " ,@ ")
-let cmap_sep_d x = cmap_sep x (tag " ,@ ")
-let tuple_or_record_sep_expr value = tuple_or_record_sep value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " ,@ "
-let tuple_or_record_sep_type value = tuple_or_record_sep value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " *@ "
 
 let constant ppf : constant' -> unit = function
   | C_INT                   -> fprintf ppf "INT"
@@ -200,6 +172,54 @@ module Ast_PP_type (PARAMETER : AST_PARAMETER_TYPE) = struct
   open Agt
   open Format
 
+  let cmap_sep value sep ppf m =
+    let lst = CMap.to_kv_list m in
+    let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
+    let new_pp ppf (k, {ctor_type;_}) = fprintf ppf "@[<h>%a -> %a@]" constructor k value ctor_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+  let cmap_sep_d x = cmap_sep x (tag " ,@ ")
+
+  let record_sep value sep ppf (m : 'a label_map) =
+    let lst = LMap.to_kv_list m in
+    let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+    let new_pp ppf (k, {field_type;_}) = fprintf ppf "@[<h>%a -> %a@]" label k value field_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let tuple_sep value sep ppf m =
+    assert (Helpers.is_tuple_lmap m);
+    let lst = Helpers.tuple_of_record m in
+    let new_pp ppf (_, {field_type;_}) = fprintf ppf "%a" value field_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let record_sep_expr value sep ppf (m : 'a label_map) =
+    let lst = LMap.to_kv_list m in
+    let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+    let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" label k value v in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let tuple_sep_expr value sep ppf m =
+    assert (Helpers.is_tuple_lmap m);
+    let lst = Helpers.tuple_of_record m in
+    let new_pp ppf (_,v) = fprintf ppf "%a" value v in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  (* Prints records which only contain the consecutive fields
+    0..(cardinal-1) as tuples *)
+  let tuple_or_record_sep_t value format_record sep_record format_tuple sep_tuple ppf m =
+    if Helpers.is_tuple_lmap m then
+      fprintf ppf format_tuple (tuple_sep value (tag sep_tuple)) m
+    else
+      fprintf ppf format_record (record_sep value (tag sep_record)) m
+
+  let tuple_or_record_sep_expr value format_record sep_record format_tuple sep_tuple ppf m =
+    if Helpers.is_tuple_lmap m then
+      fprintf ppf format_tuple (tuple_sep_expr value (tag sep_tuple)) m
+    else
+      fprintf ppf format_record (record_sep_expr value (tag sep_record)) m
+
+  let tuple_or_record_sep_expr value = tuple_or_record_sep_expr value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " ,@ "
+  let tuple_or_record_sep_type value = tuple_or_record_sep_t value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " *@ "
+
   let rec type_expression' :
          (formatter -> type_expression -> unit)
       -> formatter
@@ -231,7 +251,6 @@ module Ast_PP_type (PARAMETER : AST_PARAMETER_TYPE) = struct
       | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
       | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
       | TC_map_or_big_map (k, v) -> Format.asprintf "Map Or Big Map (%a,%a)" f k f v
-      | TC_michelson_or (k, v) -> Format.asprintf "michelson_or (%a,%a)" f k f v
       | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v
       | TC_contract te  -> Format.asprintf "Contract (%a)" f te
     in
diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml
index 6e68736aa..c2f7fba56 100644
--- a/src/stages/common/types.ml
+++ b/src/stages/common/types.ml
@@ -36,15 +36,21 @@ end
 module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
   open PARAMETER
 
+  type michelson_annotation = string
+
   type type_content =
-    | T_sum of type_expression constructor_map
-    | T_record of type_expression label_map
+    | T_sum of ctor_content constructor_map
+    | T_record of field_content label_map
     | T_arrow of arrow
     | T_variable of type_variable
     | T_constant of type_constant
     | T_operator of type_operator
 
   and arrow = {type1: type_expression; type2: type_expression}
+  
+  and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option}
+
+  and field_content = {field_type : type_expression ; field_annotation : string option}
 
   and type_operator =
     | TC_contract of type_expression
@@ -54,7 +60,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map of type_expression * type_expression
     | TC_big_map of type_expression * type_expression
     | TC_map_or_big_map of type_expression * type_expression
-    | TC_michelson_or of type_expression * type_expression
     | TC_arrow of type_expression * type_expression
 
 
@@ -69,7 +74,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map (x , y) -> TC_map (f x , f y)
     | TC_big_map (x , y)-> TC_big_map (f x , f y)
     | TC_map_or_big_map (x , y)-> TC_map_or_big_map (f x , f y)
-    | TC_michelson_or (x , y)-> TC_michelson_or (f x , f y)
     | TC_arrow (x, y) -> TC_arrow (f x, f y)
 
   let bind_map_type_operator f = function
@@ -80,7 +84,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y)
     | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
     | TC_map_or_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_map_or_big_map (x , y)
-    | TC_michelson_or (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_michelson_or (x , y)
     | TC_arrow (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y)
 
   let type_operator_name = function
@@ -91,7 +94,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
       | TC_map      _ -> "TC_map"
       | TC_big_map  _ -> "TC_big_map"
       | TC_map_or_big_map _ -> "TC_map_or_big_map"
-      | TC_michelson_or _ -> "TC_michelson_or"
       | TC_arrow    _ -> "TC_arrow"
 
   let type_expression'_of_string = function
@@ -131,7 +133,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map            (x , y) -> "TC_map"          , [x ; y]
     | TC_big_map        (x , y) -> "TC_big_map"      , [x ; y]
     | TC_map_or_big_map (x , y) -> "TC_map_or_big_map"  , [x ; y]
-    | TC_michelson_or   (x , y) -> "TC_michelson_or" , [x ; y]
     | TC_arrow          (x , y) -> "TC_arrow"        , [x ; y]
 
   let string_of_type_constant = function
diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml
index f6e362c3b..cf7dd41b8 100644
--- a/src/stages/typesystem/core.ml
+++ b/src/stages/typesystem/core.ml
@@ -15,7 +15,6 @@ type constant_tag =
   | C_variant   (* ( label , * ) … -> * *)
   | C_map       (* * -> * -> * *)
   | C_big_map   (* * -> * -> * *)
-  | C_michelson_or (* * -> * -> * *)
   | C_list      (* * -> * *)
   | C_set       (* * -> * *)
   | C_unit      (* * *)
@@ -76,11 +75,10 @@ let type_expression'_of_simple_c_constant = function
   | C_set       , [x]     -> ok @@ Ast_typed.T_operator(TC_set x)
   | C_map       , [k ; v] -> ok @@ Ast_typed.T_operator(TC_map {k ; v})
   | C_big_map   , [k ; v] -> ok @@ Ast_typed.T_operator(TC_big_map {k ; v})
-  | C_michelson_or , [l ; r] -> ok @@ Ast_typed.T_operator(TC_michelson_or {l ; r})
   | C_arrow     , [x ; y] -> ok @@ Ast_typed.T_operator(TC_arrow {type1=x ; type2=y})
   | C_record    , _lst    -> ok @@ failwith "records are not supported yet: T_record lst"
   | C_variant   , _lst    -> ok @@ failwith "sums are not supported yet: T_sum lst"
-  | (C_contract | C_option | C_list | C_set | C_map | C_big_map | C_arrow | C_michelson_or ), _ ->
+  | (C_contract | C_option | C_list | C_set | C_map | C_big_map | C_arrow ), _ ->
      failwith "internal error: wrong number of arguments for type operator"
 
   | C_unit      , [] -> ok @@ Ast_typed.T_constant(TC_unit)
diff --git a/src/test/contracts/double_michelson_or.ligo b/src/test/contracts/double_michelson_or.ligo
index e1b1d6595..3250ec37d 100644
--- a/src/test/contracts/double_michelson_or.ligo
+++ b/src/test/contracts/double_michelson_or.ligo
@@ -1,5 +1,5 @@
-type storage is michelson_or (int, string)
-type foobar is michelson_or (int, int)
+type storage is michelson_or (int,"foo",string,"bar")
+type foobar is michelson_or (int,"baz",int,"fooo")
 
 type return is list (operation) * storage 
 
diff --git a/src/test/contracts/double_michelson_or.mligo b/src/test/contracts/double_michelson_or.mligo
index f69f2b151..9b497b72e 100644
--- a/src/test/contracts/double_michelson_or.mligo
+++ b/src/test/contracts/double_michelson_or.mligo
@@ -1,5 +1,5 @@
-type storage = (int,string) michelson_or 
-type foobar = (int, int ) michelson_or
+type storage = (int,"foo",string,"bar") michelson_or 
+type foobar = (int,"baz", int, "fooo" ) michelson_or
 
 type return = operation list * storage
 
diff --git a/src/test/contracts/michelson_or_tree.ligo b/src/test/contracts/michelson_or_tree.ligo
new file mode 100644
index 000000000..96e0f5850
--- /dev/null
+++ b/src/test/contracts/michelson_or_tree.ligo
@@ -0,0 +1,8 @@
+type inner_storage is michelson_or(int,"one",nat,"two")
+type storage is michelson_or (int,"three",inner_storage,"four")
+
+type return is list(operation) * storage
+
+function main (const action : unit; const store : storage) : return is block {
+  const foo : storage = (M_right ((M_left(1) : inner_storage)) : storage) ;
+} with ((nil : list(operation)), (foo: storage))
diff --git a/src/test/contracts/michelson_or_tree.mligo b/src/test/contracts/michelson_or_tree.mligo
index 6f08f67bc..943f4506c 100644
--- a/src/test/contracts/michelson_or_tree.mligo
+++ b/src/test/contracts/michelson_or_tree.mligo
@@ -1,5 +1,5 @@
-type inner_storage = (int,nat) michelson_or
-type storage = (int,inner_storage) michelson_or 
+type inner_storage = (int,"one",nat,"two") michelson_or
+type storage = (int,"three",inner_storage,"four") michelson_or 
 
 type return = operation list * storage
 
diff --git a/src/test/contracts/michelson_pair_tree.ligo b/src/test/contracts/michelson_pair_tree.ligo
new file mode 100644
index 000000000..10a659251
--- /dev/null
+++ b/src/test/contracts/michelson_pair_tree.ligo
@@ -0,0 +1,8 @@
+type inner_storage is michelson_pair(int,"one",nat,"two")
+type storage is michelson_pair (string,"three",inner_storage,"four")
+
+type return is list(operation) * storage
+
+function main (const action : unit; const store : storage) : return is block {
+  const foo : storage = ("foo",(1,2n)) ;
+} with ((nil : list(operation)), (foo: storage))
diff --git a/src/test/contracts/michelson_pair_tree.mligo b/src/test/contracts/michelson_pair_tree.mligo
new file mode 100644
index 000000000..55624bbb4
--- /dev/null
+++ b/src/test/contracts/michelson_pair_tree.mligo
@@ -0,0 +1,8 @@
+type inner_storage = (int,"one",nat,"two") michelson_pair
+type storage = (int,"three",inner_storage,"four") michelson_pair
+
+type return = operation list * storage
+
+let main (action, store : unit * storage) : return =
+  let foo = (3,(1,2n)) in
+  (([] : operation list), (foo: storage))
\ No newline at end of file
diff --git a/src/test/contracts/michelson_pair_tree.religo b/src/test/contracts/michelson_pair_tree.religo
new file mode 100644
index 000000000..8fa2c827b
--- /dev/null
+++ b/src/test/contracts/michelson_pair_tree.religo
@@ -0,0 +1,9 @@
+type inner_storage = michelson_pair(int,"one",nat,"two");
+type storage = michelson_pair(int,"three",inner_storage,"four");
+
+type return = (list (operation) , storage);
+
+let main = ((action, store) : (unit , storage)) : return => {
+  let foo = (3,(1,2n)) ;
+  (([] : list(operation)), (foo: storage))
+};
\ No newline at end of file
diff --git a/src/test/contracts/negative/bad_michelson_or.mligo b/src/test/contracts/negative/bad_michelson_or.mligo
index 08c7fe035..1b4cdec56 100644
--- a/src/test/contracts/negative/bad_michelson_or.mligo
+++ b/src/test/contracts/negative/bad_michelson_or.mligo
@@ -1,4 +1,4 @@
-type storage = (int,string) michelson_or 
+type storage = (int,"foo",string,"bar") michelson_or 
 
 type return = operation list * storage
 
diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml
index a29963d7e..7dd3f1f42 100644
--- a/src/test/typer_tests.ml
+++ b/src/test/typer_tests.ml
@@ -55,8 +55,9 @@ module TestExpressions = struct
       O.(make_t_ez_record [("0",t_int ()); ("1",t_string ())])
 
   let constructor () : unit result =
-    let variant_foo_bar =
-      O.[(Typed.Constructor "foo", t_int ()); (Constructor "bar", t_string ())]
+    let variant_foo_bar : (Typed.constructor' * Typed.ctor_content) list = [
+        (Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None});
+        (Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None}) ]
     in test_expression
       ~env:(E.env_sum_type variant_foo_bar)
       I.(e_constructor "foo" (e_int 32))