Merge branch 'clean-sts-solver' into 'dev'

New typer in a separate folder along with old typer

See merge request ligolang/ligo!166

scripts/setup_repos.sh

@@ -5,7 +5,7 @@ set -x
 eval $(opam config env)
 
 # Remove the nomadic-labs tezos repo (from ligo switch only)
-opam repository remove tezos-opam-repository
+opam repository remove tezos-opam-repository || true
 
 # Add ligolang tezos repo
 opam repository add ligolang-tezos-opam-repository https://gitlab.com/ligolang/tezos-opam-repository.git

src/bin/cli.ml

@@ -183,9 +183,11 @@ let evaluate_value =
 let compile_expression =
   let f expression syntax display_format michelson_format =
     toplevel ~display_format @@
+    (* This is an actual compiler entry-point, so we start with a blank state *)
+    let state = Typer.Solver.initial_state in
     let%bind value =
       trace (simple_error "compile-input") @@
-      Ligo.Run.Of_source.compile_expression expression (Syntax_name syntax) in
+      Ligo.Run.Of_source.compile_expression expression state (Syntax_name syntax) in
     ok @@ Format.asprintf "%a\n" (Main.Display.michelson_pp michelson_format) value
   in
   let term =

src/main/compile/dune

@@ -8,6 +8,7 @@
     simplify
     ast_simplified
     self_ast_simplified
+    typer_new
     typer
     ast_typed
     transpiler

src/main/compile/of_simplified.ml

@@ -3,23 +3,41 @@ open Trace
 open Tezos_utils
 
 let compile_contract_entry (program : program) entry_point =
-  let%bind prog_typed = Typer.type_program program in
+  let%bind (prog_typed , state) = Typer.type_program program in
+  let () = Typer.Solver.discard_state state in
   Of_typed.compile_contract_entry prog_typed entry_point
 
 let compile_function_entry (program : program) entry_point : _ result =
-  let%bind prog_typed = Typer.type_program program in
+  let%bind (prog_typed , state) = Typer.type_program program in
+  let () = Typer.Solver.discard_state state in
   Of_typed.compile_function_entry prog_typed entry_point
 
 let compile_expression_as_function_entry (program : program) entry_point : _ result =
-  let%bind typed_program = Typer.type_program program in
+  let%bind (typed_program , state) = Typer.type_program program in
+  let () = Typer.Solver.discard_state state in
   Of_typed.compile_expression_as_function_entry typed_program entry_point
 
-let compile_expression_as_value ?(env = Ast_typed.Environment.full_empty) ae : Michelson.t result =
-  let%bind typed = Typer.type_expression env ae in
+(* TODO: do we need to thread the state here? Also, make the state arg. optional. *)
+let compile_expression_as_value ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) ae : Michelson.t result =
+  let%bind (typed , state) = Typer.type_expression env state ae in
+  (* TODO: move this to typer.ml *)
+  let typed =
+    if Typer.use_new_typer then
+      let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in typed
+    else
+      typed
+  in
   Of_typed.compile_expression_as_value typed
 
-let compile_expression_as_function ?(env = Ast_typed.Environment.full_empty) ae : _ result =
-  let%bind typed = Typer.type_expression env ae in
+let compile_expression_as_function ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression) : _ result =
+  let%bind (typed , state) = Typer.type_expression env state ae in
+  (* TODO: move this to typer.ml *)
+  let typed =
+    if false then
+      let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in typed
+    else
+      typed
+  in
   Of_typed.compile_expression_as_function typed
 
 let uncompile_typed_program_entry_expression_result program entry ex_ty_value =

src/main/compile/of_source.ml

@@ -21,19 +21,19 @@ let compile_expression_as_function : string -> s_syntax -> _ result =
   fun expression syntax ->
   let%bind syntax = syntax_to_variant syntax None in
   let%bind simplified = parsify_expression syntax expression in
-  Of_simplified.compile_expression_as_function simplified
+  Of_simplified.compile_expression_as_function ~state:Typer.Solver.initial_state (* TODO: thread state or start with initial? *) simplified
 
 let type_file ?(debug_simplify = false) ?(debug_typed = false)
-    syntax (source_filename:string) : Ast_typed.program result =
+    syntax (source_filename:string) : (Ast_typed.program * Typer.Solver.state) result =
   let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind simpl = parsify syntax source_filename in
   (if debug_simplify then
      Format.(printf "Simplified : %a\n%!" Ast_simplified.PP.program simpl)
   ) ;
-  let%bind typed =
+  let%bind (typed, state) =
     trace (simple_error "typing") @@
     Typer.type_program simpl in
   (if debug_typed then (
       Format.(printf "Typed : %a\n%!" Ast_typed.PP.program typed)
     )) ;
-  ok typed
+  ok (typed, state)

src/main/run/dune

@@ -7,6 +7,7 @@
     parser
     simplify
     ast_simplified
+    typer_new
     typer
     ast_typed
     transpiler

src/main/run/of_simplified.ml

@@ -1,24 +1,24 @@
 open Trace
 open Ast_simplified
 
-let compile_expression ?(value = false) ?env expr =
+let compile_expression ?(value = false) ?env ~state expr = (* TODO: state optional *)
   if value
   then (
-    Compile.Of_simplified.compile_expression_as_value ?env expr
+    Compile.Of_simplified.compile_expression_as_value ?env ~state expr
   )
   else (
-    let%bind code = Compile.Of_simplified.compile_expression_as_function ?env expr in
+    let%bind code = Compile.Of_simplified.compile_expression_as_function ?env ~state expr in
     Of_michelson.evaluate_michelson code
   )
 
-let run_typed_program
+let run_typed_program           (* TODO: this runs an *untyped* program, not a typed one. *)
     ?options ?input_to_value
-    (program : Ast_typed.program) (entry : string)
+    (program : Ast_typed.program) (state : Typer.Solver.state) (entry : string)
     (input : expression) : expression result =
   let%bind code = Compile.Of_typed.compile_function_entry program entry in
   let%bind input =
     let env = Ast_typed.program_environment program in
-    compile_expression ?value:input_to_value ~env input
+    compile_expression ?value:input_to_value ~env ~state input
   in
   let%bind ex_ty_value = Of_michelson.run ?options code input in
   Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry ex_ty_value

src/main/run/of_source.ml

@@ -50,43 +50,43 @@ end
 
 let compile_file_contract_parameter : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result =
   fun source_filename _entry_point expression syntax ->
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
   let env = Ast_typed.program_environment program in
   let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in
   let%bind simplified = Compile.Helpers.parsify_expression syntax expression in
-  Of_simplified.compile_expression simplified ~env
+  Of_simplified.compile_expression simplified ~env ~state
 
 let compile_file_expression : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result =
   fun source_filename _entry_point expression syntax ->
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
   let env = Ast_typed.program_environment program in
   let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in
   let%bind simplified = Compile.Helpers.parsify_expression syntax expression in
-  Of_simplified.compile_expression simplified ~env
+  Of_simplified.compile_expression simplified ~env ~state
 
-let compile_expression : string -> Compile.Helpers.s_syntax -> Michelson.t result =
-  fun expression syntax ->
+let compile_expression : string -> Typer.Solver.state -> Compile.Helpers.s_syntax -> Michelson.t result =
+  fun expression state syntax ->
   let%bind syntax = Compile.Helpers.syntax_to_variant syntax None in
   let%bind simplified = Compile.Helpers.parsify_expression syntax expression in
-  Of_simplified.compile_expression simplified
+  Of_simplified.compile_expression ~state simplified
 
 let compile_file_contract_storage ~value : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result =
   fun source_filename _entry_point expression syntax ->
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
   let env = Ast_typed.program_environment program in
   let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in
   let%bind simplified = Compile.Helpers.parsify_expression syntax expression in
-  Of_simplified.compile_expression ~value simplified ~env
+  Of_simplified.compile_expression ~value simplified ~env ~state
 
 let compile_file_contract_args =
   fun ?value source_filename _entry_point storage parameter syntax ->
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
   let env = Ast_typed.program_environment program in
   let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in
   let%bind storage_simplified = Compile.Helpers.parsify_expression syntax storage in
   let%bind parameter_simplified = Compile.Helpers.parsify_expression syntax parameter in
   let args = Ast_simplified.e_pair storage_simplified parameter_simplified in
-  Of_simplified.compile_expression ?value args ~env
+  Of_simplified.compile_expression ?value args ~env ~state
 
 type dry_run_options =
   { amount : string ;
@@ -121,7 +121,8 @@ let make_dry_run_options (opts : dry_run_options) : Of_michelson.options result
   ok @@ make_options ~amount ?source:sender ?payer:source ()
 
 let run_contract ~options ?storage_value source_filename entry_point storage parameter syntax =
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
+  let () = Typer.Solver.discard_state state in
   let%bind code = Compile.Of_typed.compile_function_entry program entry_point in
   let%bind args = compile_file_contract_args ?value:storage_value source_filename entry_point storage parameter syntax in
   let%bind options = make_dry_run_options options in
@@ -129,7 +130,8 @@ let run_contract ~options ?storage_value source_filename entry_point storage par
   Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry_point ex_value_ty
 
 let run_function_entry ~options source_filename entry_point input syntax =
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
+  let () = Typer.Solver.discard_state state in
   let%bind code = Compile.Of_typed.compile_function_entry program entry_point in
   let%bind args = compile_file_expression source_filename entry_point input syntax in
   let%bind options = make_dry_run_options options in
@@ -137,7 +139,8 @@ let run_function_entry ~options source_filename entry_point input syntax =
   Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry_point ex_value_ty
 
 let evaluate_entry ~options source_filename entry_point syntax =
-  let%bind program = Compile.Of_source.type_file syntax source_filename in
+  let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in
+  let () = Typer.Solver.discard_state state in
   let%bind code = Compile.Of_typed.compile_expression_as_function_entry program entry_point in
   let%bind options = make_dry_run_options options in
   let%bind ex_value_ty = Of_michelson.evaluate ~options code in

src/passes/4-typer-new/dune

@@ -0,0 +1,16 @@
+(library
+  (name typer_new)
+  (public_name ligo.typer_new)
+  (libraries
+    simple-utils
+    tezos-utils
+    ast_simplified
+    ast_typed
+    operators
+    union_find
+  )
+  (preprocess
+    (pps ppx_let)
+  )
+  (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
+)

src/passes/4-typer-new/typer.ml.old

@@ -0,0 +1,879 @@
+open Trace
+
+module I = Ast_simplified
+module O = Ast_typed
+open O.Combinators
+
+module SMap = O.SMap
+
+module Environment = O.Environment
+
+type environment = Environment.t
+
+module Errors = struct
+  let unbound_type_variable (e:environment) (n:string) () =
+    let title = (thunk "unbound type variable") in
+    let message () = "" in
+    let data = [
+      ("variable" , fun () -> Format.asprintf "%s" n) ;
+      (* TODO: types don't have srclocs for now. *)
+      (* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
+      ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
+    ] in
+    error ~data title message ()
+
+  let unbound_variable (e:environment) (n:string) (loc:Location.t) () =
+    let title = (thunk "unbound variable") in
+    let message () = "" in
+    let data = [
+      ("variable" , fun () -> Format.asprintf "%s" n) ;
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "match with no cases") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let unbound_constructor (e:environment) (n:string) (loc:Location.t) () =
+    let title = (thunk "unbound constructor") in
+    let message () = "" in
+    let data = [
+      ("constructor" , fun () -> Format.asprintf "%s" n) ;
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let unrecognized_constant (n:string) (loc:Location.t) () =
+    let title = (thunk "unrecognized constant") in
+    let message () = "" in
+    let data = [
+      ("constant" , fun () -> Format.asprintf "%s" n) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
+    let title () = "wrong arity" in
+    let message () = "" in
+    let data = [
+      ("function" , fun () -> Format.asprintf "%s" n) ;
+      ("expected" , fun () -> Format.asprintf "%d" expected) ;
+      ("actual" , fun () -> Format.asprintf "%d" actual) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
+    let title () = "matching tuple of different size" in
+    let message () = "" in
+    let data = [
+      ("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
+      ("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  (* TODO: this should be a trace_info? *)
+  let program_error (p:I.program) () =
+    let message () = "" in
+    let title = (thunk "typing program") in
+    let data = [
+      ("program" , fun () -> Format.asprintf "%a" I.PP.program p)
+    ] in
+    error ~data title message ()
+
+  let constant_declaration_error (name:string) (ae:I.expr) (expected: O.type_expression option) () =
+    let title = (thunk "typing constant declaration") in
+    let message () = "" in
+    let data = [
+      ("constant" , fun () -> Format.asprintf "%s" name) ;
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("expected" , fun () ->
+          match expected with
+            None -> "(no annotation for the expected type)"
+          | Some expected -> Format.asprintf "%a" O.PP.type_expression expected) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
+    ] in
+    error ~data title message ()
+
+  let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_expression -> Location.t -> unit -> _ =
+    fun ?(msg = "") ~expected ~actual loc () ->
+    let title = (thunk "typing match") in
+    let message () = msg in
+    let data = [
+      ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
+      ("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let needs_annotation (e : I.expression) (case : string) () =
+    let title = (thunk "this expression must be annotated with its type") in
+    let message () = Format.asprintf "%s needs an annotation" case in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
+    ] in
+    error ~data title message ()
+
+  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%s" expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%a" O.PP.type_expression expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () =
+    let title = (thunk "invalid tuple index") in
+    let message () = "" in
+    let data = [
+      ("index" , fun () -> Format.asprintf "%d" index) ;
+      ("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let bad_record_access (field : string) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () =
+    let title = (thunk "invalid record field") in
+    let message () = "" in
+    let data = [
+      ("field" , fun () -> Format.asprintf "%s" field) ;
+      ("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet (message : string) (ae : I.expression) () =
+    let title = (thunk "not supported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  I.PP.expression ae) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
+    let title = (thunk "not supported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  O.PP.expression ae)
+    ] in
+    error ~data title message ()
+
+  let constant_error loc lst tv_opt =
+    let title () = "typing constant" in
+    let message () = "" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
+      ("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_expression (const " , ")) lst) ;
+      ("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_expression) tv_opt) ;
+    ] in
+    error ~data title message
+end
+open Errors
+
+let rec type_program (p:I.program) : O.program result =
+  let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
+    let%bind ed' = (bind_map_location (type_declaration e)) d in
+    let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
+    let (e', d') = Location.unwrap ed' in
+    match d' with
+    | None -> ok (e', acc)
+    | Some d' -> ok (e', loc ed' d' :: acc)
+  in
+  let%bind (_, lst) =
+    trace (fun () -> program_error p ()) @@
+    bind_fold_list aux (Environment.full_empty, []) p in
+  ok @@ List.rev lst
+
+and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
+  | Declaration_type (type_name , type_expression) ->
+      let%bind tv = evaluate_type env type_expression in
+      let env' = Environment.add_type type_name tv env in
+      ok (env', None)
+  | Declaration_constant (name , tv_opt , expression) -> (
+      let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
+      let%bind ae' =
+        trace (constant_declaration_error name expression tv'_opt) @@
+        type_expression ?tv_opt:tv'_opt env expression in
+      let env' = Environment.add_ez_ae name ae' env in
+      ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
+    )
+
+and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_expression -> i I.matching -> I.expression -> Location.t -> o O.matching result =
+  fun f e t i ae loc -> match i with
+    | Match_bool {match_true ; match_false} ->
+      let%bind _ =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_bool t in
+      let%bind match_true = f e match_true in
+      let%bind match_false = f e match_false in
+      ok (O.Match_bool {match_true ; match_false})
+  | Match_option {match_none ; match_some} ->
+      let%bind t_opt =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_option t in
+      let%bind match_none = f e match_none in
+      let (n, b) = match_some in
+      let n' = n, t_opt in
+      let e' = Environment.add_ez_binder n t_opt e in
+      let%bind b' = f e' b in
+      ok (O.Match_option {match_none ; match_some = (n', b')})
+  | Match_list {match_nil ; match_cons} ->
+      let%bind t_list =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_list t in
+      let%bind match_nil = f e match_nil in
+      let (hd, tl, b) = match_cons in
+      let e' = Environment.add_ez_binder hd t_list e in
+      let e' = Environment.add_ez_binder tl t e' in
+      let%bind b' = f e' b in
+      ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
+  | Match_tuple (lst, b) ->
+      let%bind t_tuple =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_tuple t in
+      let%bind lst' =
+        generic_try (match_tuple_wrong_arity t_tuple lst loc)
+        @@ (fun () -> List.combine lst t_tuple) in
+      let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
+      let e' = List.fold_left aux e lst' in
+      let%bind b' = f e' b in
+      ok (O.Match_tuple (lst, b'))
+  | Match_variant lst ->
+      let%bind variant_opt =
+        let aux acc ((constructor_name , _) , _) =
+          let%bind (_ , variant) =
+            trace_option (unbound_constructor e constructor_name loc) @@
+            Environment.get_constructor constructor_name e in
+          let%bind acc = match acc with
+            | None -> ok (Some variant)
+            | Some variant' -> (
+                trace (type_error
+                         ~msg:"in match variant"
+                         ~expected:variant
+                         ~actual:variant'
+                         ~expression:ae
+                         loc
+                      ) @@
+                Ast_typed.assert_type_expression_eq (variant , variant') >>? fun () ->
+                ok (Some variant)
+              ) in
+          ok acc in
+        trace (simple_info "in match variant") @@
+        bind_fold_list aux None lst in
+      let%bind variant =
+        trace_option (match_empty_variant i loc) @@
+        variant_opt in
+      let%bind () =
+        let%bind variant_cases' =
+          trace (match_error ~expected:i ~actual:t loc)
+          @@ Ast_typed.Combinators.get_t_sum variant in
+        let variant_cases = List.map fst @@ Map.String.to_kv_list variant_cases' in
+        let match_cases = List.map (Function.compose fst fst) lst in
+        let test_case = fun c ->
+          Assert.assert_true (List.mem c match_cases)
+        in
+        let%bind () =
+          trace_strong (match_missing_case i loc) @@
+          bind_iter_list test_case variant_cases in
+        let%bind () =
+          trace_strong (match_redundant_case i loc) @@
+          Assert.assert_true List.(length variant_cases = length match_cases) in
+        ok ()
+      in
+      let%bind lst' =
+        let aux ((constructor_name , name) , b) =
+          let%bind (constructor , _) =
+            trace_option (unbound_constructor e constructor_name loc) @@
+            Environment.get_constructor constructor_name e in
+          let e' = Environment.add_ez_binder name constructor e in
+          let%bind b' = f e' b in
+          ok ((constructor_name , name) , b')
+        in
+        bind_map_list aux lst in
+      ok (O.Match_variant (lst' , variant))
+
+and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result =
+  let return tv' = ok (make_t tv' (Some t)) in
+  match t with
+  | T_function (a, b) ->
+      let%bind a' = evaluate_type e a in
+      let%bind b' = evaluate_type e b in
+      return (T_function (a', b'))
+  | T_tuple lst ->
+      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
+      return (T_tuple lst')
+  | T_sum m ->
+      let aux k v prev =
+        let%bind prev' = prev in
+        let%bind v' = evaluate_type e v in
+        ok @@ SMap.add k v' prev'
+      in
+      let%bind m = SMap.fold aux m (ok SMap.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 @@ SMap.add k v' prev'
+      in
+      let%bind m = SMap.fold aux m (ok SMap.empty) in
+      return (T_record m)
+  | T_variable name ->
+      let%bind tv =
+        trace_option (unbound_type_variable e name)
+        @@ Environment.get_type_opt name e in
+      ok tv
+  | T_constant (cst, lst) ->
+      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
+      return (T_constant(cst, lst'))
+
+and type_expression : environment -> ?tv_opt:O.type_expression -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
+  let module L = Logger.Stateful() in
+  let return expr tv =
+    let%bind () =
+      match tv_opt with
+      | None -> ok ()
+      | Some tv' -> O.assert_type_expression_eq (tv' , tv) in
+    let location = Location.get_location ae in
+    ok @@ make_a_e ~location expr tv e in
+  let main_error =
+    let title () = "typing expression" in
+    let content () = "" in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp @@ Location.get_location ae) ;
+      ("misc" , fun () -> L.get ()) ;
+    ] in
+    error ~data title content in
+  trace main_error @@
+  match Location.unwrap ae with
+  (* Basic *)
+  | E_failwith _ -> fail @@ needs_annotation ae "the failwith keyword"
+  | E_variable name ->
+      let%bind tv' =
+        trace_option (unbound_variable e name ae.location)
+        @@ Environment.get_opt name e in
+      return (E_variable name) tv'.type_expression
+  | E_literal (Literal_bool b) ->
+      return (E_literal (Literal_bool b)) (t_bool ())
+  | E_literal Literal_unit | E_skip ->
+      return (E_literal (Literal_unit)) (t_unit ())
+  | E_literal (Literal_string s) -> (
+      L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
+      match Option.map Ast_typed.get_type' tv_opt with
+      | Some (T_constant ("address" , [])) -> return (E_literal (Literal_address s)) (t_address ())
+      | _ -> return (E_literal (Literal_string s)) (t_string ())
+    )
+  | E_literal (Literal_bytes s) ->
+      return (E_literal (Literal_bytes s)) (t_bytes ())
+  | E_literal (Literal_int n) ->
+      return (E_literal (Literal_int n)) (t_int ())
+  | E_literal (Literal_nat n) ->
+      return (E_literal (Literal_nat n)) (t_nat ())
+  | E_literal (Literal_timestamp n) ->
+      return (E_literal (Literal_timestamp n)) (t_timestamp ())
+  | E_literal (Literal_tez n) ->
+      return (E_literal (Literal_tez n)) (t_tez ())
+  | E_literal (Literal_address s) ->
+      return (e_address s) (t_address ())
+  | E_literal (Literal_operation op) ->
+      return (e_operation op) (t_operation ())
+  (* Tuple *)
+  | E_tuple lst ->
+      let%bind lst' = bind_list @@ List.map (type_expression e) lst in
+      let tv_lst = List.map get_type_annotation lst' in
+      return (E_tuple lst') (t_tuple tv_lst ())
+  | E_accessor (ae', path) ->
+      let%bind e' = type_expression e ae' in
+      let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
+        match a with
+        | Access_tuple index -> (
+            let%bind tpl_tv = get_t_tuple prev.type_annotation in
+            let%bind tv =
+              generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
+              @@ (fun () -> List.nth tpl_tv index) in
+            return (E_tuple_accessor (prev , index)) tv
+          )
+        | Access_record property -> (
+            let%bind r_tv = get_t_record prev.type_annotation in
+            let%bind tv =
+              generic_try (bad_record_access property ae' prev.type_annotation ae.location)
+              @@ (fun () -> SMap.find property r_tv) in
+            return (E_record_accessor (prev , property)) tv
+          )
+        | Access_map ae' -> (
+            let%bind ae'' = type_expression e ae' in
+            let%bind (k , v) = get_t_map prev.type_annotation in
+            let%bind () =
+              Ast_typed.assert_type_expression_eq (k , get_type_annotation ae'') in
+            return (E_look_up (prev , ae'')) v
+          )
+      in
+      trace (simple_info "accessing") @@
+      bind_fold_list aux e' path
+
+  (* Sum *)
+  | E_constructor (c, expr) ->
+      let%bind (c_tv, sum_tv) =
+        let error =
+          let title () = "no such constructor" in
+          let content () =
+            Format.asprintf "%s in:\n%a\n"
+              c O.Environment.PP.full_environment e
+          in
+          error title content in
+        trace_option error @@
+        Environment.get_constructor c e in
+      let%bind expr' = type_expression e expr in
+      let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in
+      return (E_constructor (c , expr')) sum_tv
+  (* Record *)
+  | E_record m ->
+      let aux prev k expr =
+        let%bind expr' = type_expression e expr in
+        ok (SMap.add k expr' prev)
+      in
+      let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
+      return (E_record m') (t_record (SMap.map get_type_annotation m') ())
+  (* Data-structure *)
+  | E_list lst ->
+      let%bind lst' = bind_map_list (type_expression e) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
+              ok (Some c') in
+        let%bind init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = get_t_list ty in
+              ok (Some ty') in
+        let%bind ty =
+          let%bind opt = bind_fold_list aux init
+          @@ List.map get_type_annotation lst' in
+          trace_option (needs_annotation ae "empty list") opt in
+        ok (t_list ty ())
+      in
+      return (E_list lst') tv
+  | E_set lst ->
+      let%bind lst' = bind_map_list (type_expression e) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
+              ok (Some c') in
+        let%bind init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = get_t_set ty in
+              ok (Some ty') in
+        let%bind ty =
+          let%bind opt = bind_fold_list aux init
+          @@ List.map get_type_annotation lst' in
+          trace_option (needs_annotation ae "empty set") opt in
+        ok (t_set ty ())
+      in
+      return (E_set lst') tv
+  | E_map lst ->
+      let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in
+              ok (Some c') in
+        let%bind key_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map fst lst' in
+          let%bind annot = bind_map_option get_t_map_key tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        let%bind value_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map snd lst' in
+          let%bind annot = bind_map_option get_t_map_value tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        ok (t_map key_type value_type ())
+      in
+      return (E_map lst') tv
+  | E_lambda {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } -> (
+      let%bind input_type =
+        let%bind input_type =
+          (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
+          let default_action e () = fail @@ (needs_annotation e "the returned value") in
+          match input_type with
+          | Some ty -> ok ty
+          | None -> (
+              match Location.unwrap result with
+              | I.E_let_in li -> (
+                  match Location.unwrap li.rhs with
+                  | I.E_variable name when name = (fst binder) -> (
+                      match snd li.binder with
+                      | Some ty -> ok ty
+                      | None -> default_action li.rhs ()
+                    )
+                  | _ -> default_action li.rhs ()
+                )
+              | _ -> default_action result ()
+            )
+        in
+        evaluate_type e input_type in
+      let%bind output_type =
+        bind_map_option (evaluate_type e) output_type
+      in
+      let e' = Environment.add_ez_binder (fst binder) input_type e in
+      let%bind result = type_expression ?tv_opt:output_type e' result in
+      let output_type = result.type_annotation in
+      return (E_lambda {binder = fst binder;input_type;output_type;result}) (t_function input_type output_type ())
+    )
+  | E_constant (name, lst) ->
+      let%bind lst' = bind_list @@ List.map (type_expression e) lst in
+      let tv_lst = List.map get_type_annotation lst' in
+      let%bind (name', tv) =
+        type_constant name tv_lst tv_opt ae.location in
+      return (E_constant (name' , lst')) tv
+  | E_application (f, arg) ->
+      let%bind f' = type_expression e f in
+      let%bind arg = type_expression e arg in
+      let%bind tv = match f'.type_annotation.type_expression' with
+        | T_function (param, result) ->
+            let%bind _ = O.assert_type_expression_eq (param, arg.type_annotation) in
+            ok result
+        | _ ->
+          fail @@ type_error_approximate
+            ~expected:"should be a function type"
+            ~expression:f
+            ~actual:f'.type_annotation
+            f'.location
+      in
+      return (E_application (f' , arg)) tv
+  | E_look_up dsi ->
+      let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
+      let%bind (src, dst) = get_t_map ds.type_annotation in
+      let%bind _ = O.assert_type_expression_eq (ind.type_annotation, src) in
+      return (E_look_up (ds , ind)) (t_option dst ())
+  (* Advanced *)
+  | E_matching (ex, m) -> (
+      let%bind ex' = type_expression e ex in
+      match m with
+      (* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
+      | I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> (
+          let%bind fw = I.get_e_failwith match_true in
+          let%bind fw' = type_expression e fw in
+          let%bind mf' = type_expression e match_false in
+          let t = get_type_annotation ex' in
+          let%bind () =
+            trace_strong (match_error ~expected:m ~actual:t ae.location)
+            @@ assert_t_bool t in
+          let%bind () =
+            trace_strong (match_error
+                            ~msg:"matching not-unit on an assert"
+                            ~expected:m
+                            ~actual:t
+                            ae.location)
+            @@ assert_t_unit (get_type_annotation mf') in
+          let mt' = make_a_e
+              (E_constant ("ASSERT_INFERRED" , [ex' ; fw']))
+              (t_unit ())
+              e
+          in
+          let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in
+          return (O.E_matching (ex' , m')) (t_unit ())
+        )
+      | _ -> (
+          let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
+          let tvs =
+            let aux (cur:O.value O.matching) =
+              match cur with
+              | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
+              | Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ]
+              | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
+              | Match_tuple (_ , match_tuple) -> [ match_tuple ]
+              | Match_variant (lst , _) -> List.map snd lst in
+            List.map get_type_annotation @@ aux m' in
+          let aux prec cur =
+            let%bind () =
+              match prec with
+              | None -> ok ()
+              | Some cur' -> Ast_typed.assert_type_expression_eq (cur , cur') in
+            ok (Some cur) in
+          let%bind tv_opt = bind_fold_list aux None tvs in
+          let%bind tv =
+            trace_option (match_empty_variant m ae.location) @@
+            tv_opt in
+          return (O.E_matching (ex', m')) tv
+        )
+    )
+  | E_sequence (a , b) ->
+    let%bind a' = type_expression e a in
+    let%bind b' = type_expression e b in
+    let a'_type_annot = get_type_annotation a' in
+    let%bind () =
+      trace_strong (type_error
+                      ~msg:"first part of the sequence should be of unit type"
+                      ~expected:(O.t_unit ())
+                      ~actual:a'_type_annot
+                      ~expression:a
+                      a'.location) @@
+      Ast_typed.assert_type_expression_eq (t_unit () , a'_type_annot) in
+    return (O.E_sequence (a' , b')) (get_type_annotation b')
+  | E_loop (expr , body) ->
+    let%bind expr' = type_expression e expr in
+    let%bind body' = type_expression e body in
+    let t_expr' = get_type_annotation expr' in
+    let%bind () =
+      trace_strong (type_error
+                      ~msg:"while condition isn't of type bool"
+                      ~expected:(O.t_bool ())
+                      ~actual:t_expr'
+                      ~expression:expr
+                      expr'.location) @@
+      Ast_typed.assert_type_expression_eq (t_bool () , t_expr') in
+    let t_body' = get_type_annotation body' in
+    let%bind () =
+      trace_strong (type_error
+                     ~msg:"while body isn't of unit type"
+                     ~expected:(O.t_unit ())
+                     ~actual:t_body'
+                     ~expression:body
+                     body'.location) @@
+      Ast_typed.assert_type_expression_eq (t_unit () , t_body') in
+    return (O.E_loop (expr' , body')) (t_unit ())
+  | E_assign (name , path , expr) ->
+    let%bind typed_name =
+      let%bind ele = Environment.get_trace name e in
+      ok @@ make_n_t name ele.type_expression in
+    let%bind (assign_tv , path') =
+      let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path ->
+        match cur_path with
+        | Access_tuple index -> (
+            let%bind tpl = get_t_tuple prec_tv in
+            let%bind tv' =
+              trace_option (bad_tuple_index index ae prec_tv ae.location) @@
+              List.nth_opt tpl index in
+            ok (tv' , prec_path @ [O.Access_tuple index])
+          )
+        | Access_record property -> (
+            let%bind m = get_t_record prec_tv in
+            let%bind tv' =
+              trace_option (bad_record_access property ae prec_tv ae.location) @@
+              Map.String.find_opt property m in
+            ok (tv' , prec_path @ [O.Access_record property])
+          )
+        | Access_map _ ->
+          fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
+      in
+      bind_fold_list aux (typed_name.type_expression , []) path in
+    let%bind expr' = type_expression e expr in
+    let t_expr' = get_type_annotation expr' in
+    let%bind () =
+      trace_strong (type_error
+                     ~msg:"type of the expression to assign doesn't match left-hand-side"
+                     ~expected:assign_tv
+                     ~actual:t_expr'
+                     ~expression:expr
+                     expr'.location) @@
+      Ast_typed.assert_type_expression_eq (assign_tv , t_expr') in
+    return (O.E_assign (typed_name , path' , expr')) (t_unit ())
+  | E_let_in {binder ; rhs ; result} ->
+    let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
+    let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in
+    let e' = Environment.add_ez_declaration (fst binder) rhs e in
+    let%bind result = type_expression e' result in
+    return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
+  | E_annotation (expr , te) ->
+    let%bind tv = evaluate_type e te in
+    let%bind expr' = type_expression ~tv_opt:tv e expr in
+    let%bind type_annotation =
+      O.merge_annotation
+        (Some tv)
+        (Some expr'.type_annotation)
+        (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
+    ok {expr' with type_annotation}
+
+
+and type_constant (name:string) (lst:O.type_expression list) (tv_opt:O.type_expression option) (loc : Location.t) : (string * O.type_expression) result =
+  (* Constant poorman's polymorphism *)
+  let ct = Operators.Typer.constant_typers in
+  let%bind typer =
+    trace_option (unrecognized_constant name loc) @@
+    Map.String.find_opt name ct in
+  trace (constant_error loc lst tv_opt) @@
+  typer lst tv_opt
+
+let untype_type_expression (t:O.type_expression) : (I.type_expression) result =
+  match t.simplified with
+  | Some s -> ok s
+  | _ -> fail @@ internal_assertion_failure "trying to untype generated type"
+
+let untype_literal (l:O.literal) : I.literal result =
+  let open I in
+  match l with
+  | Literal_unit -> ok Literal_unit
+  | Literal_bool b -> ok (Literal_bool b)
+  | Literal_nat n -> ok (Literal_nat n)
+  | Literal_timestamp n -> ok (Literal_timestamp n)
+  | Literal_tez n -> ok (Literal_tez n)
+  | Literal_int n -> ok (Literal_int n)
+  | Literal_string s -> ok (Literal_string s)
+  | Literal_bytes b -> ok (Literal_bytes b)
+  | Literal_address s -> ok (Literal_address s)
+  | Literal_operation s -> ok (Literal_operation s)
+
+let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
+  let open I in
+  let return e = ok e in
+  match e.expression with
+  | E_literal l ->
+      let%bind l = untype_literal l in
+      return (e_literal l)
+  | E_constant (n, lst) ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_constant n lst')
+  | E_variable n ->
+      return (e_variable n)
+  | E_application (f, arg) ->
+      let%bind f' = untype_expression f in
+      let%bind arg' = untype_expression arg in
+      return (e_application f' arg')
+  | E_lambda {binder;input_type;output_type;result} ->
+      let%bind input_type = untype_type_expression input_type in
+      let%bind output_type = untype_type_expression output_type in
+      let%bind result = untype_expression result in
+      return (e_lambda binder (Some input_type) (Some output_type) result)
+  | E_tuple lst ->
+      let%bind lst' = bind_list
+        @@ List.map untype_expression lst in
+      return (e_tuple lst')
+  | E_tuple_accessor (tpl, ind)  ->
+      let%bind tpl' = untype_expression tpl in
+      return (e_accessor tpl' [Access_tuple ind])
+  | E_constructor (n, p) ->
+      let%bind p' = untype_expression p in
+      return (e_constructor n p')
+  | E_record r ->
+      let%bind r' = bind_smap
+        @@ SMap.map untype_expression r in
+      return (e_record r')
+  | E_record_accessor (r, s) ->
+      let%bind r' = untype_expression r in
+      return (e_accessor r' [Access_record s])
+  | E_map m ->
+      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
+      return (e_map m')
+  | E_list lst ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_list lst')
+  | E_set lst ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_set lst')
+  | E_look_up dsi ->
+      let%bind (a , b) = bind_map_pair untype_expression dsi in
+      return (e_look_up a b)
+  | E_matching (ae, m) ->
+      let%bind ae' = untype_expression ae in
+      let%bind m' = untype_matching untype_expression m in
+      return (e_matching ae' m')
+  | E_failwith ae ->
+      let%bind ae' = untype_expression ae in
+      return (e_failwith ae')
+  | E_sequence _
+  | E_loop _
+  | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
+  | E_let_in {binder;rhs;result} ->
+      let%bind tv = untype_type_expression rhs.type_annotation in
+      let%bind rhs = untype_expression rhs in
+      let%bind result = untype_expression result in
+      return (e_let_in (binder , (Some tv)) rhs result)
+
+and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
+  let open I in
+  match m with
+  | Match_bool {match_true ; match_false} ->
+      let%bind match_true = f match_true in
+      let%bind match_false = f match_false in
+      ok @@ Match_bool {match_true ; match_false}
+  | Match_tuple (lst, b) ->
+      let%bind b = f b in
+      ok @@ Match_tuple (lst, b)
+  | Match_option {match_none ; match_some = (v, some)} ->
+      let%bind match_none = f match_none in
+      let%bind some = f some in
+      let match_some = fst v, some in
+      ok @@ Match_option {match_none ; match_some}
+  | Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
+      let%bind match_nil = f match_nil in
+      let%bind cons = f cons in
+      let match_cons = hd, tl, cons in
+      ok @@ Match_list {match_nil ; match_cons}
+  | Match_variant (lst , _) ->
+      let aux ((a,b),c) =
+        let%bind c' = f c in
+        ok ((a,b),c') in
+      let%bind lst' = bind_map_list aux lst in
+      ok @@ Match_variant lst'

src/passes/4-typer-new/typer.mli

@@ -0,0 +1,57 @@
+open Trace
+
+module I = Ast_simplified
+module O = Ast_typed
+
+module SMap = O.SMap
+module Environment = O.Environment
+
+module Solver = Solver
+
+type environment = Environment.t
+
+module Errors : sig
+  (*
+  val unbound_type_variable : environment -> string -> unit -> error
+  val unbound_variable : environment -> string -> Location.t -> unit -> error
+  val match_empty_variant : 'a I.matching -> Location.t -> unit -> error
+  val match_missing_case : 'a I.matching -> Location.t -> unit -> error
+  val match_redundant_case : 'a I.matching -> Location.t -> unit -> error
+  val unbound_constructor : environment -> string -> Location.t -> unit -> error
+  val unrecognized_constant : string -> Location.t -> unit -> error
+  *)
+  val wrong_arity : string -> int -> int -> Location.t -> unit -> error
+  (*
+  val match_tuple_wrong_arity : 'a list -> 'b list -> Location.t -> unit -> error
+
+  (* TODO: this should be a trace_info? *)
+  val program_error : I.program -> unit -> error
+  val constant_declaration_error : string -> I.expr -> O.type_value option -> unit -> error
+  val match_error : ?msg:string -> expected:'a I.matching -> actual:O.type_value -> Location.t -> unit -> error
+  val needs_annotation : I.expression -> string -> unit -> error
+  val type_error_approximate : ?msg:string -> expected:string -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
+  val type_error : ?msg:string -> expected:O.type_value -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
+  val bad_tuple_index : int -> I.expression -> O.type_value -> Location.t -> unit -> error
+  val bad_record_access : string -> I.expression -> O.type_value -> Location.t -> unit -> error
+  val not_supported_yet : string -> I.expression -> unit -> error
+  val not_supported_yet_untranspile : string -> O.expression -> unit -> error
+  val constant_error : Location.t -> O.type_value list -> O.type_value option -> unit -> error
+  *)
+end
+
+val type_program : I.program -> (O.program * Solver.state) result
+val type_program' : I.program -> (O.program) result (* TODO: merge with type_program *)
+val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result
+(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
+val evaluate_type : environment -> I.type_expression -> O.type_value result
+val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_constant : string -> O.type_value list -> O.type_value option -> Location.t -> (string * O.type_value) result
+(*
+val untype_type_value : O.type_value -> (I.type_expression) result
+val untype_literal : O.literal -> I.literal result
+*)
+val untype_type_expression : O.type_value -> I.type_expression result
+val untype_expression : O.annotated_expression -> I.expression result
+(*
+val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result
+*)

src/passes/4-typer-new/typer_new.ml

@@ -0,0 +1 @@
+include Typer

src/passes/4-typer-old/dune

@@ -0,0 +1,16 @@
+(library
+  (name typer_old)
+  (public_name ligo.typer_old)
+  (libraries
+    simple-utils
+    tezos-utils
+    ast_simplified
+    ast_typed
+    typer_new
+    operators
+  )
+  (preprocess
+    (pps ppx_let)
+  )
+  (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
+)

src/passes/4-typer-old/typer.ml

@@ -0,0 +1,913 @@
+open Trace
+
+module I = Ast_simplified
+module O = Ast_typed
+open O.Combinators
+
+module SMap = O.SMap
+
+module Environment = O.Environment
+
+module Solver = Typer_new.Solver
+
+type environment = Environment.t
+
+module Errors = struct
+  let unbound_type_variable (e:environment) (n:string) () =
+    let title = (thunk "unbound type variable") in
+    let message () = "" in
+    let data = [
+      ("variable" , fun () -> Format.asprintf "%s" n) ;
+      (* TODO: types don't have srclocs for now. *)
+      (* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
+      ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
+    ] in
+    error ~data title message ()
+
+  let unbound_variable (e:environment) (n:string) (loc:Location.t) () =
+    let title = (thunk "unbound variable") in
+    let message () = "" in
+    let data = [
+      ("variable" , fun () -> Format.asprintf "%s" n) ;
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "match with no cases") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ =
+    fun matching loc () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let unbound_constructor (e:environment) (n:string) (loc:Location.t) () =
+    let title = (thunk "unbound constructor") in
+    let message () = "" in
+    let data = [
+      ("constructor" , fun () -> Format.asprintf "%s" n) ;
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let unrecognized_constant (n:string) (loc:Location.t) () =
+    let title = (thunk "unrecognized constant") in
+    let message () = "" in
+    let data = [
+      ("constant" , fun () -> Format.asprintf "%s" n) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
+    let title () = "wrong arity" in
+    let message () = "" in
+    let data = [
+      ("function" , fun () -> Format.asprintf "%s" n) ;
+      ("expected" , fun () -> Format.asprintf "%d" expected) ;
+      ("actual" , fun () -> Format.asprintf "%d" actual) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
+    let title () = "matching tuple of different size" in
+    let message () = "" in
+    let data = [
+      ("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
+      ("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  (* TODO: this should be a trace_info? *)
+  let program_error (p:I.program) () =
+    let message () = "" in
+    let title = (thunk "typing program") in
+    let data = [
+      ("program" , fun () -> Format.asprintf "%a" I.PP.program p)
+    ] in
+    error ~data title message ()
+
+  let constant_declaration_error (name:string) (ae:I.expr) (expected: O.type_value option) () =
+    let title = (thunk "typing constant declaration") in
+    let message () = "" in
+    let data = [
+      ("constant" , fun () -> Format.asprintf "%s" name) ;
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("expected" , fun () ->
+          match expected with
+            None -> "(no annotation for the expected type)"
+          | Some expected -> Format.asprintf "%a" O.PP.type_value expected) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
+    ] in
+    error ~data title message ()
+
+  let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_value -> Location.t -> unit -> _ =
+    fun ?(msg = "") ~expected ~actual loc () ->
+    let title = (thunk "typing match") in
+    let message () = msg in
+    let data = [
+      ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
+      ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let needs_annotation (e : I.expression) (case : string) () =
+    let title = (thunk "this expression must be annotated with its type") in
+    let message () = Format.asprintf "%s needs an annotation" case in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
+    ] in
+    error ~data title message ()
+
+  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%s" expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%a" O.PP.type_value expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_value) (loc:Location.t) () =
+    let title = (thunk "invalid tuple index") in
+    let message () = "" in
+    let data = [
+      ("index" , fun () -> Format.asprintf "%d" index) ;
+      ("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let bad_record_access (field : string) (ae : I.expression) (t : O.type_value) (loc:Location.t) () =
+    let title = (thunk "invalid record field") in
+    let message () = "" in
+    let data = [
+      ("field" , fun () -> Format.asprintf "%s" field) ;
+      ("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet (message : string) (ae : I.expression) () =
+    let title = (thunk "not suported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  I.PP.expression ae) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
+    let title = (thunk "not suported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  O.PP.expression ae)
+    ] in
+    error ~data title message ()
+
+  let constant_error loc lst tv_opt =
+    let title () = "typing constant" in
+    let message () = "" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
+      ("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_value (const " , ")) lst) ;
+      ("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_value) tv_opt) ;
+    ] in
+    error ~data title message
+end
+open Errors
+
+let rec type_program (p:I.program) : (O.program * Solver.state) result =
+  let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
+    let%bind ed' = (bind_map_location (type_declaration e (Solver.placeholder_for_state_of_new_typer ()))) d in
+    let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
+    let (e', _placeholder_for_state_of_new_typer , d') = Location.unwrap ed' in
+    match d' with
+    | None -> ok (e', acc)
+    | Some d' -> ok (e', loc ed' d' :: acc)
+  in
+  let%bind (_, lst) =
+    trace (fun () -> program_error p ()) @@
+    bind_fold_list aux (Environment.full_empty, []) p in
+  ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ()))
+
+and type_declaration env (_placeholder_for_state_of_new_typer : Solver.state) : I.declaration -> (environment * Solver.state * O.declaration option) result = function
+  | Declaration_type (type_name , type_expression) ->
+      let%bind tv = evaluate_type env type_expression in
+      let env' = Environment.add_type type_name tv env in
+      ok (env', (Solver.placeholder_for_state_of_new_typer ()) , None)
+  | Declaration_constant (name , tv_opt , expression) -> (
+      let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
+      let%bind ae' =
+        trace (constant_declaration_error name expression tv'_opt) @@
+        type_expression' ?tv_opt:tv'_opt env expression in
+      let env' = Environment.add_ez_ae name ae' env in
+      ok (env', (Solver.placeholder_for_state_of_new_typer ()) , Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
+    )
+
+and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result =
+  fun f e t i ae loc -> match i with
+    | Match_bool {match_true ; match_false} ->
+      let%bind _ =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_bool t in
+      let%bind match_true = f e match_true in
+      let%bind match_false = f e match_false in
+      ok (O.Match_bool {match_true ; match_false})
+  | Match_option {match_none ; match_some} ->
+      let%bind t_opt =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_option t in
+      let%bind match_none = f e match_none in
+      let (n, b) = match_some in
+      let n' = n, t_opt in
+      let e' = Environment.add_ez_binder n t_opt e in
+      let%bind b' = f e' b in
+      ok (O.Match_option {match_none ; match_some = (n', b')})
+  | Match_list {match_nil ; match_cons} ->
+      let%bind t_list =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_list t in
+      let%bind match_nil = f e match_nil in
+      let (hd, tl, b) = match_cons in
+      let e' = Environment.add_ez_binder hd t_list e in
+      let e' = Environment.add_ez_binder tl t e' in
+      let%bind b' = f e' b in
+      ok (O.Match_list {match_nil ; match_cons = (((hd , t_list), (tl , t)), b')})
+  | Match_tuple (lst, b) ->
+      let%bind t_tuple =
+        trace_strong (match_error ~expected:i ~actual:t loc)
+        @@ get_t_tuple t in
+      let%bind lst' =
+        generic_try (match_tuple_wrong_arity t_tuple lst loc)
+        @@ (fun () -> List.combine lst t_tuple) in
+      let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
+      let e' = List.fold_left aux e lst' in
+      let%bind b' = f e' b in
+      ok (O.Match_tuple (lst, b'))
+  | Match_variant lst ->
+      let%bind variant_opt =
+        let aux acc ((constructor_name , _) , _) =
+          let%bind (_ , variant) =
+            trace_option (unbound_constructor e constructor_name loc) @@
+            Environment.get_constructor constructor_name e in
+          let%bind acc = match acc with
+            | None -> ok (Some variant)
+            | Some variant' -> (
+                trace (type_error
+                         ~msg:"in match variant"
+                         ~expected:variant
+                         ~actual:variant'
+                         ~expression:ae
+                         loc
+                      ) @@
+                Ast_typed.assert_type_value_eq (variant , variant') >>? fun () ->
+                ok (Some variant)
+              ) in
+          ok acc in
+        trace (simple_info "in match variant") @@
+        bind_fold_list aux None lst in
+      let%bind variant =
+        trace_option (match_empty_variant i loc) @@
+        variant_opt in
+      let%bind () =
+        let%bind variant_cases' =
+          trace (match_error ~expected:i ~actual:t loc)
+          @@ Ast_typed.Combinators.get_t_sum variant in
+        let variant_cases = List.map fst @@ Map.String.to_kv_list variant_cases' in
+        let match_cases = List.map (Function.compose fst fst) lst in
+        let test_case = fun c ->
+          Assert.assert_true (List.mem c match_cases)
+        in
+        let%bind () =
+          trace_strong (match_missing_case i loc) @@
+          bind_iter_list test_case variant_cases in
+        let%bind () =
+          trace_strong (match_redundant_case i loc) @@
+          Assert.assert_true List.(length variant_cases = length match_cases) in
+        ok ()
+      in
+      let%bind lst' =
+        let aux ((constructor_name , name) , b) =
+          let%bind (constructor , _) =
+            trace_option (unbound_constructor e constructor_name loc) @@
+            Environment.get_constructor constructor_name e in
+          let e' = Environment.add_ez_binder name constructor e in
+          let%bind b' = f e' b in
+          ok ((constructor_name , name) , b')
+        in
+        bind_map_list aux lst in
+      ok (O.Match_variant (lst' , variant))
+
+and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
+  let return tv' = ok (make_t tv' (Some t)) in
+  match t with
+  | T_function (a, b) ->
+      let%bind a' = evaluate_type e a in
+      let%bind b' = evaluate_type e b in
+      return (T_function (a', b'))
+  | T_tuple lst ->
+      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
+      return (T_tuple lst')
+  | T_sum m ->
+      let aux k v prev =
+        let%bind prev' = prev in
+        let%bind v' = evaluate_type e v in
+        ok @@ SMap.add k v' prev'
+      in
+      let%bind m = SMap.fold aux m (ok SMap.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 @@ SMap.add k v' prev'
+      in
+      let%bind m = SMap.fold aux m (ok SMap.empty) in
+      return (T_record m)
+  | T_variable name ->
+      let%bind tv =
+        trace_option (unbound_type_variable e name)
+        @@ Environment.get_type_opt name e in
+      ok tv
+  | T_constant (cst, lst) ->
+      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
+      return (T_constant(Type_name cst, lst'))
+
+and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+  = fun e _placeholder_for_state_of_new_typer ?tv_opt ae ->
+    let%bind res = type_expression' e ?tv_opt ae in
+    ok (res, (Solver.placeholder_for_state_of_new_typer ()))
+and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
+  let module L = Logger.Stateful() in
+  let return expr tv =
+    let%bind () =
+      match tv_opt with
+      | None -> ok ()
+      | Some tv' -> O.assert_type_value_eq (tv' , tv) in
+    let location = ae.location in
+    ok @@ make_a_e ~location expr tv e in
+  let main_error =
+    let title () = "typing expression" in
+    let content () = "" in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) ;
+      ("misc" , fun () -> L.get ()) ;
+    ] in
+    error ~data title content in
+  trace main_error @@
+  match ae.expression with
+  (* Basic *)
+  | E_variable name ->
+      let%bind tv' =
+        trace_option (unbound_variable e name ae.location)
+        @@ Environment.get_opt name e in
+      return (E_variable name) tv'.type_value
+  | E_literal (Literal_bool b) ->
+      return (E_literal (Literal_bool b)) (t_bool ())
+  | E_literal Literal_unit | E_skip ->
+      return (E_literal (Literal_unit)) (t_unit ())
+  | E_literal (Literal_string s) ->
+      return (E_literal (Literal_string s)) (t_string ())
+  | E_literal (Literal_bytes s) ->
+      return (E_literal (Literal_bytes s)) (t_bytes ())
+  | E_literal (Literal_int n) ->
+      return (E_literal (Literal_int n)) (t_int ())
+  | E_literal (Literal_nat n) ->
+      return (E_literal (Literal_nat n)) (t_nat ())
+  | E_literal (Literal_timestamp n) ->
+      return (E_literal (Literal_timestamp n)) (t_timestamp ())
+  | E_literal (Literal_mutez n) ->
+      return (E_literal (Literal_mutez n)) (t_mutez ())
+  | E_literal (Literal_address s) ->
+      return (e_address s) (t_address ())
+  | E_literal (Literal_operation op) ->
+      return (e_operation op) (t_operation ())
+  (* Tuple *)
+  | E_tuple lst ->
+      let%bind lst' = bind_list @@ List.map (type_expression' e) lst in
+      let tv_lst = List.map get_type_annotation lst' in
+      return (E_tuple lst') (t_tuple tv_lst ())
+  | E_accessor (ae', path) ->
+      let%bind e' = type_expression' e ae' in
+      let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
+        match a with
+        | Access_tuple index -> (
+            let%bind tpl_tv = get_t_tuple prev.type_annotation in
+            let%bind tv =
+              generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
+              @@ (fun () -> List.nth tpl_tv index) in
+            return (E_tuple_accessor (prev , index)) tv
+          )
+        | Access_record property -> (
+            let%bind r_tv = get_t_record prev.type_annotation in
+            let%bind tv =
+              generic_try (bad_record_access property ae' prev.type_annotation ae.location)
+              @@ (fun () -> SMap.find property r_tv) in
+            return (E_record_accessor (prev , property)) tv
+          )
+        | Access_map ae' -> (
+            let%bind ae'' = type_expression' e ae' in
+            let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in
+            let%bind () =
+              Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in
+            return (E_look_up (prev , ae'')) v
+          )
+      in
+      trace (simple_info "accessing") @@
+      bind_fold_list aux e' path
+  (* Sum *)
+  | E_constructor (c, expr) ->
+      let%bind (c_tv, sum_tv) =
+        let error =
+          let title () = "no such constructor" in
+          let content () =
+            Format.asprintf "%s in:\n%a\n"
+              c O.Environment.PP.full_environment e
+          in
+          error title content in
+        trace_option error @@
+        Environment.get_constructor c e in
+      let%bind expr' = type_expression' e expr in
+      let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
+      return (E_constructor (c , expr')) sum_tv
+  (* Record *)
+  | E_record m ->
+      let aux prev k expr =
+        let%bind expr' = type_expression' e expr in
+        ok (SMap.add k expr' prev)
+      in
+      let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
+      return (E_record m') (t_record (SMap.map get_type_annotation m') ())
+  (* Data-structure *)
+  | E_list lst ->
+      let%bind lst' = bind_map_list (type_expression' e) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+              ok (Some c') in
+        let%bind init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = get_t_list ty in
+              ok (Some ty') in
+        let%bind ty =
+          let%bind opt = bind_fold_list aux init
+          @@ List.map get_type_annotation lst' in
+          trace_option (needs_annotation ae "empty list") opt in
+        ok (t_list ty ())
+      in
+      return (E_list lst') tv
+  | E_set lst ->
+      let%bind lst' = bind_map_list (type_expression' e) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+              ok (Some c') in
+        let%bind init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = get_t_set ty in
+              ok (Some ty') in
+        let%bind ty =
+          let%bind opt = bind_fold_list aux init
+          @@ List.map get_type_annotation lst' in
+          trace_option (needs_annotation ae "empty set") opt in
+        ok (t_set ty ())
+      in
+      return (E_set lst') tv
+  | E_map lst ->
+      let%bind lst' = bind_map_list (bind_map_pair (type_expression' e)) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+              ok (Some c') in
+        let%bind key_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map fst lst' in
+          let%bind annot = bind_map_option get_t_map_key tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        let%bind value_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map snd lst' in
+          let%bind annot = bind_map_option get_t_map_value tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        ok (t_map key_type value_type ())
+      in
+      return (E_map lst') tv
+  | E_big_map lst ->
+      let%bind lst' = bind_map_list (bind_map_pair (type_expression' e)) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+              ok (Some c') in
+        let%bind key_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map fst lst' in
+          let%bind annot = bind_map_option get_t_big_map_key tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        let%bind value_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map snd lst' in
+          let%bind annot = bind_map_option get_t_big_map_value tv_opt in
+          trace (simple_info "empty map expression without a type annotation") @@
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
+        in
+        ok (t_big_map key_type value_type ())
+      in
+      return (E_big_map lst') tv
+  | E_lambda {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } -> (
+      let%bind input_type =
+        let%bind input_type =
+          (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
+          let default_action e () = fail @@ (needs_annotation e "the returned value") in
+          match input_type with
+          | Some ty -> ok ty
+          | None -> (
+              match result.expression with
+              | I.E_let_in li -> (
+                  match li.rhs.expression with
+                  | I.E_variable name when name = (fst binder) -> (
+                      match snd li.binder with
+                      | Some ty -> ok ty
+                      | None -> default_action li.rhs ()
+                    )
+                  | _ -> default_action li.rhs ()
+                )
+              | _ -> default_action result ()
+            )
+        in
+        evaluate_type e input_type in
+      let%bind output_type =
+        bind_map_option (evaluate_type e) output_type
+      in
+      let e' = Environment.add_ez_binder (fst binder) input_type e in
+      let%bind body = type_expression' ?tv_opt:output_type e' result in
+      let output_type = body.type_annotation in
+      return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
+    )
+  | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") as opname ,
+                  [ collect ; 
+                    init_record ;
+                    ( { expression = (I.E_lambda { binder = (lname, None) ;
+                                                   input_type = None ; 
+                                                   output_type = None ; 
+                                                   result }) ;
+                        location = _ }) as _lambda
+                  ] ) ->
+      (* this special case is here force annotation of the untyped lambda
+         generated by pascaligo's for_collect loop *)
+      let%bind (v_col , v_initr ) = bind_map_pair (type_expression' e) (collect , init_record ) in
+      let tv_col = get_type_annotation v_col   in (* this is the type of the collection  *) 
+      let tv_out = get_type_annotation v_initr in (* this is the output type of the lambda*)
+      let%bind input_type = match tv_col.type_value' with
+        | O.T_constant ( (Type_name "list"|Type_name "set") , t) -> ok @@ t_tuple (tv_out::t) ()
+        | O.T_constant ( Type_name "map" , t) -> ok @@ t_tuple (tv_out::[(t_tuple t ())]) () 
+        | _ ->
+          let wtype = Format.asprintf
+            "Loops over collections expect lists, sets or maps, got type %a" O.PP.type_value tv_col in 
+          fail @@ simple_error wtype in 
+      let e' = Environment.add_ez_binder lname input_type e in
+      let%bind body = type_expression' ?tv_opt:(Some tv_out) e' result in
+      let output_type = body.type_annotation in
+      let lambda' = make_a_e (E_lambda {binder = lname ; body}) (t_function input_type output_type ()) e in
+      let lst' = [v_col; v_initr ; lambda'] in
+      let tv_lst = List.map get_type_annotation lst' in
+      let%bind (opname', tv) =
+        type_constant opname tv_lst tv_opt ae.location in
+      return (E_constant (opname' , lst')) tv
+  | E_constant (name, lst) ->
+      let%bind lst' = bind_list @@ List.map (type_expression' e) lst in
+      let tv_lst = List.map get_type_annotation lst' in
+      let%bind (name', tv) =
+        type_constant name tv_lst tv_opt ae.location in
+      return (E_constant (name' , lst')) tv
+  | E_application (f, arg) ->
+      let%bind f' = type_expression' e f in
+      let%bind arg = type_expression' e arg in
+      let%bind tv = match f'.type_annotation.type_value' with
+        | T_function (param, result) ->
+            let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
+            ok result
+        | _ ->
+          fail @@ type_error_approximate
+            ~expected:"should be a function type"
+            ~expression:f
+            ~actual:f'.type_annotation
+            f'.location
+      in
+      return (E_application (f' , arg)) tv
+  | E_look_up dsi ->
+      let%bind (ds, ind) = bind_map_pair (type_expression' e) dsi in
+      let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
+      let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
+      return (E_look_up (ds , ind)) (t_option dst ())
+  (* Advanced *)
+  | E_matching (ex, m) -> (
+      let%bind ex' = type_expression' e ex in
+      let%bind m' = type_match (type_expression' ?tv_opt:None) e ex'.type_annotation m ae ae.location in
+      let tvs =
+        let aux (cur:O.value O.matching) =
+          match cur with
+          | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
+          | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
+          | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
+          | Match_tuple (_ , match_tuple) -> [ match_tuple ]
+          | Match_variant (lst , _) -> List.map snd lst in
+        List.map get_type_annotation @@ aux m' in
+      let aux prec cur =
+        let%bind () =
+          match prec with
+          | None -> ok ()
+          | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
+        ok (Some cur) in
+      let%bind tv_opt = bind_fold_list aux None tvs in
+      let%bind tv =
+        trace_option (match_empty_variant m ae.location) @@
+        tv_opt in
+      return (O.E_matching (ex', m')) tv
+    )
+  | E_sequence (a , b) ->
+    let%bind a' = type_expression' e a in
+    let%bind b' = type_expression' e b in
+    let a'_type_annot = get_type_annotation a' in
+    let%bind () =
+      trace_strong (type_error
+                      ~msg:"first part of the sequence should be of unit type"
+                      ~expected:(O.t_unit ())
+                      ~actual:a'_type_annot
+                      ~expression:a
+                      a'.location) @@
+      Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
+    return (O.E_sequence (a' , b')) (get_type_annotation b')
+  | E_loop (expr , body) ->
+    let%bind expr' = type_expression' e expr in
+    let%bind body' = type_expression' e body in
+    let t_expr' = get_type_annotation expr' in
+    let%bind () =
+      trace_strong (type_error
+                      ~msg:"while condition isn't of type bool"
+                      ~expected:(O.t_bool ())
+                      ~actual:t_expr'
+                      ~expression:expr
+                      expr'.location) @@
+      Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
+    let t_body' = get_type_annotation body' in
+    let%bind () =
+      trace_strong (type_error
+                     ~msg:"while body isn't of unit type"
+                     ~expected:(O.t_unit ())
+                     ~actual:t_body'
+                     ~expression:body
+                     body'.location) @@
+      Ast_typed.assert_type_value_eq (t_unit () , t_body') in
+    return (O.E_loop (expr' , body')) (t_unit ())
+  | E_assign (name , path , expr) ->
+    let%bind typed_name =
+      let%bind ele = Environment.get_trace name e in
+      ok @@ make_n_t name ele.type_value in
+    let%bind (assign_tv , path') =
+      let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path ->
+        match cur_path with
+        | Access_tuple index -> (
+            let%bind tpl = get_t_tuple prec_tv in
+            let%bind tv' =
+              trace_option (bad_tuple_index index ae prec_tv ae.location) @@
+              List.nth_opt tpl index in
+            ok (tv' , prec_path @ [O.Access_tuple index])
+          )
+        | Access_record property -> (
+            let%bind m = get_t_record prec_tv in
+            let%bind tv' =
+              trace_option (bad_record_access property ae prec_tv ae.location) @@
+              Map.String.find_opt property m in
+            ok (tv' , prec_path @ [O.Access_record property])
+          )
+        | Access_map _ ->
+          fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
+      in
+      bind_fold_list aux (typed_name.type_value , []) path in
+    let%bind expr' = type_expression' e ~tv_opt:assign_tv expr in
+    let t_expr' = get_type_annotation expr' in
+    let%bind () =
+      trace_strong (type_error
+                     ~msg:"type of the expression to assign doesn't match left-hand-side"
+                     ~expected:assign_tv
+                     ~actual:t_expr'
+                     ~expression:expr
+                     expr'.location) @@
+      Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
+    return (O.E_assign (typed_name , path' , expr')) (t_unit ())
+  | E_let_in {binder ; rhs ; result} ->
+    let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
+    let%bind rhs = type_expression' ?tv_opt:rhs_tv_opt e rhs in
+    let e' = Environment.add_ez_declaration (fst binder) rhs e in
+    let%bind result = type_expression' e' result in
+    return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
+  | E_annotation (expr , te) ->
+    let%bind tv = evaluate_type e te in
+    let%bind expr' = type_expression' ~tv_opt:tv e expr in
+    let%bind type_annotation =
+      O.merge_annotation
+        (Some tv)
+        (Some expr'.type_annotation)
+        (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
+    ok {expr' with type_annotation}
+
+
+and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) (loc : Location.t) : (string * O.type_value) result =
+  (* Constant poorman's polymorphism *)
+  let ct = Operators.Typer.constant_typers in
+  let%bind typer =
+    trace_option (unrecognized_constant name loc) @@
+    Map.String.find_opt name ct in
+  trace (constant_error loc lst tv_opt) @@
+  typer lst tv_opt
+
+let untype_type_value (t:O.type_value) : (I.type_expression) result =
+  match t.simplified with
+  | Some s -> ok s
+  | _ -> fail @@ internal_assertion_failure "trying to untype generated type"
+
+let untype_literal (l:O.literal) : I.literal result =
+  let open I in
+  match l with
+  | Literal_unit -> ok Literal_unit
+  | Literal_bool b -> ok (Literal_bool b)
+  | Literal_nat n -> ok (Literal_nat n)
+  | Literal_timestamp n -> ok (Literal_timestamp n)
+  | Literal_mutez n -> ok (Literal_mutez n)
+  | Literal_int n -> ok (Literal_int n)
+  | Literal_string s -> ok (Literal_string s)
+  | Literal_bytes b -> ok (Literal_bytes b)
+  | Literal_address s -> ok (Literal_address s)
+  | Literal_operation s -> ok (Literal_operation s)
+
+let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
+  let open I in
+  let return e = ok e in
+  match e.expression with
+  | E_literal l ->
+      let%bind l = untype_literal l in
+      return (e_literal l)
+  | E_constant (n, lst) ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_constant n lst')
+  | E_variable n ->
+      return (e_variable n)
+  | E_application (f, arg) ->
+      let%bind f' = untype_expression f in
+      let%bind arg' = untype_expression arg in
+      return (e_application f' arg')
+  | E_lambda {binder ; body} -> (
+      let%bind io = get_t_function e.type_annotation in
+      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
+      let%bind result = untype_expression body in
+      return (e_lambda binder (Some input_type) (Some output_type) result)
+    )
+  | E_tuple lst ->
+      let%bind lst' = bind_list
+        @@ List.map untype_expression lst in
+      return (e_tuple lst')
+  | E_tuple_accessor (tpl, ind)  ->
+      let%bind tpl' = untype_expression tpl in
+      return (e_accessor tpl' [Access_tuple ind])
+  | E_constructor (n, p) ->
+      let%bind p' = untype_expression p in
+      return (e_constructor n p')
+  | E_record r ->
+      let%bind r' = bind_smap
+        @@ SMap.map untype_expression r in
+      return (e_record r')
+  | E_record_accessor (r, s) ->
+      let%bind r' = untype_expression r in
+      return (e_accessor r' [Access_record s])
+  | E_map m ->
+      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
+      return (e_map m')
+  | E_big_map m ->
+      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
+      return (e_big_map m')
+  | E_list lst ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_list lst')
+  | E_set lst ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_set lst')
+  | E_look_up dsi ->
+      let%bind (a , b) = bind_map_pair untype_expression dsi in
+      return (e_look_up a b)
+  | E_matching (ae, m) ->
+      let%bind ae' = untype_expression ae in
+      let%bind m' = untype_matching untype_expression m in
+      return (e_matching ae' m')
+  | E_sequence _
+  | E_loop _
+  | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
+  | E_let_in {binder;rhs;result} ->
+      let%bind tv = untype_type_value rhs.type_annotation in
+      let%bind rhs = untype_expression rhs in
+      let%bind result = untype_expression result in
+      return (e_let_in (binder , (Some tv)) rhs result)
+
+and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
+  let open I in
+  match m with
+  | Match_bool {match_true ; match_false} ->
+      let%bind match_true = f match_true in
+      let%bind match_false = f match_false in
+      ok @@ Match_bool {match_true ; match_false}
+  | Match_tuple (lst, b) ->
+      let%bind b = f b in
+      ok @@ Match_tuple (lst, b)
+  | Match_option {match_none ; match_some = (v, some)} ->
+      let%bind match_none = f match_none in
+      let%bind some = f some in
+      let match_some = fst v, some in
+      ok @@ Match_option {match_none ; match_some}
+  | Match_list {match_nil ; match_cons = (((hd_name , _) , (tl_name , _)), cons)} ->
+      let%bind match_nil = f match_nil in
+      let%bind cons = f cons in
+      let match_cons = hd_name , tl_name , cons in
+      ok @@ Match_list {match_nil ; match_cons}
+  | Match_variant (lst , _) ->
+      let aux ((a,b),c) =
+        let%bind c' = f c in
+        ok ((a,b),c') in
+      let%bind lst' = bind_map_list aux lst in
+      ok @@ Match_variant lst'

src/passes/4-typer-old/typer.mli

@@ -0,0 +1,55 @@
+open Trace
+
+module I = Ast_simplified
+module O = Ast_typed
+
+module SMap = O.SMap
+module Environment = O.Environment
+
+module Solver : module type of Typer_new.Solver
+
+type environment = Environment.t
+
+module Errors : sig
+  (*
+  val unbound_type_variable : environment -> string -> unit -> error
+  val unbound_variable : environment -> string -> Location.t -> unit -> error
+  val match_empty_variant : 'a I.matching -> Location.t -> unit -> error
+  val match_missing_case : 'a I.matching -> Location.t -> unit -> error
+  val match_redundant_case : 'a I.matching -> Location.t -> unit -> error
+  val unbound_constructor : environment -> string -> Location.t -> unit -> error
+  val unrecognized_constant : string -> Location.t -> unit -> error
+  *)
+  val wrong_arity : string -> int -> int -> Location.t -> unit -> error
+  (*
+  val match_tuple_wrong_arity : 'a list -> 'b list -> Location.t -> unit -> error
+
+  (* TODO: this should be a trace_info? *)
+  val program_error : I.program -> unit -> error
+  val constant_declaration_error : string -> I.expr -> O.type_value option -> unit -> error
+  val match_error : ?msg:string -> expected:'a I.matching -> actual:O.type_value -> Location.t -> unit -> error
+  val needs_annotation : I.expression -> string -> unit -> error
+  val type_error_approximate : ?msg:string -> expected:string -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
+  val type_error : ?msg:string -> expected:O.type_value -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
+  val bad_tuple_index : int -> I.expression -> O.type_value -> Location.t -> unit -> error
+  val bad_record_access : string -> I.expression -> O.type_value -> Location.t -> unit -> error
+  val not_supported_yet : string -> I.expression -> unit -> error
+  val not_supported_yet_untranspile : string -> O.expression -> unit -> error
+  val constant_error : Location.t -> O.type_value list -> O.type_value option -> unit -> error
+  *)
+end
+
+val type_program : I.program -> (O.program * Solver.state) result
+val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result
+(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
+val evaluate_type : environment -> I.type_expression -> O.type_value result
+val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_constant : string -> O.type_value list -> O.type_value option -> Location.t -> (string * O.type_value) result
+(*
+val untype_type_value : O.type_value -> (I.type_expression) result
+val untype_literal : O.literal -> I.literal result
+*)
+val untype_expression : O.annotated_expression -> I.expression result
+(*
+val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result
+*)

src/passes/4-typer-old/typer_old.ml

@@ -0,0 +1 @@
+include Typer

src/passes/4-typer/dune

@@ -6,6 +6,8 @@
     tezos-utils
     ast_simplified
     ast_typed
+    typer_old
+    typer_new
     operators
   )
   (preprocess

src/passes/4-typer/typer.ml

@@ -1,907 +1,15 @@
-open Trace
+let use_new_typer = false
 
 module I = Ast_simplified
 module O = Ast_typed
-open O.Combinators
 
 module SMap = O.SMap
-
 module Environment = O.Environment
 
+module Solver = Typer_new.Solver (* Both the old typer and the new typer use the same solver state. *)
+
 type environment = Environment.t
 
-module Errors = struct
-  let unbound_type_variable (e:environment) (n:string) () =
-    let title = (thunk "unbound type variable") in
-    let message () = "" in
-    let data = [
-      ("variable" , fun () -> Format.asprintf "%s" n) ;
-      (* TODO: types don't have srclocs for now. *)
-      (* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
-      ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
-    ] in
-    error ~data title message ()
-
-  let unbound_variable (e:environment) (n:string) (loc:Location.t) () =
-    let title = (thunk "unbound variable") in
-    let message () = "" in
-    let data = [
-      ("variable" , fun () -> Format.asprintf "%s" n) ;
-      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ =
-    fun matching loc () ->
-    let title = (thunk "match with no cases") in
-    let message () = "" in
-    let data = [
-      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ =
-    fun matching loc () ->
-    let title = (thunk "missing case in match") in
-    let message () = "" in
-    let data = [
-      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ =
-    fun matching loc () ->
-    let title = (thunk "missing case in match") in
-    let message () = "" in
-    let data = [
-      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let unbound_constructor (e:environment) (n:string) (loc:Location.t) () =
-    let title = (thunk "unbound constructor") in
-    let message () = "" in
-    let data = [
-      ("constructor" , fun () -> Format.asprintf "%s" n) ;
-      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let unrecognized_constant (n:string) (loc:Location.t) () =
-    let title = (thunk "unrecognized constant") in
-    let message () = "" in
-    let data = [
-      ("constant" , fun () -> Format.asprintf "%s" n) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
-    let title () = "wrong arity" in
-    let message () = "" in
-    let data = [
-      ("function" , fun () -> Format.asprintf "%s" n) ;
-      ("expected" , fun () -> Format.asprintf "%d" expected) ;
-      ("actual" , fun () -> Format.asprintf "%d" actual) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
-    let title () = "matching tuple of different size" in
-    let message () = "" in
-    let data = [
-      ("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
-      ("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  (* TODO: this should be a trace_info? *)
-  let program_error (p:I.program) () =
-    let message () = "" in
-    let title = (thunk "typing program") in
-    let data = [
-      ("program" , fun () -> Format.asprintf "%a" I.PP.program p)
-    ] in
-    error ~data title message ()
-
-  let constant_declaration_error (name:string) (ae:I.expr) (expected: O.type_value option) () =
-    let title = (thunk "typing constant declaration") in
-    let message () = "" in
-    let data = [
-      ("constant" , fun () -> Format.asprintf "%s" name) ;
-      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
-      ("expected" , fun () ->
-          match expected with
-            None -> "(no annotation for the expected type)"
-          | Some expected -> Format.asprintf "%a" O.PP.type_value expected) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
-    ] in
-    error ~data title message ()
-
-  let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_value -> Location.t -> unit -> _ =
-    fun ?(msg = "") ~expected ~actual loc () ->
-    let title = (thunk "typing match") in
-    let message () = msg in
-    let data = [
-      ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
-      ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let needs_annotation (e : I.expression) (case : string) () =
-    let title = (thunk "this expression must be annotated with its type") in
-    let message () = Format.asprintf "%s needs an annotation" case in
-    let data = [
-      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
-    ] in
-    error ~data title message ()
-
-  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
-    let title = (thunk "type error") in
-    let message () = msg in
-    let data = [
-      ("expected"   , fun () -> Format.asprintf "%s" expected);
-      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
-      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
-    let title = (thunk "type error") in
-    let message () = msg in
-    let data = [
-      ("expected"   , fun () -> Format.asprintf "%a" O.PP.type_value expected);
-      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
-      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_value) (loc:Location.t) () =
-    let title = (thunk "invalid tuple index") in
-    let message () = "" in
-    let data = [
-      ("index" , fun () -> Format.asprintf "%d" index) ;
-      ("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
-      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let bad_record_access (field : string) (ae : I.expression) (t : O.type_value) (loc:Location.t) () =
-    let title = (thunk "invalid record field") in
-    let message () = "" in
-    let data = [
-      ("field" , fun () -> Format.asprintf "%s" field) ;
-      ("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
-      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
-    ] in
-    error ~data title message ()
-
-  let not_supported_yet (message : string) (ae : I.expression) () =
-    let title = (thunk "not suported yet") in
-    let message () = message in
-    let data = [
-      ("expression" , fun () -> Format.asprintf "%a"  I.PP.expression ae) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
-    ] in
-    error ~data title message ()
-
-  let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
-    let title = (thunk "not suported yet") in
-    let message () = message in
-    let data = [
-      ("expression" , fun () -> Format.asprintf "%a"  O.PP.expression ae)
-    ] in
-    error ~data title message ()
-
-  let constant_error loc lst tv_opt =
-    let title () = "typing constant" in
-    let message () = "" in
-    let data = [
-      ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
-      ("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_value (const " , ")) lst) ;
-      ("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_value) tv_opt) ;
-    ] in
-    error ~data title message
-end
-open Errors
-
-let rec type_program (p:I.program) : O.program result =
-  let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
-    let%bind ed' = (bind_map_location (type_declaration e)) d in
-    let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
-    let (e', d') = Location.unwrap ed' in
-    match d' with
-    | None -> ok (e', acc)
-    | Some d' -> ok (e', loc ed' d' :: acc)
-  in
-  let%bind (_, lst) =
-    trace (fun () -> program_error p ()) @@
-    bind_fold_list aux (Environment.full_empty, []) p in
-  ok @@ List.rev lst
-
-and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
-  | Declaration_type (type_name , type_expression) ->
-      let%bind tv = evaluate_type env type_expression in
-      let env' = Environment.add_type type_name tv env in
-      ok (env', None)
-  | Declaration_constant (name , tv_opt , expression) -> (
-      let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
-      let%bind ae' =
-        trace (constant_declaration_error name expression tv'_opt) @@
-        type_expression ?tv_opt:tv'_opt env expression in
-      let env' = Environment.add_ez_ae name ae' env in
-      ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
-    )
-
-and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result =
-  fun f e t i ae loc -> match i with
-    | Match_bool {match_true ; match_false} ->
-      let%bind _ =
-        trace_strong (match_error ~expected:i ~actual:t loc)
-        @@ get_t_bool t in
-      let%bind match_true = f e match_true in
-      let%bind match_false = f e match_false in
-      ok (O.Match_bool {match_true ; match_false})
-  | Match_option {match_none ; match_some} ->
-      let%bind t_opt =
-        trace_strong (match_error ~expected:i ~actual:t loc)
-        @@ get_t_option t in
-      let%bind match_none = f e match_none in
-      let (n, b) = match_some in
-      let n' = n, t_opt in
-      let e' = Environment.add_ez_binder n t_opt e in
-      let%bind b' = f e' b in
-      ok (O.Match_option {match_none ; match_some = (n', b')})
-  | Match_list {match_nil ; match_cons} ->
-      let%bind t_list =
-        trace_strong (match_error ~expected:i ~actual:t loc)
-        @@ get_t_list t in
-      let%bind match_nil = f e match_nil in
-      let (hd, tl, b) = match_cons in
-      let e' = Environment.add_ez_binder hd t_list e in
-      let e' = Environment.add_ez_binder tl t e' in
-      let%bind b' = f e' b in
-      ok (O.Match_list {match_nil ; match_cons = (((hd , t_list), (tl , t)), b')})
-  | Match_tuple (lst, b) ->
-      let%bind t_tuple =
-        trace_strong (match_error ~expected:i ~actual:t loc)
-        @@ get_t_tuple t in
-      let%bind lst' =
-        generic_try (match_tuple_wrong_arity t_tuple lst loc)
-        @@ (fun () -> List.combine lst t_tuple) in
-      let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
-      let e' = List.fold_left aux e lst' in
-      let%bind b' = f e' b in
-      ok (O.Match_tuple (lst, b'))
-  | Match_variant lst ->
-      let%bind variant_opt =
-        let aux acc ((constructor_name , _) , _) =
-          let%bind (_ , variant) =
-            trace_option (unbound_constructor e constructor_name loc) @@
-            Environment.get_constructor constructor_name e in
-          let%bind acc = match acc with
-            | None -> ok (Some variant)
-            | Some variant' -> (
-                trace (type_error
-                         ~msg:"in match variant"
-                         ~expected:variant
-                         ~actual:variant'
-                         ~expression:ae
-                         loc
-                      ) @@
-                Ast_typed.assert_type_value_eq (variant , variant') >>? fun () ->
-                ok (Some variant)
-              ) in
-          ok acc in
-        trace (simple_info "in match variant") @@
-        bind_fold_list aux None lst in
-      let%bind variant =
-        trace_option (match_empty_variant i loc) @@
-        variant_opt in
-      let%bind () =
-        let%bind variant_cases' =
-          trace (match_error ~expected:i ~actual:t loc)
-          @@ Ast_typed.Combinators.get_t_sum variant in
-        let variant_cases = List.map fst @@ Map.String.to_kv_list variant_cases' in
-        let match_cases = List.map (Function.compose fst fst) lst in
-        let test_case = fun c ->
-          Assert.assert_true (List.mem c match_cases)
-        in
-        let%bind () =
-          trace_strong (match_missing_case i loc) @@
-          bind_iter_list test_case variant_cases in
-        let%bind () =
-          trace_strong (match_redundant_case i loc) @@
-          Assert.assert_true List.(length variant_cases = length match_cases) in
-        ok ()
-      in
-      let%bind lst' =
-        let aux ((constructor_name , name) , b) =
-          let%bind (constructor , _) =
-            trace_option (unbound_constructor e constructor_name loc) @@
-            Environment.get_constructor constructor_name e in
-          let e' = Environment.add_ez_binder name constructor e in
-          let%bind b' = f e' b in
-          ok ((constructor_name , name) , b')
-        in
-        bind_map_list aux lst in
-      ok (O.Match_variant (lst' , variant))
-
-and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
-  let return tv' = ok (make_t tv' (Some t)) in
-  match t with
-  | T_function (a, b) ->
-      let%bind a' = evaluate_type e a in
-      let%bind b' = evaluate_type e b in
-      return (T_function (a', b'))
-  | T_tuple lst ->
-      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      return (T_tuple lst')
-  | T_sum m ->
-      let aux k v prev =
-        let%bind prev' = prev in
-        let%bind v' = evaluate_type e v in
-        ok @@ SMap.add k v' prev'
-      in
-      let%bind m = SMap.fold aux m (ok SMap.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 @@ SMap.add k v' prev'
-      in
-      let%bind m = SMap.fold aux m (ok SMap.empty) in
-      return (T_record m)
-  | T_variable name ->
-      let%bind tv =
-        trace_option (unbound_type_variable e name)
-        @@ Environment.get_type_opt name e in
-      ok tv
-  | T_constant (cst, lst) ->
-      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      return (T_constant(cst, lst'))
-
-and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae ->
-  let module L = Logger.Stateful() in
-  let return expr tv =
-    let%bind () =
-      match tv_opt with
-      | None -> ok ()
-      | Some tv' -> O.assert_type_value_eq (tv' , tv) in
-    let location = ae.location in
-    ok @@ make_a_e ~location expr tv e in
-  let main_error =
-    let title () = "typing expression" in
-    let content () = "" in
-    let data = [
-      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
-      ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) ;
-      ("misc" , fun () -> L.get ()) ;
-    ] in
-    error ~data title content in
-  trace main_error @@
-  match ae.expression with
-  (* Basic *)
-  | E_variable name ->
-      let%bind tv' =
-        trace_option (unbound_variable e name ae.location)
-        @@ Environment.get_opt name e in
-      return (E_variable name) tv'.type_value
-  | E_literal (Literal_bool b) ->
-      return (E_literal (Literal_bool b)) (t_bool ())
-  | E_literal Literal_unit | E_skip ->
-      return (E_literal (Literal_unit)) (t_unit ())
-  | E_literal (Literal_string s) ->
-      return (E_literal (Literal_string s)) (t_string ())
-  | E_literal (Literal_bytes s) ->
-      return (E_literal (Literal_bytes s)) (t_bytes ())
-  | E_literal (Literal_int n) ->
-      return (E_literal (Literal_int n)) (t_int ())
-  | E_literal (Literal_nat n) ->
-      return (E_literal (Literal_nat n)) (t_nat ())
-  | E_literal (Literal_timestamp n) ->
-      return (E_literal (Literal_timestamp n)) (t_timestamp ())
-  | E_literal (Literal_mutez n) ->
-      return (E_literal (Literal_mutez n)) (t_tez ())
-  | E_literal (Literal_address s) ->
-      return (e_address s) (t_address ())
-  | E_literal (Literal_operation op) ->
-      return (e_operation op) (t_operation ())
-  (* Tuple *)
-  | E_tuple lst ->
-      let%bind lst' = bind_list @@ List.map (type_expression e) lst in
-      let tv_lst = List.map get_type_annotation lst' in
-      return (E_tuple lst') (t_tuple tv_lst ())
-  | E_accessor (ae', path) ->
-      let%bind e' = type_expression e ae' in
-      let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result =
-        match a with
-        | Access_tuple index -> (
-            let%bind tpl_tv = get_t_tuple prev.type_annotation in
-            let%bind tv =
-              generic_try (bad_tuple_index index ae' prev.type_annotation ae.location)
-              @@ (fun () -> List.nth tpl_tv index) in
-            return (E_tuple_accessor (prev , index)) tv
-          )
-        | Access_record property -> (
-            let%bind r_tv = get_t_record prev.type_annotation in
-            let%bind tv =
-              generic_try (bad_record_access property ae' prev.type_annotation ae.location)
-              @@ (fun () -> SMap.find property r_tv) in
-            return (E_record_accessor (prev , property)) tv
-          )
-        | Access_map ae' -> (
-            let%bind ae'' = type_expression e ae' in
-            let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in
-            let%bind () =
-              Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in
-            return (E_look_up (prev , ae'')) v
-          )
-      in
-      trace (simple_info "accessing") @@
-      bind_fold_list aux e' path
-  (* Sum *)
-  | E_constructor (c, expr) ->
-      let%bind (c_tv, sum_tv) =
-        let error =
-          let title () = "no such constructor" in
-          let content () =
-            Format.asprintf "%s in:\n%a\n"
-              c O.Environment.PP.full_environment e
-          in
-          error title content in
-        trace_option error @@
-        Environment.get_constructor c e in
-      let%bind expr' = type_expression e expr in
-      let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
-      return (E_constructor (c , expr')) sum_tv
-  (* Record *)
-  | E_record m ->
-      let aux prev k expr =
-        let%bind expr' = type_expression e expr in
-        ok (SMap.add k expr' prev)
-      in
-      let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
-      return (E_record m') (t_record (SMap.map get_type_annotation m') ())
-  (* Data-structure *)
-  | E_list lst ->
-      let%bind lst' = bind_map_list (type_expression e) lst in
-      let%bind tv =
-        let aux opt c =
-          match opt with
-          | None -> ok (Some c)
-          | Some c' ->
-              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
-              ok (Some c') in
-        let%bind init = match tv_opt with
-          | None -> ok None
-          | Some ty ->
-              let%bind ty' = get_t_list ty in
-              ok (Some ty') in
-        let%bind ty =
-          let%bind opt = bind_fold_list aux init
-          @@ List.map get_type_annotation lst' in
-          trace_option (needs_annotation ae "empty list") opt in
-        ok (t_list ty ())
-      in
-      return (E_list lst') tv
-  | E_set lst ->
-      let%bind lst' = bind_map_list (type_expression e) lst in
-      let%bind tv =
-        let aux opt c =
-          match opt with
-          | None -> ok (Some c)
-          | Some c' ->
-              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
-              ok (Some c') in
-        let%bind init = match tv_opt with
-          | None -> ok None
-          | Some ty ->
-              let%bind ty' = get_t_set ty in
-              ok (Some ty') in
-        let%bind ty =
-          let%bind opt = bind_fold_list aux init
-          @@ List.map get_type_annotation lst' in
-          trace_option (needs_annotation ae "empty set") opt in
-        ok (t_set ty ())
-      in
-      return (E_set lst') tv
-  | E_map lst ->
-      let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
-      let%bind tv =
-        let aux opt c =
-          match opt with
-          | None -> ok (Some c)
-          | Some c' ->
-              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
-              ok (Some c') in
-        let%bind key_type =
-          let%bind sub =
-            bind_fold_list aux None
-            @@ List.map get_type_annotation
-            @@ List.map fst lst' in
-          let%bind annot = bind_map_option get_t_map_key tv_opt in
-          trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub (needs_annotation ae "this map literal")
-        in
-        let%bind value_type =
-          let%bind sub =
-            bind_fold_list aux None
-            @@ List.map get_type_annotation
-            @@ List.map snd lst' in
-          let%bind annot = bind_map_option get_t_map_value tv_opt in
-          trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub (needs_annotation ae "this map literal")
-        in
-        ok (t_map key_type value_type ())
-      in
-      return (E_map lst') tv
-  | E_big_map lst ->
-      let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
-      let%bind tv =
-        let aux opt c =
-          match opt with
-          | None -> ok (Some c)
-          | Some c' ->
-              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
-              ok (Some c') in
-        let%bind key_type =
-          let%bind sub =
-            bind_fold_list aux None
-            @@ List.map get_type_annotation
-            @@ List.map fst lst' in
-          let%bind annot = bind_map_option get_t_big_map_key tv_opt in
-          trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub (needs_annotation ae "this map literal")
-        in
-        let%bind value_type =
-          let%bind sub =
-            bind_fold_list aux None
-            @@ List.map get_type_annotation
-            @@ List.map snd lst' in
-          let%bind annot = bind_map_option get_t_big_map_value tv_opt in
-          trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub (needs_annotation ae "this map literal")
-        in
-        ok (t_big_map key_type value_type ())
-      in
-      return (E_big_map lst') tv
-  | E_lambda {
-      binder ;
-      input_type ;
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type =
-        let%bind input_type =
-          (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
-          let default_action e () = fail @@ (needs_annotation e "the returned value") in
-          match input_type with
-          | Some ty -> ok ty
-          | None -> (
-              match result.expression with
-              | I.E_let_in li -> (
-                  match li.rhs.expression with
-                  | I.E_variable name when name = (fst binder) -> (
-                      match snd li.binder with
-                      | Some ty -> ok ty
-                      | None -> default_action li.rhs ()
-                    )
-                  | _ -> default_action li.rhs ()
-                )
-              | _ -> default_action result ()
-            )
-        in
-        evaluate_type e input_type in
-      let%bind output_type =
-        bind_map_option (evaluate_type e) output_type
-      in
-      let e' = Environment.add_ez_binder (fst binder) input_type e in
-      let%bind body = type_expression ?tv_opt:output_type e' result in
-      let output_type = body.type_annotation in
-      return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
-    )
-  | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") as opname ,
-                  [ collect ; 
-                    init_record ;
-                    ( { expression = (I.E_lambda { binder = (lname, None) ;
-                                                   input_type = None ; 
-                                                   output_type = None ; 
-                                                   result }) ;
-                        location = _ }) as _lambda
-                  ] ) ->
-      (* this special case is here force annotation of the untyped lambda
-         generated by pascaligo's for_collect loop *)
-      let%bind (v_col , v_initr ) = bind_map_pair (type_expression e) (collect , init_record ) in
-      let tv_col = get_type_annotation v_col   in (* this is the type of the collection  *) 
-      let tv_out = get_type_annotation v_initr in (* this is the output type of the lambda*)
-      let%bind input_type = match tv_col.type_value' with
-        | O.T_constant ( ("list"|"set") , t) -> ok @@ t_tuple (tv_out::t) ()
-        | O.T_constant ( "map" , t) -> ok @@ t_tuple (tv_out::[(t_tuple t ())]) () 
-        | _ ->
-          let wtype = Format.asprintf
-            "Loops over collections expect lists, sets or maps, got type %a" O.PP.type_value tv_col in 
-          fail @@ simple_error wtype in 
-      let e' = Environment.add_ez_binder lname input_type e in
-      let%bind body = type_expression ?tv_opt:(Some tv_out) e' result in
-      let output_type = body.type_annotation in
-      let lambda' = make_a_e (E_lambda {binder = lname ; body}) (t_function input_type output_type ()) e in
-      let lst' = [v_col; v_initr ; lambda'] in
-      let tv_lst = List.map get_type_annotation lst' in
-      let%bind (opname', tv) =
-        type_constant opname tv_lst tv_opt ae.location in
-      return (E_constant (opname' , lst')) tv
-  | E_constant (name, lst) ->
-      let%bind lst' = bind_list @@ List.map (type_expression e) lst in
-      let tv_lst = List.map get_type_annotation lst' in
-      let%bind (name', tv) =
-        type_constant name tv_lst tv_opt ae.location in
-      return (E_constant (name' , lst')) tv
-  | E_application (f, arg) ->
-      let%bind f' = type_expression e f in
-      let%bind arg = type_expression e arg in
-      let%bind tv = match f'.type_annotation.type_value' with
-        | T_function (param, result) ->
-            let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
-            ok result
-        | _ ->
-          fail @@ type_error_approximate
-            ~expected:"should be a function type"
-            ~expression:f
-            ~actual:f'.type_annotation
-            f'.location
-      in
-      return (E_application (f' , arg)) tv
-  | E_look_up dsi ->
-      let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
-      let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
-      let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
-      return (E_look_up (ds , ind)) (t_option dst ())
-  (* Advanced *)
-  | E_matching (ex, m) -> (
-      let%bind ex' = type_expression e ex in
-      let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
-      let tvs =
-        let aux (cur:O.value O.matching) =
-          match cur with
-          | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
-          | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
-          | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
-          | Match_tuple (_ , match_tuple) -> [ match_tuple ]
-          | Match_variant (lst , _) -> List.map snd lst in
-        List.map get_type_annotation @@ aux m' in
-      let aux prec cur =
-        let%bind () =
-          match prec with
-          | None -> ok ()
-          | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
-        ok (Some cur) in
-      let%bind tv_opt = bind_fold_list aux None tvs in
-      let%bind tv =
-        trace_option (match_empty_variant m ae.location) @@
-        tv_opt in
-      return (O.E_matching (ex', m')) tv
-    )
-  | E_sequence (a , b) ->
-    let%bind a' = type_expression e a in
-    let%bind b' = type_expression e b in
-    let a'_type_annot = get_type_annotation a' in
-    let%bind () =
-      trace_strong (type_error
-                      ~msg:"first part of the sequence should be of unit type"
-                      ~expected:(O.t_unit ())
-                      ~actual:a'_type_annot
-                      ~expression:a
-                      a'.location) @@
-      Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
-    return (O.E_sequence (a' , b')) (get_type_annotation b')
-  | E_loop (expr , body) ->
-    let%bind expr' = type_expression e expr in
-    let%bind body' = type_expression e body in
-    let t_expr' = get_type_annotation expr' in
-    let%bind () =
-      trace_strong (type_error
-                      ~msg:"while condition isn't of type bool"
-                      ~expected:(O.t_bool ())
-                      ~actual:t_expr'
-                      ~expression:expr
-                      expr'.location) @@
-      Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
-    let t_body' = get_type_annotation body' in
-    let%bind () =
-      trace_strong (type_error
-                     ~msg:"while body isn't of unit type"
-                     ~expected:(O.t_unit ())
-                     ~actual:t_body'
-                     ~expression:body
-                     body'.location) @@
-      Ast_typed.assert_type_value_eq (t_unit () , t_body') in
-    return (O.E_loop (expr' , body')) (t_unit ())
-  | E_assign (name , path , expr) ->
-    let%bind typed_name =
-      let%bind ele = Environment.get_trace name e in
-      ok @@ make_n_t name ele.type_value in
-    let%bind (assign_tv , path') =
-      let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path ->
-        match cur_path with
-        | Access_tuple index -> (
-            let%bind tpl = get_t_tuple prec_tv in
-            let%bind tv' =
-              trace_option (bad_tuple_index index ae prec_tv ae.location) @@
-              List.nth_opt tpl index in
-            ok (tv' , prec_path @ [O.Access_tuple index])
-          )
-        | Access_record property -> (
-            let%bind m = get_t_record prec_tv in
-            let%bind tv' =
-              trace_option (bad_record_access property ae prec_tv ae.location) @@
-              Map.String.find_opt property m in
-            ok (tv' , prec_path @ [O.Access_record property])
-          )
-        | Access_map _ ->
-          fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
-      in
-      bind_fold_list aux (typed_name.type_value , []) path in
-    let%bind expr' = type_expression e ~tv_opt:assign_tv expr in
-    let t_expr' = get_type_annotation expr' in
-    let%bind () =
-      trace_strong (type_error
-                     ~msg:"type of the expression to assign doesn't match left-hand-side"
-                     ~expected:assign_tv
-                     ~actual:t_expr'
-                     ~expression:expr
-                     expr'.location) @@
-      Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
-    return (O.E_assign (typed_name , path' , expr')) (t_unit ())
-  | E_let_in {binder ; rhs ; result} ->
-    let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
-    let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in
-    let e' = Environment.add_ez_declaration (fst binder) rhs e in
-    let%bind result = type_expression e' result in
-    return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation
-  | E_annotation (expr , te) ->
-    let%bind tv = evaluate_type e te in
-    let%bind expr' = type_expression ~tv_opt:tv e expr in
-    let%bind type_annotation =
-      O.merge_annotation
-        (Some tv)
-        (Some expr'.type_annotation)
-        (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
-    ok {expr' with type_annotation}
-
-
-and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) (loc : Location.t) : (string * O.type_value) result =
-  (* Constant poorman's polymorphism *)
-  let ct = Operators.Typer.constant_typers in
-  let%bind typer =
-    trace_option (unrecognized_constant name loc) @@
-    Map.String.find_opt name ct in
-  trace (constant_error loc lst tv_opt) @@
-  typer lst tv_opt
-
-let untype_type_value (t:O.type_value) : (I.type_expression) result =
-  match t.simplified with
-  | Some s -> ok s
-  | _ -> fail @@ internal_assertion_failure "trying to untype generated type"
-
-let untype_literal (l:O.literal) : I.literal result =
-  let open I in
-  match l with
-  | Literal_unit -> ok Literal_unit
-  | Literal_bool b -> ok (Literal_bool b)
-  | Literal_nat n -> ok (Literal_nat n)
-  | Literal_timestamp n -> ok (Literal_timestamp n)
-  | Literal_mutez n -> ok (Literal_mutez n)
-  | Literal_int n -> ok (Literal_int n)
-  | Literal_string s -> ok (Literal_string s)
-  | Literal_bytes b -> ok (Literal_bytes b)
-  | Literal_address s -> ok (Literal_address s)
-  | Literal_operation s -> ok (Literal_operation s)
-
-let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
-  let open I in
-  let return e = ok e in
-  match e.expression with
-  | E_literal l ->
-      let%bind l = untype_literal l in
-      return (e_literal l)
-  | E_constant (n, lst) ->
-      let%bind lst' = bind_map_list untype_expression lst in
-      return (e_constant n lst')
-  | E_variable n ->
-      return (e_variable n)
-  | E_application (f, arg) ->
-      let%bind f' = untype_expression f in
-      let%bind arg' = untype_expression arg in
-      return (e_application f' arg')
-  | E_lambda {binder ; body} -> (
-      let%bind io = get_t_function e.type_annotation in
-      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
-      let%bind result = untype_expression body in
-      return (e_lambda binder (Some input_type) (Some output_type) result)
-    )
-  | E_tuple lst ->
-      let%bind lst' = bind_list
-        @@ List.map untype_expression lst in
-      return (e_tuple lst')
-  | E_tuple_accessor (tpl, ind)  ->
-      let%bind tpl' = untype_expression tpl in
-      return (e_accessor tpl' [Access_tuple ind])
-  | E_constructor (n, p) ->
-      let%bind p' = untype_expression p in
-      return (e_constructor n p')
-  | E_record r ->
-      let%bind r' = bind_smap
-        @@ SMap.map untype_expression r in
-      return (e_record r')
-  | E_record_accessor (r, s) ->
-      let%bind r' = untype_expression r in
-      return (e_accessor r' [Access_record s])
-  | E_map m ->
-      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
-      return (e_map m')
-  | E_big_map m ->
-      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
-      return (e_big_map m')
-  | E_list lst ->
-      let%bind lst' = bind_map_list untype_expression lst in
-      return (e_list lst')
-  | E_set lst ->
-      let%bind lst' = bind_map_list untype_expression lst in
-      return (e_set lst')
-  | E_look_up dsi ->
-      let%bind (a , b) = bind_map_pair untype_expression dsi in
-      return (e_look_up a b)
-  | E_matching (ae, m) ->
-      let%bind ae' = untype_expression ae in
-      let%bind m' = untype_matching untype_expression m in
-      return (e_matching ae' m')
-  | E_sequence _
-  | E_loop _
-  | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
-  | E_let_in {binder;rhs;result} ->
-      let%bind tv = untype_type_value rhs.type_annotation in
-      let%bind rhs = untype_expression rhs in
-      let%bind result = untype_expression result in
-      return (e_let_in (binder , (Some tv)) rhs result)
-
-and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
-  let open I in
-  match m with
-  | Match_bool {match_true ; match_false} ->
-      let%bind match_true = f match_true in
-      let%bind match_false = f match_false in
-      ok @@ Match_bool {match_true ; match_false}
-  | Match_tuple (lst, b) ->
-      let%bind b = f b in
-      ok @@ Match_tuple (lst, b)
-  | Match_option {match_none ; match_some = (v, some)} ->
-      let%bind match_none = f match_none in
-      let%bind some = f some in
-      let match_some = fst v, some in
-      ok @@ Match_option {match_none ; match_some}
-  | Match_list {match_nil ; match_cons = (((hd_name , _) , (tl_name , _)), cons)} ->
-      let%bind match_nil = f match_nil in
-      let%bind cons = f cons in
-      let match_cons = hd_name , tl_name , cons in
-      ok @@ Match_list {match_nil ; match_cons}
-  | Match_variant (lst , _) ->
-      let aux ((a,b),c) =
-        let%bind c' = f c in
-        ok ((a,b),c') in
-      let%bind lst' = bind_map_list aux lst in
-      ok @@ Match_variant lst'
+let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program
+let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression
+let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression

src/passes/4-typer/typer.mli

@@ -1,3 +1,5 @@
+val use_new_typer : bool
+
 open Trace
 
 module I = Ast_simplified
@@ -6,48 +8,11 @@ module O = Ast_typed
 module SMap = O.SMap
 module Environment = O.Environment
 
+module Solver = Typer_new.Solver
+
 type environment = Environment.t
 
-module Errors : sig
-  (*
-  val unbound_type_variable : environment -> string -> unit -> error
-  val unbound_variable : environment -> string -> Location.t -> unit -> error
-  val match_empty_variant : 'a I.matching -> Location.t -> unit -> error
-  val match_missing_case : 'a I.matching -> Location.t -> unit -> error
-  val match_redundant_case : 'a I.matching -> Location.t -> unit -> error
-  val unbound_constructor : environment -> string -> Location.t -> unit -> error
-  val unrecognized_constant : string -> Location.t -> unit -> error
-  *)
-  val wrong_arity : string -> int -> int -> Location.t -> unit -> error
-  (*
-  val match_tuple_wrong_arity : 'a list -> 'b list -> Location.t -> unit -> error
-
-  (* TODO: this should be a trace_info? *)
-  val program_error : I.program -> unit -> error
-  val constant_declaration_error : string -> I.expr -> O.type_value option -> unit -> error
-  val match_error : ?msg:string -> expected:'a I.matching -> actual:O.type_value -> Location.t -> unit -> error
-  val needs_annotation : I.expression -> string -> unit -> error
-  val type_error_approximate : ?msg:string -> expected:string -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
-  val type_error : ?msg:string -> expected:O.type_value -> actual:O.type_value -> expression:I.expression -> Location.t -> unit -> error
-  val bad_tuple_index : int -> I.expression -> O.type_value -> Location.t -> unit -> error
-  val bad_record_access : string -> I.expression -> O.type_value -> Location.t -> unit -> error
-  val not_supported_yet : string -> I.expression -> unit -> error
-  val not_supported_yet_untranspile : string -> O.expression -> unit -> error
-  val constant_error : Location.t -> O.type_value list -> O.type_value option -> unit -> error
-  *)
-end
-
-val type_program : I.program -> O.program result
-val type_declaration : environment -> I.declaration -> (environment * O.declaration option) result
-val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result
-val evaluate_type : environment -> I.type_expression -> O.type_value result
-val type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result
-val type_constant : string -> O.type_value list -> O.type_value option -> Location.t -> (string * O.type_value) result
-(*
-val untype_type_value : O.type_value -> (I.type_expression) result
-val untype_literal : O.literal -> I.literal result
-*)
+val type_program : I.program -> (O.program * Solver.state) result
+val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val untype_expression : O.annotated_expression -> I.expression result
-(*
-val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result
-*)
+

src/passes/6-transpiler/transpiler.ml

@@ -32,6 +32,11 @@ them. please report this to the developers." in
     let content () = name in
     error title content
 
+  let no_type_variable name =
+    let title () = "type variables can't be transpiled" in
+    let content () = name in
+    error title content
+
   let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l)
 
   let unsupported_pattern_matching kind location =
@@ -101,41 +106,49 @@ them. please report this to the developers." in
       ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
     ] in
     error ~data title content
+
+  let not_found content =
+    let title () = "Not_found" in
+    let content () = content in
+    let data = [
+    ] in
+    error ~data title content
 end
 open Errors
 
 let rec transpile_type (t:AST.type_value) : type_value result =
   match t.type_value' with
-  | T_constant ("bool", []) -> ok (T_base Base_bool)
-  | T_constant ("int", []) -> ok (T_base Base_int)
-  | T_constant ("nat", []) -> ok (T_base Base_nat)
-  | T_constant ("tez", []) -> ok (T_base Base_tez)
-  | T_constant ("string", []) -> ok (T_base Base_string)
-  | T_constant ("bytes", []) -> ok (T_base Base_bytes)
-  | T_constant ("address", []) -> ok (T_base Base_address)
-  | T_constant ("timestamp", []) -> ok (T_base Base_timestamp)
-  | T_constant ("unit", []) -> ok (T_base Base_unit)
-  | T_constant ("operation", []) -> ok (T_base Base_operation)
-  | T_constant ("signature", []) -> ok (T_base Base_signature)
-  | T_constant ("contract", [x]) ->
+  | T_variable (Type_name name) -> fail @@ no_type_variable name
+  | T_constant (Type_name "bool", []) -> ok (T_base Base_bool)
+  | T_constant (Type_name "int", []) -> ok (T_base Base_int)
+  | T_constant (Type_name "nat", []) -> ok (T_base Base_nat)
+  | T_constant (Type_name "tez", []) -> ok (T_base Base_tez)
+  | T_constant (Type_name "string", []) -> ok (T_base Base_string)
+  | T_constant (Type_name "bytes", []) -> ok (T_base Base_bytes)
+  | T_constant (Type_name "address", []) -> ok (T_base Base_address)
+  | T_constant (Type_name "timestamp", []) -> ok (T_base Base_timestamp)
+  | T_constant (Type_name "unit", []) -> ok (T_base Base_unit)
+  | T_constant (Type_name "operation", []) -> ok (T_base Base_operation)
+  | T_constant (Type_name "signature", []) -> ok (T_base Base_signature)
+  | T_constant (Type_name "contract", [x]) ->
       let%bind x' = transpile_type x in
       ok (T_contract x')
-  | T_constant ("map", [key;value]) ->
+  | T_constant (Type_name "map", [key;value]) ->
       let%bind kv' = bind_map_pair transpile_type (key, value) in
       ok (T_map kv')
-  | T_constant ("big_map", [key;value] ) ->
+  | T_constant (Type_name "big_map", [key;value] ) ->
       let%bind kv' = bind_map_pair transpile_type (key, value) in
       ok (T_big_map kv')
-  | T_constant ("list", [t]) ->
+  | T_constant (Type_name "list", [t]) ->
       let%bind t' = transpile_type t in
       ok (T_list t')
-  | T_constant ("set", [t]) ->
+  | T_constant (Type_name "set", [t]) ->
       let%bind t' = transpile_type t in
       ok (T_set t')
-  | T_constant ("option", [o]) ->
+  | T_constant (Type_name "option", [o]) ->
       let%bind o' = transpile_type o in
       ok (T_option o')
-  | T_constant (name , _lst) -> fail @@ unrecognized_type_constant name
+  | T_constant (Type_name name , _lst) -> fail @@ unrecognized_type_constant name
   (* TODO hmm *)
   | T_sum m ->
       let node = Append_tree.of_list @@ kv_list_of_map m in
@@ -492,7 +505,10 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
               let%bind ty'_map = bind_map_smap transpile_type ty_map in
               let%bind path = record_access_to_lr ty' ty'_map prop in
               let path' = List.map snd path in
-            ok (Map.String.find prop ty_map, acc @ path')
+            let%bind prop_in_ty_map = trace_option
+                (Errors.not_found "acessing prop in ty_map [TODO: better error message]")
+                (Map.String.find_opt prop ty_map) in
+            ok (prop_in_ty_map, acc @ path')
           )
           | Access_map _k -> fail (corner_case ~loc:__LOC__ "no patch for map yet")
       in

src/passes/6-transpiler/untranspiler.ml

@@ -53,61 +53,61 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
   let open! AST in
   let return e = ok (make_a_e_empty e t) in
   match t.type_value' with
-  | T_constant ("unit", []) -> (
+  | T_constant (Type_name "unit", []) -> (
       let%bind () =
         trace_strong (wrong_mini_c_value "unit" v) @@
         get_unit v in
       return (E_literal Literal_unit)
     )
-  | T_constant ("bool", []) -> (
+  | T_constant (Type_name "bool", []) -> (
       let%bind b =
         trace_strong (wrong_mini_c_value "bool" v) @@
         get_bool v in
       return (E_literal (Literal_bool b))
     )
-  | T_constant ("int", []) -> (
+  | T_constant (Type_name "int", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "int" v) @@
         get_int v in
       return (E_literal (Literal_int n))
     )
-  | T_constant ("nat", []) -> (
+  | T_constant (Type_name "nat", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "nat" v) @@
         get_nat v in
       return (E_literal (Literal_nat n))
     )
-  | T_constant ("timestamp", []) -> (
+  | T_constant (Type_name "timestamp", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "timestamp" v) @@
         get_timestamp v in
       return (E_literal (Literal_timestamp n))
     )
-  | T_constant ("tez", []) -> (
+  | T_constant (Type_name "tez", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "tez" v) @@
         get_mutez v in
       return (E_literal (Literal_mutez n))
     )
-  | T_constant ("string", []) -> (
+  | T_constant (Type_name "string", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "string" v) @@
         get_string v in
       return (E_literal (Literal_string n))
     )
-  | T_constant ("bytes", []) -> (
+  | T_constant (Type_name "bytes", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "bytes" v) @@
         get_bytes v in
       return (E_literal (Literal_bytes n))
     )
-  | T_constant ("address", []) -> (
+  | T_constant (Type_name "address", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "address" v) @@
         get_string v in
       return (E_literal (Literal_address n))
     )
-  | T_constant ("option", [o]) -> (
+  | T_constant (Type_name "option", [o]) -> (
       let%bind opt =
         trace_strong (wrong_mini_c_value "option" v) @@
         get_option v in
@@ -117,7 +117,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
           let%bind s' = untranspile s o in
           ok (e_a_empty_some s')
     )
-  | T_constant ("map", [k_ty;v_ty]) -> (
+  | T_constant (Type_name "map", [k_ty;v_ty]) -> (
       let%bind lst =
         trace_strong (wrong_mini_c_value "map" v) @@
         get_map v in
@@ -129,7 +129,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_map lst')
     )
-  | T_constant ("big_map", [k_ty;v_ty]) -> (
+  | T_constant (Type_name "big_map", [k_ty;v_ty]) -> (
       let%bind lst =
         trace_strong (wrong_mini_c_value "big_map" v) @@
         get_big_map v in
@@ -141,7 +141,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_big_map lst')
     )
-  | T_constant ("list", [ty]) -> (
+  | T_constant (Type_name "list", [ty]) -> (
       let%bind lst =
         trace_strong (wrong_mini_c_value "list" v) @@
         get_list v in
@@ -150,7 +150,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_list lst')
     )
-  | T_constant ("set", [ty]) -> (
+  | T_constant (Type_name "set", [ty]) -> (
       let%bind lst =
         trace_strong (wrong_mini_c_value "set" v) @@
         get_set v in
@@ -159,15 +159,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_set lst')
     )
-  | T_constant ("contract" , [_ty]) ->
+  | T_constant (Type_name "contract" , [_ty]) ->
     fail @@ bad_untranspile "contract" v
-  | T_constant ("operation" , []) -> (
+  | T_constant (Type_name "operation" , []) -> (
       let%bind op =
         trace_strong (wrong_mini_c_value "operation" v) @@
         get_operation v in
       return (E_literal (Literal_operation op))
     )
-  | T_constant (name , _lst) ->
+  | T_constant (Type_name name , _lst) ->
     fail @@ unknown_untranspile name v
   | T_sum m ->
       let lst = kv_list_of_map m in
@@ -203,3 +203,4 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
       let m' = map_of_kv_list lst in
       return (E_record m')
   | T_function _ -> fail @@ bad_untranspile "function" v
+  | T_variable (Type_name v) -> return (E_variable v)

src/passes/operators/dune

@@ -5,6 +5,7 @@
     simple-utils
     tezos-utils
     ast_typed
+    typesystem
     mini_c
   )
   (preprocess

src/passes/operators/helpers.ml

@@ -113,7 +113,7 @@ module Typer = struct
       List.exists (eq_2 (a , b)) [
         t_int () ;
         t_nat () ;
-        t_tez () ;
+        t_mutez () ;
         t_string () ;
         t_bytes () ;
         t_address () ;

src/passes/operators/operators.ml

@@ -239,6 +239,65 @@ module Typer = struct
   open Helpers.Typer
   open Ast_typed
 
+  module Operators_types = struct
+    open Typesystem.Shorthands
+
+    let tc_subarg   a b c = tc [a;b;c] [ (*TODO…*) ]
+    let tc_sizearg  a     = tc [a]     [ [int] ]
+    let tc_packable a     = tc [a]     [ [int] ; [string] ; [bool] (*TODO…*) ]
+    let tc_timargs  a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
+    let tc_divargs  a b c = tc [a;b;c] [ (*TODO…*) ]
+    let tc_modargs  a b c = tc [a;b;c] [ (*TODO…*) ]
+    let tc_addargs  a b c = tc [a;b;c] [ (*TODO…*) ]
+
+    let t_none         = forall "a" @@ fun a -> option a
+    let t_sub          = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_subarg a b c] => a --> b --> c (* TYPECLASS *)
+    let t_some         = forall "a" @@ fun a -> a --> option a
+    let t_map_remove   = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> map src dst
+    let t_map_add      = forall2 "src" "dst" @@ fun src dst -> src --> dst --> map src dst --> map src dst
+    let t_map_update   = forall2 "src" "dst" @@ fun src dst -> src --> option dst --> map src dst --> map src dst
+    let t_map_mem      = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> bool
+    let t_map_find     = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst
+    let t_map_find_opt = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> option dst
+    let t_map_fold     = forall3 "src" "dst" "acc" @@ fun src dst acc -> ( ( (src * dst) * acc ) --> acc ) --> map src dst --> acc --> acc
+    let t_map_map      = forall3 "k" "v" "result" @@ fun k v result -> ((k * v) --> result) --> map k v --> map k result
+
+    (* TODO: the type of map_map_fold might be wrong, check it. *)
+    let t_map_map_fold = forall4 "k" "v" "acc" "dst" @@ fun k v acc dst -> ( ((k * v) * acc) --> acc * dst ) --> map k v --> (k * v) --> (map k dst * acc)
+    let t_map_iter     = forall2 "k" "v" @@ fun k v -> ( (k * v) --> unit ) --> map k v --> unit
+    let t_size         = forall_tc "c" @@ fun c -> [tc_sizearg c] => c --> nat (* TYPECLASS *)
+    let t_slice        = nat --> nat --> string --> string
+    let t_failwith     = string --> unit
+    let t_get_force    = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst
+    let t_int          = nat --> int
+    let t_bytes_pack   = forall_tc "a" @@ fun a -> [tc_packable a] => a --> bytes (* TYPECLASS *)
+    let t_bytes_unpack = forall_tc "a" @@ fun a -> [tc_packable a] => bytes --> a (* TYPECLASS *)
+    let t_hash256      = bytes --> bytes
+    let t_hash512      = bytes --> bytes
+    let t_blake2b      = bytes --> bytes
+    let t_hash_key     = key --> key_hash
+    let t_check_signature = key --> signature --> bytes --> bool
+    let t_sender       = address
+    let t_source       = address
+    let t_unit         = unit
+    let t_amount       = tez
+    let t_address      = address
+    let t_now          = timestamp
+    let t_transaction  = forall "a" @@ fun a -> a --> tez --> contract a --> operation
+    let t_get_contract = forall "a" @@ fun a -> contract a
+    let t_abs          = int --> nat
+    let t_cons         = forall "a" @@ fun a -> a --> list a --> list a
+    let t_assertion    = bool --> unit
+    let t_times        = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_timargs a b c] => a --> b --> c (* TYPECLASS *)
+    let t_div          = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_divargs a b c] => a --> b --> c (* TYPECLASS *)
+    let t_mod          = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_modargs a b c] => a --> b --> c (* TYPECLASS *)
+    let t_add          = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_addargs a b c] => a --> b --> c (* TYPECLASS *)
+    let t_set_mem      = forall "a" @@ fun a -> a --> set a --> bool
+    let t_set_add      = forall "a" @@ fun a -> a --> set a --> set a
+    let t_set_remove   = forall "a" @@ fun a -> a --> set a --> set a
+    let t_not          = bool --> bool
+  end
+
   let none = typer_0 "NONE" @@ fun tv_opt ->
     match tv_opt with
     | None -> simple_fail "untyped NONE"
@@ -258,8 +317,8 @@ module Typer = struct
     then ok @@ t_int () else
     if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ()))
     then ok @@ t_timestamp () else
-    if (eq_2 (a , b) (t_tez ()))
-    then ok @@ t_tez () else
+    if (eq_2 (a , b) (t_mutez ()))
+    then ok @@ t_mutez () else
       fail (simple_error "Typing substraction, bad parameters.")
 
   let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
@@ -389,16 +448,16 @@ module Typer = struct
 
   let unit = constant "UNIT" @@ t_unit ()
 
-  let amount = constant "AMOUNT" @@ t_tez ()
+  let amount = constant "AMOUNT" @@ t_mutez ()
 
-  let balance = constant "BALANCE" @@ t_tez ()
+  let balance = constant "BALANCE" @@ t_mutez ()
 
   let address = constant "ADDRESS" @@ t_address ()
 
   let now = constant "NOW" @@ t_timestamp ()
 
   let transaction = typer_3 "CALL" @@ fun param amount contract ->
-    let%bind () = assert_t_tez amount in
+    let%bind () = assert_t_mutez amount in
     let%bind contract_param = get_t_contract contract in
     let%bind () = assert_type_value_eq (param , contract_param) in
     ok @@ t_operation ()
@@ -408,7 +467,7 @@ module Typer = struct
     let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in
     let%bind () = assert_eq_1 spendable (t_bool ()) in
     let%bind () = assert_eq_1 delegatable (t_bool ()) in
-    let%bind () = assert_t_tez init_balance in
+    let%bind () = assert_t_mutez init_balance in
     let%bind (arg , res) = get_t_function code in
     let%bind (_param , storage) = get_t_pair arg in
     let%bind (storage' , op_lst) = get_t_pair res in
@@ -449,8 +508,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if (eq_1 a (t_nat ()) && eq_1 b (t_tez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_tez ()))
-    then ok @@ t_tez () else
+    if (eq_1 a (t_nat ()) && eq_1 b (t_mutez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_mutez ()))
+    then ok @@ t_mutez () else
       simple_fail "Multiplying with wrong types"
 
   let div = typer_2 "DIV" @@ fun a b ->
@@ -458,17 +517,17 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if eq_1 a (t_tez ()) && eq_1 b (t_nat ())
-    then ok @@ t_tez () else
-    if eq_1 a (t_tez ()) && eq_1 b (t_tez ())
+    if eq_1 a (t_mutez ()) && eq_1 b (t_nat ())
+    then ok @@ t_mutez () else
+    if eq_1 a (t_mutez ()) && eq_1 b (t_mutez ())
     then ok @@ t_nat () else
       simple_fail "Dividing with wrong types"
 
   let mod_ = typer_2 "MOD" @@ fun a b ->
     if (eq_1 a (t_nat ()) || eq_1 a (t_int ())) && (eq_1 b (t_nat ()) || eq_1 b (t_int ()))
     then ok @@ t_nat () else
-    if eq_1 a (t_tez ()) && eq_1 b (t_tez ())
-    then ok @@ t_tez () else
+    if eq_1 a (t_mutez ()) && eq_1 b (t_mutez ())
+    then ok @@ t_mutez () else
       simple_fail "Computing modulo with wrong types"
 
   let add = typer_2 "ADD" @@ fun a b ->
@@ -476,8 +535,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
-    if eq_2 (a , b) (t_tez ())
-    then ok @@ t_tez () else
+    if eq_2 (a , b) (t_mutez ())
+    then ok @@ t_mutez () else
     if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
     then ok @@ t_int () else
     if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ()))
@@ -697,6 +756,7 @@ module Typer = struct
       get_contract ;
       neg ;
       abs ;
+      cons ;
       now ;
       slice ;
       address ;

src/passes/operators/operators.mli

@@ -22,6 +22,79 @@ module Typer : sig
   open Helpers.Typer
   open Ast_typed
 
+  module Operators_types : sig
+    (* TODO: we need a map from type names to type values. Then, all
+       these bindings don't need to be exported anymore. *)
+      val tc_subarg :
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_sizearg :
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_packable :
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_timargs :
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_divargs :
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_modargs :
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val tc_addargs :
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value ->
+        Typesystem.Core.type_value -> Typesystem.Core.type_constraint
+      val t_none : Typesystem.Core.type_value
+      val t_sub : Typesystem.Core.type_value
+      val t_some : Typesystem.Core.type_value
+      val t_map_remove : Typesystem.Core.type_value
+      val t_map_add : Typesystem.Core.type_value
+      val t_map_update : Typesystem.Core.type_value
+      val t_map_mem : Typesystem.Core.type_value
+      val t_map_find : Typesystem.Core.type_value
+      val t_map_find_opt : Typesystem.Core.type_value
+      val t_map_fold : Typesystem.Core.type_value
+      val t_map_map : Typesystem.Core.type_value
+      val t_map_map_fold : Typesystem.Core.type_value
+      val t_map_iter : Typesystem.Core.type_value
+      val t_size : Typesystem.Core.type_value
+      val t_slice : Typesystem.Core.type_value
+      val t_failwith : Typesystem.Core.type_value
+      val t_get_force : Typesystem.Core.type_value
+      val t_int : Typesystem.Core.type_value
+      val t_bytes_pack : Typesystem.Core.type_value
+      val t_bytes_unpack : Typesystem.Core.type_value
+      val t_hash256 : Typesystem.Core.type_value
+      val t_hash512 : Typesystem.Core.type_value
+      val t_blake2b : Typesystem.Core.type_value
+      val t_hash_key : Typesystem.Core.type_value
+      val t_check_signature : Typesystem.Core.type_value
+      val t_sender : Typesystem.Core.type_value
+      val t_source : Typesystem.Core.type_value
+      val t_unit : Typesystem.Core.type_value
+      val t_amount : Typesystem.Core.type_value
+      val t_address : Typesystem.Core.type_value
+      val t_now : Typesystem.Core.type_value
+      val t_transaction : Typesystem.Core.type_value
+      val t_get_contract : Typesystem.Core.type_value
+      val t_abs : Typesystem.Core.type_value
+      val t_cons : Typesystem.Core.type_value
+      val t_assertion : Typesystem.Core.type_value
+      val t_times : Typesystem.Core.type_value
+      val t_div : Typesystem.Core.type_value
+      val t_mod : Typesystem.Core.type_value
+      val t_add : Typesystem.Core.type_value
+      val t_set_mem : Typesystem.Core.type_value
+      val t_set_add : Typesystem.Core.type_value
+      val t_set_remove : Typesystem.Core.type_value
+      val t_not : Typesystem.Core.type_value
+    end
+
   (*
   val none : typer
   val set_empty : typer

src/stages/ast_typed/PP.ml

@@ -12,8 +12,9 @@ let rec type_value' ppf (tv':type_value') : unit =
   | T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_value) m
   | T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_value) m
   | T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
-  | T_constant (c, []) -> fprintf ppf "%s" c
-  | T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
+  | T_constant (Type_name c, []) -> fprintf ppf "%s" c
+  | T_constant (Type_name c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
+  | T_variable (Type_name name) -> fprintf ppf "%s" name
 
 and type_value ppf (tv:type_value) : unit =
   type_value' ppf tv.type_value'

src/stages/ast_typed/combinators.ml

@@ -5,30 +5,30 @@ let make_t type_value' simplified = { type_value' ; simplified }
 let make_a_e ?(location = Location.generated) expression type_annotation environment = {
   expression ;
   type_annotation ;
-  dummy_field = () ;
   environment ;
   location ;
 }
 let make_n_e name a_e = { name ; annotated_expression = a_e }
 let make_n_t type_name type_value = { type_name ; type_value }
 
-let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
-let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
-let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
-let t_key ?s () : type_value = make_t (T_constant ("key", [])) s
-let t_key_hash ?s () : type_value = make_t (T_constant ("key_hash", [])) s
-let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
-let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
-let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
-let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
-let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s
-let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) s
-let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
-let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
+let t_bool ?s () : type_value = make_t (T_constant (Type_name "bool", [])) s
+let t_string ?s () : type_value = make_t (T_constant (Type_name "string", [])) s
+let t_bytes ?s () : type_value = make_t (T_constant (Type_name "bytes", [])) s
+let t_key ?s () : type_value = make_t (T_constant (Type_name "key", [])) s
+let t_key_hash ?s () : type_value = make_t (T_constant (Type_name "key_hash", [])) s
+let t_int ?s () : type_value = make_t (T_constant (Type_name "int", [])) s
+let t_address ?s () : type_value = make_t (T_constant (Type_name "address", [])) s
+let t_operation ?s () : type_value = make_t (T_constant (Type_name "operation", [])) s
+let t_nat ?s () : type_value = make_t (T_constant (Type_name "nat", [])) s
+let t_mutez ?s () : type_value = make_t (T_constant (Type_name "tez", [])) s
+let t_timestamp ?s () : type_value = make_t (T_constant (Type_name "timestamp", [])) s
+let t_unit ?s () : type_value = make_t (T_constant (Type_name "unit", [])) s
+let t_option o ?s () : type_value = make_t (T_constant (Type_name "option", [o])) s
 let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
-let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
-let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s
-let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
+let t_variable t ?s () : type_value = make_t (T_variable t) s
+let t_list t ?s () : type_value = make_t (T_constant (Type_name "list", [t])) s
+let t_set t ?s () : type_value = make_t (T_constant (Type_name "set", [t])) s
+let t_contract t ?s () : type_value = make_t (T_constant (Type_name "contract", [t])) s
 let t_pair a b ?s () = t_tuple [a ; b] ?s ()
 
 let t_record m ?s () : type_value = make_t (T_record m) s
@@ -40,8 +40,8 @@ let ez_t_record lst ?s () : type_value =
   let m = SMap.of_list lst in
   t_record m ?s ()
 
-let t_map key value ?s () = make_t (T_constant ("map", [key ; value])) s
-let t_big_map key value ?s () = make_t (T_constant ("big_map", [key ; value])) s
+let t_map key value ?s () = make_t (T_constant (Type_name "map", [key ; value])) s
+let t_big_map key value ?s () = make_t (T_constant (Type_name "big_map", [key ; value])) s
 
 let t_sum m ?s () : type_value = make_t (T_sum m) s
 let make_t_ez_sum (lst:(string * type_value) list) : type_value =
@@ -67,59 +67,59 @@ let get_lambda_with_type e =
   | _ -> simple_fail "not a lambda with functional type"
 
 let get_t_bool (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("bool", []) -> ok ()
+  | T_constant (Type_name "bool", []) -> ok ()
   | _ -> simple_fail "not a bool"
 
 let get_t_int (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("int", []) -> ok ()
+  | T_constant (Type_name "int", []) -> ok ()
   | _ -> simple_fail "not a int"
 
 let get_t_nat (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("nat", []) -> ok ()
+  | T_constant (Type_name "nat", []) -> ok ()
   | _ -> simple_fail "not a nat"
 
 let get_t_unit (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("unit", []) -> ok ()
+  | T_constant (Type_name "unit", []) -> ok ()
   | _ -> simple_fail "not a unit"
 
-let get_t_tez (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("tez", []) -> ok ()
+let get_t_mutez (t:type_value) : unit result = match t.type_value' with
+  | T_constant (Type_name "tez", []) -> ok ()
   | _ -> simple_fail "not a tez"
 
 let get_t_bytes (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("bytes", []) -> ok ()
+  | T_constant (Type_name "bytes", []) -> ok ()
   | _ -> simple_fail "not a bytes"
 
 let get_t_string (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("string", []) -> ok ()
+  | T_constant (Type_name "string", []) -> ok ()
   | _ -> simple_fail "not a string"
 
 let get_t_contract (t:type_value) : type_value result = match t.type_value' with
-  | T_constant ("contract", [x]) -> ok x
+  | T_constant (Type_name "contract", [x]) -> ok x
   | _ -> simple_fail "not a contract"
 
 let get_t_option (t:type_value) : type_value result = match t.type_value' with
-  | T_constant ("option", [o]) -> ok o
+  | T_constant (Type_name "option", [o]) -> ok o
   | _ -> simple_fail "not a option"
 
 let get_t_list (t:type_value) : type_value result = match t.type_value' with
-  | T_constant ("list", [o]) -> ok o
+  | T_constant (Type_name "list", [o]) -> ok o
   | _ -> simple_fail "not a list"
 
 let get_t_set (t:type_value) : type_value result = match t.type_value' with
-  | T_constant ("set", [o]) -> ok o
+  | T_constant (Type_name "set", [o]) -> ok o
   | _ -> simple_fail "not a set"
 
 let get_t_key (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("key", []) -> ok ()
+  | T_constant (Type_name "key", []) -> ok ()
   | _ -> simple_fail "not a key"
 
 let get_t_signature (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("signature", []) -> ok ()
+  | T_constant (Type_name "signature", []) -> ok ()
   | _ -> simple_fail "not a signature"
 
 let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
-  | T_constant ("key_hash", []) -> ok ()
+  | T_constant (Type_name "key_hash", []) -> ok ()
   | _ -> simple_fail "not a key_hash"
 
 let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
@@ -148,12 +148,12 @@ let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value'
 
 let get_t_map (t:type_value) : (type_value * type_value) result =
   match t.type_value' with
-  | T_constant ("map", [k;v]) -> ok (k, v)
+  | T_constant (Type_name "map", [k;v]) -> ok (k, v)
   | _ -> simple_fail "get: not a map"
 
 let get_t_big_map (t:type_value) : (type_value * type_value) result =
   match t.type_value' with
-  | T_constant ("big_map", [k;v]) -> ok (k, v)
+  | T_constant (Type_name "big_map", [k;v]) -> ok (k, v)
   | _ -> simple_fail "get: not a big_map"
 
 let get_t_map_key : type_value -> type_value result = fun t ->
@@ -179,7 +179,7 @@ let assert_t_map = fun t ->
 let is_t_map = Function.compose to_bool get_t_map
 let is_t_big_map = Function.compose to_bool get_t_big_map
 
-let assert_t_tez : type_value -> unit result = get_t_tez
+let assert_t_mutez : type_value -> unit result = get_t_mutez
 let assert_t_key = get_t_key
 let assert_t_signature = get_t_signature
 let assert_t_key_hash = get_t_key_hash
@@ -201,7 +201,7 @@ let assert_t_bytes = fun t ->
 
 let assert_t_operation (t:type_value) : unit result =
   match t.type_value' with
-  | T_constant ("operation" , []) -> ok ()
+  | T_constant (Type_name "operation" , []) -> ok ()
   | _ -> simple_fail "assert: not an operation"
 
 let assert_t_list_operation (t : type_value) : unit result =
@@ -209,11 +209,11 @@ let assert_t_list_operation (t : type_value) : unit result =
   assert_t_operation t'
 
 let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with
-  | T_constant ("int", []) -> ok ()
+  | T_constant (Type_name "int", []) -> ok ()
   | _ -> simple_fail "not an int"
 
 let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with
-  | T_constant ("nat", []) -> ok ()
+  | T_constant (Type_name "nat", []) -> ok ()
   | _ -> simple_fail "not an nat"
 
 let assert_t_bool : type_value -> unit result = fun v -> get_t_bool v
@@ -235,6 +235,8 @@ let e_nat n : expression = E_literal (Literal_nat n)
 let e_mutez n : expression = E_literal (Literal_mutez n)
 let e_bool b : expression = E_literal (Literal_bool b)
 let e_string s : expression = E_literal (Literal_string s)
+let e_bytes s : expression = E_literal (Literal_bytes s)
+let e_timestamp s : expression = E_literal (Literal_timestamp s)
 let e_address s : expression = E_literal (Literal_address s)
 let e_operation s : expression = E_literal (Literal_operation s)
 let e_lambda l : expression = E_lambda l
@@ -243,11 +245,12 @@ let e_application a b : expression = E_application (a , b)
 let e_variable v : expression = E_variable v
 let e_list lst : expression = E_list lst
 let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
+let e_tuple lst : expression = E_tuple lst
 
 let e_a_unit = make_a_e e_unit (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
 let e_a_nat n = make_a_e (e_nat n) (t_nat ())
-let e_a_mutez n = make_a_e (e_mutez n) (t_tez ())
+let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ())
 let e_a_bool b = make_a_e (e_bool b) (t_bool ())
 let e_a_string s = make_a_e (e_string s) (t_string ())
 let e_a_address s = make_a_e (e_address s) (t_address ())

src/stages/ast_typed/combinators.mli

@@ -17,13 +17,14 @@ val t_set : type_value -> ?s:S.type_expression -> unit -> type_value
 val t_contract : type_value -> ?s:S.type_expression -> unit -> type_value
 val t_int : ?s:S.type_expression -> unit -> type_value
 val t_nat : ?s:S.type_expression -> unit -> type_value
-val t_tez : ?s:S.type_expression -> unit -> type_value
+val t_mutez : ?s:S.type_expression -> unit -> type_value
 val t_address : ?s:S.type_expression -> unit -> type_value
 val t_unit : ?s:S.type_expression -> unit -> type_value
 val t_option : type_value -> ?s:S.type_expression -> unit -> type_value
 val t_pair : type_value -> type_value -> ?s:S.type_expression -> unit -> type_value
 val t_list  : type_value -> ?s:S.type_expression -> unit -> type_value
 val t_tuple : type_value list -> ?s:S.type_expression -> unit -> type_value
+val t_variable : type_name -> ?s:S.type_expression -> unit -> type_value
 val t_record : tv_map -> ?s:S.type_expression -> unit -> type_value
 val make_t_ez_record : (string * type_value) list -> type_value 
 (*
@@ -47,7 +48,7 @@ val get_t_bool : type_value -> unit result
 val get_t_int : type_value -> unit result
 val get_t_nat : type_value -> unit result
 val get_t_unit : type_value -> unit result
-val get_t_tez : type_value -> unit result
+val get_t_mutez : type_value -> unit result
 val get_t_bytes : type_value -> unit result 
 val get_t_string : type_value -> unit result
 *)
@@ -77,7 +78,7 @@ val assert_t_map : type_value -> unit result
 val is_t_map : type_value -> bool
 val is_t_big_map : type_value -> bool 
 
-val assert_t_tez : type_value -> unit result
+val assert_t_mutez : type_value -> unit result
 val assert_t_key : type_value -> unit result
 val assert_t_signature : type_value -> unit result
 val assert_t_key_hash : type_value -> unit result
@@ -104,26 +105,27 @@ val assert_t_unit : type_value -> unit result
 val e_record : ae_map -> expression
 val ez_e_record : ( string * annotated_expression ) list -> expression
 
+*)
 val e_some : value -> expression
 val e_none : expression
 val e_map : ( value * value ) list -> expression
 val e_unit : expression
 val e_int : int -> expression
 val e_nat : int -> expression
-val e_tez : int -> expression
+val e_mutez : int -> expression
 val e_bool : bool -> expression
 val e_string : string -> expression
-*)
+val e_bytes : bytes -> expression
+val e_timestamp : int -> expression
 val e_address : string -> expression
 val e_operation : Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation -> expression
-(*
 val e_lambda : lambda -> expression
 val e_pair : value -> value -> expression
 val e_application : value -> value -> expression
 val e_variable : name -> expression
 val e_list : value list -> expression
 val e_let_in : string -> value -> value -> expression
-*)
+val e_tuple : value list -> expression
 
 val e_a_unit : full_environment -> annotated_expression
 val e_a_int : int -> full_environment -> annotated_expression

src/stages/ast_typed/environment.ml

@@ -43,7 +43,10 @@ let get_constructor : string -> t -> (type_value * type_value) option = fun k x
   let aux = fun x ->
     let aux = fun (_type_name , x) ->
       match x.type_value' with
-      | T_sum m when Map.String.mem k m -> Some (Map.String.find k m , x)
+      | T_sum m ->
+        (match Map.String.find_opt k m with
+           Some km -> Some (km , x)
+         | None -> None)
       | _ -> None
     in
     List.find_map aux (Small.get_type_environment x) in

src/stages/ast_typed/misc.ml

@@ -296,7 +296,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       bind_list_iter assert_type_value_eq (List.combine ta tb)
     )
   | T_tuple _, _ -> fail @@ different_kinds a b
-  | T_constant (ca, lsta), T_constant (cb, lstb) -> (
+  | T_constant (Type_name ca, lsta), T_constant (Type_name cb, lstb) -> (
       let%bind _ =
         trace_strong (different_size_constants a b)
         @@ Assert.assert_true List.(length lsta = length lstb) in
@@ -346,6 +346,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ = assert_type_value_eq (result, result') in
       ok ()
   | T_function _, _ -> fail @@ different_kinds a b
+  | T_variable x, T_variable y -> let _ = (x = y) in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding"
+  | T_variable _, _ -> fail @@ different_kinds a b
 
 (* No information about what made it fail *)
 let type_value_eq ab = Trace.to_bool @@ assert_type_value_eq ab

src/stages/ast_typed/types.ml

@@ -5,7 +5,7 @@ module S = Ast_simplified
 module SMap = Map.String
 
 type name = string
-type type_name = string
+type type_name = Type_name of string
 type constructor_name = string
 
 type 'a name_map = 'a SMap.t
@@ -24,21 +24,20 @@ and environment_element_definition =
 and free_variables = name list
 
 and environment_element = {
-  type_value : type_value ;
+  type_value : type_value ;     (* SUBST ??? *)
   source_environment : full_environment ;
   definition : environment_element_definition ;
 }
 and environment = (string * environment_element) list
-and type_environment = (string * type_value) list
+and type_environment = (string * type_value) list (* SUBST ??? *)
 and small_environment = (environment * type_environment)
 and full_environment = small_environment List.Ne.t
 
 and annotated_expression = {
   expression : expression ;
-  type_annotation : tv ;
+  type_annotation : tv ;        (* SUBST *)
   environment : full_environment ;
   location : Location.t ;
-  dummy_field : unit ;
 }
 
 and named_expression = {
@@ -55,19 +54,24 @@ and type_value' =
   | T_tuple of tv list
   | T_sum of tv_map
   | T_record of tv_map
-  | T_constant of type_name * tv list
+  | T_constant of type_name * tv list (* SUBST ??? I think not, at least not necessary for now and the types don't match *)
+  | T_variable of type_name     (* SUBST *)
   | T_function of (tv * tv)
 
 and type_value = {
   type_value' : type_value' ;
-  simplified : S.type_expression option ;
+  simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *)
 }
 
+(* This is used in E_assign of (named_type_value * access_path * ae).
+   In mini_c, we need the type associated with `x` in the assignment
+   expression `x.y.z := 42`, so it is stored here. *)
 and named_type_value = {
   type_name: name ;
   type_value : type_value ;
 }
 
+(* E_lamba and other expressions are always wrapped as an annotated_expression. *)
 and lambda = {
   binder : name ;
   (* input_type: tv ;

src/stages/typesystem/core.ml

@@ -0,0 +1,74 @@
+type type_variable = (*Type_variable *) string
+
+(* generate a new type variable and gave it an id *)
+let fresh_type_variable : ?name:string -> unit -> type_variable =
+  let id = ref 0 in
+  let inc () = id := !id + 1 in
+  fun ?name () ->
+    inc () ;
+    match name with
+    | None -> (*Type_variable*) "type_variable_" ^ (string_of_int !id)
+    | Some name -> (*Type_variable*)"tv_" ^ name ^ "_" ^ (string_of_int !id)
+
+
+(* add information on the type or the kind for operator*)
+type constant_tag =
+  | C_arrow     (* * -> * -> * *) (* isn't this wrong*)
+  | C_option    (* * -> * *)
+  | C_tuple     (* * … -> * *)
+  | C_record    (* ( label , * ) … -> * *)
+  | C_variant   (* ( label , * ) … -> * *)
+  | C_map       (* * -> * -> * *)
+  | C_big_map   (* * -> * -> * *)
+  | C_list      (* * -> * *)
+  | C_set       (* * -> * *)
+  | C_unit      (* * *)
+  | C_bool      (* * *)
+  | C_string    (* * *)
+  | C_nat       (* * *)
+  | C_tez       (* * *)
+  | C_timestamp (* * *)
+  | C_int       (* * *)
+  | C_address   (* * *)
+  | C_bytes     (* * *)
+  | C_key_hash  (* * *)
+  | C_key       (* * *)
+  | C_signature (* * *)
+  | C_operation (* * *)
+  | C_contract  (* * -> * *)
+
+type label =
+  | L_int of int
+  | L_string of string
+
+(* Weird stuff; please explain *)
+type type_value =
+  | P_forall       of p_forall
+  | P_variable     of type_variable (* how a value can be a variable? *)
+  | P_constant     of (constant_tag * type_value list)
+  | P_apply        of (type_value * type_value)
+
+and p_forall = {
+  binder      : type_variable ;
+  constraints : type_constraint list ;
+  body        : type_value
+}
+
+(* Different type of constraint *) (* why isn't this a variant ? *)
+and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *)
+and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *)
+and c_const = (type_variable * type_value)
+and c_equation = (type_value * type_value)
+and c_typeclass = (type_value list * typeclass)
+and c_access_label = (type_value * label * type_variable)
+
+(*What i was saying just before *)
+and type_constraint =
+  (* | C_assignment of (type_variable * type_pattern) *)
+  | C_equation of c_equation (* TVA = TVB *)
+  | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
+  | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *)
+(* | … *)
+
+(* is the first list in case on of the type of the type class as a kind *->*->* ? *)
+and typeclass = type_value list list

src/stages/typesystem/dune

@@ -0,0 +1,14 @@
+(library
+  (name typesystem)
+  (public_name ligo.typesystem)
+  (libraries
+    simple-utils
+    tezos-utils
+    ast_typed
+    mini_c
+  )
+  (preprocess
+    (pps ppx_let)
+  )
+  (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
+)

src/stages/typesystem/misc.ml

@@ -0,0 +1,288 @@
+open Core
+
+let pair_map = fun f (x , y) -> (f x , f y)
+
+module Substitution = struct
+
+  module Pattern = struct
+
+    open Trace
+    module T = Ast_typed
+    module TSMap = Trace.TMap(String)
+
+    type 'a w = 'a -> 'a result
+
+    let rec rec_yes = true
+    and s_environment_element_definition ~v ~expr = function
+      | T.ED_binder -> ok @@ T.ED_binder
+      | T.ED_declaration (val_, free_variables) ->
+        let%bind val_ = s_annotated_expression ~v ~expr  val_ in
+        let%bind free_variables = bind_map_list (s_type_variable ~v ~expr) free_variables in
+        ok @@ T.ED_declaration (val_, free_variables)
+    and s_environment ~v ~expr = fun lst ->
+      bind_map_list (fun (type_variable, T.{ type_value; source_environment; definition }) ->
+          let _ = type_value in
+          let%bind type_variable = s_type_variable ~v ~expr type_variable in
+          let%bind type_value = s_type_value ~v ~expr type_value in
+          let%bind source_environment = s_full_environment ~v ~expr source_environment in
+          let%bind definition = s_environment_element_definition ~v ~expr definition in
+          ok @@ (type_variable, T.{ type_value; source_environment; definition })
+        ) lst
+    and s_type_environment ~v ~expr : T.type_environment w = fun tenv ->
+      bind_map_list (fun (type_variable , type_value) ->
+        let%bind type_variable = s_type_variable ~v ~expr type_variable in
+        let%bind type_value = s_type_value ~v ~expr type_value in
+        ok @@ (type_variable , type_value)) tenv
+    and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) ->
+      let%bind environment = s_environment ~v ~expr environment in
+      let%bind type_environment = s_type_environment ~v ~expr type_environment in
+      ok @@ (environment, type_environment)
+    and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) ->
+      let%bind a = s_small_environment ~v ~expr a in
+      let%bind b = bind_map_list (s_small_environment ~v ~expr) b in
+      ok (a , b)
+
+    and s_variable ~v ~expr : T.name w = fun var ->
+      let () = ignore (v, expr) in
+      ok var
+
+    and s_type_variable ~v ~expr : T.name w = fun tvar ->
+      let _TODO = ignore (v, expr) in
+      Printf.printf "TODO: subst: unimplemented case s_type_variable";
+      ok @@ tvar
+      (* if String.equal tvar v then
+       *   expr
+       * else
+       *   ok tvar *)
+
+    and s_type_name_constant ~v ~expr : T.type_name w = fun type_name ->
+      (* TODO: we don't need to subst anything, right? *)
+      let () = ignore (v , expr) in
+      ok @@ type_name
+
+    and s_type_value' ~v ~expr : T.type_value' w = function
+        | T.T_tuple type_value_list ->
+          let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
+          ok @@ T.T_tuple type_value_list
+        | T.T_sum _ -> failwith "TODO: T_sum"
+        | T.T_record _ -> failwith "TODO: T_record"
+        | T.T_constant (type_name, type_value_list) ->
+          let%bind type_name = s_type_name_constant ~v ~expr type_name in
+          let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
+          ok @@ T.T_constant (type_name, type_value_list)
+        | T.T_variable _ -> failwith "TODO: T_variable"
+        | T.T_function _ ->
+          let _TODO = (v, expr) in
+          failwith "TODO: T_function"
+
+    and s_type_expression ~v ~expr : Ast_simplified.type_expression w = function
+      | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression"
+      | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression"
+      | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression"
+      | Ast_simplified.T_function (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression"
+      | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression"
+      | Ast_simplified.T_constant (_, _) ->
+        let _TODO = (v, expr) in
+        failwith "TODO: subst: unimplemented case s_type_expression"
+
+    and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } ->
+      let%bind type_value' = s_type_value' ~v ~expr type_value' in
+      let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in
+      ok @@ T.{ type_value'; simplified }
+    and s_literal ~v ~expr : T.literal w = function
+      | T.Literal_unit ->
+        let () = ignore (v, expr) in
+        ok @@ T.Literal_unit
+      | (T.Literal_bool _ as x)
+      | (T.Literal_int _ as x)
+      | (T.Literal_nat _ as x)
+      | (T.Literal_timestamp _ as x)
+      | (T.Literal_mutez _ as x)
+      | (T.Literal_string _ as x)
+      | (T.Literal_bytes _ as x)
+      | (T.Literal_address _ as x)
+      | (T.Literal_operation _ as x) ->
+        ok @@ x
+    and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->
+      let _TODO = v, expr in
+      failwith "TODO: subst: unimplemented case s_matching"
+    and s_named_type_value ~v ~expr : T.named_type_value w = fun _ ->
+      let _TODO = v, expr in
+      failwith "TODO: subst: unimplemented case s_named_type_value"
+    and s_access_path  ~v ~expr : T.access_path w = fun _ ->
+      let _TODO = v, expr in
+      failwith "TODO: subst: unimplemented case s_access_path"
+
+    and s_expression ~v ~expr : T.expression w = function
+      | T.E_literal         x ->
+        let%bind x = s_literal ~v ~expr x in
+        ok @@ T.E_literal x
+      | T.E_constant        (var, vals) ->
+        let%bind var = s_variable ~v ~expr var in
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_constant (var, vals)
+      | T.E_variable        tv ->
+        let%bind tv = s_variable ~v ~expr tv in
+        ok @@ T.E_variable tv
+      | T.E_application     (val1 , val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_application (val1 , val2)
+      | T.E_lambda          { binder; body } ->
+        let%bind binder = s_variable ~v ~expr binder in
+        let%bind body = s_annotated_expression ~v ~expr body in
+        ok @@ T.E_lambda { binder; body }
+      | T.E_let_in          { binder; rhs; result } ->
+        let%bind binder = s_variable ~v ~expr binder in
+        let%bind rhs = s_annotated_expression ~v ~expr rhs in
+        let%bind result = s_annotated_expression ~v ~expr result in
+        ok @@ T.E_let_in { binder; rhs; result }
+      | T.E_tuple           vals ->
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_tuple vals
+      | T.E_tuple_accessor  (val_, i) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let i = i in
+        ok @@ T.E_tuple_accessor (val_, i)
+      | T.E_constructor     (tvar, val_) ->
+        let%bind tvar = s_type_variable ~v ~expr tvar in
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        ok @@ T.E_constructor (tvar, val_)
+      | T.E_record          aemap ->
+        let _TODO = aemap in
+        failwith "TODO: subst in record"
+        (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
+         *     let key = s_type_variable ~v ~expr key in
+         *     let val_ = s_annotated_expression ~v ~expr val_ in
+         *     ok @@ (key , val_)) aemap in
+         * ok @@ T.E_record aemap *)
+      | T.E_record_accessor (val_, tvar) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind tvar = s_type_variable ~v ~expr tvar in
+        ok @@ T.E_record_accessor (val_, tvar)
+      | T.E_map             val_val_list ->
+        let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
+            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            ok @@ (val1 , val2)
+          ) val_val_list in
+        ok @@ T.E_map val_val_list
+      | T.E_big_map         val_val_list ->
+        let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
+            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            ok @@ (val1 , val2)
+          ) val_val_list in
+        ok @@ T.E_big_map val_val_list
+      | T.E_list            vals ->
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_list vals
+      | T.E_set             vals ->
+        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        ok @@ T.E_set vals
+      | T.E_look_up         (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_look_up (val1 , val2)
+      | T.E_matching         (val_ , matching_expr) ->
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind matching = s_matching_expr ~v ~expr matching_expr in
+        ok @@ T.E_matching (val_ , matching)
+      | T.E_sequence        (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_sequence (val1 , val2)
+      | T.E_loop            (val1, val2) ->
+        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        ok @@ T.E_loop (val1 , val2)
+      | T.E_assign          (named_tval, access_path, val_) ->
+        let%bind named_tval = s_named_type_value ~v ~expr named_tval in
+        let%bind access_path = s_access_path ~v ~expr access_path in
+        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        ok @@ T.E_assign (named_tval, access_path, val_)
+
+    and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } ->
+      let%bind expression = s_expression ~v ~expr expression in
+      let%bind type_annotation = s_type_value ~v ~expr type_annotation in
+      let%bind environment = s_full_environment ~v ~expr environment in
+      let location = location in
+      ok T.{ expression; type_annotation; environment; location }
+
+    and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } ->
+      let%bind name = s_type_variable ~v ~expr name in
+      let%bind annotated_expression = s_annotated_expression ~v ~expr annotated_expression in
+      ok T.{ name; annotated_expression }
+
+    and s_declaration ~v ~expr : T.declaration w =
+      function
+        Ast_typed.Declaration_constant (e, (env1, env2)) ->
+        let%bind e = s_named_expression ~v ~expr e in
+        let%bind env1 = s_full_environment ~v ~expr env1 in
+        let%bind env2 = s_full_environment ~v ~expr env2 in
+        ok @@ Ast_typed.Declaration_constant (e, (env1, env2))
+
+    and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d ->
+      Trace.bind_map_location (s_declaration ~v ~expr) d
+
+    (* Replace the type variable ~v with ~expr everywhere within the
+       program ~p. TODO: issues with scoping/shadowing. *)
+    and program ~(p : Ast_typed.program) ~(v:string (* this string is a type_name or type_variable I think *)) ~expr : Ast_typed.program Trace.result =
+      Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
+
+    (*
+       Computes `P[v := expr]`.
+    *)
+    and type_value ~tv ~v ~expr =
+      let self tv = type_value ~tv ~v ~expr in
+      match tv with
+      | P_variable v' when v' = v -> expr
+      | P_variable _ -> tv
+      | P_constant (x , lst) -> (
+          let lst' = List.map self lst in
+          P_constant (x , lst')
+        )
+      | P_apply ab -> (
+          let ab' = pair_map self ab in
+          P_apply ab'
+        )
+      | P_forall p -> (
+          let aux c = constraint_ ~c ~v ~expr in
+          let constraints = List.map aux p.constraints in
+          if (p.binder = v) then (
+            P_forall { p with constraints }
+          ) else (
+            let body = self p.body in
+            P_forall { p with constraints ; body }
+          )
+        )
+
+    and constraint_ ~c ~v ~expr =
+      match c with
+      | C_equation ab -> (
+          let ab' = pair_map (fun tv -> type_value ~tv ~v ~expr) ab in
+          C_equation ab'
+        )
+      | C_typeclass (tvs , tc) -> (
+          let tvs' = List.map (fun tv -> type_value ~tv ~v ~expr) tvs in
+          let tc' = typeclass ~tc ~v ~expr in
+          C_typeclass (tvs' , tc')
+        )
+      | C_access_label (tv , l , v') -> (
+          let tv' = type_value ~tv ~v ~expr in
+          C_access_label (tv' , l , v')
+        )
+
+    and typeclass ~tc ~v ~expr =
+      List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc
+
+    (* Performs beta-reduction at the root of the type *)
+    let eval_beta_root ~(tv : type_value) =
+      match tv with
+        P_apply (P_forall { binder; constraints; body }, arg) ->
+        let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in
+        (type_value ~tv:body ~v:binder ~expr:arg , constraints)
+      | _ -> (tv , [])
+  end
+
+end

src/stages/typesystem/shorthands.ml

@@ -0,0 +1,63 @@
+open Core
+
+let tc type_vars allowed_list =
+  Core.C_typeclass (type_vars , allowed_list)
+
+let forall binder f =
+  let () = ignore binder in
+  let freshvar = fresh_type_variable () in
+  P_forall { binder = freshvar ; constraints = [] ; body = f (P_variable freshvar) }
+
+let forall_tc binder f =
+  let () = ignore binder in
+  let freshvar = fresh_type_variable () in
+  let (tc, ty) = f (P_variable freshvar) in
+  P_forall { binder = freshvar ; constraints = tc ; body = ty }
+
+(* chained forall *)
+let forall2 a b f =
+  forall a @@ fun a' ->
+  forall b @@ fun b' ->
+  f a' b'
+
+let forall3 a b c f =
+  forall a @@ fun a' ->
+  forall b @@ fun b' ->
+  forall c @@ fun c' ->
+  f a' b' c'
+
+let forall4 a b c d f =
+  forall a @@ fun a' ->
+  forall b @@ fun b' ->
+  forall c @@ fun c' ->
+  forall d @@ fun d' ->
+  f a' b' c' d'
+
+let forall3_tc a b c f =
+  forall    a @@ fun a' ->
+  forall    b @@ fun b' ->
+  forall_tc c @@ fun c' ->
+  f a' b' c'
+
+let (-->) arg ret = P_constant (C_arrow  , [arg; ret])
+let (=>) tc ty = (tc , ty)
+let option t  = P_constant (C_option  , [t])
+let pair a b  = P_constant (C_tuple , [a; b])
+let map  k v  = P_constant (C_map   , [k; v])
+let unit      = P_constant (C_unit    , [])
+let list   t  = P_constant (C_list    , [t])
+let set    t  = P_constant (C_set     , [t])
+let bool      = P_constant (C_bool    , [])
+let string    = P_constant (C_string  , [])
+let nat       = P_constant (C_nat     , [])
+let tez       = P_constant (C_tez     , [])
+let timestamp = P_constant (C_timestamp , [])
+let int       = P_constant (C_int     , [])
+let address   = P_constant (C_address , [])
+let bytes     = P_constant (C_bytes   , [])
+let key       = P_constant (C_key     , [])
+let key_hash  = P_constant (C_key_hash  , [])
+let signature = P_constant (C_signature , [])
+let operation = P_constant (C_operation , [])
+let contract t = P_constant (C_contract , [t])
+let ( * ) a b = pair a b

src/stages/typesystem/typesystem.ml

@@ -0,0 +1,3 @@
+module Core = Core
+module Shorthands = Shorthands
+module Misc = Misc

src/test/coase_tests.ml

@@ -10,7 +10,8 @@ let get_program =
   fun () -> match !s with
     | Some s -> ok s
     | None -> (
-        let%bind program = type_file "./contracts/coase.ligo" in
+        let%bind (program , state) = type_file "./contracts/coase.ligo" in
+        let () = Typer.Solver.discard_state state in
         s := Some program ;
         ok program
       )

src/test/heap_tests.ml

@@ -8,7 +8,8 @@ let get_program =
   fun () -> match !s with
     | Some s -> ok s
     | None -> (
-        let%bind program = type_file "./contracts/heap-instance.ligo" in
+        let%bind (program , state) = type_file "./contracts/heap-instance.ligo" in
+        let () = Typer.Solver.discard_state state in
         s := Some program ;
         ok program
       )

src/test/integration_tests.ml

@@ -3,8 +3,14 @@ open Test_helpers
 
 open Ast_simplified.Combinators
 
-let mtype_file ?debug_simplify ?debug_typed = Ligo.Compile.Of_source.type_file ?debug_simplify ?debug_typed (Syntax_name "cameligo")
-let type_file = Ligo.Compile.Of_source.type_file (Syntax_name "pascaligo")
+let mtype_file ?debug_simplify ?debug_typed f =
+  let%bind (typed , state) = Ligo.Compile.Of_source.type_file ?debug_simplify ?debug_typed (Syntax_name "cameligo") f in
+  let () = Typer.Solver.discard_state state in
+  ok typed
+let type_file f =
+  let%bind (typed , state) = Ligo.Compile.Of_source.type_file (Syntax_name "pascaligo") f in
+  let () = Typer.Solver.discard_state state in
+  ok typed
 
 let type_alias () : unit result =
   let%bind program = type_file "./contracts/type-alias.ligo" in
@@ -277,9 +283,9 @@ let bytes_arithmetic () : unit result =
   let%bind () = expect_eq program "slice_op" tata at in
   let%bind () = expect_fail program "slice_op" foo in
   let%bind () = expect_fail program "slice_op" ba in
-  let%bind b1 = Run.Of_simplified.run_typed_program program "hasherman" foo in
+  let%bind b1 = Run.Of_simplified.run_typed_program program Typer.Solver.initial_state "hasherman" foo in
   let%bind () = expect_eq program "hasherman" foo b1 in
-  let%bind b3 = Run.Of_simplified.run_typed_program program "hasherman" foototo in
+  let%bind b3 = Run.Of_simplified.run_typed_program program Typer.Solver.initial_state "hasherman" foototo in
   let%bind () = Assert.assert_fail @@ Ast_simplified.Misc.assert_value_eq (b3 , b1) in
   ok ()
 

src/test/test.ml

@@ -2,9 +2,8 @@
 
 open Test_helpers
 
-
 let () =
-  (* Printexc.record_backtrace true ; *)
+  Printexc.record_backtrace true ;
   run_test @@ test_suite "LIGO" [
     Integration_tests.main ;
     Compiler_tests.main ;

src/test/test_helpers.ml

@@ -38,7 +38,7 @@ let expect ?input_to_value ?options program entry_point input expecter =
       let content () = Format.asprintf "Entry_point: %s" entry_point in
       error title content in
     trace run_error @@
-    Ligo.Run.Of_simplified.run_typed_program ?input_to_value ?options program entry_point input in
+    Ligo.Run.Of_simplified.run_typed_program ?input_to_value ?options program Typer.Solver.initial_state entry_point input in
   expecter result
 
 let expect_fail ?options program entry_point input =
@@ -49,7 +49,7 @@ let expect_fail ?options program entry_point input =
   in
   trace run_error @@
   Assert.assert_fail
-  @@ Ligo.Run.Of_simplified.run_typed_program ?options program entry_point input
+  @@ Ligo.Run.Of_simplified.run_typed_program ?options program Typer.Solver.initial_state entry_point input
 
 
 let expect_eq ?input_to_value ?options program entry_point input expected =

src/test/typer_tests.ml

@@ -11,7 +11,9 @@ let int () : unit result =
   let pre = e_int 32 in
   let open Typer in
   let e = Environment.full_empty in
-  let%bind post = type_expression e pre in
+  let state = Typer.Solver.initial_state in
+  let%bind (post , new_state) = type_expression e state pre in
+  let () = Typer.Solver.discard_state new_state in
   let open! Typed in
   let open Combinators in
   let%bind () = assert_type_value_eq (post.type_annotation, t_int ()) in
@@ -19,12 +21,14 @@ let int () : unit result =
 
 module TestExpressions = struct
   let test_expression ?(env = Typer.Environment.full_empty)
+                      ?(state = Typer.Solver.initial_state)
                       (expr : expression)
                       (test_expected_ty : Typed.tv) =
     let pre = expr in
     let open Typer in
     let open! Typed in
-    let%bind post = type_expression env pre in
+    let%bind (post , new_state) = type_expression env state pre in
+    let () = Typer.Solver.discard_state new_state in
     let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
     ok ()
 

src/test/vote_tests.ml

@@ -8,9 +8,9 @@ let get_program =
   fun () -> match !s with
     | Some s -> ok s
     | None -> (
-        let%bind program = type_file "./contracts/vote.mligo" in
-        s := Some program ;
-        ok program
+        let%bind (program , state) = type_file "./contracts/vote.mligo" in
+        s := Some (program , state) ;
+        ok (program , state)
       )
 
 open Ast_simplified
@@ -39,8 +39,8 @@ let vote str =
   e_constructor "Vote" vote
 
 let init_vote () =
-  let%bind program = get_program () in
-  let%bind result = Ligo.Run.Of_simplified.run_typed_program program "main" (e_pair (vote "Yes") (init_storage "basic")) in
+  let%bind (program , state) = get_program () in
+  let%bind result = Ligo.Run.Of_simplified.run_typed_program program state "main" (e_pair (vote "Yes") (init_storage "basic")) in
   let%bind (_ , storage) = extract_pair result in
   let%bind storage' = extract_record storage in
   let votes = List.assoc "candidates" storage' in

src/union_find/.links

@@ -0,0 +1 @@
+../OCaml-build/Makefile

src/union_find/LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2018 Christian Rinderknecht
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

src/union_find/Makefile.cfg

@@ -0,0 +1,4 @@
+SHELL := dash
+BFLAGS := -strict-sequence -w +A-48-4
+#OCAMLC := ocamlcp
+#OCAMLOPT := ocamloptp

src/union_find/Partition.mli

@@ -0,0 +1,64 @@
+(** This module offers the abstract data type of a partition of
+    classes of equivalent items (Union & Find). *)
+
+(** The items are of type [Item.t], that is, they have to obey
+    a total order, but also they must be printable to ease
+    debugging. The signature [Item] is the input signature of
+    the functor {!Partition.Make}. *)
+module type Item =
+  sig
+    (** Type of items *)
+    type t
+
+    (** Same convention as {!Pervasives.compare} *)
+    val compare : t -> t -> int
+
+    val to_string : t -> string
+  end
+
+(** The module signature [S] is the output signature of the functor
+    {!Partition.Make}. *)
+module type S =
+  sig
+    type item
+    type partition
+    type t = partition
+
+    (** {1 Creation} *)
+
+    (** The value [empty] is an empty partition. *)
+    val empty : partition
+
+    (** The value of [equiv i j p] is the partition [p] extended with
+        the equivalence of items [i] and [j]. If both [i] and [j] are
+        already known to be equivalent, then [equiv i j p == p]. *)
+    val equiv : item -> item -> partition -> partition
+
+    (** The value of [alias i j p] is the partition [p] extended with
+        the fact that item [i] is an alias of item [j]. This is the
+        same as [equiv i j p], except that it is guaranteed that the
+        item [i] is not the representative of its equivalence class in
+        [alias i j p]. *)
+    val alias : item -> item -> partition -> partition
+
+    (** {1 Projection} *)
+
+    (** The value of the call [repr i p] is the representative of item
+        [i] in the partition [p]. The built-in exception [Not_found]
+        is raised if [i] is not in [p]. *)
+    val repr : item -> partition -> item
+
+    (** The side-effect of the call [print p] is the printing of the
+        partition [p] on standard output, based on [Ord.to_string]. *)
+    val print : partition -> unit
+
+    (** {1 Predicates} *)
+
+    (** The value of [is_equiv i j p] is [true] if, and only if, the
+        items [i] and [j] belong to the same equivalence class in the
+        partition [p], that is, [i] and [j] have the same
+        representative. *)
+    val is_equiv : item -> item -> partition -> bool
+  end
+
+module Make (Ord : Item) : S with type item = Ord.t

src/union_find/Partition0.ml

@@ -0,0 +1,47 @@
+(* Naive persistent implementation of Union/Find: O(n^2) worst case *)
+
+module Make (Item: Partition.Item) =
+  struct
+
+    type item = Item.t
+    type repr = item   (** Class representatives *)
+
+    let equal i j = Item.compare i j = 0
+
+    module ItemMap = Map.Make (Item)
+
+    type height = int
+
+    type partition = item ItemMap.t
+    type t = partition
+
+    let empty = ItemMap.empty
+
+    let rec repr item partition =
+      let parent = ItemMap.find item partition in
+      if   equal parent item
+      then item
+      else repr parent partition
+
+    let is_equiv (i: item) (j: item) (p: partition) =
+      equal (repr i p) (repr j p)
+
+    let get_or_set (i: item) (p: partition) : item * partition =
+      try repr i p, p with Not_found -> i, ItemMap.add i i p
+
+    let equiv (i: item) (j :item) (p: partition) : partition =
+      let ri, p = get_or_set i p in
+      let rj, p = get_or_set j p in
+      if equal ri rj then p else ItemMap.add ri rj p
+
+    let alias = equiv
+
+   (* Printing *)
+
+    let print p =
+      let print src dst =
+        Printf.printf "%s -> %s\n"
+          (Item.to_string src) (Item.to_string dst)
+      in ItemMap.iter print p
+
+  end

src/union_find/Partition1.ml

@@ -0,0 +1,69 @@
+(* Persistent implementation of Union/Find with height-balanced
+   forests and without path compression: O(n*log(n)).
+
+   In the definition of type [t], the height component is that of the
+   source, that is, if [ItemMap.find i m = (j,h)], then [h] is the
+   height of [i] (_not_ [j]).
+*)
+
+module Make (Item: Partition.Item) =
+  struct
+
+    type item = Item.t
+    type repr = item   (** Class representatives *)
+
+    let equal i j = Item.compare i j = 0
+
+    module ItemMap = Map.Make (Item)
+
+    type height = int
+
+    type partition = (item * height) ItemMap.t
+    type t = partition
+
+    let empty = ItemMap.empty
+
+    let rec seek (i: item) (p: partition) : repr * height =
+      let j, _ as i' = ItemMap.find i p in
+      if equal i j then i' else seek j p
+
+    let repr item partition = fst (seek item partition)
+
+    let is_equiv (i: item) (j: item) (p: partition) =
+      equal (repr i p) (repr j p)
+
+    let get_or_set (i: item) (p: partition) =
+      try seek i p, p with
+        Not_found -> let i' = i,0 in (i', ItemMap.add i i' p)
+
+    let equiv (i: item) (j: item) (p: partition) : partition =
+      let (ri,hi), p = get_or_set i p in
+      let (rj,hj), p = get_or_set j p in
+      let add = ItemMap.add in
+      if   equal ri rj
+      then p
+      else if   hi > hj
+           then add rj (ri,hj) p
+           else add ri (rj,hi) (if hi < hj then p else add rj (rj,hj+1) p)
+
+    let alias (i: item) (j: item) (p: partition) : partition =
+      let (ri,hi), p = get_or_set i p in
+      let (rj,hj), p = get_or_set j p in
+      let add = ItemMap.add in
+      if   equal ri rj
+      then p
+      else if   hi = hj || equal ri i
+           then add ri (rj,hi) @@ add rj (rj, max hj (hi+1)) p
+           else if hi < hj then add ri (rj,hi) p
+                           else add rj (ri,hj) p
+
+    (* Printing *)
+
+    let print (p: partition) =
+      let print i (j,hi) =
+        let _,hj = ItemMap.find j p in
+        Printf.printf "%s,%d -> %s,%d\n"
+          (Item.to_string i) hi (Item.to_string j) hj
+      in ItemMap.iter print p
+
+  end

src/union_find/Partition2.ml

@@ -0,0 +1,115 @@
+(** Persistent implementation of the Union/Find algorithm with
+    height-balanced forests and without path compression. *)
+
+module Make (Item: Partition.Item) =
+  struct
+
+    type item = Item.t
+    type repr = item   (** Class representatives *)
+
+    let equal i j = Item.compare i j = 0
+
+    type height = int
+
+    (** Each equivalence class is implemented by a Catalan tree linked
+        upwardly and otherwise is a link to another node. Those trees
+        are height-balanced. The type [node] implements nodes in those
+        trees. *)
+    type node =
+      Root of height
+      (** The value of [Root h] denotes the root of a tree, that is,
+          the representative of the associated class.  The height [h]
+          is that of the tree, so a tree reduced to its root alone has
+          heigh 0. *)
+
+    | Link of item * height
+      (** If not a root, a node is a link to another node. Because the
+          links are upward, that is, bottom-up, and we seek a purely
+          functional implementation, we need to uncouple the nodes and
+          the items here, so the first component of [Link] is an item,
+          not a node. That is why the type [node] is not recursive,
+          and called [node], not [tree]: to become a traversable tree,
+          it needs to be complemented by the type [partition] below to
+          associate items back to nodes. In order to follow a path
+          upward in the tree until the root, we start from a link node
+          giving us the next item, then find the node corresponding to
+          the item thanks to [partition], and again until we arrive at
+          the root.
+
+          The height component is that of the source of the link, that
+          is, [h] is the height of the node linking to the node [Link
+          (j,h)], _not_ of [j], except when [equal i j]. *)
+
+    module ItemMap = Map.Make (Item)
+
+    (** The type [partition] implements a partition of classes of
+        equivalent items by means of a map from items to nodes of type
+        [node] in trees. *)
+    type partition = node ItemMap.t
+
+    type t = partition
+
+    let empty = ItemMap.empty
+
+    let root (item, height) = ItemMap.add item (Root height)
+
+    let link (src, height) dst = ItemMap.add src (Link (dst, height))
+
+    let rec seek (i: item) (p: partition) : repr * height =
+      match ItemMap.find i p with
+           Root hi -> i,hi
+      | Link (j,_) -> seek j p
+
+    let repr item partition = fst (seek item partition)
+
+    let is_equiv (i: item) (j: item) (p: partition) =
+      equal (repr i p) (repr j p)
+
+    let get_or_set (i: item) (p: partition) =
+      try seek i p, p with
+        Not_found -> let n = i,0 in (n, root n p)
+
+    let equiv (i: item) (j: item) (p: partition) : partition =
+      let (ri,hi as ni), p = get_or_set i p in
+      let (rj,hj as nj), p = get_or_set j p in
+      if   equal ri rj
+      then p
+      else if   hi > hj
+           then link nj ri p
+           else link ni rj (if hi < hj then p else root (rj, hj+1) p)
+
+    (** The call [alias i j p] results in the same partition as [equiv
+        i j p], except that [i] is not the representative of its class
+        in [alias i j p] (whilst it may be in [equiv i j p]).
+
+        This property is irrespective of the heights of the
+        representatives of [i] and [j], that is, of the trees
+        implementing their classes. If [i] is not a representative of
+        its class before calling [alias], then the height criteria is
+        applied (which, without the constraint above, would yield a
+        height-balanced new tree). *)
+    let alias (i: item) (j: item) (p: partition) : partition =
+      let (ri,hi as ni), p = get_or_set i p in
+      let (rj,hj as nj), p = get_or_set j p in
+      if   equal ri rj
+      then p
+      else if   hi = hj || equal ri i
+           then link ni rj @@ root (rj, max hj (hi+1)) p
+           else if hi < hj then link ni rj p
+                           else link nj ri p
+
+    (** {1 Printing} *)
+
+    let print (p: partition) =
+      let print i node =
+        let hi, hj, j =
+          match node with
+            Root hi -> hi,hi,i
+          | Link (j,hi) ->
+              match ItemMap.find j p with
+                Root hj | Link (_,hj) -> hi,hj,j in
+        Printf.printf "%s,%d -> %s,%d\n"
+          (Item.to_string i) hi (Item.to_string j) hj
+      in ItemMap.iter print p
+
+  end

src/union_find/Partition3.ml

@@ -0,0 +1,86 @@
+(* Destructive implementation of union/find with height-balanced
+   forests but without path compression: O(n*log(n)). *)
+
+module Make (Item: Partition.Item) =
+  struct
+
+    type item = Item.t
+    type repr = item   (** Class representatives *)
+
+    let equal i j = Item.compare i j = 0
+
+    type height = int
+
+    (** Each equivalence class is implemented by a Catalan tree linked
+        upwardly and otherwise is a link to another node. Those trees
+        are height-balanced. The type [node] implements nodes in those
+        trees. *)
+    type node = {item: item; mutable height: int; mutable parent: node}
+
+    module ItemMap = Map.Make (Item)
+
+    (** The type [partition] implements a partition of classes of
+        equivalent items by means of a map from items to nodes of type
+        [node] in trees. *)
+    type partition = node ItemMap.t
+
+    type t = partition
+
+    let empty = ItemMap.empty
+
+    (** The function [repr] is faster than a persistent implementation
+        in the worst case because, in the latter case, the cost is O(log n)
+        for accessing each node in the path to the root, whereas, in the
+        former, only the access to the first node in the path incurs a cost
+        of O(log n) -- the other nodes are accessed in constant time by
+        following the [next] field of type [node]. *)
+   let seek (i: item) (p: partition) : node =
+     let rec find_root node =
+       if node.parent == node then node else find_root node.parent
+     in find_root (ItemMap.find i p)
+
+   let repr item partition = (seek item partition).item
+
+   let is_equiv (i: item) (j: item) (p: partition) =
+     equal (repr i p) (repr j p)
+
+   let get_or_set item (p: partition) =
+     try seek item p, p with
+       Not_found -> let rec loop = {item; height=0; parent=loop}
+                    in loop, ItemMap.add item loop p
+
+   let link src dst = src.parent <- dst
+
+   let equiv (i: item) (j: item) (p: partition) : partition =
+     let ni,p  = get_or_set i p in
+     let nj,p  = get_or_set j p in
+     let hi,hj = ni.height, nj.height in
+     let () =
+       if   not (equal ni.item nj.item)
+       then if   hi > hj
+            then link nj ni
+            else (link ni nj; nj.height <- max hj (hi+1))
+     in p
+
+   let alias (i: item) (j: item) (p: partition) : partition =
+     let ni,p  = get_or_set i p in
+     let nj,p  = get_or_set j p in
+     let hi,hj = ni.height, nj.height in
+     let () =
+      if   not (equal ni.item nj.item)
+      then if   hi = hj || equal ni.item i
+           then (link ni nj; nj.height <- max hj (hi+1))
+           else if hi < hj then link ni nj
+                           else link nj ni
+     in p
+
+   (* Printing *)
+
+    let print p =
+      let print _ node =
+        Printf.printf "%s,%d -> %s,%d\n"
+          (Item.to_string node.item) node.height
+          (Item.to_string node.parent.item) node.parent.height
+      in ItemMap.iter print p
+
+  end

src/union_find/PartitionMain.ml

@@ -0,0 +1,40 @@
+module Int =
+  struct
+    type t = int
+    let compare (i: int) (j: int) = Pervasives.compare i j
+    let to_string = string_of_int
+  end
+
+module Test (Part: Partition.S with type item = Int.t) =
+  struct
+    open Part
+
+    let () = empty
+             |> equiv 4 3
+             |> equiv 3 8
+             |> equiv 6 5
+             |> equiv 9 4
+             |> equiv 2 1
+             |> equiv 8 9
+             |> equiv 5 0
+             |> equiv 7 2
+             |> equiv 6 1
+             |> equiv 1 0
+             |> equiv 6 7
+             |> equiv 8 0
+             |> equiv 7 7
+             |> equiv 10 10
+             |> print
+  end
+
+
+module Test0 = Test (Partition0.Make(Int))
+let () = print_newline ()
+
+module Test1 = Test (Partition1.Make(Int))
+let () = print_newline ()
+
+module Test2 = Test (Partition2.Make(Int))
+let () = print_newline ()
+
+module Test3 = Test (Partition3.Make(Int))

src/union_find/README.md

@@ -0,0 +1,39 @@
+# Some implementations in OCaml of the Union/Find algorithm
+
+All modules implementing Union/Find can be coerced by the same
+signature `Partition.S`.
+
+Note the function `alias` which is equivalent to `equiv`, but not
+symmetric: `alias x y` means that `x` is an alias of `y`, which
+translates in the present context as `x` not being the representative
+of the equivalence class containing the equivalence between `x` and
+`y`. The function `alias` is useful when managing aliases during the
+static analyses of programming languages, so the representatives of
+the classes are always the original object.
+
+The module `PartitionMain` tests each with the same equivalence
+relations.
+
+## `Partition0.ml`
+
+This is a naive, persistent implementation of Union/Find featuring an
+asymptotic worst case cost of O(n^2).
+
+## `Partition1.ml`
+
+This is a persistent implementation of Union/Find with height-balanced
+forests and without path compression, featuring an asymptotic worst
+case cost of O(n*log(n)).
+
+## `Partition2.ml`
+
+This is an alternate version of `Partition1.ml`, using a different
+data type.
+
+## `Partition3.ml`
+
+This is a destructive implementation of Union/Find with
+height-balanced forests but without path compression, featuring an
+asymptotic worst case of O(n*log(n)). In practice, though, this
+implementation should be faster than the previous ones, due to a
+smaller multiplicative constant term.

src/union_find/build.sh

@@ -0,0 +1,14 @@
+#!/bin/sh
+set -x
+ocamlfind ocamlc -strict-sequence -w +A-48-4 -c Partition.mli
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml
+ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml
+ocamlfind ocamlopt -o PartitionMain.opt Partition0.cmx Partition1.cmx Partition2.cmx Partition3.cmx PartitionMain.cmx

src/union_find/clean.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+\rm -f *.cmi *.cmo *.cmx *.o *.byte *.opt

src/union_find/dune

@@ -0,0 +1,16 @@
+(library
+  (name union_find)
+  (public_name ligo.union_find)
+  (wrapped false) ;; TODO: do we need this?
+  (modules Partition0 Partition1 Partition2 Partition3 Partition Union_find)
+  (modules_without_implementation Partition)
+;;   (preprocess
+;;     (pps simple-utils.ppx_let_generalized)
+;;   )
+;;   (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
+  )
+
+(test
+ (modules PartitionMain)
+ (libraries union_find)
+ (name PartitionMain))

src/union_find/union_find.ml

@@ -0,0 +1,2 @@
+module Partition = Partition
+module Partition0 = Partition0

vendors/ligo-utils/simple-utils/trace.ml

@@ -592,7 +592,28 @@ let bind_fold_list f init lst =
   in
   List.fold_left aux (ok init) lst
 
-let bind_fold_pair f init (a,b) = 
+module TMap(X : Map.OrderedType) = struct
+  module MX = Map.Make(X)
+  let bind_fold_Map f init map =
+    let aux k v x  =
+      x >>? fun x ->
+      f ~x ~k ~v
+    in
+    MX.fold aux map (ok init)
+
+  let bind_map_Map f map =
+    let aux k v map'  =
+      map' >>? fun map' ->
+      f ~k ~v >>? fun v' ->
+      ok @@ MX.update k (function
+          | None -> Some v'
+          | Some _ -> failwith "key collision, shouldn't happen in bind_map_Map")
+        map'
+    in
+    MX.fold aux map (ok MX.empty)
+end
+
+let bind_fold_pair f init (a,b) =
   let aux x y =
     x >>? fun x ->
     f x y
@@ -613,8 +634,8 @@ let bind_fold_map_list = fun f acc lst ->
         f acc hd >>? fun (acc' , hd') ->
         aux (acc' , hd' :: prev) f tl
   in
-  aux (acc , []) f lst >>? fun (_acc' , lst') ->
-  ok @@ List.rev lst'
+  aux (acc , []) f lst >>? fun (acc' , lst') ->
+  ok @@ (acc' , List.rev lst')
 
 let bind_fold_map_right_list = fun f acc lst ->
   let rec aux (acc , prev) f = function
@@ -684,6 +705,10 @@ let bind_and3 (a, b, c) =
 let bind_pair = bind_and
 let bind_map_pair f (a, b) =
   bind_pair (f a, f b)
+let bind_fold_map_pair f acc (a, b) =
+  f acc a >>? fun (acc' , a') ->
+  f acc' b >>? fun (acc'' , b') ->
+  ok (acc'' , (a' , b'))
 let bind_map_triple f (a, b, c) =
   bind_and3 (f a, f b, f c)