diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml
index 21b6c98be..ce3c6902c 100644
--- a/src/ast_typed/combinators.ml
+++ b/src/ast_typed/combinators.ml
@@ -50,6 +50,14 @@ let get_t_bool (t:type_value) : unit result = match t.type_value' with
   | T_constant ("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 ()
+  | _ -> simple_fail "not a int"
+
+let get_t_nat (t:type_value) : unit result = match t.type_value' with
+  | T_constant ("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 ()
   | _ -> simple_fail "not a unit"
@@ -58,6 +66,10 @@ let get_t_tez (t:type_value) : unit result = match t.type_value' with
   | T_constant ("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 ()
+  | _ -> simple_fail "not a bytes"
+
 let get_t_contract (t:type_value) : type_value result = match t.type_value' with
   | T_constant ("contract", [x]) -> ok x
   | _ -> simple_fail "not a contract"
@@ -107,17 +119,25 @@ let get_t_map_value : type_value -> type_value result = fun t ->
   let%bind (_ , value) = get_t_map t in
   ok value
 
+let assert_t_map = fun t ->
+  let%bind _ = get_t_map t in
+  ok ()
+
+let is_t_map = Function.compose to_bool get_t_map
+
 let assert_t_tez :type_value -> unit result = get_t_tez
 
-let assert_t_map (t:type_value) : unit result =
-  match t.type_value' with
-  | T_constant ("map", [_ ; _]) -> ok ()
-  | _ -> simple_fail "not a map"
+let assert_t_list t =
+  let%bind _ = get_t_list t in
+  ok ()
 
-let assert_t_list (t:type_value) : unit result =
-  match t.type_value' with
-  | T_constant ("list", [_]) -> ok ()
-  | _ -> simple_fail "assert: not a list"
+let is_t_list = Function.compose to_bool get_t_list
+let is_t_nat = Function.compose to_bool get_t_nat
+let is_t_int = Function.compose to_bool get_t_int
+
+let assert_t_bytes = fun t ->
+  let%bind _ = get_t_bytes t in
+  ok ()
 
 let assert_t_operation (t:type_value) : unit result =
   match t.type_value' with
diff --git a/src/operators/operators.ml b/src/operators/operators.ml
index 11596e0a2..2674bbc99 100644
--- a/src/operators/operators.ml
+++ b/src/operators/operators.ml
@@ -3,314 +3,274 @@ open Trace
 module Simplify = struct
 
   let type_constants = [
-    ("unit" , 0) ;
-    ("string" , 0) ;
-    ("bytes" , 0) ;
-    ("nat" , 0) ;
-    ("int" , 0) ;
-    ("tez" , 0) ;
-    ("bool" , 0) ;
-    ("operation" , 0) ;
-    ("address" , 0) ;
-    ("contract" , 1) ;
-    ("list" , 1) ;
-    ("option" , 1) ;
-    ("set" , 1) ;
-    ("map" , 2) ;
-    ("big_map" , 2) ;
+    ("unit" , "unit") ;
+    ("string" , "string") ;
+    ("bytes" , "bytes") ;
+    ("nat" , "nat") ;
+    ("int" , "int") ;
+    ("tez" , "tez") ;
+    ("bool" , "bool") ;
+    ("operation" , "operation") ;
+    ("address" , "address") ;
+    ("contract" , "contract") ;
+    ("list" , "list") ;
+    ("option" , "option") ;
+    ("set" , "set") ;
+    ("map" , "map") ;
+    ("big_map" , "big_map") ;
   ]
 
-  let constants = [
-    ("get_force" , 2) ;
-    ("transaction" , 3) ;
-    ("get_contract" , 1) ;
-    ("size" , 1) ;
-    ("int" , 1) ;
-    ("abs" , 1) ;
-    ("amount" , 0) ;
-    ("unit" , 0) ;
-    ("source" , 0) ;
-  ]
+  module Pascaligo = struct
+
+    let constants = [
+      ("get_force" , "MAP_GET_FORCE") ;
+      ("transaction" , "CALL") ;
+      ("get_contract" , "CONTRACT") ;
+      ("size" , "SIZE") ;
+      ("int" , "INT") ;
+      ("abs" , "ABS") ;
+      ("amount" , "AMOUNT") ;
+      ("unit" , "UNIT") ;
+      ("source" , "SOURCE") ;
+    ]
+
+    let type_constants = type_constants
+  end
 
   module Camligo = struct
     let constants = [
-      ("Bytes.pack" , 1) ;
-      ("Crypto.hash" , 1) ;
-      ("Operation.transaction" , 3) ;
-      ("Operation.get_contract" , 1) ;
-      ("sender" , 0) ;
-      ("unit" , 0) ;
-      ("source" , 0) ;
+      ("Bytes.pack" , "PACK") ;
+      ("Crypto.hash" , "HASH") ;
+      ("Operation.transaction" , "CALL") ;
+      ("Operation.get_contract" , "GET_CONTRACT") ;
+      ("sender" , "SENDER") ;
+      ("unit" , "UNIT") ;
+      ("source" , "SOURCE") ;
     ]
+
+    let type_constants = type_constants
+  end
+
+  module Ligodity = struct
+    include Pascaligo
   end
 
 end
 
 module Typer = struct
-  module Errors = struct
-    let wrong_param_number = fun name ->
-      let title () = "wrong number of params" in
-      let full () = name in
-      error title full
-  end
 
   open Ast_typed
 
-  type typer_predicate = type_value list -> bool
+  module Errors = struct
+    let wrong_param_number = fun name expected got ->
+      let title () = "wrong number of params" in
+      let full () = Format.asprintf "constant name: %s\nexpected: %d\ngot: %d\n"
+          name expected (List.length got) in
+      error title full
+  end
+
+
   type type_result = string * type_value
   type typer' = type_value list -> type_value option -> type_result result
-  type typer = string * int * (typer_predicate * typer') list
+  type typer = string * typer'
 
-  let predicate_0 : typer_predicate = fun lst ->
+  let typer'_0 : name -> (type_value option -> type_value result) -> typer' = fun s f lst tv_opt ->
     match lst with
-    | [] -> true
-    | _ -> false
+    | [] -> (
+      let%bind tv' = f tv_opt in
+      ok (s , tv')
+    )
+    | _ -> fail @@ Errors.wrong_param_number s 0 lst
+  let typer_0 name f : typer = (name , typer'_0 name f)
 
-  let predicate_1 : (type_value -> bool) -> typer_predicate = fun f lst ->
+  let typer'_1 : name -> (type_value -> type_value result) -> typer' = fun s f lst _ ->
     match lst with
-    | [ a ] -> f a
-    | _ -> false
+    | [ a ] -> (
+        let%bind tv' = f a in
+        ok (s , tv')
+      )
+    | _ -> fail @@ Errors.wrong_param_number s 1 lst
+  let typer_1 name f : typer = (name , typer'_1 name f)
 
-  let predicate_2 : (type_value -> type_value -> bool) -> typer_predicate = fun f lst ->
+  let typer'_1_opt : name -> (type_value -> type_value option -> type_value result) -> typer' = fun s f lst tv_opt ->
     match lst with
-    | [ a ; b ] -> f a b
-    | _ -> false
+    | [ a ] -> (
+        let%bind tv' = f a tv_opt in
+        ok (s , tv')
+      )
+    | _ -> fail @@ Errors.wrong_param_number s 1 lst
+  let typer_1_opt name f : typer = (name , typer'_1_opt name f)
 
-  let predicate_3 : (type_value -> type_value -> type_value -> bool) -> typer_predicate = fun f lst ->
+  let typer'_2 : name -> (type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
     match lst with
-    | [ a ; b ; c ] -> f a b c
-    | _ -> false
+    | [ a ; b ] -> (
+        let%bind tv' = f a b in
+        ok (s , tv')
+      )
+    | _ -> fail @@ Errors.wrong_param_number s 2 lst
+  let typer_2 name f : typer = (name , typer'_2 name f)
 
-  let true_1 = predicate_1 (fun _ -> true)
-  let true_2 = predicate_2 (fun _ _ -> true)
-  let true_3 = predicate_3 (fun _ _ _ -> true)
-
-  let eq_1 : type_value -> typer_predicate = fun v ->
-    let aux = fun a -> type_value_eq (a, v) in
-    predicate_1 aux
-
-  let eq_2 : type_value -> typer_predicate = fun v ->
-    let aux = fun a b -> type_value_eq (a, v) && type_value_eq (b, v) in
-    predicate_2 aux
-
-  let typer'_0 : (type_value option -> type_result result) -> typer' = fun f lst tv ->
+  let typer'_3 : name -> (type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
     match lst with
-    | [] -> f tv
-    | _ -> simple_fail "!!!"
+    | [ a ; b ; c ] -> (
+        let%bind tv' = f a b c in
+        ok (s , tv')
+      )
+    | _ -> fail @@ Errors.wrong_param_number s 3 lst
+  let typer_3 name f : typer = (name , typer'_3 name f)
 
-  let typer'_1 : (type_value -> type_result result) -> typer' = fun f lst _ ->
-    match lst with
-    | [ a ] -> f a
-    | _ -> simple_fail "!!!"
-
-  let typer'_1_opt : (type_value -> type_value option -> type_result result) -> typer' = fun f lst tv_opt ->
-    match lst with
-    | [ a ] -> f a tv_opt
-    | _ -> simple_fail "!!!"
-
-  let typer'_2 : (type_value -> type_value -> type_result result) -> typer' = fun f lst _ ->
-    match lst with
-    | [ a ; b ] -> f a b
-    | _ -> simple_fail "!!!"
-
-  let typer'_3 : (type_value -> type_value -> type_value -> type_result result) -> typer' = fun f lst _ ->
-    match lst with
-    | [ a ; b ; c ] -> f a b c
-    | _ -> simple_fail "!!!"
-
-  let typer_constant cst : typer' = fun _ _ -> ok cst
-
-  let constant_2 : string -> type_value -> typer' = fun s tv ->
-    let aux = fun _ _ -> ok (s, tv) in
-    typer'_2 aux
-
-  let make_2 : string -> _ list -> typer = fun name pfs ->
-    (name , 2 , List.map (Tuple.map_h_2 predicate_2 typer'_2) pfs)
-
-  let same_2 : string -> (string * type_value) list -> typer = fun s lst ->
-    let aux (s, tv) = eq_2 tv, constant_2 s tv in
-    (s , 2 , List.map aux lst)
-
-  let very_same_2 : string -> type_value -> typer = fun s tv -> same_2 s [s , tv]
+  let constant name cst = typer_0 name (fun _ -> ok cst)
 
   open Combinators
 
-  let comparator : string -> typer = fun s -> s , 2 , [
-      (eq_2 (t_int ()), constant_2 s (t_bool ())) ;
-      (eq_2 (t_nat ()), constant_2 s (t_bool ())) ;
-      (eq_2 (t_tez ()), constant_2 s (t_bool ())) ;
-      (eq_2 (t_bytes ()), constant_2 s (t_bool ())) ;
-      (eq_2 (t_string ()), constant_2 s (t_bool ())) ;
-      (eq_2 (t_address ()), constant_2 s (t_bool ())) ;
-    ]
+  let eq_1 a cst = type_value_eq (a , cst)
+  let eq_2 (a , b) cst = type_value_eq (a , cst) && type_value_eq (b , cst)
 
-  let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ())
+  let comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
+    let%bind () =
+      trace_strong (simple_error "Types a and b aren't comparable") @@
+      Assert.assert_true @@
+      List.exists (eq_2 (a , b)) [
+        t_int () ;
+        t_nat () ;
+        t_tez () ;
+        t_string () ;
+        t_bytes () ;
+        t_address () ;
+      ] in
+    ok @@ t_bool ()
 
-  let none = "NONE" , 0 , [
-      predicate_0 , typer'_0 (fun tv_opt -> match tv_opt with
-          | None -> simple_fail "untyped NONE"
-          | Some t -> ok ("NONE", t))
-    ]
+  let boolean_operator_2 : string -> typer = fun s -> typer_2 s @@ fun a b ->
+    let%bind () =
+      trace_strong (simple_error "A isn't of type bool") @@
+      Assert.assert_true @@
+      type_value_eq (t_bool () , a) in
+    let%bind () =
+      trace_strong (simple_error "B isn't of type bool") @@
+      Assert.assert_true @@
+      type_value_eq (t_bool () , b) in
+    ok @@ t_bool ()
 
-  let sub = "SUB" , 2 , [
-      eq_2 (t_int ()) , constant_2 "SUB_INT" (t_int ()) ;
-      eq_2 (t_nat ()) , constant_2 "SUB_NAT" (t_int ()) ;
-    ]
+  let none = typer_0 "NONE" @@ fun tv_opt ->
+    match tv_opt with
+    | None -> simple_fail "untyped NONE"
+    | Some t -> ok t
 
-  let some = "SOME" , 1 , [
-      true_1 , typer'_1 (fun s -> ok ("SOME", t_option s ())) ;
-    ]
+  let sub = typer_2 "SUB" @@ fun a b ->
+    let%bind () =
+      trace_strong (simple_error "Types a and b aren't numbers") @@
+      Assert.assert_true @@
+      List.exists (eq_2 (a , b)) [
+        t_int () ;
+        t_nat () ;
+      ] in
+    ok @@ t_int ()
 
-  let map_remove : typer = "MAP_REMOVE" , 2 , [
-      (true_2 , typer'_2 (fun k m ->
-          let%bind (src, _) = get_t_map m in
-          let%bind () = assert_type_value_eq (src, k) in
-          ok ("MAP_REMOVE", m)
-        ))
-    ]
+  let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
 
-  let map_update : typer = "MAP_UPDATE" , 3 , [
-      (true_3 , typer'_3 (fun k v m ->
-           let%bind (src, dst) = get_t_map m in
-           let%bind () = assert_type_value_eq (src, k) in
-           let%bind () = assert_type_value_eq (dst, v) in
-           ok ("MAP_UPDATE", m)))
-    ]
+  let map_remove : typer = typer_2 "MAP_REMOVE" @@ fun k m ->
+    let%bind (src , _) = get_t_map m in
+    let%bind () = assert_type_value_eq (src , k) in
+    ok m
 
-  let size : typer = "size" , 1 , [
-      (true_1, typer'_1 (fun t ->
-           let%bind () = bind_or (assert_t_map t, assert_t_list t) in
-           ok ("SIZE", t_nat ())))
-    ]
+  let map_update : typer = typer_3 "MAP_UPDATE" @@ fun k v m ->
+    let%bind (src, dst) = get_t_map m in
+    let%bind () = assert_type_value_eq (src, k) in
+    let%bind () = assert_type_value_eq (dst, v) in
+    ok m
 
-  let get_force : typer = "get_force" , 2 , [
-      (true_2, typer'_2 (fun i_ty m_ty ->
-           let%bind (src, dst) = get_t_map m_ty in
-           let%bind _ = assert_type_value_eq (src, i_ty) in
-           ok ("GET_FORCE", dst)))
-    ]
+  let size = typer_1 "SIZE" @@ fun t ->
+    let%bind () =
+      Assert.assert_true @@
+      (is_t_map t || is_t_list t) in
+    ok @@ t_nat ()
 
-  let int : typer = "int" , 1 , [
-      (eq_1 (t_nat ()), typer_constant ("INT" , t_int ()))
-    ]
+  let get_force = typer_2 "MAP_GET_FORCE" @@ fun i m ->
+    let%bind (src, dst) = get_t_map m in
+    let%bind _ = assert_type_value_eq (src, i) in
+    ok dst
 
-  let bytes_pack : typer = "Bytes.pack" , 1 , [
-      (true_1 , typer'_1 (fun _ -> ok ("PACK" , t_bytes ())))
-    ]
+  let int : typer = typer_1 "INT" @@ fun t ->
+    let%bind () = assert_t_nat t in
+    ok @@ t_int ()
 
-  let bytes_unpack = "Bytes.unpack" , 1 , [
-      eq_1 (t_bytes ()) , typer'_1_opt (fun _ tv_opt -> match tv_opt with
-          | None -> simple_fail "untyped UNPACK"
-          | Some t -> ok ("UNPACK", t))
-    ]
+  let bytes_pack : typer = typer_1 "PACK" @@ fun _t ->
+    ok @@ t_bytes ()
 
-  let crypto_hash = "Crypto.hash" , 1 , [
-      eq_1 (t_bytes ()) , typer_constant ("HASH" , t_bytes ()) ;
-    ]
+  let bytes_unpack = typer_1_opt "UNPACK" @@ fun input output_opt ->
+    let%bind () = assert_t_bytes input in
+    trace_option (simple_error "untyped UNPACK") @@
+    output_opt
 
-  let sender = "sender" , 0 , [
-      predicate_0 , typer_constant ("SENDER", t_address ())
-    ]
+  let crypto_hash = typer_1 "HASH" @@ fun t ->
+    let%bind () = assert_t_bytes t in
+    ok @@ t_bytes ()
 
-  let source = "source" , 0 , [
-      predicate_0 , typer_constant ("SOURCE", t_address ())
-    ]
+  let sender = constant "SENDER" @@ t_address ()
 
-  let unit = "unit" , 0 , [
-      predicate_0 , typer_constant ("UNIT", t_unit ())
-    ]
+  let source = constant "SOURCE" @@ t_address ()
 
-  let amount = "amount" , 0 , [
-      predicate_0 , typer_constant ("AMOUNT", t_tez ())
-    ]
+  let unit = constant "UNIT" @@ t_unit ()
 
-  let transaction = "Operation.transaction" , 3 , [
-      true_3 , typer'_3 (
-        fun param amount contract ->
-          let%bind () =
-            assert_t_tez amount in
-          let%bind contract_param =
-            get_t_contract contract in
-          let%bind () =
-            assert_type_value_eq (param , contract_param) in
-          ok ("TRANSFER_TOKENS" , t_operation ())
-      )
-    ]
-  let transaction' = "transaction" , 3 , [
-      true_3 , typer'_3 (
-        fun param amount contract ->
-          let%bind () =
-            assert_t_tez amount in
-          let%bind contract_param =
-            get_t_contract contract in
-          let%bind () =
-            assert_type_value_eq (param , contract_param) in
-          ok ("TRANSFER_TOKENS" , t_operation ())
-      )
-    ]
+  let amount = constant "AMOUNT" @@ t_tez ()
 
-  let get_contract = "Operation.get_contract" , 1 , [
-      eq_1 (t_address ()) , typer'_1_opt (
-        fun _ tv_opt ->
-          let%bind tv =
-            trace_option (simple_error "get_contract needs a type annotation") tv_opt in
-          let%bind tv' =
-            trace_strong (simple_error "get_contract has a not-contract annotation") @@
-            get_t_contract tv in
-          ok ("CONTRACT" , t_contract tv' ())
-      )
-    ]
-  let get_contract' = "get_contract" , 1 , [
-      eq_1 (t_address ()) , typer'_1_opt (
-        fun _ tv_opt ->
-          let%bind tv =
-            trace_option (simple_error "get_contract needs a type annotation") tv_opt in
-          let%bind tv' =
-            trace_strong (simple_error "get_contract has a not-contract annotation") @@
-            get_t_contract tv in
-          ok ("CONTRACT" , t_contract tv' ())
-      )
-    ]
+  let transaction = typer_3 "CALL" @@ fun param amount contract ->
+    let%bind () = assert_t_tez amount in
+    let%bind contract_param = get_t_contract contract in
+    let%bind () = assert_type_value_eq (param , contract_param) in
+    ok @@ t_operation ()
 
-  let num_2 : typer_predicate =
-    let aux = fun a b ->
-      (type_value_eq (a , t_int ()) || type_value_eq (a , t_nat ())) &&
-      (type_value_eq (b , t_int ()) || type_value_eq (b , t_nat ())) in
-    predicate_2 aux
+  let get_contract = typer_1_opt "CONTRACT" @@ fun _ tv_opt ->
+    let%bind tv =
+      trace_option (simple_error "get_contract needs a type annotation") tv_opt in
+    let%bind tv' =
+      trace_strong (simple_error "get_contract has a not-contract annotation") @@
+      get_t_contract tv in
+    ok @@ t_contract tv' ()
 
-  let mod_ = "MOD" , 2 , [
-      num_2 , constant_2 "MOD" (t_nat ()) ;
-    ]
+  let abs = typer_1 "ABS" @@ fun t ->
+    let%bind () = assert_t_int t in
+    ok @@ t_nat ()
+
+  let times = typer_2 "TIMES" @@ fun a b ->
+    if eq_2 (a , b) (t_nat ())
+    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
+      simple_fail "Multiplying with wrong types"
+
+  let div = typer_2 "DIV" @@ fun a b ->
+    if eq_2 (a , b) (t_nat ())
+    then ok @@ t_nat () else
+    if eq_2 (a , b) (t_int ())
+    then ok @@ t_int () 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
+      simple_fail "Computing modulo with wrong types"
+
+  let add = typer_2 "ADD" @@ fun a b ->
+    if eq_2 (a , b) (t_nat ())
+    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_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
+    then ok @@ t_int () else
+      simple_fail "Adding with wrong types"
 
-  let abs = "abs" , 1 , [
-      eq_1 (t_int ()) , typer_constant ("ABS" , (t_nat ())) ;
-    ]
 
-  let times = "TIMES" , 2 , [
-      (eq_2 (t_nat ()) , constant_2 "TIMES_NAT" (t_nat ())) ;
-      (num_2 , constant_2 "TIMES_INT" (t_int ())) ;
-      (
-        let aux a b =
-          (type_value_eq (a , t_nat ()) && type_value_eq (b , t_tez ())) ||
-          (type_value_eq (b , t_nat ()) && type_value_eq (a , t_tez ())) in
-       predicate_2 aux , constant_2 "TIMES_TEZ" (t_tez ())
-     ) ;
-    ]
 
   let constant_typers =
-    let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
+    let typer_to_kv : typer -> (string * _) = fun x -> x in
     Map.String.of_list
     @@ List.map typer_to_kv [
-      same_2 "ADD" [
-        ("ADD_INT" , t_int ()) ;
-        ("ADD_NAT" , t_nat ()) ;
-        ("CONCAT" , t_string ()) ;
-      ] ;
+      add ;
       times ;
-      same_2 "DIV" [
-        ("DIV_INT" , t_int ()) ;
-        ("DIV_NAT" , t_nat ()) ;
-      ] ;
+      div ;
       mod_ ;
       sub ;
       none ;
@@ -336,9 +296,7 @@ module Typer = struct
       unit ;
       amount ;
       transaction ;
-      transaction' ;
       get_contract ;
-      get_contract' ;
       abs ;
     ]
 
@@ -364,15 +322,10 @@ module Compiler = struct
   let simple_ternary c = Ternary c
 
   let predicates = Map.String.of_list [
-    ("ADD_INT" , simple_binary @@ prim I_ADD) ;
-    ("ADD_NAT" , simple_binary @@ prim I_ADD) ;
-    ("SUB_INT" , simple_binary @@ prim I_SUB) ;
-    ("SUB_NAT" , simple_binary @@ prim I_SUB) ;
-    ("TIMES_INT" , simple_binary @@ prim I_MUL) ;
-    ("TIMES_NAT" , simple_binary @@ prim I_MUL) ;
-    ("TIMES_TEZ" , simple_binary @@ prim I_MUL) ;
-    ("DIV_INT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
-    ("DIV_NAT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
+    ("ADD" , simple_binary @@ prim I_ADD) ;
+    ("SUB" , simple_binary @@ prim I_SUB) ;
+    ("TIMES" , simple_binary @@ prim I_MUL) ;
+    ("DIV" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
     ("MOD" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr]) ;
     ("NEG" , simple_unary @@ prim I_NEG) ;
     ("OR" , simple_binary @@ prim I_OR) ;
@@ -388,8 +341,8 @@ module Compiler = struct
     ("GE" , simple_binary @@ seq [prim I_COMPARE ; prim I_GE]) ;
     ("UPDATE" , simple_ternary @@ prim I_UPDATE) ;
     ("SOME" , simple_unary @@ prim I_SOME) ;
-    ("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
-    ("GET" , simple_binary @@ prim I_GET) ;
+    ("MAP_GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
+    ("MAP_GET" , simple_binary @@ prim I_GET) ;
     ("SIZE" , simple_unary @@ prim I_SIZE) ;
     ("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
     ("ASSERT" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
@@ -398,7 +351,7 @@ module Compiler = struct
     ("CONS" , simple_binary @@ prim I_CONS) ;
     ("UNIT" , simple_constant @@ prim I_UNIT) ;
     ("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
-    ("TRANSFER_TOKENS" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
+    ("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
     ("SOURCE" , simple_constant @@ prim I_SOURCE) ;
     ("SENDER" , simple_constant @@ prim I_SENDER) ;
     ( "MAP_UPDATE" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
diff --git a/src/simplify/camligo.ml b/src/simplify/camligo.ml
index 99fd94415..151116253 100644
--- a/src/simplify/camligo.ml
+++ b/src/simplify/camligo.ml
@@ -6,13 +6,11 @@ open O.Combinators
 
 let unwrap : type a . a Location.wrap -> a = Location.unwrap
 
-let type_constants = Operators.Simplify.type_constants
-let constants = Operators.Simplify.Camligo.constants
+open Operators.Simplify.Camligo
 
 let type_variable : string -> O.type_expression result = fun str ->
   match List.assoc_opt str type_constants with
-  | Some 0 -> ok @@ O.T_constant (str, [])
-  | Some _ -> simple_fail "non-nullary type constructor"
+  | Some s -> ok @@ O.T_constant (s , [])
   | None -> ok @@ O.T_variable str
 
 let get_param_restricted_pattern : I.param -> I.restricted_pattern Location.wrap result = fun p ->
@@ -145,19 +143,10 @@ let rec type_expression : I.type_expression -> O.type_expression result = fun te
       match unwrap f with
         | I.T_variable v -> (
             match List.assoc_opt v.wrap_content type_constants with
-            | Some n -> (
-                let error expected got =
-                  let title () = "bad arity" in
-                  let content () = Format.asprintf "Expected: %d. Got: %d." expected got in
-                  error title content in
+            | Some s -> (
                 match arg'.wrap_content with
-                | T_tuple lst -> (
-                    let%bind () =
-                      trace (error n (List.length lst)) @@
-                      Assert.assert_list_size lst n in
-                    ok @@ O.T_constant (v.wrap_content , lst)
-                  )
-                | e -> ok @@ O.T_constant ((unwrap v) , [ e ])
+                | T_tuple lst -> ok @@ O.T_constant (s , lst)
+                | e -> ok @@ O.T_constant (s , [ e ])
               )
             | None -> (
                 let error =
@@ -345,23 +334,13 @@ and expression_main : I.expression_main Location.wrap -> O.expression result = f
 and identifier_application : (string Location.wrap) list * string Location.wrap -> O.expression option -> _ result = fun (lst , v) param_opt ->
   let constant_name = String.concat "." ((List.map unwrap lst) @ [unwrap v]) in
   match List.assoc_opt constant_name constants , param_opt with
-  | Some 0 , None ->
-      ok O.(E_constant (constant_name , []))
-  | Some _ , None ->
-      simple_fail "n-ary constant without parameter"
-  | Some 0 , Some _ -> simple_fail "applying to nullary constant"
-  | Some 1 , Some param -> (
-      ok O.(E_constant (constant_name , [param]))
-    )
-  | Some n , Some param -> (
+  | Some s , None -> ok O.(E_constant (s , []))
+  | Some s , Some param -> (
       let params =
         match param with
         | E_tuple lst -> lst
         | _ -> [ param ] in
-      let%bind () =
-        trace_strong (simple_error "bad constant arity") @@
-        Assert.assert_list_size params n in
-      ok O.(E_constant (constant_name , params))
+      ok O.(E_constant (s , params))
     )
   | None , param_opt -> (
       let%bind () =
diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml
index c374f5c5a..970a42930 100644
--- a/src/simplify/ligodity.ml
+++ b/src/simplify/ligodity.ml
@@ -17,20 +17,15 @@ let pseq_to_list = function
   | Some lst -> npseq_to_list lst
 let get_value : 'a Raw.reg -> 'a = fun x -> x.value
 
-let type_constants = Operators.Simplify.type_constants
-let constants = Operators.Simplify.constants
+open Operators.Simplify.Ligodity
 
 let rec simpl_type_expression : Raw.type_expr -> type_expression result =
   function
   | TPar x -> simpl_type_expression x.value.inside
   | TAlias v -> (
       match List.assoc_opt v.value type_constants with
-      | Some 0 ->
-          ok @@ T_constant (v.value, [])
-      | Some _ ->
-          simple_fail "type constructor with wrong number of args"
-      | None ->
-          ok @@ T_variable v.value
+      | Some s -> ok @@ T_constant (s , [])
+      | None -> ok @@ T_variable v.value
     )
   | TFun x -> (
       let%bind (a , b) =
@@ -41,12 +36,11 @@ let rec simpl_type_expression : Raw.type_expr -> type_expression result =
   | TApp x ->
       let (name, tuple) = x.value in
       let lst = npseq_to_list tuple.value.inside in
-      let%bind _ = match List.assoc_opt name.value type_constants with
-        | Some n when n = List.length lst -> ok ()
-        | Some _ -> simple_fail "type constructor with wrong number of args"
-        | None -> simple_fail "unrecognized type constants" in
+      let%bind cst =
+        trace_option (simple_error "unrecognized type constants") @@
+        List.assoc_opt name.value type_constants in
       let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
-      ok @@ T_constant (name.value, lst')
+      ok @@ T_constant (cst , lst')
   | TProd p ->
       let%bind tpl = simpl_list_type_expression
         @@ npseq_to_list p.value in
@@ -134,32 +128,22 @@ let rec simpl_expression :
       let c' = c.value in
       match List.assoc_opt c' constants with
       | None -> return @@ E_variable c.value
-      | Some 0 -> return @@ E_constant (c' , [])
-      | Some n -> (
-          let error =
-            let title () = "non nullary constant without parameters" in
-            let content () = Format.asprintf "%s (%d)" c' n in
-            error title content in
-          fail error
-        )
+      | Some s -> return @@ E_constant (s , [])
     )
   | ECall x -> (
       let (e1, e2) = x.value in
       let%bind args = bind_map_list simpl_expression (nseq_to_list e2) in
       match e1 with
-        EVar f ->
+      | EVar f ->
           (match List.assoc_opt f.value constants with
           | None ->
               let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
               return @@ E_application (e_variable f.value, arg)
-          | Some arity ->
-              let%bind _arity =
-                trace (simple_error "wrong arity for constants") @@
-                Assert.assert_equal_int arity (List.length args) in
-              return @@ E_constant (f.value, args))
-      | e1 -> let%bind e1' = simpl_expression e1 in
-             let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
-             return @@ E_application (e1', arg)
+          | Some s -> return @@ E_constant (s , args))
+      | e1 ->
+        let%bind e1' = simpl_expression e1 in
+        let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
+        return @@ E_application (e1' , arg)
     )
   | EPar x -> simpl_expression ?te_annot x.value.inside
   | EUnit _ -> return @@ E_literal Literal_unit
diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml
index 62f64b8e5..038fd4484 100644
--- a/src/simplify/pascaligo.ml
+++ b/src/simplify/pascaligo.ml
@@ -14,8 +14,7 @@ let pseq_to_list = function
   | Some lst -> npseq_to_list lst
 let get_value : 'a Raw.reg -> 'a = fun x -> x.value
 
-let type_constants = Operators.Simplify.type_constants
-let constants = Operators.Simplify.constants
+open Operators.Simplify.Pascaligo
 
 let return expr = ok @@ fun expr'_opt ->
   let expr = expr in
@@ -33,12 +32,8 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
   | TPar x -> simpl_type_expression x.value.inside
   | TAlias v -> (
       match List.assoc_opt v.value type_constants with
-      | Some 0 ->
-          ok @@ T_constant (v.value, [])
-      | Some _ ->
-          simple_fail "type constructor with wrong number of args"
-      | None ->
-          ok @@ T_variable v.value
+      | Some s -> ok @@ T_constant (s , [])
+      | None -> ok @@ T_variable v.value
     )
   | TFun x -> (
       let%bind (a , b) =
@@ -49,12 +44,11 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
   | TApp x ->
       let (name, tuple) = x.value in
       let lst = npseq_to_list tuple.value.inside in
-      let%bind _ = match List.assoc_opt name.value type_constants with
-        | Some n when n = List.length lst -> ok ()
-        | Some _ -> simple_fail "type constructor with wrong number of args"
-        | None -> simple_fail "unrecognized type constants" in
       let%bind lst' = bind_list @@ List.map simpl_type_expression lst in
-      ok @@ T_constant (name.value, lst')
+      let%bind cst =
+        trace_option (simple_error "unrecognized type constants") @@
+        List.assoc_opt name.value type_constants in
+      ok @@ T_constant (cst , lst')
   | TProd p ->
       let%bind tpl = simpl_list_type_expression
         @@ npseq_to_list p.value in
@@ -119,14 +113,7 @@ let rec simpl_expression (t:Raw.expr) : expr result =
       let c' = c.value in
       match List.assoc_opt c' constants with
       | None -> return @@ E_variable c.value
-      | Some 0 -> return @@ E_constant (c' , [])
-      | Some n -> (
-          let error =
-            let title () = "non nullary constant without parameters" in
-            let content () = Format.asprintf "%s (%d)" c' n in
-            error title content in
-          fail error
-        )
+      | Some s -> return @@ E_constant (s , [])
     )
   | ECall x -> (
       let (name, args) = x.value in
@@ -136,12 +123,9 @@ let rec simpl_expression (t:Raw.expr) : expr result =
       | None ->
           let%bind arg = simpl_tuple_expression args' in
           return @@ E_application (e_variable f, arg)
-      | Some arity ->
-          let%bind _arity =
-            trace (simple_error "wrong arity for constants") @@
-            Assert.assert_equal_int arity (List.length args') in
+      | Some s ->
           let%bind lst = bind_map_list simpl_expression args' in
-          return @@ E_constant (f, lst)
+          return @@ E_constant (s , lst)
     )
   | EPar x -> simpl_expression x.value.inside
   | EUnit _ -> return @@ E_literal Literal_unit
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 262b9c722..98792fe6b 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -292,7 +292,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
       List.fold_left aux init m
   | E_look_up dsi ->
       let%bind (ds', i') = bind_map_pair f dsi in
-      return @@ E_constant ("GET", [i' ; ds'])
+      return @@ E_constant ("MAP_GET", [i' ; ds'])
   | E_sequence (a , b) -> (
       let%bind a' = translate_annotated_expression a in
       let%bind b' = translate_annotated_expression b in
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index 978faf1ed..d17962f53 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -497,34 +497,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
 and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
   (* Constant poorman's polymorphism *)
   let ct = Operators.Typer.constant_typers in
-  let%bind v =
+  let%bind typer =
     trace_option (unrecognized_constant name) @@
     Map.String.find_opt name ct in
-  let (arity, typer) = v in
-  let%bind () =
-    let l = List.length lst in
-    trace_strong (wrong_arity name arity l) @@
-    Assert.assert_true (arity = l) in
-
-  let error =
-    let title () = "typing: constant predicates all failed" in
-    let content () =
-      Format.asprintf "%s in %a"
-      name
-      PP_helpers.(list_sep Ast_typed.PP.type_value (const " , "))
-      lst
-    in
-    error title content in
-  let rec aux = fun ts ->
-    match ts with
-    | [] -> fail error
-    | (predicate, typer') :: tl -> (
-        match predicate lst with
-        | false -> aux tl
-        | true -> typer' lst tv_opt
-      )
-  in
-  aux typer
+  typer lst tv_opt
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =
   match t.simplified with