diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml
index fa1396188..f6a821cef 100644
--- a/src/base/as_prover0.ml
+++ b/src/base/as_prover0.ml
@@ -6,7 +6,9 @@ module Make (Backend : sig
   end
 end)
 (Types : Types.Types
-           with type 'a As_prover.t =
+           with type field = Backend.Field.t
+            and type field_var = Backend.Field.t Cvar.t
+            and type 'a As_prover.t =
              (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a) =
 struct
   type 'a t = 'a Types.As_prover.t
@@ -37,8 +39,8 @@ struct
   let read_var (v : 'var) : 'field t = fun tbl -> tbl v
 
   let read
-      (Typ { var_to_fields; value_of_fields; _ } :
-        ('var, 'value, 'field) Types.Typ.t ) (var : 'var) : 'value t =
+      (Typ { var_to_fields; value_of_fields; _ } : ('var, 'value) Types.Typ.t)
+      (var : 'var) : 'value t =
    fun tbl ->
     let field_vars, aux = var_to_fields var in
     let fields = Array.map ~f:tbl field_vars in
diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml
index b4c2f3668..eeabefcee 100644
--- a/src/base/as_prover_intf.ml
+++ b/src/base/as_prover_intf.ml
@@ -13,7 +13,7 @@ module type Basic = sig
 
   val read_var : field Cvar.t -> field t
 
-  val read : ('var, 'value, field) Types.Typ.t -> 'var -> 'value t
+  val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t
 
   module Provider : sig
     type 'a t
diff --git a/src/base/checked.ml b/src/base/checked.ml
index f765d1e9d..d6aa33b2c 100644
--- a/src/base/checked.ml
+++ b/src/base/checked.ml
@@ -13,7 +13,7 @@ end)
   Checked_intf.S with module Types := Types with type field = Field.t = struct
   include Basic
 
-  let request_witness (typ : ('var, 'value, field) Types.Typ.t)
+  let request_witness (typ : ('var, 'value) Types.Typ.t)
       (r : 'value Request.t As_prover.t) =
     let%map h = exists typ (Request r) in
     Handle.var h
diff --git a/src/base/checked_intf.ml b/src/base/checked_intf.ml
index 4bbbdefe1..9d237f91b 100644
--- a/src/base/checked_intf.ml
+++ b/src/base/checked_intf.ml
@@ -18,7 +18,7 @@ module type Basic = sig
   val with_handler : Request.Handler.single -> (unit -> 'a t) -> 'a t
 
   val exists :
-       ('var, 'value, field) Types.Typ.t
+       ('var, 'value) Types.Typ.t
     -> 'value Types.Provider.t
     -> ('var, 'value) Handle.t t
 
@@ -47,26 +47,24 @@ module type S = sig
   val mk_lazy : (unit -> 'a t) -> 'a Lazy.t t
 
   val request_witness :
-       ('var, 'value, field) Types.Typ.t
-    -> 'value Request.t Types.As_prover.t
-    -> 'var t
+    ('var, 'value) Types.Typ.t -> 'value Request.t Types.As_prover.t -> 'var t
 
   val request :
        ?such_that:('var -> unit t)
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'value Request.t
     -> 'var t
 
   val exists_handle :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> ('var, 'value) Handle.t t
 
   val exists :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'var t
 
   type response = Request.response
diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml
index 0a00b961c..6e481edbc 100644
--- a/src/base/checked_runner.ml
+++ b/src/base/checked_runner.ml
@@ -12,9 +12,13 @@ type ('a, 'f) t =
   | Function of ('f Run_state.t -> 'f Run_state.t * 'a)
 
 module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct
-  type 'a checked = ('a, Backend.Field.t) t
+  type field = Backend.Field.t
+
+  type field_var = field Cvar.t
+
+  type 'a checked = ('a, field) t
 
-  type 'a as_prover = (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a
+  type 'a as_prover = (field_var -> field) -> 'a
 end)
 
 module Simple = struct
@@ -53,17 +57,14 @@ end
 module Make_checked
     (Backend : Backend_extended.S)
     (Types : Types.Types
-               with type 'a Checked.t = 'a Simple_types(Backend).Checked.t
+               with type field = Backend.Field.t
+                and type field_var = Backend.Field.t Cvar.t
+                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
                 and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
-                and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
-                 ( 'var
-                 , 'value
-                 , 'aux
-                 , 'field
-                 , 'checked )
-                 Simple_types(Backend).Typ.typ'
-                and type ('var, 'value, 'field, 'checked) Typ.typ =
-                 ('var, 'value, 'field, 'checked) Simple_types(Backend).Typ.typ)
+                and type ('var, 'value, 'aux) Typ.typ' =
+                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
+                and type ('var, 'value) Typ.typ =
+                 ('var, 'value) Simple_types(Backend).Typ.typ)
     (As_prover : As_prover_intf.Basic
                    with type field := Backend.Field.t
                    with module Types := Types) =
@@ -228,7 +229,7 @@ struct
          ; constraint_system_auxiliary
          ; _
          } :
-        (_, _, _, _ t) Types.Typ.typ ) p : _ t =
+        (_, _) Types.Typ.typ ) p : _ t =
     Function
       (fun s ->
         if Run_state.has_witness s then (
@@ -318,17 +319,14 @@ end
 module Make
     (Backend : Backend_extended.S)
     (Types : Types.Types
-               with type 'a Checked.t = 'a Simple_types(Backend).Checked.t
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t
+                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
                 and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
-                and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
-                 ( 'var
-                 , 'value
-                 , 'aux
-                 , 'field
-                 , 'checked )
-                 Simple_types(Backend).Typ.typ'
-                and type ('var, 'value, 'field, 'checked) Typ.typ =
-                 ('var, 'value, 'field, 'checked) Simple_types(Backend).Typ.typ
+                and type ('var, 'value, 'aux) Typ.typ' =
+                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
+                and type ('var, 'value) Typ.typ =
+                 ('var, 'value) Simple_types(Backend).Typ.typ
                 and type ('request, 'compute) Provider.provider =
                  ('request, 'compute) Simple_types(Backend).Provider.provider) =
 struct
diff --git a/src/base/runners.ml b/src/base/runners.ml
index 0362c0440..453e87e79 100644
--- a/src/base/runners.ml
+++ b/src/base/runners.ml
@@ -2,7 +2,9 @@ open Core_kernel
 
 module Make
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with type field = Backend.Field.t
                  with module Types := Types)
@@ -159,26 +161,15 @@ struct
         }
 
       val build :
-           input_typ:
-             ( 'input_var
-             , 'input_value
-             , field
-             , unit Types.Checked.t )
-             Types.Typ.typ
-        -> return_typ:
-             ('retvar, 'retval, field, unit Types.Checked.t) Types.Typ.typ
+           input_typ:('input_var, 'input_value) Types.Typ.typ
+        -> return_typ:('retvar, 'retval) Types.Typ.typ
         -> ('input_var, 'retvar, field, 'checked) t
     end = struct
       let allocate_public_inputs :
           type input_var input_value output_var output_value.
              int ref
-          -> input_typ:
-               ( input_var
-               , input_value
-               , field
-               , unit Types.Checked.t )
-               Types.Typ.typ
-          -> return_typ:(output_var, output_value, field) Types.Typ.t
+          -> input_typ:(input_var, input_value) Types.Typ.typ
+          -> return_typ:(output_var, output_value) Types.Typ.t
           -> input_var * output_var =
        fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) ->
         (* allocate variables for the public input and the public output *)
@@ -205,13 +196,8 @@ struct
 
       let build :
           type checked input_var input_value retvar retval.
-             input_typ:
-               ( input_var
-               , input_value
-               , field
-               , unit Types.Checked.t )
-               Types.Typ.typ
-          -> return_typ:(retvar, retval, _) Types.Typ.t
+             input_typ:(input_var, input_value) Types.Typ.typ
+          -> return_typ:(retvar, retval) Types.Typ.t
           -> (input_var, retvar, field, checked) t =
        fun ~input_typ ~return_typ ->
         let next_input = ref 0 in
@@ -259,7 +245,7 @@ struct
 
     let constraint_system (type a checked input_var) :
            run:(a, checked) Runner.run
-        -> input_typ:(input_var, _, _, _) Types.Typ.typ
+        -> input_typ:(input_var, _) Types.Typ.typ
         -> return_typ:_
         -> (input_var -> checked)
         -> R1CS_constraint_system.t =
@@ -271,7 +257,7 @@ struct
       builder.finish_computation (state, res)
 
     let generate_public_input :
-           ('input_var, 'input_value, _, _) Types.Typ.typ
+           ('input_var, 'input_value) Types.Typ.typ
         -> 'input_value
         -> Field.Vector.t =
      fun (Typ { value_to_fields; _ }) value ->
@@ -291,7 +277,7 @@ struct
         }
 
       let receive_public_input :
-             ('input_var, 'input_value, _) Types.Typ.t
+             ('input_var, 'input_value) Types.Typ.t
           -> _ Types.Typ.t
           -> 'input_value
           -> _ =
@@ -382,7 +368,7 @@ struct
     let conv :
         type r_var r_value.
            (int -> _ -> r_var -> Field.Vector.t -> r_value)
-        -> ('input_var, 'input_value, _) Types.Typ.t
+        -> ('input_var, 'input_value) Types.Typ.t
         -> _ Types.Typ.t
         -> (unit -> 'input_var -> r_var)
         -> 'input_value
@@ -396,7 +382,7 @@ struct
     let generate_auxiliary_input :
            run:('a, 'checked) Runner.run
         -> input_typ:_ Types.Typ.t
-        -> return_typ:(_, _, _) Types.Typ.t
+        -> return_typ:(_, _) Types.Typ.t
         -> ?handlers:Handler.t list
         -> 'k_var
         -> 'k_value =
diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index a1c3cb9db..bfd72e48e 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -10,7 +10,9 @@ let set_eval_constraints b = Runner.eval_constraints := b
 
 module Make_basic
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with type field = Backend.Field.t
                  with module Types := Types)
@@ -31,7 +33,7 @@ struct
     module T = Typ.Make (Types) (Checked)
     include T.T
 
-    type ('var, 'value) t = ('var, 'value, Field.t) T.t
+    type ('var, 'value) t = ('var, 'value) T.t
 
     let unit : (unit, unit) t = unit ()
 
diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 12e642102..caeda7505 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -128,32 +128,27 @@ module type Typ_intf = sig
 
   type field_var
 
-  type _ checked
-
   type 'field checked_unit
 
-  type ('var, 'value, 'aux, 'field, 'checked) typ' =
-    { var_to_fields : 'var -> 'field Cvar.t array * 'aux
-    ; var_of_fields : 'field Cvar.t array * 'aux -> 'var
-    ; value_to_fields : 'value -> 'field array * 'aux
-    ; value_of_fields : 'field array * 'aux -> 'value
+  type ('var, 'value, 'aux) typ' =
+    { var_to_fields : 'var -> field_var array * 'aux
+    ; var_of_fields : field_var array * 'aux -> 'var
+    ; value_to_fields : 'value -> field array * 'aux
+    ; value_of_fields : field array * 'aux -> 'value
     ; size_in_field_elements : int
     ; constraint_system_auxiliary : unit -> 'aux
-    ; check : 'var -> 'checked
+    ; check : 'var -> field checked_unit
     }
 
-  type ('var, 'value, 'field, 'checked) typ =
-    | Typ :
-        ('var, 'value, 'aux, 'field, 'checked) typ'
-        -> ('var, 'value, 'field, 'checked) typ
+  type ('var, 'value) typ =
+    | Typ : ('var, 'value, 'aux) typ' -> ('var, 'value) typ
 
   module Data_spec : sig
-    type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t =
+    type ('r_var, 'r_value, 'k_var, 'k_value) t =
       | ( :: ) :
-          ('var, 'value, 'field, 'field checked_unit) typ
-          * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t
-          -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t
-      | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t
+          ('var, 'value) typ * ('r_var, 'r_value, 'k_var, 'k_value) t
+          -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value) t
+      | [] : ('r_var, 'r_value, 'r_var, 'r_value) t
   end
 
   (** The type [('var, 'value) t] describes a mapping from the OCaml type
@@ -169,7 +164,7 @@ module type Typ_intf = sig
           example, that a [Boolean.t] is either a {!val:Field.zero} or a
           {!val:Field.one}.
     *)
-  type ('var, 'value) t = ('var, 'value, field, field checked_unit) typ
+  type ('var, 'value) t = ('var, 'value) typ
 
   (** Basic instances: *)
 
@@ -223,7 +218,7 @@ module type Typ_intf = sig
   (** Unpack a {!type:Data_spec.t} list to a {!type:t}. The return value relates
         a polymorphic list of OCaml types to a polymorphic list of R1CS types. *)
   val hlist :
-       (unit, unit, 'k_var, 'k_value, field) Data_spec.t
+       (unit, unit, 'k_var, 'k_value) Data_spec.t
     -> ((unit, 'k_var) H_list.t, (unit, 'k_value) H_list.t) t
 
   (** Convert relationships over
@@ -246,7 +241,7 @@ module type Typ_intf = sig
         {!type:Data_spec.t}.
     *)
   val of_hlistable :
-       (unit, unit, 'k_var, 'k_value, field) Data_spec.t
+       (unit, unit, 'k_var, 'k_value) Data_spec.t
     -> var_to_hlist:('var -> (unit, 'k_var) H_list.t)
     -> var_of_hlist:((unit, 'k_var) H_list.t -> 'var)
     -> value_to_hlist:('value -> (unit, 'k_value) H_list.t)
@@ -584,7 +579,6 @@ module type Basic = sig
         with type field := Field.t
          and type field_var := Field.Var.t
          and type _ checked_unit := unit Checked.t
-         and type _ checked := unit Checked.t
   end
 
   (** Representation of booleans within a field.
@@ -1122,10 +1116,13 @@ module type Run_basic = sig
   (** Mappings from OCaml types to R1CS variables and constraints. *)
   and Typ :
     (Typ_intf
-      with type field := Field.Constant.t
-       and type field_var := Field.t
+      with type field := Internal_Basic.field
+       and type field_var := Internal_Basic.Field.Var.t
        and type _ checked_unit := unit Internal_Basic.Checked.t
-       and type _ checked := unit)
+       and type ('var, 'value, 'aux) typ' =
+        ('var, 'value, 'aux) Internal_Basic.Typ.typ'
+       and type ('var, 'value) typ = ('var, 'value) Internal_Basic.Typ.typ
+       and type 'a prover_value = 'a Internal_Basic.Typ.prover_value)
 
   (** Representation of booleans within a field.
 
@@ -1228,12 +1225,7 @@ module type Run_basic = sig
   and Internal_Basic :
     (Basic
       with type field = field
-       and type 'a Checked.t = ('a, field) Checked_runner.t
-       and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
-        ('var, 'value, 'aux, 'field, 'checked) Typ.typ'
-       and type ('var, 'value, 'field, 'checked) Typ.typ =
-        ('var, 'value, 'field, 'checked) Typ.typ
-       and type 'a Typ.prover_value = 'a Typ.prover_value)
+       and type 'a Checked.t = ('a, field) Checked_runner.t)
 
   module Bitstring_checked : sig
     type t = Boolean.var list
diff --git a/src/base/typ.ml b/src/base/typ.ml
index 42afadb8b..b5228c380 100644
--- a/src/base/typ.ml
+++ b/src/base/typ.ml
@@ -44,9 +44,9 @@ module Make
     (Types : Types.Types)
     (Checked : Checked_monad with module Types := Types) =
 struct
-  type ('var, 'value, 'field) t = ('var, 'value, 'field) Types.Typ.t
+  type ('var, 'value) t = ('var, 'value) Types.Typ.t
 
-  type ('var, 'value, 'field) typ = ('var, 'value, 'field) t
+  type ('var, 'value) typ = ('var, 'value) t
 
   module type S = sig
     type field
@@ -60,15 +60,14 @@ struct
 
   module T = struct
     module Data_spec = struct
-      type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t =
+      type ('r_var, 'r_value, 'k_var, 'k_value) t =
         | ( :: ) :
-            ('var, 'value, 'field) typ
-            * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t
-            -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t
-        | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t
+            ('var, 'value) typ * ('r_var, 'r_value, 'k_var, 'k_value) t
+            -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value) t
+        | [] : ('r_var, 'r_value, 'r_var, 'r_value) t
     end
 
-    let unit () : (unit, unit, 'field) t =
+    let unit () : (unit, unit) t =
       Typ
         { var_to_fields = (fun () -> ([||], ()))
         ; var_of_fields = (fun _ -> ())
@@ -79,7 +78,7 @@ struct
         ; check = (fun () -> Checked.return ())
         }
 
-    let field () : ('field Cvar.t, 'field, 'field) t =
+    let field () : ('field_var, 'field) t =
       Typ
         { var_to_fields = (fun f -> ([| f |], ()))
         ; var_of_fields = (fun (fields, _) -> fields.(0))
@@ -105,7 +104,7 @@ struct
           }
     end
 
-    let transport (type var value1 value2 field)
+    let transport (type var value1 value2)
         (Typ
            { var_to_fields
            ; var_of_fields
@@ -115,8 +114,8 @@ struct
            ; constraint_system_auxiliary
            ; check
            } :
-          (var, value1, field) t ) ~(there : value2 -> value1)
-        ~(back : value1 -> value2) : (var, value2, field) t =
+          (var, value1) t ) ~(there : value2 -> value1)
+        ~(back : value1 -> value2) : (var, value2) t =
       Typ
         { var_to_fields
         ; var_of_fields
@@ -127,7 +126,7 @@ struct
         ; check
         }
 
-    let transport_var (type var1 var2 value field)
+    let transport_var (type var1 var2 value)
         (Typ
            { var_to_fields
            ; var_of_fields
@@ -137,8 +136,8 @@ struct
            ; constraint_system_auxiliary
            ; check
            } :
-          (var1, value, field) t ) ~(there : var2 -> var1) ~(back : var1 -> var2)
-        : (var2, value, field) t =
+          (var1, value) t ) ~(there : var2 -> var1) ~(back : var1 -> var2) :
+        (var2, value) t =
       Typ
         { var_to_fields = (fun x -> var_to_fields (there x))
         ; var_of_fields = (fun x -> back (var_of_fields x))
@@ -159,8 +158,7 @@ struct
            ; constraint_system_auxiliary
            ; check
            } :
-          ('elt_var, 'elt_value, 'field) t ) :
-        ('elt_var list, 'elt_value list, 'field) t =
+          ('elt_var, 'elt_value) t ) : ('elt_var list, 'elt_value list) t =
       (* NB: We store the size_in_field_elements of each in the auxiliary
          data, to allow for 'reads' of e.g. list of lists of different
          lengths.
@@ -240,12 +238,12 @@ struct
       |> transport_var ~there:Array.to_list ~back:Array.of_list
 
     let hlist (type k_var k_value)
-        (spec0 : (unit, unit, k_var, k_value, 'f) Data_spec.t) :
-        ((unit, k_var) H_list.t, (unit, k_value) H_list.t, 'f) t =
+        (spec0 : (unit, unit, k_var, k_value) Data_spec.t) :
+        ((unit, k_var) H_list.t, (unit, k_value) H_list.t) t =
       let rec go :
           type k_var k_value.
-             (unit, unit, k_var, k_value, 'f) Data_spec.t
-          -> ((unit, k_var) H_list.t, (unit, k_value) H_list.t, 'f) t =
+             (unit, unit, k_var, k_value) Data_spec.t
+          -> ((unit, k_var) H_list.t, (unit, k_value) H_list.t) t =
        fun spec0 ->
         let open H_list in
         match spec0 with
@@ -390,12 +388,12 @@ struct
                         (unit, _ -> _ -> _ -> _ -> _ -> _ -> unit) H_list.t ) ->
              (a, b, c, d, e, f) )
 
-    let of_hlistable (spec : (unit, unit, 'k_var, 'k_value, 'f) Data_spec.t)
+    let of_hlistable (spec : (unit, unit, 'k_var, 'k_value) Data_spec.t)
         ~(var_to_hlist : 'var -> (unit, 'k_var) H_list.t)
         ~(var_of_hlist : (unit, 'k_var) H_list.t -> 'var)
         ~(value_to_hlist : 'value -> (unit, 'k_value) H_list.t)
         ~(value_of_hlist : (unit, 'k_value) H_list.t -> 'value) :
-        ('var, 'value, 'f) t =
+        ('var, 'value) t =
       hlist spec
       |> transport ~there:value_to_hlist ~back:value_of_hlist
       |> transport_var ~there:var_to_hlist ~back:var_of_hlist
diff --git a/src/base/types.ml b/src/base/types.ml
index ec1d584e5..37344c3ae 100644
--- a/src/base/types.ml
+++ b/src/base/types.ml
@@ -21,18 +21,19 @@ module Provider = struct
 end
 
 module type Types = sig
+  type field
+
+  type field_var
+
   module Checked : sig
     type 'a t
   end
 
   module Typ : sig
-    (** The type [('var, 'value, 'field, 'checked) t] describes a mapping from
+    (** The type [('var, 'value) t] describes a mapping from
       OCaml types to the variables and constraints they represent:
       - ['value] is the OCaml type
-      - ['field] is the type of the field elements
-      - ['var] is some other type that contains some R1CS variables
-      - ['checked] is the type of checked computation that verifies the stored
-        contents as R1CS variables.
+      - ['var] is some other type that contains some R1CS variables.
 
       For convenience and readability, it is usually best to have the ['var]
       type mirror the ['value] type in structure, for example:
@@ -47,22 +48,20 @@ module type Types = sig
     let or (x : t) = Snark.Boolean.(x.b1 || x.b2)
   end
 ]}*)
-    type ('var, 'value, 'aux, 'field, 'checked) typ' =
-      { var_to_fields : 'var -> 'field Cvar.t array * 'aux
-      ; var_of_fields : 'field Cvar.t array * 'aux -> 'var
-      ; value_to_fields : 'value -> 'field array * 'aux
-      ; value_of_fields : 'field array * 'aux -> 'value
+    type ('var, 'value, 'aux) typ' =
+      { var_to_fields : 'var -> field_var array * 'aux
+      ; var_of_fields : field_var array * 'aux -> 'var
+      ; value_to_fields : 'value -> field array * 'aux
+      ; value_of_fields : field array * 'aux -> 'value
       ; size_in_field_elements : int
       ; constraint_system_auxiliary : unit -> 'aux
-      ; check : 'var -> 'checked
+      ; check : 'var -> unit Checked.t
       }
 
-    type ('var, 'value, 'field, 'checked) typ =
-      | Typ :
-          ('var, 'value, 'aux, 'field, 'checked) typ'
-          -> ('var, 'value, 'field, 'checked) typ
+    type ('var, 'value) typ =
+      | Typ : ('var, 'value, 'aux) typ' -> ('var, 'value) typ
 
-    type ('var, 'value, 'f) t = ('var, 'value, 'f, unit Checked.t) typ
+    type ('var, 'value) t = ('var, 'value) typ
   end
 
   module As_prover : sig
@@ -77,23 +76,28 @@ module type Types = sig
 end
 
 module Make_types (Minimal : sig
+  type field
+
+  type field_var
+
   type 'a checked
 
   type 'a as_prover
 end) =
 struct
+  type field = Minimal.field
+
+  type field_var = Minimal.field_var
+
   module Checked = struct
     type 'a t = 'a Minimal.checked
   end
 
   module Typ = struct
-    (** The type [('var, 'value, 'field, 'checked) t] describes a mapping from
+    (** The type [('var, 'value) t] describes a mapping from
       OCaml types to the variables and constraints they represent:
       - ['value] is the OCaml type
-      - ['field] is the type of the field elements
-      - ['var] is some other type that contains some R1CS variables
-      - ['checked] is the type of checked computation that verifies the stored
-        contents as R1CS variables.
+      - ['var] is some other type that contains some R1CS variables.
 
       For convenience and readability, it is usually best to have the ['var]
       type mirror the ['value] type in structure, for example:
@@ -108,22 +112,20 @@ struct
     let or (x : t) = Snark.Boolean.(x.b1 || x.b2)
   end
 ]}*)
-    type ('var, 'value, 'aux, 'field, 'checked) typ' =
-      { var_to_fields : 'var -> 'field Cvar.t array * 'aux
-      ; var_of_fields : 'field Cvar.t array * 'aux -> 'var
-      ; value_to_fields : 'value -> 'field array * 'aux
-      ; value_of_fields : 'field array * 'aux -> 'value
+    type ('var, 'value, 'aux) typ' =
+      { var_to_fields : 'var -> field_var array * 'aux
+      ; var_of_fields : field_var array * 'aux -> 'var
+      ; value_to_fields : 'value -> field array * 'aux
+      ; value_of_fields : field array * 'aux -> 'value
       ; size_in_field_elements : int
       ; constraint_system_auxiliary : unit -> 'aux
-      ; check : 'var -> 'checked
+      ; check : 'var -> unit Checked.t
       }
 
-    type ('var, 'value, 'field, 'checked) typ =
-      | Typ :
-          ('var, 'value, 'aux, 'field, 'checked) typ'
-          -> ('var, 'value, 'field, 'checked) typ
+    type ('var, 'value) typ =
+      | Typ : ('var, 'value, 'aux) typ' -> ('var, 'value) typ
 
-    type ('var, 'value, 'f) t = ('var, 'value, 'f, unit Checked.t) typ
+    type ('var, 'value) t = ('var, 'value) typ
   end
 
   module As_prover = struct
diff --git a/src/base/utils.ml b/src/base/utils.ml
index 0522b4ff1..944edeb91 100644
--- a/src/base/utils.ml
+++ b/src/base/utils.ml
@@ -6,7 +6,9 @@ let set_eval_constraints b = Runner.eval_constraints := b
 
 module Make
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with type field = Backend.Field.t
                  with module Types := Types)
@@ -17,11 +19,9 @@ module Make
              with type field := Backend.Field.t
               and type field_var := Backend.Cvar.t
               and type 'field checked_unit := unit Types.Checked.t
-              and type _ checked := unit Checked.t
-              and type ('var, 'value, 'aux, 'field, 'checked) typ' :=
-               ('var, 'value, 'aux, 'field, 'checked) Types.Typ.typ'
-              and type ('var, 'value, 'field, 'checked) typ :=
-               ('var, 'value, 'field, 'checked) Types.Typ.typ)
+              and type ('var, 'value, 'aux) typ' :=
+               ('var, 'value, 'aux) Types.Typ.typ'
+              and type ('var, 'value) typ := ('var, 'value) Types.Typ.typ)
     (Runner : Runner.S
                 with module Types := Types
                 with type field := Backend.Field.t
diff --git a/src/base/utils.mli b/src/base/utils.mli
index d056b1c64..0fa8633eb 100644
--- a/src/base/utils.mli
+++ b/src/base/utils.mli
@@ -5,7 +5,9 @@ val set_eval_constraints : bool -> unit
 
 module Make : functor
   (Backend : Backend_extended.S)
-  (Types : Types.Types)
+  (Types : Types.Types
+             with type field = Backend.Field.t
+              and type field_var = Backend.Cvar.t)
   (Checked : Checked_intf.Extended
                with type field = Backend.Field.t
                with module Types := Types)
@@ -16,11 +18,9 @@ module Make : functor
            with type field := Backend.Field.t
             and type field_var := Backend.Cvar.t
             and type 'field checked_unit := unit Types.Checked.t
-            and type 'a checked := 'a Checked.t
-            and type ('var, 'value, 'aux, 'field, 'checked) typ' :=
-             ('var, 'value, 'aux, 'field, 'checked) Types.Typ.typ'
-            and type ('var, 'value, 'field, 'checked) typ :=
-             ('var, 'value, 'field, 'checked) Types.Typ.typ)
+            and type ('var, 'value, 'aux) typ' :=
+             ('var, 'value, 'aux) Types.Typ.typ'
+            and type ('var, 'value) typ := ('var, 'value) Types.Typ.typ)
   (Runner : Runner.S
               with module Types := Types
               with type field := Backend.Field.t