Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to

one_inductive_body so that when eta-expanding at "match" printing time
we know if a let is part of the expected signature or part of the
body.

This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.

7 files changed, 22 insertions, 7 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index b1e3abbedd..e9e21d30d9 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -43,7 +43,8 @@ type case_printing =
 type case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
+    ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
     ci_pp_info    : case_printing (* not interpreted by the kernel *)
   }
 
@@ -773,6 +774,7 @@ struct
     ci.ci_ind == ci'.ci_ind &&
     Int.equal ci.ci_npar ci'.ci_npar &&
     Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+    Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
     pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
   open Hashset.Combine
   let hash_pp_info info =
@@ -788,8 +790,9 @@ struct
     let h1 = ind_hash ci.ci_ind in
     let h2 = Int.hash ci.ci_npar in
     let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
-    let h4 = hash_pp_info ci.ci_pp_info in
-    combine4 h1 h2 h3 h4
+    let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in
+    let h5 = hash_pp_info ci.ci_pp_info in
+    combine5 h1 h2 h3 h4 h5
 end
 
 module Hcaseinfo = Hashcons.Make(CaseinfoHash)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f2d9ac9f54..82a2de0945 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -25,7 +25,8 @@ type case_printing =
 type case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
+    ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
     ci_pp_info    : case_printing (** not interpreted by the kernel *)
   }
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e6025790a3..1e94e243c0 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -110,6 +110,10 @@ type one_inductive_body = {
  (** Length of the signature of the constructors (with let, w/o params)
     (not used in the kernel) *)
 
+    mind_consnrealargs : int array;
+ (** Length of the signature of the constructors (w/o let, w/o params)
+    (not used in the kernel) *)
+
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
 (** {8 Datas for bytecode compilation } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 214aac5ec0..2defb66f4b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -630,9 +630,12 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     (* Type of constructors in normal form *)
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
-    let consnrealargs =
+    let consnrealdecls =
       Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
 	splayed_lc in
+    let consnrealargs =
+      Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+	splayed_lc in
     (* Elimination sorts *)
     let arkind,kelim = match ar_kind with
       | Inr (param_levels,lev) ->
@@ -668,7 +671,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
-	mind_consnrealdecls = consnrealargs;
+	mind_consnrealdecls = consnrealdecls;
+	mind_consnrealargs = consnrealargs;
 	mind_user_lc = lc;
 	mind_nf_lc = nf_lc;
 	mind_recargs = recarg;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c0857566df..2b2caaf3bf 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -370,7 +370,8 @@ let check_case_info env indsp ci =
   if
     not (eq_ind indsp ci.ci_ind) ||
     not (Int.equal mib.mind_nparams ci.ci_npar) ||
-    not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls)
+    not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
+    not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
diff --git a/kernel/term.ml b/kernel/term.ml
index 44a10aa355..24fe6d9622 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -47,6 +47,7 @@ type case_info = Constr.case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
     ci_cstr_ndecls : int array;
+    ci_cstr_nargs : int array;
     ci_pp_info    : case_printing
   }
 
diff --git a/kernel/term.mli b/kernel/term.mli
index dab1d2ceab..f2f5e8495d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -46,6 +46,7 @@ type case_info = Constr.case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
     ci_cstr_ndecls : int array;
+    ci_cstr_nargs : int array;
     ci_pp_info    : case_printing
   }