diff --git a/client/DeBruijn.ml b/client/DeBruijn.ml
index 6eb3c7497e8629cde8323636f086be44586490b8..16a75ea5a2451f2a6f13f97fa4b6aae2ed24f2c7 100644
--- a/client/DeBruijn.ml
+++ b/client/DeBruijn.ml
@@ -79,21 +79,6 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
     let current = current + 1 in
     { map; current }
 
-  (* [concat env1 env2] extends [env1] with all the bindings of [env2];
-     bindings of [env2] shadow any binding of the same variable in [env1]. *)
-
-  let concat env1 env2 =
-    (* We need to shift the de Bruijn levels of [env2] (and its
-       [current] value) by as many bindings as there are in [env1]. *)
-    let shift _x in1 in2 =
-      match in2 with
-      | None -> in1
-      | Some lvl -> Some (env1.current + lvl)
-    in
-    {
-      current = env1.current + env2.current;
-      map = M.merge shift env1.map env2.map;
-    }
 end
 
 (* -------------------------------------------------------------------------- *)
diff --git a/client/DeBruijn.mli b/client/DeBruijn.mli
index 0c3e76106a8254f90f679b5471fe68dea7d39e48..7b85c2871af45dfdba6c9afb66cc805733e7ce46 100644
--- a/client/DeBruijn.mli
+++ b/client/DeBruijn.mli
@@ -49,11 +49,6 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
      to [slide (bump env) x]. *)
 
   val bump: env -> env
-
-  (* [concat env1 env2] extends [env1] with all the bindings of [env2];
-     bindings of [env2] shadow any binding of the same variable in [env1]. *)
-
-  val concat: env -> env -> env
 end
 
 (* -------------------------------------------------------------------------- *)
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 6084e76e23f0589c5ffba7e88e9e7b36297b12d9..18582366cdece785d5b924018aa1c7f217ee4ce4 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -117,6 +117,11 @@ let extend_with_tevar { types; names; equations } x ty =
     names = N2DB.slide names x;
     equations; }
 
+let extend_with_tevar_no_dup ({ types; _ } as env) x ty =
+  if TermVarMap.mem x types then
+    raise (TypeError (TwoOccurencesOfSameVariable x));
+  extend_with_tevar env x ty
+
 let extend_with_tyvar { types; names; equations } =
   match equations with
   | Inconsistent ->
@@ -130,41 +135,6 @@ let extend_with_tyvar { types; names; equations } =
      let names = N2DB.bump names in
      { types; names ; equations = Equations { store ; tyvars } }
 
-let singleton x ty =
-  extend_with_tevar empty x ty
-
-let concat env1 env2 =
-  let combine _ _ ty2 = Some ty2 in
-  let types = TermVarMap.union combine env1.types env2.types in
-  let names = N2DB.concat env1.names env2.names in
-  match (env1.equations, env2.equations) with
-  | Inconsistent,_ | _, Inconsistent ->
-     { types; names; equations = Inconsistent }
-  | Equations { store = store1; tyvars = tyvars1 },
-    Equations { store = store2; tyvars = tyvars2 } ->
-     assert (store1 == store2);
-     let store = store1 in
-     let tyvars = tyvars1 @ tyvars2 in
-     { types; names; equations = Equations { store; tyvars} }
-
-let concat_disjoint env1 env2 =
-  let exception Conflict of TermVarMap.key in
-  try
-    let combine x _ _ =
-      raise (Conflict x) in
-    let types = TermVarMap.union combine env1.types env2.types in
-    let names = N2DB.concat env1.names env2.names in
-    match (env1.equations, env2.equations) with
-    | Inconsistent,_ | _, Inconsistent ->
-       Ok { types; names; equations = Inconsistent }
-    | Equations { store = store1; tyvars = tyvars1 },
-      Equations { store = store2; tyvars = tyvars2 } ->
-       assert (store1 == store2);
-       let store = store1 in
-       let tyvars = tyvars1 @ tyvars2 in
-       Ok { types; names; equations = Equations { store; tyvars } }
-  with Conflict x -> Error x
-
 (* -------------------------------------------------------------------------- *)
 
 (* Destructors. *)
@@ -483,34 +453,30 @@ and typeof_variant datatype_env lbl (tid, tyargs) =
     Type.subst ty 0 arg_type
   ) tyargs type_params arg_type
 
-and typeof_branch datatype_env env scrutinee_ty (pat, rhs) =
-  let new_bindings = binding_pattern datatype_env env scrutinee_ty pat in
-  let new_env = concat env new_bindings in
+and typeof_branch datatype_env env scrutinee_ty (pat, rhs) : debruijn_type =
+  let new_env = binding_pattern datatype_env env scrutinee_ty pat in
   typeof datatype_env new_env rhs
 
-and binding_pattern datatype_env env scrutinee_ty pat =
-  let binding_pattern = binding_pattern datatype_env env in
+and binding_pattern datatype_env env scrutinee_ty pat : env =
+  let binding_pattern = binding_pattern datatype_env in
   match pat with
   | PVar (_, x) ->
-      singleton x scrutinee_ty
+      extend_with_tevar_no_dup env x scrutinee_ty
   | PWildcard _ ->
-      empty
+      env
   | PAnnot (_, pat, ty) ->
       enforce_equal env scrutinee_ty ty;
-      binding_pattern ty pat
+      binding_pattern env ty pat
   | PTuple (_, ps) ->
       let tys = as_product scrutinee_ty in
-      let envs = List.map2 binding_pattern tys ps in
-      let f env1 env2 =
-        match concat_disjoint env1 env2 with
-        | Ok env -> env
-        | Error x -> raise (TypeError (TwoOccurencesOfSameVariable x))
-      in
-      List.fold_left f empty envs
+      if List.length ps <> List.length tys then
+        raise
+          (TypeError (ArityMismatch (Total (List.length ps), scrutinee_ty)));
+      List.fold_left2 binding_pattern env tys ps
   | PVariant (_, lbl, dty, pat) ->
       let arg_type = typeof_variant datatype_env lbl dty in
       enforce_equal env scrutinee_ty (TyConstr dty);
-      binding_pattern arg_type pat
+      binding_pattern env arg_type pat
 
 let typeof datatype_env t =
   typeof datatype_env empty t