Allow to name existentials in pattern-matching (ocaml#9584)

smuenzel · Mar 30, 2021 · e0eb793 · e0eb793
1 parent 4cd54ea
commit e0eb793
Show file tree

Hide file tree

Showing 34 changed files with 6,070 additions and 2,298 deletions.
diff --git a/.depend b/.depend
@@ -527,6 +527,7 @@ typing/ctype.cmi : \
     typing/type_immediacy.cmi \
     typing/path.cmi \
     parsing/longident.cmi \
+    parsing/location.cmi \
     typing/ident.cmi \
     typing/env.cmi \
     parsing/asttypes.cmi

diff --git a/Changes b/Changes
@@ -10,6 +10,11 @@ Working version
 
 ### Type system:
 
+- #9584, #7074: Allow to name existentials in pattern-matching
+  One can now write '(Cstr (type a) (x, y : int * a))' to give a name to
+  existentials freshly introduced by GADT constructors.
+  (Jacques Garrigue, review by Leo White and Gabriel Scherer)
+
 - #10174: Make Tsubst more robust by avoiding strange workarounds
   (Takafumi Saikawa and Jacques Garrigue, review by Gabriel Scherer and
    Florian Angeletti)

diff --git a/boot/menhir/parser.ml b/boot/menhir/parser.ml
diff --git a/lambda/matching.ml b/lambda/matching.ml
@@ -1746,12 +1746,12 @@ let divide_constant ctx m =
 (* Matching against a constructor *)
 
 let get_key_constr = function
-  | { pat_desc = Tpat_construct (_, cstr, _) } -> cstr
+  | { pat_desc = Tpat_construct (_, cstr, _, _) } -> cstr
   | _ -> assert false
 
 let get_pat_args_constr p rem =
   match p with
-  | { pat_desc = Tpat_construct (_, _, args) } -> args @ rem
+  | { pat_desc = Tpat_construct (_, _, args, _) } -> args @ rem
   | _ -> assert false
 
 let get_expr_args_constr ~scopes head (arg, _mut) rem =