diff --git a/lambda/translcore.ml b/lambda/translcore.ml
index 9d6db3318..6ce621326 100644
--- a/lambda/translcore.ml
+++ b/lambda/translcore.ml
@@ -133,7 +133,7 @@ let rec push_defaults loc bindings cases partial =
       let exp =
         let cases =
           let pure_case ({c_lhs; _} as case) =
-            {case with c_lhs = {c_lhs with pat_desc = Tpat_value c_lhs}} in
+            {case with c_lhs = as_computation_pattern c_lhs} in
           List.map pure_case cases in
         { exp with exp_loc = loc; exp_env = env; exp_desc =
           Texp_match
diff --git a/typing/typecore.ml b/typing/typecore.ml
index d1c600909..e5129600d 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1181,7 +1181,7 @@ let pure
   = fun category pat ->
   match category with
   | Value -> pat
-  | Computation -> { pat with pat_desc = Tpat_value pat }
+  | Computation -> as_computation_pattern pat
 
 let only_impure
   : type k . k pattern_category ->
@@ -1199,7 +1199,7 @@ let as_comp_pattern
              k general_pattern -> computation general_pattern
   = fun category pat ->
   match category with
-  | Value -> { pat with pat_desc = Tpat_value pat }
+  | Value -> as_computation_pattern pat
   | Computation -> pat
 
 (* type_pat propagates the expected type as well as maps for
diff --git a/typing/typedtree.ml b/typing/typedtree.ml
index 002190b3a..6a6319a97 100644
--- a/typing/typedtree.ml
+++ b/typing/typedtree.ml
@@ -613,6 +613,16 @@ and 'a class_infos =
 
 (* Auxiliary functions over the a.s.t. *)
 
+let as_computation_pattern (p : pattern) : computation general_pattern =
+  {
+    pat_desc = Tpat_value p;
+    pat_loc = p.pat_loc;
+    pat_extra = [];
+    pat_type = p.pat_type;
+    pat_env = p.pat_env;
+    pat_attributes = [];
+  }
+
 let rec classify_pattern_desc : type k . k pattern_desc -> k pattern_category =
   function
   | Tpat_alias _ -> Value
diff --git a/typing/typedtree.mli b/typing/typedtree.mli
index 3cdc1ab0c..9c25e18d8 100644
--- a/typing/typedtree.mli
+++ b/typing/typedtree.mli
@@ -120,7 +120,15 @@ and 'k pattern_desc =
   | Tpat_value : value general_pattern -> computation pattern_desc
         (** P
 
-            Invariant: TODO
+            Invariant: Tpat_value pattern should not carry
+            pat_attributes or pat_extra metadata coming from user
+            syntax, which must be on the inner pattern node -- to
+            facilitate searching for a certain value pattern
+            constructor with a specific attributed.
+
+            To enforce this restriction it suffices to use the
+            [as_computation_pattern] function below instead of the
+            [Tpat_value] constructor directly.
          *)
   | Tpat_exception : value general_pattern -> computation pattern_desc
         (** exception P *)
@@ -743,6 +751,12 @@ and 'a class_infos =
 
 (* Auxiliary functions over the a.s.t. *)
 
+(** [as_computation_pattern p] is a computation pattern with description
+    [Tpat_value p], which enforces a correct placement of pat_attributes
+    and pat_extra metadata (on the inner value pattern, rather than on
+    the computation pattern). *)
+val as_computation_pattern: pattern -> computation general_pattern
+
 val classify_pattern_desc: 'k pattern_desc -> 'k pattern_category
 val classify_pattern: 'k general_pattern -> 'k pattern_category