Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanup of constrintern.ml

Reviewed-by: SkySkimmer
Ack-by: ppedrot

4 files changed, 37 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a793e217d4..d2859b1b4e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of
+      {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+  | WrongNumargInductive of
+      {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
@@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind =
   raise_pattern_matching_error ?loc
     (env, Evd.empty, BadConstructor (cstr,ind))
 
-let error_wrong_numarg_constructor ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n))
+let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+  raise_pattern_matching_error ?loc (env, Evd.empty,
+    WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls})
 
-let error_wrong_numarg_inductive ?loc env c n =
-  raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))
+let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+  raise_pattern_matching_error ?loc (env, Evd.empty,
+    WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls})
 
 let list_try_compile f l =
   let rec aux errors = function
@@ -519,13 +523,18 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
         (* Check the constructor has the right number of args *)
         let ci = cstrs.(i-1) in
         let nb_args_constr = ci.cs_nargs in
-        if Int.equal (List.length args) nb_args_constr then pat
+        let nargs = List.length args in
+        if Int.equal nargs nb_args_constr then pat
         else
           try
             let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
             in DAst.make ?loc @@ PatCstr (cstr, args', alias)
           with NotAdjustable ->
-            error_wrong_numarg_constructor ?loc env cstr nb_args_constr
+            let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in
+            (* In practice, this is already checked at interning *)
+            error_wrong_numarg_constructor ?loc env ~cstr
+              (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr
+              ~expected_ndecls:(nb_args_constr + nlet)
       else
         (* Try to insert a coercion *)
         try
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9a986bc14c..ade1fbf3d3 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,17 +23,21 @@ open Evardefine
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor * int
-  | WrongNumargInductive of inductive * int
+  | WrongNumargConstructor of
+      {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+  | WrongNumargInductive of
+      {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
   | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
   | CannotInferPredicate of (constr * types) array
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor :
+  ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
 
-val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive :
+  ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
 
 val irrefutable : env -> cases_pattern -> bool
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23145b1629..bd875cf68b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) =
 let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
 [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
 
+let inductive_alltags env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags mip.mind_arity_ctxt
+
+let constructor_alltags env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
+
 let constructor_has_local_defs env (indsp,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env indsp in
   let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1e2bba9f73..3705d39280 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int
 val constructor_nrealdecls_env : env -> constructor -> int
 [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
 
+(** @return tags of all decls: true = assumption, false = letin *)
+val inductive_alltags : env -> inductive -> bool list
+val constructor_alltags : env -> constructor -> bool list
+
 (** Is there local defs in params or args ? *)
 val constructor_has_local_defs : env -> constructor -> bool
 val inductive_has_local_defs : env -> inductive -> bool