diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
index c8dbb9166664ce5e8d0eb6cd7d12023dcdc2d623..ad311af130124f475f5d369835a35ece0623d0b8 100644
--- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml
+++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml
@@ -256,7 +256,7 @@ module type S = sig
   end
 
   module rec Random_value : sig
-    val value : 'a Script_typed_ir.ty -> 'a sampler
+    val value : ('a, _) Script_typed_ir.ty -> 'a sampler
 
     val comparable : 'a Script_typed_ir.comparable_ty -> 'a sampler
 
@@ -489,7 +489,7 @@ end)
 
   (* Type-directed generation of random values. *)
   module rec Random_value : sig
-    val value : 'a Script_typed_ir.ty -> 'a sampler
+    val value : ('a, _) Script_typed_ir.ty -> 'a sampler
 
     val comparable : 'a Script_typed_ir.comparable_ty -> 'a sampler
 
@@ -538,7 +538,7 @@ end)
     let signature rng_state =
       Script_signature.make (Michelson_base.signature rng_state)
 
-    let rec value : type a. a Script_typed_ir.ty -> a sampler =
+    let rec value : type a ac. (a, ac) Script_typed_ir.ty -> a sampler =
       let open Script_typed_ir in
       fun typ ->
         match typ with
@@ -597,16 +597,17 @@ end)
         | Chest_t -> fail_sampling "Michelson_samplers: chest not handled yet"
 
     and generate_lambda :
-        type arg ret.
-        arg Script_typed_ir.ty ->
-        ret Script_typed_ir.ty ->
+        type arg argc ret retc.
+        (arg, argc) Script_typed_ir.ty ->
+        (ret, retc) Script_typed_ir.ty ->
         (arg, ret) Script_typed_ir.lambda sampler =
      fun _arg_ty _ret_ty _rng_state ->
       fail_sampling "Michelson_samplers: lambda not handled yet"
 
     and generate_list :
-        type elt.
-        elt Script_typed_ir.ty -> elt Script_typed_ir.boxed_list sampler =
+        type elt eltc.
+        (elt, eltc) Script_typed_ir.ty -> elt Script_typed_ir.boxed_list sampler
+        =
      fun elt_type ->
       let open M in
       let* (length, elements) =
@@ -636,9 +637,9 @@ end)
            elements
 
     and generate_map :
-        type key elt.
+        type key elt eltc.
         key Script_typed_ir.comparable_ty ->
-        elt Script_typed_ir.ty ->
+        (elt, eltc) Script_typed_ir.ty ->
         (key, elt) Script_typed_ir.map sampler =
      fun key_ty elt_ty rng_state ->
       let size =
@@ -654,9 +655,9 @@ end)
         elts
 
     and generate_big_map :
-        type key elt.
+        type key elt eltc.
         key Script_typed_ir.comparable_ty ->
-        elt Script_typed_ir.ty ->
+        (elt, eltc) Script_typed_ir.ty ->
         (key, elt) Script_typed_ir.big_map sampler =
       let open Script_typed_ir in
       fun key_ty elt_ty rng_state ->
@@ -688,8 +689,9 @@ end)
             fail_sampling "raise_if_error"
 
     and generate_contract :
-        type arg.
-        arg Script_typed_ir.ty -> arg Script_typed_ir.typed_contract sampler =
+        type arg argc.
+        (arg, argc) Script_typed_ir.ty ->
+        arg Script_typed_ir.typed_contract sampler =
      fun arg_ty ->
       let open M in
       let* address = value address_t in
@@ -726,7 +728,8 @@ end)
       | None -> assert false
 
     and generate_ticket :
-        type a. a Script_typed_ir.ty -> a Script_typed_ir.ticket sampler =
+        type a ac.
+        (a, ac) Script_typed_ir.ty -> a Script_typed_ir.ticket sampler =
      fun ty rng_state ->
       let contents = value ty rng_state in
       let ticketer =
diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.mli b/src/proto_alpha/lib_benchmark/michelson_samplers.mli
index b8833c70bec8e65073aad1cbd541a7aa3802a32f..04894568be258456e944e77300a3b8e6f214f0a1 100644
--- a/src/proto_alpha/lib_benchmark/michelson_samplers.mli
+++ b/src/proto_alpha/lib_benchmark/michelson_samplers.mli
@@ -79,7 +79,7 @@ module type S = sig
       supported types as listed at the beginning of this file. *)
   module rec Random_value : sig
     (** Sample a value given its type. *)
-    val value : 'a Script_typed_ir.ty -> 'a sampler
+    val value : ('a, _) Script_typed_ir.ty -> 'a sampler
 
     (** Sample a comparable value given its type. *)
     val comparable : 'a Script_typed_ir.comparable_ty -> 'a sampler
diff --git a/src/proto_alpha/lib_benchmark/test/test_distribution.ml b/src/proto_alpha/lib_benchmark/test/test_distribution.ml
index 2dee94ce5adba393a239b3261e688bc659cb21ac..74ad9d815f44f18a13d618fa35925823295e9c57 100644
--- a/src/proto_alpha/lib_benchmark/test/test_distribution.ml
+++ b/src/proto_alpha/lib_benchmark/test/test_distribution.ml
@@ -55,7 +55,7 @@ module Type_name_multiset =
   Basic_structures.Basic_impl.Free_module.Float_valued.Make_with_map (Type_name)
 
 let rec tnames_of_type :
-    type a. a Script_typed_ir.ty -> type_name list -> type_name list =
+    type a ac. (a, ac) Script_typed_ir.ty -> type_name list -> type_name list =
  fun t acc ->
   match t with
   | Script_typed_ir.Unit_t -> `TUnit :: acc
@@ -120,15 +120,15 @@ and tnames_of_comparable_type :
   | Script_typed_ir.Chain_id_key -> `TChain_id :: acc
   | Script_typed_ir.Address_key -> `TAddress :: acc
   | Script_typed_ir.Tx_rollup_l2_address_key -> `TTx_rollup_l2_address :: acc
-  | Script_typed_ir.Pair_key (lty, rty, _) ->
+  | Script_typed_ir.Pair_key (lty, rty, _, YesYes) ->
       tnames_of_comparable_type
         lty
         (tnames_of_comparable_type rty (`TPair :: acc))
-  | Script_typed_ir.Union_key (lty, rty, _) ->
+  | Script_typed_ir.Union_key (lty, rty, _, YesYes) ->
       tnames_of_comparable_type
         lty
         (tnames_of_comparable_type rty (`TUnion :: acc))
-  | Script_typed_ir.Option_key (ty, _) ->
+  | Script_typed_ir.Option_key (ty, _, Yes) ->
       tnames_of_comparable_type ty (`TOption :: acc)
 
 module Crypto_samplers = Crypto_samplers.Make_finite_key_pool (struct
diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml
index 1a91337abea3e293973554bdb3edd53887ed9e73..aaf5cac030f39614f6b1358df6fb5faf723cc4c1 100644
--- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml
+++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml
@@ -43,7 +43,7 @@ type ex_stack_and_continuation =
       -> ex_stack_and_continuation
 
 type ex_value =
-  | Ex_value : {value : 'a; ty : 'a Script_typed_ir.ty} -> ex_value
+  | Ex_value : {value : 'a; ty : ('a, _) Script_typed_ir.ty} -> ex_value
 
 (* ------------------------------------------------------------------------- *)
 
diff --git a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml
index 019736f39f94b73e09bcc141d6d17398de619447..efc4a0999951602afc26db61eac5f2e8651f458e 100644
--- a/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml
+++ b/src/proto_alpha/lib_benchmarks_proto/michelson_types.ml
@@ -96,17 +96,17 @@ let set k = match set_t (-1) k with Error _ -> assert false | Ok t -> t
 let pair k1 k2 =
   match pair_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t
 
-(* (will become) comparable pair type constructor *)
+(* comparable pair type constructor *)
 let cpair k1 k2 =
-  match pair_t (-1) k1 k2 with Error _ -> assert false | Ok (Ty_ex_c t) -> t
+  match comparable_pair_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t
 
 (* union type constructor*)
 let union k1 k2 =
   match union_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t
 
-(* (will become) comparable union type constructor *)
+(* comparable union type constructor *)
 let cunion k1 k2 =
-  match union_t (-1) k1 k2 with Error _ -> assert false | Ok (Ty_ex_c t) -> t
+  match comparable_union_t (-1) k1 k2 with Error _ -> assert false | Ok t -> t
 
 let lambda x y =
   match lambda_t (-1) x y with Error _ -> assert false | Ok t -> t
diff --git a/src/proto_alpha/lib_plugin/plugin.ml b/src/proto_alpha/lib_plugin/plugin.ml
index 8e0fe2cf24e54d8d3daaca4d9f29b684833fcf85..8e353635a1a732bd06241ebbd88e02843fc1a994 100644
--- a/src/proto_alpha/lib_plugin/plugin.ml
+++ b/src/proto_alpha/lib_plugin/plugin.ml
@@ -2001,15 +2001,15 @@ module RPC = struct
         | Address_key -> Prim (loc, T_address, [], [])
         | Tx_rollup_l2_address_key -> Prim (loc, T_tx_rollup_l2_address, [], [])
         | Chain_id_key -> Prim (loc, T_chain_id, [], [])
-        | Pair_key (l, r, _meta) ->
+        | Pair_key (l, r, _meta, YesYes) ->
             let tl = unparse_comparable_ty ~loc l in
             let tr = unparse_comparable_ty ~loc r in
             Prim (loc, T_pair, [tl; tr], [])
-        | Union_key (l, r, _meta) ->
+        | Union_key (l, r, _meta, YesYes) ->
             let tl = unparse_comparable_ty ~loc l in
             let tr = unparse_comparable_ty ~loc r in
             Prim (loc, T_or, [tl; tr], [])
-        | Option_key (t, _meta) ->
+        | Option_key (t, _meta, Yes) ->
             Prim (loc, T_option, [unparse_comparable_ty ~loc t], [])
 
       let unparse_memo_size ~loc memo_size =
@@ -2017,7 +2017,8 @@ module RPC = struct
         Int (loc, z)
 
       let rec unparse_ty :
-          type a loc. loc:loc -> a ty -> (loc, Script.prim) Micheline.node =
+          type a ac loc.
+          loc:loc -> (a, ac) ty -> (loc, Script.prim) Micheline.node =
        fun ~loc ty ->
         let return (name, args, annot) = Prim (loc, name, args, annot) in
         match ty with
diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL
index f799885d5d4397cfb93584c38f177c7b0de12fd7..0f4d060409cfeedd168896b612869c0013860591 100644
--- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL
+++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL
@@ -137,6 +137,7 @@
         "Script_tc_errors",
         "Gas_monad",
         "Script_ir_annot",
+        "Dependent_bool",
         "Script_typed_ir",
         "Script_comparable",
         "Gas_comparable_input_size",
diff --git a/src/proto_alpha/lib_protocol/apply.ml b/src/proto_alpha/lib_protocol/apply.ml
index aa21522186282635aac7e64a2821f77617c16acc..82640479660dcabe275ebc6d99cf8469b370ad5c 100644
--- a/src/proto_alpha/lib_protocol/apply.ml
+++ b/src/proto_alpha/lib_protocol/apply.ml
@@ -877,7 +877,9 @@ let apply_delegation ~ctxt ~source ~delegate ~since =
   (ctxt, Delegation_result {consumed_gas = Gas.consumed ~since ~until:ctxt}, [])
 
 type execution_arg =
-  | Typed_arg : Script.location * 'a Script_typed_ir.ty * 'a -> execution_arg
+  | Typed_arg :
+      Script.location * ('a, _) Script_typed_ir.ty * 'a
+      -> execution_arg
   | Untyped_arg : Script.expr -> execution_arg
 
 let apply_transaction_to_implicit ~ctxt ~contract ~parameter ~entrypoint
diff --git a/src/proto_alpha/lib_protocol/dependent_bool.ml b/src/proto_alpha/lib_protocol/dependent_bool.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8fb3c49ec11a721d14ccc754e6edf352c0664918
--- /dev/null
+++ b/src/proto_alpha/lib_protocol/dependent_bool.ml
@@ -0,0 +1,64 @@
+(*****************************************************************************)
+(*                                                                           *)
+(* Open Source License                                                       *)
+(* Copyright (c) 2022 Nomadic Labs <contact@nomadic-labs.com>                *)
+(*                                                                           *)
+(* 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.                                                 *)
+(*                                                                           *)
+(*****************************************************************************)
+
+type no = private DNo
+
+type yes = private DYes
+
+type _ dbool = No : no dbool | Yes : yes dbool
+
+type ('a, 'b, 'r) dand =
+  | NoNo : (no, no, no) dand
+  | NoYes : (no, yes, no) dand
+  | YesNo : (yes, no, no) dand
+  | YesYes : (yes, yes, yes) dand
+
+type ('a, 'b) ex_dand = Ex_dand : ('a, 'b, _) dand -> ('a, 'b) ex_dand
+[@@unboxed]
+
+let dand : type a b. a dbool -> b dbool -> (a, b) ex_dand =
+ fun a b ->
+  match (a, b) with
+  | (No, No) -> Ex_dand NoNo
+  | (No, Yes) -> Ex_dand NoYes
+  | (Yes, No) -> Ex_dand YesNo
+  | (Yes, Yes) -> Ex_dand YesYes
+
+let dbool_of_dand : type a b r. (a, b, r) dand -> r dbool = function
+  | NoNo -> No
+  | NoYes -> No
+  | YesNo -> No
+  | YesYes -> Yes
+
+type (_, _) eq = Eq : ('a, 'a) eq
+
+let merge_dand :
+    type a b c1 c2. (a, b, c1) dand -> (a, b, c2) dand -> (c1, c2) eq =
+ fun w1 w2 ->
+  match (w1, w2) with
+  | (NoNo, NoNo) -> Eq
+  | (NoYes, NoYes) -> Eq
+  | (YesNo, YesNo) -> Eq
+  | (YesYes, YesYes) -> Eq
diff --git a/src/proto_alpha/lib_protocol/dependent_bool.mli b/src/proto_alpha/lib_protocol/dependent_bool.mli
new file mode 100644
index 0000000000000000000000000000000000000000..54416d9fd9c3ed36b714b280fedb1cf6bc399293
--- /dev/null
+++ b/src/proto_alpha/lib_protocol/dependent_bool.mli
@@ -0,0 +1,65 @@
+(*****************************************************************************)
+(*                                                                           *)
+(* Open Source License                                                       *)
+(* Copyright (c) 2022 Nomadic Labs <contact@nomadic-labs.com>                *)
+(*                                                                           *)
+(* 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.                                                 *)
+(*                                                                           *)
+(*****************************************************************************)
+
+(** Dependent booleans *)
+
+type no = private DNo
+
+type yes = private DYes
+
+(** 
+    ['b dbool] is a boolean whose value depends on its type parameter ['b].
+    [yes dbool] can only be [Yes]. [no dbool] can only be [No].
+*)
+type _ dbool = No : no dbool | Yes : yes dbool
+
+(** 
+    [('a, 'b, 'r) dand] is a witness of the logical conjunction of dependent
+    booleans. ['r] is the result of ['a] and ['b].
+*)
+type ('a, 'b, 'r) dand =
+  | NoNo : (no, no, no) dand
+  | NoYes : (no, yes, no) dand
+  | YesNo : (yes, no, no) dand
+  | YesYes : (yes, yes, yes) dand
+
+type ('a, 'b) ex_dand = Ex_dand : ('a, 'b, _) dand -> ('a, 'b) ex_dand
+[@@unboxed]
+
+(** Logical conjunction of dependent booleans. *)
+val dand : 'a dbool -> 'b dbool -> ('a, 'b) ex_dand
+
+(** Result of the logical conjunction of dependent booleans. *)
+val dbool_of_dand : ('a, 'b, 'r) dand -> 'r dbool
+
+(** Type equality witness. *)
+type (_, _) eq = Eq : ('a, 'a) eq
+
+(**
+    [merge_dand] proves that the type [dand] represents a function, i.e. that
+    there is a unique ['r] such that [('a, 'b, 'r) dand] is inhabited for a
+    given ['a] and a given ['b].
+*)
+val merge_dand : ('a, 'b, 'c1) dand -> ('a, 'b, 'c2) dand -> ('c1, 'c2) eq
diff --git a/src/proto_alpha/lib_protocol/dune.inc b/src/proto_alpha/lib_protocol/dune.inc
index f662b0950347bc6c24c0c544ef2a6df843f3bb6b..de7d31cf75a25dc78c696bfe3566ab8ae3310ac8 100644
--- a/src/proto_alpha/lib_protocol/dune.inc
+++ b/src/proto_alpha/lib_protocol/dune.inc
@@ -153,6 +153,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end
    script_tc_errors.ml
    gas_monad.mli gas_monad.ml
    script_ir_annot.mli script_ir_annot.ml
+   dependent_bool.mli dependent_bool.ml
    script_typed_ir.mli script_typed_ir.ml
    script_comparable.mli script_comparable.ml
    gas_comparable_input_size.mli gas_comparable_input_size.ml
@@ -329,6 +330,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end
    script_tc_errors.ml
    gas_monad.mli gas_monad.ml
    script_ir_annot.mli script_ir_annot.ml
+   dependent_bool.mli dependent_bool.ml
    script_typed_ir.mli script_typed_ir.ml
    script_comparable.mli script_comparable.ml
    gas_comparable_input_size.mli gas_comparable_input_size.ml
@@ -505,6 +507,7 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end
    script_tc_errors.ml
    gas_monad.mli gas_monad.ml
    script_ir_annot.mli script_ir_annot.ml
+   dependent_bool.mli dependent_bool.ml
    script_typed_ir.mli script_typed_ir.ml
    script_comparable.mli script_comparable.ml
    gas_comparable_input_size.mli gas_comparable_input_size.ml
@@ -703,6 +706,7 @@ include Tezos_raw_protocol_alpha.Main
    Script_tc_errors
    Gas_monad
    Script_ir_annot
+   Dependent_bool
    Script_typed_ir
    Script_comparable
    Gas_comparable_input_size
@@ -920,6 +924,7 @@ include Tezos_raw_protocol_alpha.Main
    script_tc_errors.ml
    gas_monad.mli gas_monad.ml
    script_ir_annot.mli script_ir_annot.ml
+   dependent_bool.mli dependent_bool.ml
    script_typed_ir.mli script_typed_ir.ml
    script_comparable.mli script_comparable.ml
    gas_comparable_input_size.mli gas_comparable_input_size.ml
diff --git a/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml b/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml
index 9cbda6412b3cd12e540c6921a7a441c5f89d8529..040574b5c01bdf3535c6a010876ae68e29a00612 100644
--- a/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml
+++ b/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml
@@ -122,20 +122,20 @@ let rec size_of_comparable_value :
    | Timestamp_key -> timestamp v
    | Address_key -> address v
    | Tx_rollup_l2_address_key -> tx_rollup_l2_address v
-   | Pair_key (leaf, node, _) ->
+   | Pair_key (leaf, node, _, YesYes) ->
        let (lv, rv) = v in
        let size =
          size_of_comparable_value leaf lv + size_of_comparable_value node rv
        in
        size + 1
-   | Union_key (left, right, _) ->
+   | Union_key (left, right, _, YesYes) ->
        let size =
          match v with
          | L v -> size_of_comparable_value left v
          | R v -> size_of_comparable_value right v
        in
        size + 1
-   | Option_key (ty, _) -> (
+   | Option_key (ty, _, Yes) -> (
        match v with None -> 1 | Some x -> size_of_comparable_value ty x + 1)
    | Signature_key -> signature v
    | Key_key -> public_key v
diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
index 842cf0ba9f1c5728cacf3045ce789fe88eb9efab..39eb3d58ee201231b8cbc59b0ba95f15f09d7119 100644
--- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
+++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
@@ -1419,7 +1419,7 @@ module Cost_of = struct
         | Tx_rollup_l2_address_key ->
             (apply [@tailcall]) Gas.(acc +@ compare_tx_rollup_l2_address) k
         | Chain_id_key -> (apply [@tailcall]) Gas.(acc +@ compare_chain_id) k
-        | Pair_key (tl, tr, _) ->
+        | Pair_key (tl, tr, _, YesYes) ->
             (* Reasonable over-approximation of the cost of lexicographic comparison. *)
             let (xl, xr) = x in
             let (yl, yr) = y in
@@ -1429,7 +1429,7 @@ module Cost_of = struct
               yl
               Gas.(acc +@ compare_pair_tag)
               (Compare (tr, xr, yr, k))
-        | Union_key (tl, tr, _) -> (
+        | Union_key (tl, tr, _, YesYes) -> (
             match (x, y) with
             | (L x, L y) ->
                 (compare [@tailcall]) tl x y Gas.(acc +@ compare_union_tag) k
@@ -1437,7 +1437,7 @@ module Cost_of = struct
             | (R _, L _) -> (apply [@tailcall]) Gas.(acc +@ compare_union_tag) k
             | (R x, R y) ->
                 (compare [@tailcall]) tr x y Gas.(acc +@ compare_union_tag) k)
-        | Option_key (t, _) -> (
+        | Option_key (t, _, Yes) -> (
             match (x, y) with
             | (None, None) ->
                 (apply [@tailcall]) Gas.(acc +@ compare_option_tag) k
diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli
index 0ab0e9bea5e3a0f46f6a4a0ce74c093def36f2be..15a04ef478f30ef60a415e6906deb6666b105ac4 100644
--- a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli
+++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli
@@ -487,7 +487,7 @@ module Cost_of : sig
 
     val bls12_381_fr : Gas.cost
 
-    val unparse_type : 'a Script_typed_ir.ty -> Gas.cost
+    val unparse_type : ('a, _) Script_typed_ir.ty -> Gas.cost
 
     val unparse_comparable_type : 'a Script_typed_ir.comparable_ty -> Gas.cost
 
diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml
index d27805c044d69c6d1418ecfd85d456be8a86bfa7..cf152247ac95334d0205591372e072ebf1a9196c 100644
--- a/src/proto_alpha/lib_protocol/script_comparable.ml
+++ b/src/proto_alpha/lib_protocol/script_comparable.ml
@@ -68,22 +68,22 @@ let compare_comparable : type a. a comparable_ty -> a -> a -> int =
     | (Bytes_key, x, y) -> (apply [@tailcall]) (Compare.Bytes.compare x y) k
     | (Chain_id_key, x, y) ->
         (apply [@tailcall]) (Script_chain_id.compare x y) k
-    | (Pair_key (tl, tr, _), (lx, rx), (ly, ry)) ->
+    | (Pair_key (tl, tr, _, YesYes), (lx, rx), (ly, ry)) ->
         (compare_comparable [@tailcall])
           tl
           (Compare_comparable (tr, rx, ry, k))
           lx
           ly
-    | (Union_key (tl, _, _), L x, L y) ->
+    | (Union_key (tl, _, _, YesYes), L x, L y) ->
         (compare_comparable [@tailcall]) tl k x y
     | (Union_key _, L _, R _) -> -1
     | (Union_key _, R _, L _) -> 1
-    | (Union_key (_, tr, _), R x, R y) ->
+    | (Union_key (_, tr, _, YesYes), R x, R y) ->
         (compare_comparable [@tailcall]) tr k x y
     | (Option_key _, None, None) -> (apply [@tailcall]) 0 k
     | (Option_key _, None, Some _) -> -1
     | (Option_key _, Some _, None) -> 1
-    | (Option_key (t, _), Some x, Some y) ->
+    | (Option_key (t, _, Yes), Some x, Some y) ->
         (compare_comparable [@tailcall]) t k x y
   and apply ret k =
     match (ret, k) with
diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml
index 44bf5999956a9b9548339525fe2cd3aa28c9f521..70fb97fca2c445301a2ffeaa2df508d0ef48408c 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter.ml
@@ -1714,10 +1714,12 @@ let step logger ctxt step_constants descr stack =
 
 *)
 type execution_arg =
-  | Typed_arg : Script.location * 'a Script_typed_ir.ty * 'a -> execution_arg
+  | Typed_arg :
+      Script.location * ('a, _) Script_typed_ir.ty * 'a
+      -> execution_arg
   | Untyped_arg : Script.expr -> execution_arg
 
-let lift_execution_arg (type a) ctxt ~internal (entrypoint_ty : a ty)
+let lift_execution_arg (type a ac) ctxt ~internal (entrypoint_ty : (a, ac) ty)
     (box : a -> 'b) arg : ('b * context) tzresult Lwt.t =
   (match arg with
   | Untyped_arg arg ->
diff --git a/src/proto_alpha/lib_protocol/script_interpreter.mli b/src/proto_alpha/lib_protocol/script_interpreter.mli
index bfbde28e35d1d6579d178f2bf853de5d66bb9a84..c57869e469d08e6599d3c2ef07e5b01f017f1dc2 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter.mli
+++ b/src/proto_alpha/lib_protocol/script_interpreter.mli
@@ -126,7 +126,7 @@ val execute_with_typed_parameter :
   step_constants ->
   script:Script.t ->
   entrypoint:Entrypoint.t ->
-  parameter_ty:'a Script_typed_ir.ty ->
+  parameter_ty:('a, _) Script_typed_ir.ty ->
   location:Script.location ->
   parameter:'a ->
   internal:bool ->
diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index 3a0e161d00c7722a548291d58656e747183a27b3..7dbabb9d1c80a13138c4f774f769f1350a34f3e0 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -510,9 +510,9 @@ let transfer (ctxt, sc) gas amount location parameters_ty parameters destination
      parameters submitted by the interpreter to prepare them for the
      [Transaction] operation. *)
   let craft_transfer_parameters :
-      type a.
+      type a ac.
       context ->
-      a ty ->
+      (a, ac) ty ->
       (location, prim) Micheline.node ->
       Destination.t ->
       ((location, prim) Micheline.node * context) tzresult =
@@ -886,12 +886,12 @@ type ('a, 'b, 'c, 'd, 'e, 'f) ilsr_nat_type =
 
 type ifailwith_type = {
   ifailwith :
-    'a 'b.
+    'a 'ac 'b.
     logger option ->
     outdated_context * step_constants ->
     local_gas_counter ->
     Script.location ->
-    'a ty ->
+    ('a, 'ac) ty ->
     'a ->
     ('b, error trace) result Lwt.t;
 }
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 313f14a5abd6afde84dd17becd65161df95ca7a5..ee490f8b4ab774f383ce1ff94811d8349ac39dbb 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -161,7 +161,8 @@ let check_kind kinds expr =
    (everything that cannot contain a lambda). The rest is located at
    the end of the file. *)
 
-let rec ty_of_comparable_ty : type a. a comparable_ty -> a ty = function
+let rec ty_of_comparable_ty :
+    type a. a comparable_ty -> (a, Dependent_bool.yes) ty = function
   | Unit_key -> Unit_t
   | Never_key -> Never_t
   | Int_key -> Int_t
@@ -177,11 +178,11 @@ let rec ty_of_comparable_ty : type a. a comparable_ty -> a ty = function
   | Address_key -> Address_t
   | Tx_rollup_l2_address_key -> Tx_rollup_l2_address_t
   | Chain_id_key -> Chain_id_t
-  | Pair_key (l, r, meta) ->
-      Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, ())
-  | Union_key (l, r, meta) ->
-      Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, ())
-  | Option_key (t, meta) -> Option_t (ty_of_comparable_ty t, meta, ())
+  | Pair_key (l, r, meta, YesYes) ->
+      Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, YesYes)
+  | Union_key (l, r, meta, YesYes) ->
+      Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, YesYes)
+  | Option_key (t, meta, Yes) -> Option_t (ty_of_comparable_ty t, meta, Yes)
 
 let rec unparse_comparable_ty_uncarbonated :
     type a loc. loc:loc -> a comparable_ty -> loc Script.michelson_node =
@@ -201,7 +202,7 @@ let rec unparse_comparable_ty_uncarbonated :
   | Address_key -> Prim (loc, T_address, [], [])
   | Tx_rollup_l2_address_key -> Prim (loc, T_tx_rollup_l2_address, [], [])
   | Chain_id_key -> Prim (loc, T_chain_id, [], [])
-  | Pair_key (l, r, _meta) -> (
+  | Pair_key (l, r, _meta, YesYes) -> (
       let tl = unparse_comparable_ty_uncarbonated ~loc l in
       let tr = unparse_comparable_ty_uncarbonated ~loc r in
       (* Fold [pair a1 (pair ... (pair an-1 an))] into [pair a1 ... an] *)
@@ -210,11 +211,11 @@ let rec unparse_comparable_ty_uncarbonated :
       match tr with
       | Prim (_, T_pair, ts, []) -> Prim (loc, T_pair, tl :: ts, [])
       | _ -> Prim (loc, T_pair, [tl; tr], []))
-  | Union_key (l, r, _meta) ->
+  | Union_key (l, r, _meta, YesYes) ->
       let tl = unparse_comparable_ty_uncarbonated ~loc l in
       let tr = unparse_comparable_ty_uncarbonated ~loc r in
       Prim (loc, T_or, [tl; tr], [])
-  | Option_key (t, _meta) ->
+  | Option_key (t, _meta, Yes) ->
       Prim (loc, T_option, [unparse_comparable_ty_uncarbonated ~loc t], [])
 
 let unparse_memo_size ~loc memo_size =
@@ -222,7 +223,8 @@ let unparse_memo_size ~loc memo_size =
   Int (loc, z)
 
 let rec unparse_ty_entrypoints_uncarbonated :
-    type a loc. loc:loc -> a ty -> a entrypoints -> loc Script.michelson_node =
+    type a ac loc.
+    loc:loc -> (a, ac) ty -> a entrypoints -> loc Script.michelson_node =
  fun ~loc ty {nested = nested_entrypoints; name = entrypoint_name} ->
   let (name, args) =
     match ty with
@@ -332,8 +334,11 @@ let serialize_ty_for_error ty =
   unparse_ty_uncarbonated ~loc:() ty |> Micheline.strip_locations
 
 let[@coq_axiom_with_reason "gadt"] rec comparable_ty_of_ty :
-    type a.
-    context -> Script.location -> a ty -> (a comparable_ty * context) tzresult =
+    type a ac.
+    context ->
+    Script.location ->
+    (a, ac) ty ->
+    (a comparable_ty * context) tzresult =
  fun ctxt loc ty ->
   Gas.consume ctxt Typecheck_costs.comparable_ty_of_ty_cycle >>? fun ctxt ->
   match ty with
@@ -355,14 +360,14 @@ let[@coq_axiom_with_reason "gadt"] rec comparable_ty_of_ty :
   | Pair_t (l, r, pname, _) ->
       comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) ->
       comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) ->
-      (Pair_key (lty, rty, pname), ctxt)
+      (Pair_key (lty, rty, pname, YesYes), ctxt)
   | Union_t (l, r, meta, _) ->
       comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) ->
       comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) ->
-      (Union_key (lty, rty, meta), ctxt)
+      (Union_key (lty, rty, meta, YesYes), ctxt)
   | Option_t (tt, meta, _) ->
       comparable_ty_of_ty ctxt loc tt >|? fun (ty, ctxt) ->
-      (Option_key (ty, meta), ctxt)
+      (Option_key (ty, meta, Yes), ctxt)
   | Lambda_t _ | List_t _ | Ticket_t _ | Set_t _ | Map_t _ | Big_map_t _
   | Contract_t _ | Operation_t | Bls12_381_fr_t | Bls12_381_g1_t
   | Bls12_381_g2_t | Sapling_state_t _ | Sapling_transaction_t _
@@ -584,7 +589,7 @@ let unparse_option ~loc unparse_v ctxt = function
 
 let comparable_comb_witness2 :
     type t. t comparable_ty -> (t, unit -> unit -> unit) comb_witness = function
-  | Pair_key (_, Pair_key _, _) -> Comb_Pair (Comb_Pair Comb_Any)
+  | Pair_key (_, Pair_key _, _, YesYes) -> Comb_Pair (Comb_Pair Comb_Any)
   | Pair_key _ -> Comb_Pair Comb_Any
   | _ -> Comb_Any
 
@@ -624,16 +629,16 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_comparable_data :
   | (Key_hash_key, k) -> Lwt.return @@ unparse_key_hash ~loc ctxt mode k
   | (Chain_id_key, chain_id) ->
       Lwt.return @@ unparse_chain_id ~loc ctxt mode chain_id
-  | (Pair_key (tl, tr, _), pair) ->
+  | (Pair_key (tl, tr, _, YesYes), pair) ->
       let r_witness = comparable_comb_witness2 tr in
       let unparse_l ctxt v = unparse_comparable_data ~loc ctxt mode tl v in
       let unparse_r ctxt v = unparse_comparable_data ~loc ctxt mode tr v in
       unparse_pair ~loc unparse_l unparse_r ctxt mode r_witness pair
-  | (Union_key (tl, tr, _), v) ->
+  | (Union_key (tl, tr, _, YesYes), v) ->
       let unparse_l ctxt v = unparse_comparable_data ~loc ctxt mode tl v in
       let unparse_r ctxt v = unparse_comparable_data ~loc ctxt mode tr v in
       unparse_union ~loc unparse_l unparse_r ctxt v
-  | (Option_key (t, _), v) ->
+  | (Option_key (t, _, Yes), v) ->
       let unparse_v ctxt v = unparse_comparable_data ~loc ctxt mode t v in
       unparse_option ~loc unparse_v ctxt v
   | (Never_key, _) -> .
@@ -675,7 +680,7 @@ let check_dupable_comparable_ty : type a. a comparable_ty -> unit = function
       ()
 
 let check_dupable_ty ctxt loc ty =
-  let rec aux : type a. location -> a ty -> (unit, error) Gas_monad.t =
+  let rec aux : type a ac. location -> (a, ac) ty -> (unit, error) Gas_monad.t =
    fun loc ty ->
     let open Gas_monad.Syntax in
     let* () = Gas_monad.consume_gas Typecheck_costs.check_dupable_cycle in
@@ -817,21 +822,21 @@ let rec comparable_ty_eq :
     | (Address_key, _) -> not_equal ()
     | (Tx_rollup_l2_address_key, Tx_rollup_l2_address_key) -> return Eq
     | (Tx_rollup_l2_address_key, _) -> not_equal ()
-    | (Pair_key (left_a, right_a, meta_a), Pair_key (left_b, right_b, meta_b))
-      ->
+    | ( Pair_key (left_a, right_a, meta_a, YesYes),
+        Pair_key (left_b, right_b, meta_b, YesYes) ) ->
         let* () = type_metadata_eq meta_a meta_b in
         let* Eq = comparable_ty_eq ~error_details left_a left_b in
         let+ Eq = comparable_ty_eq ~error_details right_a right_b in
         (Eq : (ta comparable_ty, tb comparable_ty) eq)
     | (Pair_key _, _) -> not_equal ()
-    | (Union_key (left_a, right_a, meta_a), Union_key (left_b, right_b, meta_b))
-      ->
+    | ( Union_key (left_a, right_a, meta_a, YesYes),
+        Union_key (left_b, right_b, meta_b, YesYes) ) ->
         let* () = type_metadata_eq meta_a meta_b in
         let* Eq = comparable_ty_eq ~error_details left_a left_b in
         let+ Eq = comparable_ty_eq ~error_details right_a right_b in
         (Eq : (ta comparable_ty, tb comparable_ty) eq)
     | (Union_key _, _) -> not_equal ()
-    | (Option_key (ta, meta_a), Option_key (tb, meta_b)) ->
+    | (Option_key (ta, meta_a, Yes), Option_key (tb, meta_b, Yes)) ->
         let* () = type_metadata_eq meta_a meta_b in
         let+ Eq = comparable_ty_eq ~error_details ta tb in
         (Eq : (ta comparable_ty, tb comparable_ty) eq)
@@ -853,12 +858,12 @@ let memo_size_eq :
 
 (** Same as comparable_ty_eq but for any types. *)
 let ty_eq :
-    type a b error_trace.
+    type a ac b bc error_trace.
     error_details:error_trace error_details ->
     Script.location ->
-    a ty ->
-    b ty ->
-    ((a ty, b ty) eq, error_trace) Gas_monad.t =
+    (a, ac) ty ->
+    (b, bc) ty ->
+    (((a, ac) ty, (b, bc) ty) eq, error_trace) Gas_monad.t =
  fun ~error_details loc ty1 ty2 ->
   let type_metadata_eq meta1 meta2 =
     Gas_monad.of_result (type_metadata_eq ~error_details meta1 meta2)
@@ -871,15 +876,19 @@ let ty_eq :
     Gas_monad.of_result (memo_size_eq ~error_details ms1 ms2)
   in
   let rec help :
-      type ta tb. ta ty -> tb ty -> ((ta ty, tb ty) eq, error_trace) Gas_monad.t
-      =
+      type ta tac tb tbc.
+      (ta, tac) ty ->
+      (tb, tbc) ty ->
+      (((ta, tac) ty, (tb, tbc) ty) eq, error_trace) Gas_monad.t =
    fun ty1 ty2 ->
     help0 ty1 ty2
     |> Gas_monad.record_trace_eval ~error_details (fun () ->
            default_ty_eq_error ty1 ty2)
   and help0 :
-      type ta tb. ta ty -> tb ty -> ((ta ty, tb ty) eq, error_trace) Gas_monad.t
-      =
+      type ta tac tb tbc.
+      (ta, tac) ty ->
+      (tb, tbc) ty ->
+      (((ta, tac) ty, (tb, tbc) ty) eq, error_trace) Gas_monad.t =
    fun ty1 ty2 ->
     let open Gas_monad.Syntax in
     let* () = Gas_monad.consume_gas Typecheck_costs.merge_cycle in
@@ -891,7 +900,7 @@ let ty_eq :
            | Informative -> trace_of_error @@ default_ty_eq_error ty1 ty2)
     in
     match (ty1, ty2) with
-    | (Unit_t, Unit_t) -> return (Eq : (ta ty, tb ty) eq)
+    | (Unit_t, Unit_t) -> return (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Unit_t, _) -> not_equal ()
     | (Int_t, Int_t) -> return Eq
     | (Int_t, _) -> not_equal ()
@@ -933,56 +942,58 @@ let ty_eq :
         let* () = type_metadata_eq meta1 meta2 in
         let* Eq = help tar tbr in
         let+ Eq = comparable_ty_eq ~error_details tal tbl in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Map_t _, _) -> not_equal ()
     | (Big_map_t (tal, tar, meta1), Big_map_t (tbl, tbr, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let* Eq = help tar tbr in
         let+ Eq = comparable_ty_eq ~error_details tal tbl in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Big_map_t _, _) -> not_equal ()
     | (Set_t (ea, meta1), Set_t (eb, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let+ Eq = comparable_ty_eq ~error_details ea eb in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Set_t _, _) -> not_equal ()
     | (Ticket_t (ea, meta1), Ticket_t (eb, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let+ Eq = comparable_ty_eq ~error_details ea eb in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Ticket_t _, _) -> not_equal ()
-    | (Pair_t (tal, tar, meta1, _), Pair_t (tbl, tbr, meta2, _)) ->
+    | (Pair_t (tal, tar, meta1, cmp1), Pair_t (tbl, tbr, meta2, cmp2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let* Eq = help tal tbl in
         let+ Eq = help tar tbr in
-        (Eq : (ta ty, tb ty) eq)
+        let Eq = Dependent_bool.merge_dand cmp1 cmp2 in
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Pair_t _, _) -> not_equal ()
-    | (Union_t (tal, tar, meta1, _), Union_t (tbl, tbr, meta2, _)) ->
+    | (Union_t (tal, tar, meta1, cmp1), Union_t (tbl, tbr, meta2, cmp2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let* Eq = help tal tbl in
         let+ Eq = help tar tbr in
-        (Eq : (ta ty, tb ty) eq)
+        let Eq = Dependent_bool.merge_dand cmp1 cmp2 in
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Union_t _, _) -> not_equal ()
     | (Lambda_t (tal, tar, meta1), Lambda_t (tbl, tbr, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let* Eq = help tal tbl in
         let+ Eq = help tar tbr in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Lambda_t _, _) -> not_equal ()
     | (Contract_t (tal, meta1), Contract_t (tbl, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let+ Eq = help tal tbl in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Contract_t _, _) -> not_equal ()
     | (Option_t (tva, meta1, _), Option_t (tvb, meta2, _)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let+ Eq = help tva tvb in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (Option_t _, _) -> not_equal ()
     | (List_t (tva, meta1), List_t (tvb, meta2)) ->
         let* () = type_metadata_eq meta1 meta2 in
         let+ Eq = help tva tvb in
-        (Eq : (ta ty, tb ty) eq)
+        (Eq : ((ta, tac) ty, (tb, tbc) ty) eq)
     | (List_t _, _) -> not_equal ()
     | (Sapling_state_t ms1, Sapling_state_t ms2) ->
         let+ () = memo_size_eq ms1 ms2 in
@@ -1215,11 +1226,11 @@ let[@coq_struct "ty"] rec parse_comparable_ty :
                T_key;
              ]
 
-type ex_ty = Ex_ty : 'a ty -> ex_ty
+type ex_ty = Ex_ty : ('a, _) ty -> ex_ty
 
 type ex_parameter_ty_and_entrypoints =
   | Ex_parameter_ty_and_entrypoints : {
-      arg_type : 'a ty;
+      arg_type : ('a, _) ty;
       entrypoints : 'a entrypoints;
     }
       -> ex_parameter_ty_and_entrypoints
@@ -1730,7 +1741,7 @@ let parse_storage_ty :
   | _ -> (parse_normal_storage_ty [@tailcall]) ctxt ~stack_depth ~legacy node
 
 let check_packable ~legacy loc root =
-  let rec check : type t. t ty -> unit tzresult = function
+  let rec check : type t tc. (t, tc) ty -> unit tzresult = function
     (* /!\ When adding new lazy storage kinds, be sure to return an error. /!\
        Lazy storage should not be packable. *)
     | Big_map_t _ -> error (Unexpected_lazy_storage loc)
@@ -1782,8 +1793,8 @@ type ('arg, 'storage) code =
   | Code : {
       code :
         (('arg, 'storage) pair, (operation boxed_list, 'storage) pair) lambda;
-      arg_type : 'arg ty;
-      storage_type : 'storage ty;
+      arg_type : ('arg, _) ty;
+      storage_type : ('storage, _) ty;
       views : view_map;
       entrypoints : 'arg entrypoints;
       code_size : Cache_memory_helpers.sint;
@@ -1794,9 +1805,9 @@ type ex_script =
   | Ex_script : {
       code :
         (('arg, 'storage) pair, (operation boxed_list, 'storage) pair) lambda;
-      arg_type : 'arg ty;
+      arg_type : ('arg, _) ty;
       storage : 'storage;
-      storage_type : 'storage ty;
+      storage_type : ('storage, _) ty;
       views : view_map;
       entrypoints : 'arg entrypoints;
       code_size : Cache_memory_helpers.sint;
@@ -1818,7 +1829,7 @@ type 'storage ex_view =
 type (_, _) dig_proof_argument =
   | Dig_proof_argument :
       ('x, 'a * 's, 'a, 's, 'b, 't, 'c, 'u) stack_prefix_preservation_witness
-      * 'x ty
+      * ('x, _) ty
       * ('c, 'u) stack_ty
       -> ('b, 't) dig_proof_argument
 
@@ -1854,24 +1865,24 @@ type 'before uncomb_proof_argument =
 
 type 'before comb_get_proof_argument =
   | Comb_get_proof_argument :
-      ('before, 'after) comb_get_gadt_witness * 'after ty
+      ('before, 'after) comb_get_gadt_witness * ('after, _) ty
       -> 'before comb_get_proof_argument
 
 type ('rest, 'before) comb_set_proof_argument =
   | Comb_set_proof_argument :
-      ('rest, 'before, 'after) comb_set_gadt_witness * 'after ty
+      ('rest, 'before, 'after) comb_set_gadt_witness * ('after, _) ty
       -> ('rest, 'before) comb_set_proof_argument
 
 type 'before dup_n_proof_argument =
   | Dup_n_proof_argument :
-      ('before, 'a) dup_n_gadt_witness * 'a ty
+      ('before, 'a) dup_n_gadt_witness * ('a, _) ty
       -> 'before dup_n_proof_argument
 
 let rec make_dug_proof_argument :
-    type a s x.
+    type a s x xc.
     location ->
     int ->
-    x ty ->
+    (x, xc) ty ->
     (a, s) stack_ty ->
     (a, s, x) dug_proof_argument option =
  fun loc n x stk ->
@@ -1885,7 +1896,7 @@ let rec make_dug_proof_argument :
   | (_, _) -> None
 
 let rec make_comb_get_proof_argument :
-    type b. int -> b ty -> b comb_get_proof_argument option =
+    type b bc. int -> (b, bc) ty -> b comb_get_proof_argument option =
  fun n ty ->
   match (n, ty) with
   | (0, value_ty) -> Some (Comb_get_proof_argument (Comb_get_zero, value_ty))
@@ -1899,13 +1910,13 @@ let rec make_comb_get_proof_argument :
   | _ -> None
 
 let rec make_comb_set_proof_argument :
-    type value before a s.
+    type value valuec before beforec a s.
     context ->
     (a, s) stack_ty ->
     location ->
     int ->
-    value ty ->
-    before ty ->
+    (value, valuec) ty ->
+    (before, beforec) ty ->
     (value, before) comb_set_proof_argument tzresult =
  fun ctxt stack_ty loc n value_ty ty ->
   match (n, ty) with
@@ -1922,17 +1933,19 @@ let rec make_comb_set_proof_argument :
       let whole_stack = serialize_stack_for_error ctxt stack_ty in
       error (Bad_stack (loc, I_UPDATE, 2, whole_stack))
 
-type 'a ex_ty_cstr = Ex_ty_cstr : 'b ty * ('b -> 'a) -> 'a ex_ty_cstr
+type 'a ex_ty_cstr = Ex_ty_cstr : ('b, _) ty * ('b -> 'a) -> 'a ex_ty_cstr
 
-let find_entrypoint (type full error_trace)
-    ~(error_details : error_trace error_details) (full : full ty)
+let find_entrypoint (type full fullc error_trace)
+    ~(error_details : error_trace error_details) (full : (full, fullc) ty)
     (entrypoints : full entrypoints) entrypoint :
     (full ex_ty_cstr, error_trace) Gas_monad.t =
   let open Gas_monad.Syntax in
   let rec find_entrypoint :
-      type t.
-      t ty -> t entrypoints -> Entrypoint.t -> (t ex_ty_cstr, unit) Gas_monad.t
-      =
+      type t tc.
+      (t, tc) ty ->
+      t entrypoints ->
+      Entrypoint.t ->
+      (t ex_ty_cstr, unit) Gas_monad.t =
    fun ty entrypoints entrypoint ->
     let* () = Gas_monad.consume_gas Typecheck_costs.find_entrypoint_cycle in
     match (ty, entrypoints) with
@@ -1960,9 +1973,10 @@ let find_entrypoint (type full error_trace)
              | Fast -> (Inconsistent_types_fast : error_trace)
              | Informative -> trace_of_error @@ No_such_entrypoint entrypoint)
 
-let find_entrypoint_for_type (type full exp error_trace) ~error_details
-    ~(full : full ty) ~(expected : exp ty) entrypoints entrypoint loc :
-    (Entrypoint.t * exp ty, error_trace) Gas_monad.t =
+let find_entrypoint_for_type (type full fullc exp expc error_trace)
+    ~error_details ~(full : (full, fullc) ty) ~(expected : (exp, expc) ty)
+    entrypoints entrypoint loc :
+    (Entrypoint.t * (exp, expc) ty, error_trace) Gas_monad.t =
   let open Gas_monad.Syntax in
   let* res = find_entrypoint ~error_details full entrypoints entrypoint in
   match res with
@@ -1972,17 +1986,18 @@ let find_entrypoint_for_type (type full exp error_trace) ~error_details
           Gas_monad.bind_recover
             (ty_eq ~error_details:Fast loc ty expected)
             (function
-              | Ok Eq -> return (Entrypoint.default, (ty : exp ty))
+              | Ok Eq -> return (Entrypoint.default, (ty : (exp, expc) ty))
               | Error Inconsistent_types_fast ->
                   let+ Eq = ty_eq ~error_details loc full expected in
-                  (Entrypoint.root, (full : exp ty)))
+                  (Entrypoint.root, (full : (exp, expc) ty)))
       | _ ->
           let+ Eq = ty_eq ~error_details loc ty expected in
-          (entrypoint, (ty : exp ty)))
+          (entrypoint, (ty : (exp, expc) ty)))
 
-let well_formed_entrypoints (type full) (full : full ty) entrypoints =
-  let merge path (type t) (ty : t ty) (entrypoints : t entrypoints) reachable
-      ((first_unreachable, all) as acc) =
+let well_formed_entrypoints (type full fullc) (full : (full, fullc) ty)
+    entrypoints =
+  let merge path (type t tc) (ty : (t, tc) ty) (entrypoints : t entrypoints)
+      reachable ((first_unreachable, all) as acc) =
     match entrypoints.name with
     | None ->
         ok
@@ -2000,8 +2015,8 @@ let well_formed_entrypoints (type full) (full : full ty) entrypoints =
         else ok ((first_unreachable, Entrypoint.Set.add name all), true)
   in
   let rec check :
-      type t.
-      t ty ->
+      type t tc.
+      (t, tc) ty ->
       t entrypoints ->
       prim list ->
       bool ->
@@ -2475,23 +2490,24 @@ let[@coq_axiom_with_reason "gadt"] rec parse_comparable_data :
       Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr
   | (Tx_rollup_l2_address_key, expr) ->
       Lwt.return @@ traced_no_lwt @@ parse_tx_rollup_l2_address ctxt expr
-  | (Pair_key (tl, tr, _), expr) ->
+  | (Pair_key (tl, tr, _, YesYes), expr) ->
       let r_witness = comparable_comb_witness1 tr in
       let parse_l ctxt v = parse_comparable_data ?type_logger ctxt tl v in
       let parse_r ctxt v = parse_comparable_data ?type_logger ctxt tr v in
       traced @@ parse_pair parse_l parse_r ctxt ~legacy r_witness expr
-  | (Union_key (tl, tr, _), expr) ->
+  | (Union_key (tl, tr, _, YesYes), expr) ->
       let parse_l ctxt v = parse_comparable_data ?type_logger ctxt tl v in
       let parse_r ctxt v = parse_comparable_data ?type_logger ctxt tr v in
       traced @@ parse_union parse_l parse_r ctxt ~legacy expr
-  | (Option_key (t, _), expr) ->
+  | (Option_key (t, _, Yes), expr) ->
       let parse_v ctxt v = parse_comparable_data ?type_logger ctxt t v in
       traced @@ parse_option parse_v ctxt ~legacy expr
   | (Never_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_never expr
 
 (* -- parse data of any type -- *)
 
-let comb_witness1 : type t. t ty -> (t, unit -> unit) comb_witness = function
+let comb_witness1 : type t tc. (t, tc) ty -> (t, unit -> unit) comb_witness =
+  function
   | Pair_t _ -> Comb_Pair Comb_Any
   | _ -> Comb_Any
 
@@ -2509,13 +2525,13 @@ let comb_witness1 : type t. t ty -> (t, unit -> unit) comb_witness = function
 *)
 
 let[@coq_axiom_with_reason "gadt"] rec parse_data :
-    type a.
+    type a ac.
     ?type_logger:type_logger ->
     stack_depth:int ->
     context ->
     legacy:bool ->
     allow_forged:bool ->
-    a ty ->
+    (a, ac) ty ->
     Script.node ->
     (a * context) tzresult Lwt.t =
  fun ?type_logger ~stack_depth ctxt ~legacy ~allow_forged ty script_data ->
@@ -2953,11 +2969,11 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data :
       traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr))
 
 and parse_view_returning :
-    type storage.
+    type storage storagec.
     ?type_logger:type_logger ->
     context ->
     legacy:bool ->
-    storage ty ->
+    (storage, storagec) ty ->
     view ->
     (storage ex_view * context) tzresult Lwt.t =
  fun ?type_logger ctxt ~legacy storage_type {input_ty; output_ty; view_code} ->
@@ -3013,11 +3029,11 @@ and parse_view_returning :
       | _ -> error (ill_type_view loc aft ()))
 
 and typecheck_views :
-    type storage.
+    type storage storagec.
     ?type_logger:type_logger ->
     context ->
     legacy:bool ->
-    storage ty ->
+    (storage, storagec) ty ->
     view_map ->
     context tzresult Lwt.t =
  fun ?type_logger ctxt ~legacy storage_type views ->
@@ -3028,14 +3044,14 @@ and typecheck_views :
   Script_map.fold_es aux views ctxt
 
 and[@coq_axiom_with_reason "gadt"] parse_returning :
-    type arg ret.
+    type arg argc ret retc.
     ?type_logger:type_logger ->
     stack_depth:int ->
     tc_context ->
     context ->
     legacy:bool ->
-    arg ty ->
-    ret ty ->
+    (arg, argc) ty ->
+    (ret, retc) ty ->
     Script.node ->
     ((arg, ret) lambda * context) tzresult Lwt.t =
  fun ?type_logger ~stack_depth tc_context ctxt ~legacy arg ret script_instr ->
@@ -3080,8 +3096,8 @@ and[@coq_axiom_with_reason "gadt"] parse_instr :
     (a, s) stack_ty ->
     ((a, s) judgement * context) tzresult Lwt.t =
  fun ?type_logger ~stack_depth tc_context ctxt ~legacy script_instr stack_ty ->
-  let check_item_ty (type a b) ctxt (exp : a ty) (got : b ty) loc name n m :
-      ((a, b) eq * context) tzresult =
+  let check_item_ty (type a ac b bc) ctxt (exp : (a, ac) ty) (got : (b, bc) ty)
+      loc name n m : ((a, b) eq * context) tzresult =
     record_trace_eval (fun () ->
         let stack_ty = serialize_stack_for_error ctxt stack_ty in
         Bad_stack (loc, name, m, stack_ty))
@@ -5109,11 +5125,11 @@ and[@coq_axiom_with_reason "gadt"] parse_instr :
            ]
 
 and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contract :
-    type arg.
+    type arg argc.
     stack_depth:int ->
     context ->
     Script.location ->
-    arg ty ->
+    (arg, argc) ty ->
     Destination.t ->
     entrypoint:Entrypoint.t ->
     (context * arg typed_contract) tzresult Lwt.t =
@@ -5304,10 +5320,10 @@ and parse_toplevel :
    returned and some overapproximation of the typechecking gas is consumed.
    This can still fail on gas exhaustion. *)
 let parse_contract_for_script :
-    type arg.
+    type arg argc.
     context ->
     Script.location ->
-    arg ty ->
+    (arg, argc) ty ->
     Destination.t ->
     entrypoint:Entrypoint.t ->
     (context * arg typed_contract option) tzresult Lwt.t =
@@ -5468,7 +5484,7 @@ let parse_storage :
     context ->
     legacy:bool ->
     allow_forged:bool ->
-    'storage ty ->
+    ('storage, _) ty ->
     storage:lazy_expr ->
     ('storage * context) tzresult Lwt.t =
  fun ?type_logger ctxt ~legacy ~allow_forged storage_type ~storage ->
@@ -5569,10 +5585,10 @@ let typecheck_code :
   trace (Ill_typed_contract (code, !type_map)) views_result >|=? fun ctxt ->
   (!type_map, ctxt)
 
-let list_entrypoints ctxt (type full) (full : full ty)
+let list_entrypoints ctxt (type full fullc) (full : (full, fullc) ty)
     (entrypoints : full entrypoints) =
-  let merge path (type t) (ty : t ty) (entrypoints : t entrypoints) reachable
-      ((unreachables, all) as acc) =
+  let merge path (type t tc) (ty : (t, tc) ty) (entrypoints : t entrypoints)
+      reachable ((unreachables, all) as acc) =
     match entrypoints.name with
     | None ->
         ok
@@ -5592,8 +5608,8 @@ let list_entrypoints ctxt (type full) (full : full ty)
         >|? fun unreachable_all -> (unreachable_all, true)
   in
   let rec fold_tree :
-      type t.
-      t ty ->
+      type t tc.
+      (t, tc) ty ->
       t entrypoints ->
       prim list ->
       bool ->
@@ -5626,18 +5642,18 @@ let list_entrypoints ctxt (type full) (full : full ty)
 
 (* -- Unparsing data of any type -- *)
 
-let comb_witness2 : type t. t ty -> (t, unit -> unit -> unit) comb_witness =
-  function
+let comb_witness2 :
+    type t tc. (t, tc) ty -> (t, unit -> unit -> unit) comb_witness = function
   | Pair_t (_, Pair_t _, _, _) -> Comb_Pair (Comb_Pair Comb_Any)
   | Pair_t _ -> Comb_Pair Comb_Any
   | _ -> Comb_Any
 
 let[@coq_axiom_with_reason "gadt"] rec unparse_data :
-    type a.
+    type a ac.
     context ->
     stack_depth:int ->
     unparsing_mode ->
-    a ty ->
+    (a, ac) ty ->
     a ->
     (Script.node * context) tzresult Lwt.t =
  fun ctxt ~stack_depth mode ty a ->
@@ -5819,12 +5835,12 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data :
         Script_timelock.chest_encoding
 
 and unparse_items :
-    type k v.
+    type k v vc.
     context ->
     stack_depth:int ->
     unparsing_mode ->
     k comparable_ty ->
-    v ty ->
+    (v, vc) ty ->
     (k * v) list ->
     (Script.node list * context) tzresult Lwt.t =
  fun ctxt ~stack_depth mode kt vt items ->
@@ -6130,7 +6146,7 @@ type 'ty has_lazy_storage =
     the types, which happen to be literally written types, so the gas for them
     has already been paid.
 *)
-let rec has_lazy_storage : type t. t ty -> t has_lazy_storage =
+let rec has_lazy_storage : type t tc. (t, tc) ty -> t has_lazy_storage =
  fun ty ->
   let aux1 cons t =
     match has_lazy_storage t with False_f -> False_f | h -> cons h
@@ -6187,13 +6203,13 @@ let rec has_lazy_storage : type t. t ty -> t has_lazy_storage =
 let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode
     ~temporary ids_to_copy acc ty x =
   let rec aux :
-      type a.
+      type a ac.
       context ->
       unparsing_mode ->
       temporary:bool ->
       Lazy_storage.IdSet.t ->
       Lazy_storage.diffs ->
-      a ty ->
+      (a, ac) ty ->
       a ->
       has_lazy_storage:a has_lazy_storage ->
       (context * a * Lazy_storage.IdSet.t * Lazy_storage.diffs) tzresult Lwt.t =
@@ -6297,11 +6313,11 @@ end
     [unit] type for [error] if you are in a case where errors are impossible.
 *)
 let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage :
-    type a error.
+    type a ac error.
     f:('acc, error) Fold_lazy_storage.result Lazy_storage.IdSet.fold_f ->
     init:'acc ->
     context ->
-    a ty ->
+    (a, ac) ty ->
     a ->
     has_lazy_storage:a has_lazy_storage ->
     (('acc, error) Fold_lazy_storage.result * context) tzresult =
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.mli b/src/proto_alpha/lib_protocol/script_ir_translator.mli
index abc745a7aad191d3bfcf1b1512073886c4b9ce09..3b2285ef5a9f82fc8097d559b863b401bfdb4069 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.mli
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.mli
@@ -70,11 +70,11 @@ type ('ta, 'tb) eq = Eq : ('same, 'same) eq
 type ex_comparable_ty =
   | Ex_comparable_ty : 'a Script_typed_ir.comparable_ty -> ex_comparable_ty
 
-type ex_ty = Ex_ty : 'a Script_typed_ir.ty -> ex_ty
+type ex_ty = Ex_ty : ('a, _) Script_typed_ir.ty -> ex_ty
 
 type ex_parameter_ty_and_entrypoints =
   | Ex_parameter_ty_and_entrypoints : {
-      arg_type : 'a Script_typed_ir.ty;
+      arg_type : ('a, _) Script_typed_ir.ty;
       entrypoints : 'a Script_typed_ir.entrypoints;
     }
       -> ex_parameter_ty_and_entrypoints
@@ -90,9 +90,9 @@ type ex_script =
             'storage )
           Script_typed_ir.pair )
         Script_typed_ir.lambda;
-      arg_type : 'arg Script_typed_ir.ty;
+      arg_type : ('arg, _) Script_typed_ir.ty;
       storage : 'storage;
-      storage_type : 'storage Script_typed_ir.ty;
+      storage_type : ('storage, _) Script_typed_ir.ty;
       views : Script_typed_ir.view_map;
       entrypoints : 'arg Script_typed_ir.entrypoints;
       code_size : Cache_memory_helpers.sint;
@@ -114,8 +114,8 @@ type ('arg, 'storage) code =
             'storage )
           Script_typed_ir.pair )
         Script_typed_ir.lambda;
-      arg_type : 'arg Script_typed_ir.ty;
-      storage_type : 'storage Script_typed_ir.ty;
+      arg_type : ('arg, _) Script_typed_ir.ty;
+      storage_type : ('storage, _) Script_typed_ir.ty;
       views : Script_typed_ir.view_map;
       entrypoints : 'arg Script_typed_ir.entrypoints;
       code_size : Cache_memory_helpers.sint;
@@ -181,7 +181,7 @@ type type_logger =
 (** Create an empty big_map *)
 val empty_big_map :
   'a Script_typed_ir.comparable_ty ->
-  'b Script_typed_ir.ty ->
+  ('b, _) Script_typed_ir.ty ->
   ('a, 'b) Script_typed_ir.big_map
 
 val big_map_mem :
@@ -219,9 +219,11 @@ val big_map_get_and_update :
 val ty_eq :
   error_details:'error_trace error_details ->
   Script.location ->
-  'a Script_typed_ir.ty ->
-  'b Script_typed_ir.ty ->
-  (('a Script_typed_ir.ty, 'b Script_typed_ir.ty) eq, 'error_trace) Gas_monad.t
+  ('a, 'ac) Script_typed_ir.ty ->
+  ('b, 'bc) Script_typed_ir.ty ->
+  ( (('a, 'ac) Script_typed_ir.ty, ('b, 'bc) Script_typed_ir.ty) eq,
+    'error_trace )
+  Gas_monad.t
 
 (** {3 Parsing and Typechecking Michelson} *)
 val parse_comparable_data :
@@ -236,14 +238,14 @@ val parse_data :
   context ->
   legacy:bool ->
   allow_forged:bool ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   Script.node ->
   ('a * context) tzresult Lwt.t
 
 val unparse_data :
   context ->
   unparsing_mode ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   'a ->
   (Script.node * context) tzresult Lwt.t
 
@@ -310,7 +312,7 @@ val parse_view_returning :
   ?type_logger:type_logger ->
   context ->
   legacy:bool ->
-  'storage Script_typed_ir.ty ->
+  ('storage, _) Script_typed_ir.ty ->
   Script_typed_ir.view ->
   ('storage ex_view * context) tzresult Lwt.t
 
@@ -318,7 +320,7 @@ val typecheck_views :
   ?type_logger:type_logger ->
   context ->
   legacy:bool ->
-  'storage Script_typed_ir.ty ->
+  ('storage, _) Script_typed_ir.ty ->
   Script_typed_ir.view_map ->
   context tzresult Lwt.t
 
@@ -344,7 +346,7 @@ val parse_ty :
 val unparse_ty :
   loc:'loc ->
   context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   ('loc Script.michelson_node * context) tzresult
 
 val unparse_comparable_ty :
@@ -354,7 +356,8 @@ val unparse_comparable_ty :
   ('loc Script.michelson_node * context) tzresult
 
 val ty_of_comparable_ty :
-  'a Script_typed_ir.comparable_ty -> 'a Script_typed_ir.ty
+  'a Script_typed_ir.comparable_ty ->
+  ('a, Dependent_bool.yes) Script_typed_ir.ty
 
 val parse_toplevel :
   context -> legacy:bool -> Script.expr -> (toplevel * context) tzresult Lwt.t
@@ -362,7 +365,7 @@ val parse_toplevel :
 val unparse_parameter_ty :
   loc:'loc ->
   context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   entrypoints:'a Script_typed_ir.entrypoints ->
   ('loc Script.michelson_node * context) tzresult
 
@@ -378,7 +381,7 @@ val typecheck_code :
   Script.expr ->
   (type_map * context) tzresult Lwt.t
 
-val serialize_ty_for_error : 'a Script_typed_ir.ty -> Script.expr
+val serialize_ty_for_error : ('a, _) Script_typed_ir.ty -> Script.expr
 
 val parse_code :
   ?type_logger:type_logger ->
@@ -392,7 +395,7 @@ val parse_storage :
   context ->
   legacy:bool ->
   allow_forged:bool ->
-  'storage Script_typed_ir.ty ->
+  ('storage, _) Script_typed_ir.ty ->
   storage:Script.lazy_expr ->
   ('storage * context) tzresult Lwt.t
 
@@ -412,7 +415,7 @@ val unparse_script :
 val parse_contract :
   context ->
   Script.location ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   Destination.t ->
   entrypoint:Entrypoint.t ->
   (context * 'a Script_typed_ir.typed_contract) tzresult Lwt.t
@@ -420,7 +423,7 @@ val parse_contract :
 val parse_contract_for_script :
   context ->
   Script.location ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   Destination.t ->
   entrypoint:Entrypoint.t ->
   (context * 'a Script_typed_ir.typed_contract option) tzresult Lwt.t
@@ -436,18 +439,18 @@ val parse_tx_rollup_deposit_parameters :
     existential. Typically, it will be used to go from the type of an
     entry-point to the full type of a contract. *)
 type 'a ex_ty_cstr =
-  | Ex_ty_cstr : 'b Script_typed_ir.ty * ('b -> 'a) -> 'a ex_ty_cstr
+  | Ex_ty_cstr : ('b, _) Script_typed_ir.ty * ('b -> 'a) -> 'a ex_ty_cstr
 
 val find_entrypoint :
   error_details:'error_trace error_details ->
-  't Script_typed_ir.ty ->
+  ('t, _) Script_typed_ir.ty ->
   't Script_typed_ir.entrypoints ->
   Entrypoint.t ->
   ('t ex_ty_cstr, 'error_trace) Gas_monad.t
 
 val list_entrypoints :
   context ->
-  't Script_typed_ir.ty ->
+  ('t, _) Script_typed_ir.ty ->
   't Script_typed_ir.entrypoints ->
   (Michelson_v1_primitives.prim list list
   * (Michelson_v1_primitives.prim list * Script.unlocated_michelson_node)
@@ -455,7 +458,10 @@ val list_entrypoints :
   tzresult
 
 val pack_data :
-  context -> 'a Script_typed_ir.ty -> 'a -> (bytes * context) tzresult Lwt.t
+  context ->
+  ('a, _) Script_typed_ir.ty ->
+  'a ->
+  (bytes * context) tzresult Lwt.t
 
 val hash_comparable_data :
   context ->
@@ -465,7 +471,7 @@ val hash_comparable_data :
 
 val hash_data :
   context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   'a ->
   (Script_expr_hash.t * context) tzresult Lwt.t
 
@@ -478,7 +484,7 @@ val no_lazy_storage_id : lazy_storage_ids
  *)
 val collect_lazy_storage :
   context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   'a ->
   (lazy_storage_ids * context) tzresult
 
@@ -505,14 +511,14 @@ val extract_lazy_storage_diff :
   temporary:bool ->
   to_duplicate:lazy_storage_ids ->
   to_update:lazy_storage_ids ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   'a ->
   ('a * Lazy_storage.diffs option * context) tzresult Lwt.t
 
 (* return [None] if none or more than one found *)
 val get_single_sapling_state :
   context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   'a ->
   (Sapling.Id.t option * context) tzresult
 
diff --git a/src/proto_alpha/lib_protocol/script_tc_context.ml b/src/proto_alpha/lib_protocol/script_tc_context.ml
index 2aab85e620b9aa724e789d496b830e464d8b6d58..d0b4609e3bb3355797c651394155c355e9b04966 100644
--- a/src/proto_alpha/lib_protocol/script_tc_context.ml
+++ b/src/proto_alpha/lib_protocol/script_tc_context.ml
@@ -29,8 +29,8 @@ type in_lambda = bool
 
 type callsite =
   | Toplevel : {
-      storage_type : 'sto ty;
-      param_type : 'param ty;
+      storage_type : ('sto, _) ty;
+      param_type : ('param, _) ty;
       entrypoints : 'param Script_typed_ir.entrypoints;
     }
       -> callsite
diff --git a/src/proto_alpha/lib_protocol/script_tc_context.mli b/src/proto_alpha/lib_protocol/script_tc_context.mli
index 4f4255a17176836395bd277b9a15fa365d96ab97..14f907133eddabb0102e571c5923d209d6f2e1b4 100644
--- a/src/proto_alpha/lib_protocol/script_tc_context.mli
+++ b/src/proto_alpha/lib_protocol/script_tc_context.mli
@@ -48,8 +48,8 @@ type in_lambda = bool
     instructions for example). *)
 type callsite =
   | Toplevel : {
-      storage_type : 'sto ty;
-      param_type : 'param ty;
+      storage_type : ('sto, _) ty;
+      param_type : ('param, _) ty;
       entrypoints : 'param Script_typed_ir.entrypoints;
     }
       -> callsite
@@ -61,8 +61,8 @@ type t = {callsite : callsite; in_lambda : in_lambda}
 val init : callsite -> t
 
 val toplevel :
-  storage_type:'sto ty ->
-  param_type:'param ty ->
+  storage_type:('sto, _) ty ->
+  param_type:('param, _) ty ->
   entrypoints:'param Script_typed_ir.entrypoints ->
   t
 
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index ed6a521f498abec5142ff081cb002d10d73c8dc8..8734cd25e5dc8018aedbfc1f907948ff51e37b98 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -27,6 +27,7 @@
 
 open Alpha_context
 open Script_int
+open Dependent_bool
 
 (*
 
@@ -220,7 +221,7 @@ type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num}
 
 module type TYPE_SIZE = sig
   (* A type size represents the size of its type parameter.
-     This constraint is enforced inside this module (Script_type_ir), hence there
+     This constraint is enforced inside this module (Script_typed_ir), hence there
      should be no way to construct a type size outside of it.
 
      It allows keeping type metadata and types non-private.
@@ -328,13 +329,19 @@ type _ comparable_ty =
   | Address_key : address comparable_ty
   | Tx_rollup_l2_address_key : tx_rollup_l2_address comparable_ty
   | Pair_key :
-      'a comparable_ty * 'b comparable_ty * ('a, 'b) pair ty_metadata
+      'a comparable_ty
+      * 'b comparable_ty
+      * ('a, 'b) pair ty_metadata
+      * (yes, yes, yes) dand
       -> ('a, 'b) pair comparable_ty
   | Union_key :
-      'a comparable_ty * 'b comparable_ty * ('a, 'b) union ty_metadata
+      'a comparable_ty
+      * 'b comparable_ty
+      * ('a, 'b) union ty_metadata
+      * (yes, yes, yes) dand
       -> ('a, 'b) union comparable_ty
   | Option_key :
-      'v comparable_ty * 'v option ty_metadata
+      'v comparable_ty * 'v option ty_metadata * yes dbool
       -> 'v option comparable_ty
 
 (*
@@ -627,7 +634,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
   | IEmpty_big_map :
       ('a, 's) kinfo
       * 'b comparable_ty
-      * 'c ty
+      * ('c, _) ty
       * (('b, 'c) big_map, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IBig_map_mem :
@@ -837,7 +844,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a, ('a, 'b) lambda * 's, 'r, 'f) kinstr
   | IApply :
       ('a, ('a * 'b, 'c) lambda * 's) kinfo
-      * 'a ty
+      * ('a, _) ty
       * (('b, 'c) lambda, 's, 'r, 'f) kinstr
       -> ('a, ('a * 'b, 'c) lambda * 's, 'r, 'f) kinstr
   | ILambda :
@@ -846,7 +853,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       * (('b, 'c) lambda, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IFailwith :
-      ('a, 's) kinfo * Script.location * 'a ty
+      ('a, 's) kinfo * Script.location * ('a, _) ty
       -> ('a, 's, 'r, 'f) kinstr
   (*
      Comparison
@@ -886,7 +893,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a typed_contract, 's, 'r, 'f) kinstr
   | IContract :
       (address, 's) kinfo
-      * 'a ty
+      * ('a, _) ty
       * Entrypoint.t
       * ('a typed_contract option, 's, 'r, 'f) kinstr
       -> (address, 's, 'r, 'f) kinstr
@@ -904,8 +911,8 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> (public_key_hash, 's, 'r, 'f) kinstr
   | ICreate_contract : {
       kinfo : (public_key_hash option, Tez.t * ('a * 's)) kinfo;
-      storage_type : 'a ty;
-      arg_type : 'b ty;
+      storage_type : ('a, _) ty;
+      arg_type : ('b, _) ty;
       lambda : ('b * 'a, operation boxed_list * 'a) lambda;
       views : view_map;
       entrypoints : 'b entrypoints;
@@ -934,10 +941,10 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       (public_key, 's) kinfo * (public_key_hash, 's, 'r, 'f) kinstr
       -> (public_key, 's, 'r, 'f) kinstr
   | IPack :
-      ('a, 's) kinfo * 'a ty * (bytes, 's, 'r, 'f) kinstr
+      ('a, 's) kinfo * ('a, _) ty * (bytes, 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IUnpack :
-      (bytes, 's) kinfo * 'a ty * ('a option, 's, 'r, 'f) kinstr
+      (bytes, 's) kinfo * ('a, _) ty * ('a option, 's, 'r, 'f) kinstr
       -> (bytes, 's, 'r, 'f) kinstr
   | IBlake2b :
       (bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
@@ -956,7 +963,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a, 's, 'r, 'f) kinstr
   | ISelf :
       ('a, 's) kinfo
-      * 'b ty
+      * ('b, _) ty
       * Entrypoint.t
       * ('b typed_contract, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
@@ -1143,7 +1150,7 @@ and ('arg, 'ret) lambda =
 
 and 'arg typed_contract =
   | Typed_contract : {
-      arg_ty : 'arg ty;
+      arg_ty : ('arg, _) ty;
       address : address;
     }
       -> 'arg typed_contract
@@ -1223,61 +1230,69 @@ and logger = {
   get_log : unit -> execution_trace option tzresult Lwt.t;
 }
 
-and to_be_replaced = unit
-
 (* ---- Auxiliary types -----------------------------------------------------*)
-and 'ty ty =
-  | Unit_t : unit ty
-  | Int_t : z num ty
-  | Nat_t : n num ty
-  | Signature_t : signature ty
-  | String_t : Script_string.t ty
-  | Bytes_t : bytes ty
-  | Mutez_t : Tez.t ty
-  | Key_hash_t : public_key_hash ty
-  | Key_t : public_key ty
-  | Timestamp_t : Script_timestamp.t ty
-  | Address_t : address ty
-  | Tx_rollup_l2_address_t : tx_rollup_l2_address ty
-  | Bool_t : bool ty
+and ('ty, 'comparable) ty =
+  | Unit_t : (unit, yes) ty
+  | Int_t : (z num, yes) ty
+  | Nat_t : (n num, yes) ty
+  | Signature_t : (signature, yes) ty
+  | String_t : (Script_string.t, yes) ty
+  | Bytes_t : (bytes, yes) ty
+  | Mutez_t : (Tez.t, yes) ty
+  | Key_hash_t : (public_key_hash, yes) ty
+  | Key_t : (public_key, yes) ty
+  | Timestamp_t : (Script_timestamp.t, yes) ty
+  | Address_t : (address, yes) ty
+  | Tx_rollup_l2_address_t : (tx_rollup_l2_address, yes) ty
+  | Bool_t : (bool, yes) ty
   | Pair_t :
-      'a ty * 'b ty * ('a, 'b) pair ty_metadata * to_be_replaced
-      -> ('a, 'b) pair ty
+      ('a, 'ac) ty
+      * ('b, 'bc) ty
+      * ('a, 'b) pair ty_metadata
+      * ('ac, 'bc, 'rc) dand
+      -> (('a, 'b) pair, 'rc) ty
   | Union_t :
-      'a ty * 'b ty * ('a, 'b) union ty_metadata * to_be_replaced
-      -> ('a, 'b) union ty
+      ('a, 'ac) ty
+      * ('b, 'bc) ty
+      * ('a, 'b) union ty_metadata
+      * ('ac, 'bc, 'rc) dand
+      -> (('a, 'b) union, 'rc) ty
   | Lambda_t :
-      'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata
-      -> ('arg, 'ret) lambda ty
-  | Option_t : 'v ty * 'v option ty_metadata * to_be_replaced -> 'v option ty
-  | List_t : 'v ty * 'v boxed_list ty_metadata -> 'v boxed_list ty
-  | Set_t : 'v comparable_ty * 'v set ty_metadata -> 'v set ty
+      ('arg, _) ty * ('ret, _) ty * ('arg, 'ret) lambda ty_metadata
+      -> (('arg, 'ret) lambda, no) ty
+  | Option_t :
+      ('v, 'c) ty * 'v option ty_metadata * 'c dbool
+      -> ('v option, 'c) ty
+  | List_t : ('v, _) ty * 'v boxed_list ty_metadata -> ('v boxed_list, no) ty
+  | Set_t : 'v comparable_ty * 'v set ty_metadata -> ('v set, no) ty
   | Map_t :
-      'k comparable_ty * 'v ty * ('k, 'v) map ty_metadata
-      -> ('k, 'v) map ty
+      'k comparable_ty * ('v, _) ty * ('k, 'v) map ty_metadata
+      -> (('k, 'v) map, no) ty
   | Big_map_t :
-      'k comparable_ty * 'v ty * ('k, 'v) big_map ty_metadata
-      -> ('k, 'v) big_map ty
+      'k comparable_ty * ('v, _) ty * ('k, 'v) big_map ty_metadata
+      -> (('k, 'v) big_map, no) ty
   | Contract_t :
-      'arg ty * 'arg typed_contract ty_metadata
-      -> 'arg typed_contract ty
-  | Sapling_transaction_t : Sapling.Memo_size.t -> Sapling.transaction ty
+      ('arg, _) ty * 'arg typed_contract ty_metadata
+      -> ('arg typed_contract, no) ty
+  | Sapling_transaction_t : Sapling.Memo_size.t -> (Sapling.transaction, no) ty
   | Sapling_transaction_deprecated_t :
       Sapling.Memo_size.t
-      -> Sapling.Legacy.transaction ty
-  | Sapling_state_t : Sapling.Memo_size.t -> Sapling.state ty
-  | Operation_t : operation ty
-  | Chain_id_t : Script_chain_id.t ty
-  | Never_t : never ty
-  | Bls12_381_g1_t : Script_bls.G1.t ty
-  | Bls12_381_g2_t : Script_bls.G2.t ty
-  | Bls12_381_fr_t : Script_bls.Fr.t ty
-  | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty
-  | Chest_key_t : Script_timelock.chest_key ty
-  | Chest_t : Script_timelock.chest ty
+      -> (Sapling.Legacy.transaction, no) ty
+  | Sapling_state_t : Sapling.Memo_size.t -> (Sapling.state, no) ty
+  | Operation_t : (operation, no) ty
+  | Chain_id_t : (Script_chain_id.t, yes) ty
+  | Never_t : (never, yes) ty
+  | Bls12_381_g1_t : (Script_bls.G1.t, no) ty
+  | Bls12_381_g2_t : (Script_bls.G2.t, no) ty
+  | Bls12_381_fr_t : (Script_bls.Fr.t, no) ty
+  | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> ('a ticket, no) ty
+  | Chest_key_t : (Script_timelock.chest_key, no) ty
+  | Chest_t : (Script_timelock.chest, no) ty
 
 and ('top_ty, 'resty) stack_ty =
-  | Item_t : 'ty ty * ('ty2, 'rest) stack_ty -> ('ty, 'ty2 * 'rest) stack_ty
+  | Item_t :
+      ('ty, _) ty * ('ty2, 'rest) stack_ty
+      -> ('ty, 'ty2 * 'rest) stack_ty
   | Bot_t : (empty_cell, empty_cell) stack_ty
 
 and ('key, 'value) big_map =
@@ -1285,7 +1300,7 @@ and ('key, 'value) big_map =
       id : Big_map.Id.t option;
       diff : ('key, 'value) big_map_overlay;
       key_type : 'key comparable_ty;
-      value_type : 'value ty;
+      value_type : ('value, _) ty;
     }
       -> ('key, 'value) big_map
 
@@ -1349,8 +1364,8 @@ and (_, _) dup_n_gadt_witness =
 and ('input, 'output) view_signature =
   | View_signature : {
       name : Script_string.t;
-      input_ty : 'input ty;
-      output_ty : 'output ty;
+      input_ty : ('input, _) ty;
+      output_ty : ('output, _) ty;
     }
       -> ('input, 'output) view_signature
 
@@ -1358,7 +1373,7 @@ and 'kind manager_operation =
   | Transaction : {
       transaction : Alpha_context.transaction;
       location : Script.location;
-      parameters_ty : 'a ty;
+      parameters_ty : ('a, _) ty;
       parameters : 'a;
     }
       -> Kind.transaction manager_operation
@@ -1766,7 +1781,7 @@ let kinstr_rewritek :
 
 let meta_basic = {size = Type_size.one}
 
-let ty_metadata : type a. a ty -> a ty_metadata = function
+let ty_metadata : type a ac. (a, ac) ty -> a ty_metadata = function
   | Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t
   | Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
   | Tx_rollup_l2_address_t ->
@@ -1791,15 +1806,52 @@ let comparable_ty_metadata : type a. a comparable_ty -> a ty_metadata = function
   | Bytes_key | Mutez_key | Bool_key | Key_hash_key | Key_key | Timestamp_key
   | Chain_id_key | Address_key | Tx_rollup_l2_address_key ->
       meta_basic
-  | Pair_key (_, _, meta) -> meta
-  | Union_key (_, _, meta) -> meta
-  | Option_key (_, meta) -> meta
+  | Pair_key (_, _, meta, YesYes) -> meta
+  | Union_key (_, _, meta, YesYes) -> meta
+  | Option_key (_, meta, Yes) -> meta
 
-let ty_size t = (ty_metadata t).size
+let ty_size : type v vc. (v, vc) ty -> v Type_size.t =
+ fun t -> (ty_metadata t).size
 
 let comparable_ty_size t = (comparable_ty_metadata t).size
 
-type 'v ty_ex_c = Ty_ex_c : 'v ty -> 'v ty_ex_c [@@ocaml.unboxed]
+let is_comparable : type v c. (v, c) ty -> c dbool = function
+  | Never_t -> Yes
+  | Unit_t -> Yes
+  | Int_t -> Yes
+  | Nat_t -> Yes
+  | Signature_t -> Yes
+  | String_t -> Yes
+  | Bytes_t -> Yes
+  | Mutez_t -> Yes
+  | Bool_t -> Yes
+  | Key_hash_t -> Yes
+  | Key_t -> Yes
+  | Timestamp_t -> Yes
+  | Chain_id_t -> Yes
+  | Address_t -> Yes
+  | Tx_rollup_l2_address_t -> Yes
+  | Pair_t (_, _, _, dand) -> dbool_of_dand dand
+  | Union_t (_, _, _, dand) -> dbool_of_dand dand
+  | Option_t (_, _, cmp) -> cmp
+  | Lambda_t _ -> No
+  | List_t _ -> No
+  | Set_t _ -> No
+  | Map_t _ -> No
+  | Big_map_t _ -> No
+  | Ticket_t _ -> No
+  | Contract_t _ -> No
+  | Sapling_transaction_t _ -> No
+  | Sapling_transaction_deprecated_t _ -> No
+  | Sapling_state_t _ -> No
+  | Operation_t -> No
+  | Bls12_381_g1_t -> No
+  | Bls12_381_g2_t -> No
+  | Bls12_381_fr_t -> No
+  | Chest_t -> No
+  | Chest_key_t -> No
+
+type 'v ty_ex_c = Ty_ex_c : ('v, _) ty -> 'v ty_ex_c [@@ocaml.unboxed]
 
 let unit_t = Unit_t
 
@@ -1853,68 +1905,89 @@ let tx_rollup_l2_address_t = Tx_rollup_l2_address_t
 
 let tx_rollup_l2_address_key = Tx_rollup_l2_address_key
 
-let pair_t loc l r =
+let pair_t :
+    type a ac b bc.
+    Script.location -> (a, ac) ty -> (b, bc) ty -> (a, b) pair ty_ex_c tzresult
+    =
+ fun loc l r ->
   Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size ->
-  Ty_ex_c (Pair_t (l, r, {size}, ()))
+  let (Ex_dand cmp) = dand (is_comparable l) (is_comparable r) in
+  Ty_ex_c (Pair_t (l, r, {size}, cmp))
+
+let comparable_pair_t loc l r =
+  Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size ->
+  Pair_t (l, r, {size}, YesYes)
 
 let pair_key loc l r =
   Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r)
-  >|? fun size -> Pair_key (l, r, {size})
+  >|? fun size -> Pair_key (l, r, {size}, YesYes)
 
 let pair_3_key loc l m r = pair_key loc m r >>? fun r -> pair_key loc l r
 
-let union_t loc l r =
+let union_t :
+    type a ac b bc.
+    Script.location -> (a, ac) ty -> (b, bc) ty -> (a, b) union ty_ex_c tzresult
+    =
+ fun loc l r ->
+  Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size ->
+  let (Ex_dand cmp) = dand (is_comparable l) (is_comparable r) in
+  Ty_ex_c (Union_t (l, r, {size}, cmp))
+
+let comparable_union_t loc l r =
   Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size ->
-  Ty_ex_c (Union_t (l, r, {size}, ()))
+  Union_t (l, r, {size}, YesYes)
 
-let union_bytes_bool_t = Union_t (bytes_t, bool_t, {size = Type_size.three}, ())
+let union_bytes_bool_t =
+  Union_t (bytes_t, bool_t, {size = Type_size.three}, YesYes)
 
 let union_key loc l r =
   Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r)
-  >|? fun size -> Union_key (l, r, {size})
+  >|? fun size -> Union_key (l, r, {size}, YesYes)
 
 let lambda_t loc l r =
   Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size ->
   Lambda_t (l, r, {size})
 
 let option_t loc t =
-  Type_size.compound1 loc (ty_size t) >|? fun size -> Option_t (t, {size}, ())
+  Type_size.compound1 loc (ty_size t) >|? fun size ->
+  let cmp = is_comparable t in
+  Option_t (t, {size}, cmp)
 
-let option_mutez_t = Option_t (mutez_t, {size = Type_size.two}, ())
+let option_mutez_t = Option_t (mutez_t, {size = Type_size.two}, Yes)
 
-let option_string_t = Option_t (string_t, {size = Type_size.two}, ())
+let option_string_t = Option_t (string_t, {size = Type_size.two}, Yes)
 
-let option_bytes_t = Option_t (bytes_t, {size = Type_size.two}, ())
+let option_bytes_t = Option_t (bytes_t, {size = Type_size.two}, Yes)
 
-let option_nat_t = Option_t (nat_t, {size = Type_size.two}, ())
+let option_nat_t = Option_t (nat_t, {size = Type_size.two}, Yes)
 
 let option_pair_nat_nat_t =
   Option_t
-    ( Pair_t (nat_t, nat_t, {size = Type_size.three}, ()),
+    ( Pair_t (nat_t, nat_t, {size = Type_size.three}, YesYes),
       {size = Type_size.four},
-      () )
+      Yes )
 
 let option_pair_nat_mutez_t =
   Option_t
-    ( Pair_t (nat_t, mutez_t, {size = Type_size.three}, ()),
+    ( Pair_t (nat_t, mutez_t, {size = Type_size.three}, YesYes),
       {size = Type_size.four},
-      () )
+      Yes )
 
 let option_pair_mutez_mutez_t =
   Option_t
-    ( Pair_t (mutez_t, mutez_t, {size = Type_size.three}, ()),
+    ( Pair_t (mutez_t, mutez_t, {size = Type_size.three}, YesYes),
       {size = Type_size.four},
-      () )
+      Yes )
 
 let option_pair_int_nat_t =
   Option_t
-    ( Pair_t (int_t, nat_t, {size = Type_size.three}, ()),
+    ( Pair_t (int_t, nat_t, {size = Type_size.three}, YesYes),
       {size = Type_size.four},
-      () )
+      Yes )
 
 let option_key loc t =
   Type_size.compound1 loc (comparable_ty_size t) >|? fun size ->
-  Option_key (t, {size})
+  Option_key (t, {size}, Yes)
 
 let list_t loc t =
   Type_size.compound1 loc (ty_size t) >|? fun size -> List_t (t, {size})
@@ -2159,7 +2232,7 @@ let kinstr_traverse i init f =
   aux init i (fun accu -> accu)
 
 type 'a ty_traverse = {
-  apply : 't. 'a -> 't ty -> 'a;
+  apply : 't 'tc. 'a -> ('t, 'tc) ty -> 'a;
   apply_comparable : 't. 'a -> 't comparable_ty -> 'a;
 }
 
@@ -2184,15 +2257,15 @@ let (ty_traverse, comparable_ty_traverse) =
     | Mutez_key | Key_hash_key | Key_key | Timestamp_key | Address_key
     | Tx_rollup_l2_address_key | Bool_key | Chain_id_key | Never_key ->
         (return [@ocaml.tailcall]) ()
-    | Pair_key (ty1, ty2, _) -> (next2 [@ocaml.tailcall]) ty1 ty2
-    | Union_key (ty1, ty2, _) -> (next2 [@ocaml.tailcall]) ty1 ty2
-    | Option_key (ty, _) -> (next [@ocaml.tailcall]) ty
+    | Pair_key (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2
+    | Union_key (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2
+    | Option_key (ty, _, Yes) -> (next [@ocaml.tailcall]) ty
   and aux' :
-      type ret t accu. accu ty_traverse -> accu -> t ty -> (accu -> ret) -> ret
-      =
+      type ret t tc accu.
+      accu ty_traverse -> accu -> (t, tc) ty -> (accu -> ret) -> ret =
    fun f accu ty continue ->
     let accu = f.apply accu ty in
-    match (ty : t ty) with
+    match (ty : (t, tc) ty) with
     | Unit_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t | Mutez_t
     | Key_hash_t | Key_t | Timestamp_t | Address_t | Tx_rollup_l2_address_t
     | Bool_t | Sapling_transaction_t _ | Sapling_transaction_deprecated_t _
@@ -2218,15 +2291,20 @@ let (ty_traverse, comparable_ty_traverse) =
         (next' [@ocaml.tailcall]) f accu ty1 continue
     | Contract_t (ty1, _) -> (next' [@ocaml.tailcall]) f accu ty1 continue
   and next2' :
-      type a b ret accu.
-      accu ty_traverse -> accu -> a ty -> b ty -> (accu -> ret) -> ret =
+      type a ac b bc ret accu.
+      accu ty_traverse ->
+      accu ->
+      (a, ac) ty ->
+      (b, bc) ty ->
+      (accu -> ret) ->
+      ret =
    fun f accu ty1 ty2 continue ->
     (aux' [@ocaml.tailcall]) f accu ty1 @@ fun accu ->
     (aux' [@ocaml.tailcall]) f accu ty2 @@ fun accu ->
     (continue [@ocaml.tailcall]) accu
   and next' :
-      type a ret accu. accu ty_traverse -> accu -> a ty -> (accu -> ret) -> ret
-      =
+      type a ac ret accu.
+      accu ty_traverse -> accu -> (a, ac) ty -> (accu -> ret) -> ret =
    fun f accu ty1 continue ->
     (aux' [@ocaml.tailcall]) f accu ty1 @@ fun accu ->
     (continue [@ocaml.tailcall]) accu
@@ -2248,13 +2326,14 @@ let stack_ty_traverse (type a t) (sty : (a, t) stack_ty) init f =
   aux init sty
 
 type 'a value_traverse = {
-  apply : 't. 'a -> 't ty -> 't -> 'a;
+  apply : 't 'tc. 'a -> ('t, 'tc) ty -> 't -> 'a;
   apply_comparable : 't. 'a -> 't comparable_ty -> 't -> 'a;
 }
 
-let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f
-    =
-  let rec aux : type ret t. 'accu -> t ty -> t -> ('accu -> ret) -> ret =
+let value_traverse (type t tc) (ty : ((t, tc) ty, t comparable_ty) union)
+    (x : t) init f =
+  let rec aux : type ret t tc. 'accu -> (t, tc) ty -> t -> ('accu -> ret) -> ret
+      =
    fun accu ty x continue ->
     let accu = f.apply accu ty x in
     let next2 ty1 ty2 x1 x2 =
@@ -2315,9 +2394,13 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f
         (aux' [@ocaml.tailcall]) accu ty' x @@ fun accu ->
         (on_list' [@ocaml.tailcall]) accu ty' xs continue
   and on_bindings :
-      type ret k v.
-      'accu -> k comparable_ty -> v ty -> ('accu -> ret) -> (k * v) list -> ret
-      =
+      type ret k v vc.
+      'accu ->
+      k comparable_ty ->
+      (v, vc) ty ->
+      ('accu -> ret) ->
+      (k * v) list ->
+      ret =
    fun accu kty ty' continue xs ->
     match xs with
     | [] -> (continue [@ocaml.tailcall]) accu
@@ -2344,13 +2427,13 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f
     | Mutez_key | Key_hash_key | Key_key | Timestamp_key | Address_key
     | Tx_rollup_l2_address_key | Bool_key | Chain_id_key | Never_key ->
         (return [@ocaml.tailcall]) ()
-    | Pair_key (ty1, ty2, _) ->
+    | Pair_key (ty1, ty2, _, YesYes) ->
         (next2 [@ocaml.tailcall]) ty1 ty2 (fst x) (snd x)
-    | Union_key (ty1, ty2, _) -> (
+    | Union_key (ty1, ty2, _, YesYes) -> (
         match x with
         | L l -> (next [@ocaml.tailcall]) ty1 l
         | R r -> (next [@ocaml.tailcall]) ty2 r)
-    | Option_key (ty, _) -> (
+    | Option_key (ty, _, Yes) -> (
         match x with
         | None -> (return [@ocaml.tailcall]) ()
         | Some v -> (next [@ocaml.tailcall]) ty v)
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index b6ee0aca6e268ce12be51447cc34f34a77d54e6b..102d0a36b48e687deb238550749458f52fd16cc4 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -27,6 +27,7 @@
 
 open Alpha_context
 open Script_int
+open Dependent_bool
 
 type step_constants = {
   source : Contract.t;
@@ -203,13 +204,19 @@ type _ comparable_ty =
   | Address_key : address comparable_ty
   | Tx_rollup_l2_address_key : tx_rollup_l2_address comparable_ty
   | Pair_key :
-      'a comparable_ty * 'b comparable_ty * ('a, 'b) pair ty_metadata
+      'a comparable_ty
+      * 'b comparable_ty
+      * ('a, 'b) pair ty_metadata
+      * (yes, yes, yes) dand
       -> ('a, 'b) pair comparable_ty
   | Union_key :
-      'a comparable_ty * 'b comparable_ty * ('a, 'b) union ty_metadata
+      'a comparable_ty
+      * 'b comparable_ty
+      * ('a, 'b) union ty_metadata
+      * (yes, yes, yes) dand
       -> ('a, 'b) union comparable_ty
   | Option_key :
-      'v comparable_ty * 'v option ty_metadata
+      'v comparable_ty * 'v option ty_metadata * yes dbool
       -> 'v option comparable_ty
 
 module type Boxed_set_OPS = sig
@@ -594,7 +601,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
   | IEmpty_big_map :
       ('a, 's) kinfo
       * 'b comparable_ty
-      * 'c ty
+      * ('c, _) ty
       * (('b, 'c) big_map, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IBig_map_mem :
@@ -800,7 +807,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a, ('a, 'b) lambda * 's, 'r, 'f) kinstr
   | IApply :
       ('a, ('a * 'b, 'c) lambda * 's) kinfo
-      * 'a ty
+      * ('a, _) ty
       * (('b, 'c) lambda, 's, 'r, 'f) kinstr
       -> ('a, ('a * 'b, 'c) lambda * 's, 'r, 'f) kinstr
   | ILambda :
@@ -809,7 +816,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       * (('b, 'c) lambda, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IFailwith :
-      ('a, 's) kinfo * Script.location * 'a ty
+      ('a, 's) kinfo * Script.location * ('a, _) ty
       -> ('a, 's, 'r, 'f) kinstr
   (*
      Comparison
@@ -849,7 +856,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a typed_contract, 's, 'r, 'f) kinstr
   | IContract :
       (address, 's) kinfo
-      * 'a ty
+      * ('a, _) ty
       * Entrypoint.t
       * ('a typed_contract option, 's, 'r, 'f) kinstr
       -> (address, 's, 'r, 'f) kinstr
@@ -867,8 +874,8 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> (public_key_hash, 's, 'r, 'f) kinstr
   | ICreate_contract : {
       kinfo : (public_key_hash option, Tez.t * ('a * 's)) kinfo;
-      storage_type : 'a ty;
-      arg_type : 'b ty;
+      storage_type : ('a, _) ty;
+      arg_type : ('b, _) ty;
       lambda : ('b * 'a, operation boxed_list * 'a) lambda;
       views : view_map;
       entrypoints : 'b entrypoints;
@@ -897,10 +904,10 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       (public_key, 's) kinfo * (public_key_hash, 's, 'r, 'f) kinstr
       -> (public_key, 's, 'r, 'f) kinstr
   | IPack :
-      ('a, 's) kinfo * 'a ty * (bytes, 's, 'r, 'f) kinstr
+      ('a, 's) kinfo * ('a, _) ty * (bytes, 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
   | IUnpack :
-      (bytes, 's) kinfo * 'a ty * ('a option, 's, 'r, 'f) kinstr
+      (bytes, 's) kinfo * ('a, _) ty * ('a option, 's, 'r, 'f) kinstr
       -> (bytes, 's, 'r, 'f) kinstr
   | IBlake2b :
       (bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr
@@ -919,7 +926,7 @@ type ('before_top, 'before, 'result_top, 'result) kinstr =
       -> ('a, 's, 'r, 'f) kinstr
   | ISelf :
       ('a, 's) kinfo
-      * 'b ty
+      * ('b, _) ty
       * Entrypoint.t
       * ('b typed_contract, 'a * 's, 'r, 'f) kinstr
       -> ('a, 's, 'r, 'f) kinstr
@@ -1151,7 +1158,7 @@ and ('arg, 'ret) lambda =
 
 and 'arg typed_contract =
   | Typed_contract : {
-      arg_ty : 'arg ty;
+      arg_ty : ('arg, _) ty;
       address : address;
     }
       -> 'arg typed_contract
@@ -1327,61 +1334,69 @@ and logger = {
           produced. *)
 }
 
-and to_be_replaced = unit
-
 (* ---- Auxiliary types -----------------------------------------------------*)
-and 'ty ty =
-  | Unit_t : unit ty
-  | Int_t : z num ty
-  | Nat_t : n num ty
-  | Signature_t : signature ty
-  | String_t : Script_string.t ty
-  | Bytes_t : bytes ty
-  | Mutez_t : Tez.t ty
-  | Key_hash_t : public_key_hash ty
-  | Key_t : public_key ty
-  | Timestamp_t : Script_timestamp.t ty
-  | Address_t : address ty
-  | Tx_rollup_l2_address_t : tx_rollup_l2_address ty
-  | Bool_t : bool ty
+and ('ty, 'comparable) ty =
+  | Unit_t : (unit, yes) ty
+  | Int_t : (z num, yes) ty
+  | Nat_t : (n num, yes) ty
+  | Signature_t : (signature, yes) ty
+  | String_t : (Script_string.t, yes) ty
+  | Bytes_t : (bytes, yes) ty
+  | Mutez_t : (Tez.t, yes) ty
+  | Key_hash_t : (public_key_hash, yes) ty
+  | Key_t : (public_key, yes) ty
+  | Timestamp_t : (Script_timestamp.t, yes) ty
+  | Address_t : (address, yes) ty
+  | Tx_rollup_l2_address_t : (tx_rollup_l2_address, yes) ty
+  | Bool_t : (bool, yes) ty
   | Pair_t :
-      'a ty * 'b ty * ('a, 'b) pair ty_metadata * to_be_replaced
-      -> ('a, 'b) pair ty
+      ('a, 'ac) ty
+      * ('b, 'bc) ty
+      * ('a, 'b) pair ty_metadata
+      * ('ac, 'bc, 'rc) dand
+      -> (('a, 'b) pair, 'rc) ty
   | Union_t :
-      'a ty * 'b ty * ('a, 'b) union ty_metadata * to_be_replaced
-      -> ('a, 'b) union ty
+      ('a, 'ac) ty
+      * ('b, 'bc) ty
+      * ('a, 'b) union ty_metadata
+      * ('ac, 'bc, 'rc) dand
+      -> (('a, 'b) union, 'rc) ty
   | Lambda_t :
-      'arg ty * 'ret ty * ('arg, 'ret) lambda ty_metadata
-      -> ('arg, 'ret) lambda ty
-  | Option_t : 'v ty * 'v option ty_metadata * to_be_replaced -> 'v option ty
-  | List_t : 'v ty * 'v boxed_list ty_metadata -> 'v boxed_list ty
-  | Set_t : 'v comparable_ty * 'v set ty_metadata -> 'v set ty
+      ('arg, _) ty * ('ret, _) ty * ('arg, 'ret) lambda ty_metadata
+      -> (('arg, 'ret) lambda, no) ty
+  | Option_t :
+      ('v, 'c) ty * 'v option ty_metadata * 'c dbool
+      -> ('v option, 'c) ty
+  | List_t : ('v, _) ty * 'v boxed_list ty_metadata -> ('v boxed_list, no) ty
+  | Set_t : 'v comparable_ty * 'v set ty_metadata -> ('v set, no) ty
   | Map_t :
-      'k comparable_ty * 'v ty * ('k, 'v) map ty_metadata
-      -> ('k, 'v) map ty
+      'k comparable_ty * ('v, _) ty * ('k, 'v) map ty_metadata
+      -> (('k, 'v) map, no) ty
   | Big_map_t :
-      'k comparable_ty * 'v ty * ('k, 'v) big_map ty_metadata
-      -> ('k, 'v) big_map ty
+      'k comparable_ty * ('v, _) ty * ('k, 'v) big_map ty_metadata
+      -> (('k, 'v) big_map, no) ty
   | Contract_t :
-      'arg ty * 'arg typed_contract ty_metadata
-      -> 'arg typed_contract ty
-  | Sapling_transaction_t : Sapling.Memo_size.t -> Sapling.transaction ty
+      ('arg, _) ty * 'arg typed_contract ty_metadata
+      -> ('arg typed_contract, no) ty
+  | Sapling_transaction_t : Sapling.Memo_size.t -> (Sapling.transaction, no) ty
   | Sapling_transaction_deprecated_t :
       Sapling.Memo_size.t
-      -> Sapling.Legacy.transaction ty
-  | Sapling_state_t : Sapling.Memo_size.t -> Sapling.state ty
-  | Operation_t : operation ty
-  | Chain_id_t : Script_chain_id.t ty
-  | Never_t : never ty
-  | Bls12_381_g1_t : Script_bls.G1.t ty
-  | Bls12_381_g2_t : Script_bls.G2.t ty
-  | Bls12_381_fr_t : Script_bls.Fr.t ty
-  | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty
-  | Chest_key_t : Script_timelock.chest_key ty
-  | Chest_t : Script_timelock.chest ty
+      -> (Sapling.Legacy.transaction, no) ty
+  | Sapling_state_t : Sapling.Memo_size.t -> (Sapling.state, no) ty
+  | Operation_t : (operation, no) ty
+  | Chain_id_t : (Script_chain_id.t, yes) ty
+  | Never_t : (never, yes) ty
+  | Bls12_381_g1_t : (Script_bls.G1.t, no) ty
+  | Bls12_381_g2_t : (Script_bls.G2.t, no) ty
+  | Bls12_381_fr_t : (Script_bls.Fr.t, no) ty
+  | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> ('a ticket, no) ty
+  | Chest_key_t : (Script_timelock.chest_key, no) ty
+  | Chest_t : (Script_timelock.chest, no) ty
 
 and ('top_ty, 'resty) stack_ty =
-  | Item_t : 'ty ty * ('ty2, 'rest) stack_ty -> ('ty, 'ty2 * 'rest) stack_ty
+  | Item_t :
+      ('ty, _) ty * ('ty2, 'rest) stack_ty
+      -> ('ty, 'ty2 * 'rest) stack_ty
   | Bot_t : (empty_cell, empty_cell) stack_ty
 
 and ('key, 'value) big_map =
@@ -1389,7 +1404,7 @@ and ('key, 'value) big_map =
       id : Big_map.Id.t option;
       diff : ('key, 'value) big_map_overlay;
       key_type : 'key comparable_ty;
-      value_type : 'value ty;
+      value_type : ('value, _) ty;
     }
       -> ('key, 'value) big_map
 
@@ -1487,8 +1502,8 @@ and (_, _) dup_n_gadt_witness =
 and ('input, 'output) view_signature =
   | View_signature : {
       name : Script_string.t;
-      input_ty : 'input ty;
-      output_ty : 'output ty;
+      input_ty : ('input, _) ty;
+      output_ty : ('output, _) ty;
     }
       -> ('input, 'output) view_signature
 
@@ -1501,7 +1516,7 @@ and 'kind manager_operation =
          ([Apply_results.internal_manager_operation]). *)
       transaction : Alpha_context.transaction;
       location : Script.location;
-      parameters_ty : 'a ty;
+      parameters_ty : ('a, _) ty;
       parameters : 'a;
     }
       -> Kind.transaction manager_operation
@@ -1542,11 +1557,13 @@ type kinstr_rewritek = {
 val kinstr_rewritek :
   ('a, 's, 'r, 'f) kinstr -> kinstr_rewritek -> ('a, 's, 'r, 'f) kinstr
 
-val ty_size : 'a ty -> 'a Type_size.t
+val ty_size : ('a, _) ty -> 'a Type_size.t
 
 val comparable_ty_size : 'a comparable_ty -> 'a Type_size.t
 
-type 'v ty_ex_c = Ty_ex_c : 'v ty -> 'v ty_ex_c [@@ocaml.unboxed]
+val is_comparable : ('v, 'c) ty -> 'c dbool
+
+type 'v ty_ex_c = Ty_ex_c : ('v, _) ty -> 'v ty_ex_c [@@ocaml.unboxed]
 
 val unit_key : unit comparable_ty
 
@@ -1600,101 +1617,125 @@ val union_key :
 val option_key :
   Script.location -> 'v comparable_ty -> 'v option comparable_ty tzresult
 
-val unit_t : unit ty
+val unit_t : (unit, yes) ty
+
+val int_t : (z num, yes) ty
 
-val int_t : z num ty
+val nat_t : (n num, yes) ty
 
-val nat_t : n num ty
+val signature_t : (signature, yes) ty
 
-val signature_t : signature ty
+val string_t : (Script_string.t, yes) ty
 
-val string_t : Script_string.t ty
+val bytes_t : (Bytes.t, yes) ty
 
-val bytes_t : Bytes.t ty
+val mutez_t : (Tez.t, yes) ty
 
-val mutez_t : Tez.t ty
+val key_hash_t : (public_key_hash, yes) ty
 
-val key_hash_t : public_key_hash ty
+val key_t : (public_key, yes) ty
 
-val key_t : public_key ty
+val timestamp_t : (Script_timestamp.t, yes) ty
 
-val timestamp_t : Script_timestamp.t ty
+val address_t : (address, yes) ty
 
-val address_t : address ty
+val tx_rollup_l2_address_t : (tx_rollup_l2_address, yes) ty
 
-val tx_rollup_l2_address_t : tx_rollup_l2_address ty
+val bool_t : (bool, yes) ty
 
-val bool_t : bool ty
+val pair_t :
+  Script.location -> ('a, _) ty -> ('b, _) ty -> ('a, 'b) pair ty_ex_c tzresult
 
-val pair_t : Script.location -> 'a ty -> 'b ty -> ('a, 'b) pair ty_ex_c tzresult
+val comparable_pair_t :
+  Script.location ->
+  ('a, yes) ty ->
+  ('b, yes) ty ->
+  (('a, 'b) pair, yes) ty tzresult
 
 val union_t :
-  Script.location -> 'a ty -> 'b ty -> ('a, 'b) union ty_ex_c tzresult
+  Script.location -> ('a, _) ty -> ('b, _) ty -> ('a, 'b) union ty_ex_c tzresult
 
-val union_bytes_bool_t : (Bytes.t, bool) union ty
+val comparable_union_t :
+  Script.location ->
+  ('a, yes) ty ->
+  ('b, yes) ty ->
+  (('a, 'b) union, yes) ty tzresult
+
+val union_bytes_bool_t : ((Bytes.t, bool) union, yes) ty
 
 val lambda_t :
-  Script.location -> 'arg ty -> 'ret ty -> ('arg, 'ret) lambda ty tzresult
+  Script.location ->
+  ('arg, _) ty ->
+  ('ret, _) ty ->
+  (('arg, 'ret) lambda, no) ty tzresult
 
-val option_t : Script.location -> 'v ty -> 'v option ty tzresult
+val option_t : Script.location -> ('v, 'c) ty -> ('v option, 'c) ty tzresult
 
-val option_mutez_t : Tez.t option ty
+val option_mutez_t : (Tez.t option, yes) ty
 
-val option_string_t : Script_string.t option ty
+val option_string_t : (Script_string.t option, yes) ty
 
-val option_bytes_t : Bytes.t option ty
+val option_bytes_t : (Bytes.t option, yes) ty
 
-val option_nat_t : n num option ty
+val option_nat_t : (n num option, yes) ty
 
-val option_pair_nat_nat_t : (n num, n num) pair option ty
+val option_pair_nat_nat_t : ((n num, n num) pair option, yes) ty
 
-val option_pair_nat_mutez_t : (n num, Tez.t) pair option ty
+val option_pair_nat_mutez_t : ((n num, Tez.t) pair option, yes) ty
 
-val option_pair_mutez_mutez_t : (Tez.t, Tez.t) pair option ty
+val option_pair_mutez_mutez_t : ((Tez.t, Tez.t) pair option, yes) ty
 
-val option_pair_int_nat_t : (z num, n num) pair option ty
+val option_pair_int_nat_t : ((z num, n num) pair option, yes) ty
 
-val list_t : Script.location -> 'v ty -> 'v boxed_list ty tzresult
+val list_t : Script.location -> ('v, _) ty -> ('v boxed_list, no) ty tzresult
 
-val list_operation_t : operation boxed_list ty
+val list_operation_t : (operation boxed_list, no) ty
 
-val set_t : Script.location -> 'v comparable_ty -> 'v set ty tzresult
+val set_t : Script.location -> 'v comparable_ty -> ('v set, no) ty tzresult
 
 val map_t :
-  Script.location -> 'k comparable_ty -> 'v ty -> ('k, 'v) map ty tzresult
+  Script.location ->
+  'k comparable_ty ->
+  ('v, _) ty ->
+  (('k, 'v) map, no) ty tzresult
 
 val big_map_t :
-  Script.location -> 'k comparable_ty -> 'v ty -> ('k, 'v) big_map ty tzresult
+  Script.location ->
+  'k comparable_ty ->
+  ('v, _) ty ->
+  (('k, 'v) big_map, no) ty tzresult
 
-val contract_t : Script.location -> 'arg ty -> 'arg typed_contract ty tzresult
+val contract_t :
+  Script.location -> ('arg, _) ty -> ('arg typed_contract, no) ty tzresult
 
-val contract_unit_t : unit typed_contract ty
+val contract_unit_t : (unit typed_contract, no) ty
 
 val sapling_transaction_t :
-  memo_size:Sapling.Memo_size.t -> Sapling.transaction ty
+  memo_size:Sapling.Memo_size.t -> (Sapling.transaction, no) ty
 
 val sapling_transaction_deprecated_t :
-  memo_size:Sapling.Memo_size.t -> Sapling.Legacy.transaction ty
+  memo_size:Sapling.Memo_size.t -> (Sapling.Legacy.transaction, no) ty
 
-val sapling_state_t : memo_size:Sapling.Memo_size.t -> Sapling.state ty
+val sapling_state_t : memo_size:Sapling.Memo_size.t -> (Sapling.state, no) ty
 
-val operation_t : operation ty
+val operation_t : (operation, no) ty
 
-val chain_id_t : Script_chain_id.t ty
+val chain_id_t : (Script_chain_id.t, yes) ty
 
-val never_t : never ty
+val never_t : (never, yes) ty
 
-val bls12_381_g1_t : Script_bls.G1.t ty
+val bls12_381_g1_t : (Script_bls.G1.t, no) ty
 
-val bls12_381_g2_t : Script_bls.G2.t ty
+val bls12_381_g2_t : (Script_bls.G2.t, no) ty
 
-val bls12_381_fr_t : Script_bls.Fr.t ty
+val bls12_381_fr_t : (Script_bls.Fr.t, no) ty
 
-val ticket_t : Script.location -> 'a comparable_ty -> 'a ticket ty tzresult
+val ticket_t :
+  Script.location -> 'a comparable_ty -> ('a ticket, no) ty tzresult
 
-val chest_key_t : Script_timelock.chest_key ty
+val chest_key_t : (Script_timelock.chest_key, no) ty
 
-val chest_t : Script_timelock.chest ty
+val chest_t : (Script_timelock.chest, no) ty
 
 (**
 
@@ -1723,13 +1764,13 @@ val kinstr_traverse :
   ('a, 'b, 'c, 'd) kinstr -> 'ret -> 'ret kinstr_traverse -> 'ret
 
 type 'a ty_traverse = {
-  apply : 't. 'a -> 't ty -> 'a;
+  apply : 't 'tc. 'a -> ('t, 'tc) ty -> 'a;
   apply_comparable : 't. 'a -> 't comparable_ty -> 'a;
 }
 
 val comparable_ty_traverse : 'a comparable_ty -> 'r -> 'r ty_traverse -> 'r
 
-val ty_traverse : 'a ty -> 'r -> 'r ty_traverse -> 'r
+val ty_traverse : ('a, _) ty -> 'r -> 'r ty_traverse -> 'r
 
 type 'accu stack_ty_traverse = {
   apply : 'ty 's. 'accu -> ('ty, 's) stack_ty -> 'accu;
@@ -1738,11 +1779,11 @@ type 'accu stack_ty_traverse = {
 val stack_ty_traverse : ('a, 's) stack_ty -> 'r -> 'r stack_ty_traverse -> 'r
 
 type 'a value_traverse = {
-  apply : 't. 'a -> 't ty -> 't -> 'a;
+  apply : 't 'tc. 'a -> ('t, 'tc) ty -> 't -> 'a;
   apply_comparable : 't. 'a -> 't comparable_ty -> 't -> 'a;
 }
 
 val value_traverse :
-  ('t ty, 't comparable_ty) union -> 't -> 'r -> 'r value_traverse -> 'r
+  (('t, _) ty, 't comparable_ty) union -> 't -> 'r -> 'r value_traverse -> 'r
 
 val stack_top_ty : ('a, 'b * 's) stack_ty -> 'a ty_ex_c
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
index 8ffaabc9a1c630effae51fca259f56903ad04ee3..43a3c8b836b8c533250be12e42ff77a2a26f6af5 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
@@ -60,13 +60,13 @@ let ty_traverse_f =
     | Bool_key -> ret_succ_adding accu base_basic
     | Chain_id_key -> ret_succ_adding accu base_basic
     | Never_key -> ret_succ_adding accu base_basic
-    | Pair_key (_ty1, _ty2, a) ->
-        ret_succ_adding accu @@ (base_compound a +! (word_size *? 2))
-    | Union_key (_ty1, _ty2, a) ->
+    | Pair_key (_ty1, _ty2, a, YesYes) ->
+        ret_succ_adding accu @@ (base_compound a +! (word_size *? 3))
+    | Union_key (_ty1, _ty2, a, YesYes) ->
+        ret_succ_adding accu @@ (base_compound a +! (word_size *? 3))
+    | Option_key (_ty, a, Yes) ->
         ret_succ_adding accu @@ (base_compound a +! (word_size *? 2))
-    | Option_key (_ty, a) ->
-        ret_succ_adding accu @@ (base_compound a +! word_size)
-  and apply : type a. nodes_and_size -> a ty -> nodes_and_size =
+  and apply : type a ac. nodes_and_size -> (a, ac) ty -> nodes_and_size =
    fun accu ty ->
     match ty with
     | Unit_t -> ret_succ_adding accu base_basic
@@ -123,7 +123,7 @@ let ty_traverse_f =
 let comparable_ty_size : type a. a comparable_ty -> nodes_and_size =
  fun cty -> comparable_ty_traverse cty zero ty_traverse_f
 
-let ty_size : type a. a ty -> nodes_and_size =
+let ty_size : type a ac. (a, ac) ty -> nodes_and_size =
  fun ty -> ty_traverse ty zero ty_traverse_f
 
 let stack_ty_size s =
@@ -262,14 +262,14 @@ let kinfo_size {iloc = _; kstack_ty = _} = h2w
    cannot be nested. (See [big_map_size].) For this reason, these
    functions should not trigger stack overflows. *)
 let rec value_size :
-    type a.
+    type a ac.
     count_lambda_nodes:bool ->
     nodes_and_size ->
-    (a ty, a comparable_ty) union ->
+    ((a, ac) ty, a comparable_ty) union ->
     a ->
     nodes_and_size =
  fun ~count_lambda_nodes accu ty x ->
-  let apply : type a. nodes_and_size -> a ty -> a -> nodes_and_size =
+  let apply : type a ac. nodes_and_size -> (a, ac) ty -> a -> nodes_and_size =
    fun accu ty x ->
     match ty with
     | Unit_t -> ret_succ accu
@@ -344,9 +344,10 @@ let rec value_size :
     | Tx_rollup_l2_address_key ->
         ret_succ_adding accu (tx_rollup_l2_address_size x)
     | Bool_key -> ret_succ accu
-    | Pair_key (_, _, _) -> ret_succ_adding accu h2w
-    | Union_key (_, _, _) -> ret_succ_adding accu h1w
-    | Option_key (_, _) -> ret_succ_adding accu (option_size (fun _ -> !!0) x)
+    | Pair_key (_, _, _, YesYes) -> ret_succ_adding accu h2w
+    | Union_key (_, _, _, YesYes) -> ret_succ_adding accu h1w
+    | Option_key (_, _, Yes) ->
+        ret_succ_adding accu (option_size (fun _ -> !!0) x)
     | Chain_id_key -> ret_succ_adding accu chain_id_size
     | Never_key -> ( match x with _ -> .)
   in
@@ -354,11 +355,11 @@ let rec value_size :
  [@@coq_axiom_with_reason "unreachable expressions '.' not handled for now"]
 
 and big_map_size :
-    type a b.
+    type a b bc.
     count_lambda_nodes:bool ->
     nodes_and_size ->
     a comparable_ty ->
-    b ty ->
+    (b, bc) ty ->
     (a, b) big_map ->
     nodes_and_size =
  fun ~count_lambda_nodes accu cty ty' (Big_map {id; diff; key_type; value_type}) ->
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.mli b/src/proto_alpha/lib_protocol/script_typed_ir_size.mli
index 9b51ba8b8cacaac24278e34c5f6b89b5a464c00f..26e4b38e9a1e53d81cf33d0224aa7a255cae2f02 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir_size.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.mli
@@ -34,7 +34,7 @@
 (** [value_size ty v] returns an overapproximation of the size of the
    in-memory representation of [v] of type [ty]. *)
 val value_size :
-  'a Script_typed_ir.ty -> 'a -> Cache_memory_helpers.nodes_and_size
+  ('a, _) Script_typed_ir.ty -> 'a -> Cache_memory_helpers.nodes_and_size
 
 (** [lambda_size l] returns an overapproximation of the size of the
     internal IR for the Michelson lambda abstraction [l]. *)
@@ -61,7 +61,8 @@ val zero : Cache_memory_helpers.nodes_and_size
 module Internal_for_tests : sig
   (** [ty_size ty] returns an overapproximation of the size of the
    in-memory representation of type [ty]. *)
-  val ty_size : 'a Script_typed_ir.ty -> Cache_memory_helpers.nodes_and_size
+  val ty_size :
+    ('a, _) Script_typed_ir.ty -> Cache_memory_helpers.nodes_and_size
 
   (** [comparable_ty_size cty] returns an overapproximation of the size
    of the in-memory representation of comparable type [cty]. *)
diff --git a/src/proto_alpha/lib_protocol/test/helpers/script_big_map.mli b/src/proto_alpha/lib_protocol/test/helpers/script_big_map.mli
index d3875195820ab9f3caf9f2a7c105606417818cb3..29e7738520c337d9620a42145f1bf593c027d80f 100644
--- a/src/proto_alpha/lib_protocol/test/helpers/script_big_map.mli
+++ b/src/proto_alpha/lib_protocol/test/helpers/script_big_map.mli
@@ -36,7 +36,7 @@ val update :
   *)
 val of_list :
   'key Protocol.Script_typed_ir.comparable_ty ->
-  'value Protocol.Script_typed_ir.ty ->
+  ('value, _) Protocol.Script_typed_ir.ty ->
   ('key * 'value) list ->
   Protocol.Alpha_context.t ->
   (('key, 'value) Protocol.Script_typed_ir.big_map * Protocol.Alpha_context.t)
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml
index 60247caa3586c57a6f4535cf2db2d057ada070f6..cd0edb8952f0698bbc579165d9408bc9192a4b13 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_cache.ml
@@ -86,7 +86,8 @@ let find ctxt addr =
       return (ctxt, identifier, script, Ex_script ir)
 
 let value_as_int :
-    type a. a Script_typed_ir.ty -> a -> Script_int_repr.z Script_int_repr.num =
+    type a ac.
+    (a, ac) Script_typed_ir.ty -> a -> Script_int_repr.z Script_int_repr.num =
  fun ty v -> match ty with Int_t -> v | _ -> Stdlib.failwith "value_as_int"
 
 let add_some_contracts k src block baker =
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
index 35f7f7dd07ab53f8edd8a51da207af5fea7c74a4..2d66952a94c02667cb83d468d3ce51714a977a75 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_script_typed_ir_size.ml
@@ -159,7 +159,7 @@ module Printers = struct
         Format.eprintf "@[Error: %a@]" pp_print_trace errs ;
         exit 1
 
-  let string_of_value : type a. a Script_typed_ir.ty -> a -> string =
+  let string_of_value : type a ac. (a, ac) Script_typed_ir.ty -> a -> string =
    fun ty v ->
     string_of_something @@ fun ctxt ->
     Script_ir_translator.(
@@ -284,7 +284,7 @@ module Tests = struct
       ~expected_ratios:(1., 0.05)
 
   let contains_exceptions ty =
-    let apply : type a. bool -> a Script_typed_ir.ty -> bool =
+    let apply : type a ac. bool -> (a, ac) Script_typed_ir.ty -> bool =
      fun accu -> function
       (* Boxed sets and maps point to a shared first class module.
          This is an overapproximation that we want to ignore in
diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
index 90f03f0606f7181790e09f6efe1d74d7ab2b6d98..5e9bf5963032d333da3879854612470e240b6506 100644
--- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml
@@ -160,7 +160,8 @@ let location = function
   | Seq (loc, _) ->
       loc
 
-let test_parse_ty (type exp) ctxt node (expected : exp Script_typed_ir.ty) =
+let test_parse_ty (type exp expc) ctxt node
+    (expected : (exp, expc) Script_typed_ir.ty) =
   let legacy = false in
   let allow_lazy_storage = true in
   let allow_operation = true in
@@ -454,11 +455,27 @@ let test_parse_comb_data () =
     Big_map
       {id = Some big_map_id; diff; key_type = nat_key_ty; value_type = nat_ty}
   in
+  let ty_equal :
+      type a ac1 ac2.
+      (a, ac1) Script_typed_ir.ty -> (a, ac2) Script_typed_ir.ty -> bool =
+   fun ty1 ty2 ->
+    match Script_typed_ir.(is_comparable ty1, is_comparable ty2) with
+    | (Yes, Yes) -> ty1 = ty2
+    | (No, No) -> ty1 = ty2
+    | (Yes, No) -> assert false
+    | (No, Yes) -> assert false
+   (*
+      These last two cases can't happen because the comparable character of a
+      type is a function of its concrete type.
+      It is possible to write a function that proves it but it is not needed
+      in the protocol for the moment.
+   *)
+  in
   let equal (nat1, Big_map big_map1) (nat2, Big_map big_map2) =
     (* Custom equal needed because big maps contain boxed maps containing functional values *)
     nat1 = nat2 && big_map1.id = big_map2.id
     && big_map1.key_type = big_map2.key_type
-    && big_map1.value_type = big_map2.value_type
+    && ty_equal big_map1.value_type big_map2.value_type
     && big_map1.diff.size = big_map2.diff.size
     && Big_map_overlay.bindings big_map1.diff.map
        = Big_map_overlay.bindings big_map2.diff.map
diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml b/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml
index ce05dc44653e1a97d90b9f3fc8c5a04ec2a69426..12e3a4124e4e370818475e098a9d9b075bb76e30 100644
--- a/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml
+++ b/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml
@@ -68,17 +68,20 @@ let rec reference_compare_comparable : type a. a comparable_ty -> a -> a -> int
       normalize_compare @@ Script_comparable.compare_tx_rollup_l2_address x y
   | (Bytes_key, x, y) -> normalize_compare @@ Compare.Bytes.compare x y
   | (Chain_id_key, x, y) -> normalize_compare @@ Script_chain_id.compare x y
-  | (Pair_key (tl, tr, _), (lx, rx), (ly, ry)) ->
+  | (Pair_key (tl, tr, _, YesYes), (lx, rx), (ly, ry)) ->
       let cl = reference_compare_comparable tl lx ly in
       if Compare.Int.(cl = 0) then reference_compare_comparable tr rx ry else cl
-  | (Union_key (tl, _, _), L x, L y) -> reference_compare_comparable tl x y
+  | (Union_key (tl, _, _, YesYes), L x, L y) ->
+      reference_compare_comparable tl x y
   | (Union_key _, L _, R _) -> -1
   | (Union_key _, R _, L _) -> 1
-  | (Union_key (_, tr, _), R x, R y) -> reference_compare_comparable tr x y
+  | (Union_key (_, tr, _, YesYes), R x, R y) ->
+      reference_compare_comparable tr x y
   | (Option_key _, None, None) -> 0
   | (Option_key _, None, Some _) -> -1
   | (Option_key _, Some _, None) -> 1
-  | (Option_key (t, _), Some x, Some y) -> reference_compare_comparable t x y
+  | (Option_key (t, _, Yes), Some x, Some y) ->
+      reference_compare_comparable t x y
 
 (* Generation of one to three values of the same comparable type. *)
 
diff --git a/src/proto_alpha/lib_protocol/ticket_costs.mli b/src/proto_alpha/lib_protocol/ticket_costs.mli
index 6a216fd3057f4bc055fa9b8a2f7e843aef2af44e..fa9745b1850446be7896c9ac9829013c68b251f9 100644
--- a/src/proto_alpha/lib_protocol/ticket_costs.mli
+++ b/src/proto_alpha/lib_protocol/ticket_costs.mli
@@ -52,7 +52,7 @@ val consume_gas_steps :
 (** [has_tickets_of_ty_cost ty] returns the cost of producing a [has_tickets],
     used internally in the [Ticket_scanner] module. *)
 val has_tickets_of_ty_cost :
-  'a Script_typed_ir.ty -> Saturation_repr.may_saturate Saturation_repr.t
+  ('a, _) Script_typed_ir.ty -> Saturation_repr.may_saturate Saturation_repr.t
 
 (** [negate_cost z] returns the cost of negating the given value [z]. *)
 val negate_cost : Z.t -> Alpha_context.Gas.cost
diff --git a/src/proto_alpha/lib_protocol/ticket_operations_diff.ml b/src/proto_alpha/lib_protocol/ticket_operations_diff.ml
index 25810b64df277d8ab7cfac46fda7cb789c969688..0fcc683b02966d2ac9a410f287409d711b6bb066 100644
--- a/src/proto_alpha/lib_protocol/ticket_operations_diff.ml
+++ b/src/proto_alpha/lib_protocol/ticket_operations_diff.ml
@@ -149,9 +149,10 @@ let parse_and_cache_script ctxt ~destination ~get_non_cached_script =
       Script_cache.insert ctxt destination (script, ex_script) size
       >>?= fun ctxt -> return (ex_script, ctxt)
 
-let cast_transaction_parameter (type a b) ctxt location
-    (entry_arg_ty : a Script_typed_ir.ty) (parameters_ty : b Script_typed_ir.ty)
-    (parameters : b) : (a * context) tzresult Lwt.t =
+let cast_transaction_parameter (type a ac b bc) ctxt location
+    (entry_arg_ty : (a, ac) Script_typed_ir.ty)
+    (parameters_ty : (b, bc) Script_typed_ir.ty) (parameters : b) :
+    (a * context) tzresult Lwt.t =
   Gas_monad.run
     ctxt
     (Script_ir_translator.ty_eq
diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml
index 2130c276718fc1b83e4e243956cf5da65da050c1..d024631f13b2e401d873607e00aa622ee1ceedf9 100644
--- a/src/proto_alpha/lib_protocol/ticket_scanner.ml
+++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml
@@ -124,9 +124,9 @@ module Ticket_inspection = struct
     | Chain_id_key -> (k [@ocaml.tailcall]) False_ht
     | Address_key -> (k [@ocaml.tailcall]) False_ht
     | Tx_rollup_l2_address_key -> (k [@ocaml.tailcall]) False_ht
-    | Pair_key (_, _, _) -> (k [@ocaml.tailcall]) False_ht
-    | Union_key (_, _, _) -> (k [@ocaml.tailcall]) False_ht
-    | Option_key (_, _) -> (k [@ocaml.tailcall]) False_ht
+    | Pair_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht
+    | Union_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht
+    | Option_key (_, _, Yes) -> (k [@ocaml.tailcall]) False_ht
 
   (* Short circuit pairing of two [has_tickets] values.
      If neither left nor right branch contains a ticket, [False_ht] is
@@ -144,8 +144,8 @@ module Ticket_inspection = struct
      it collapses whole branches where no types embed tickets to [False_ht].
   *)
   let rec has_tickets_of_ty :
-      type a ret. a Script_typed_ir.ty -> (a, ret) continuation -> ret tzresult
-      =
+      type a ac ret.
+      (a, ac) Script_typed_ir.ty -> (a, ret) continuation -> ret tzresult =
    fun ty k ->
     let open Script_typed_ir in
     match ty with
@@ -220,9 +220,9 @@ module Ticket_inspection = struct
     | Chest_key_t -> (k [@ocaml.tailcall]) False_ht
 
   and has_tickets_of_pair :
-      type a b c ret.
-      a Script_typed_ir.ty ->
-      b Script_typed_ir.ty ->
+      type a ac b bc c ret.
+      (a, ac) Script_typed_ir.ty ->
+      (b, bc) Script_typed_ir.ty ->
       pair:(a has_tickets -> b has_tickets -> c has_tickets) ->
       (c, ret) continuation ->
       ret tzresult =
@@ -232,9 +232,9 @@ module Ticket_inspection = struct
             (k [@ocaml.tailcall]) (pair_has_tickets pair ht1 ht2)))
 
   and has_tickets_of_key_and_value :
-      type k v t ret.
+      type k v vc t ret.
       k Script_typed_ir.comparable_ty ->
-      v Script_typed_ir.ty ->
+      (v, vc) Script_typed_ir.ty ->
       pair:(k has_tickets -> v has_tickets -> t has_tickets) ->
       (t, ret) continuation ->
       ret tzresult =
@@ -289,9 +289,9 @@ module Ticket_collection = struct
     | Chain_id_key -> (k [@ocaml.tailcall]) ctxt acc
     | Address_key -> (k [@ocaml.tailcall]) ctxt acc
     | Tx_rollup_l2_address_key -> (k [@ocaml.tailcall]) ctxt acc
-    | Pair_key (_, _, _) -> (k [@ocaml.tailcall]) ctxt acc
-    | Union_key (_, _, _) -> (k [@ocaml.tailcall]) ctxt acc
-    | Option_key (_, _) -> (k [@ocaml.tailcall]) ctxt acc
+    | Pair_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc
+    | Union_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc
+    | Option_key (_, _, Yes) -> (k [@ocaml.tailcall]) ctxt acc
 
   let tickets_of_set :
       type a ret.
@@ -308,11 +308,11 @@ module Ticket_collection = struct
     (tickets_of_comparable [@ocaml.tailcall]) ctxt key_ty acc k
 
   let rec tickets_of_value :
-      type a ret.
+      type a ac ret.
       include_lazy:bool ->
       Alpha_context.context ->
       a Ticket_inspection.has_tickets ->
-      a Script_typed_ir.ty ->
+      (a, ac) Script_typed_ir.ty ->
       a ->
       accumulator ->
       ret continuation ->
@@ -406,11 +406,11 @@ module Ticket_collection = struct
         (k [@ocaml.tailcall]) ctxt (Ex_ticket (comp_ty, x) :: acc)
 
   and tickets_of_list :
-      type a ret.
+      type a ac ret.
       Alpha_context.context ->
       include_lazy:bool ->
       a Ticket_inspection.has_tickets ->
-      a Script_typed_ir.ty ->
+      (a, ac) Script_typed_ir.ty ->
       a list ->
       accumulator ->
       ret continuation ->
@@ -438,11 +438,11 @@ module Ticket_collection = struct
     | [] -> (k [@ocaml.tailcall]) ctxt acc
 
   and tickets_of_map :
-      type k v ret.
+      type k v vc ret.
       include_lazy:bool ->
       Alpha_context.context ->
       v Ticket_inspection.has_tickets ->
-      v Script_typed_ir.ty ->
+      (v, vc) Script_typed_ir.ty ->
       (k, v) Script_typed_ir.map ->
       accumulator ->
       ret continuation ->
@@ -515,7 +515,7 @@ end
 
 type 'a has_tickets =
   | Has_tickets :
-      'a Ticket_inspection.has_tickets * 'a Script_typed_ir.ty
+      'a Ticket_inspection.has_tickets * ('a, _) Script_typed_ir.ty
       -> 'a has_tickets
 
 let type_has_tickets ctxt ty =
diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.mli b/src/proto_alpha/lib_protocol/ticket_scanner.mli
index fe405abe137cdc2faa44bbdb25f639c8f2d0a6ef..209c633ab74abb5a5dd1cd91cd5b3e93c6f01e3d 100644
--- a/src/proto_alpha/lib_protocol/ticket_scanner.mli
+++ b/src/proto_alpha/lib_protocol/ticket_scanner.mli
@@ -46,7 +46,7 @@ type 'a has_tickets
  *)
 val type_has_tickets :
   Alpha_context.context ->
-  'a Script_typed_ir.ty ->
+  ('a, _) Script_typed_ir.ty ->
   ('a has_tickets * Alpha_context.context) tzresult
 
 (** [tickets_of_value ctxt ~include_lazy ht value] extracts all tickets from