Constructor type information uses the expanded form.

It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.

Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.

4 files changed, 15 insertions, 16 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 68626597fc..affed5389f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -514,12 +514,11 @@ let rec cases_pattern_of_glob_constr na c =
   ) c
 
 open Declarations
-open Term
 open Context
 
 (* Keep only patterns which are not bound to a local definitions *)
-let drop_local_defs typi args =
-    let (decls,_) = decompose_prod_assum typi in
+let drop_local_defs params decls args =
+    let decls = List.skipn (Rel.length params) (List.rev decls) in
     let rec aux decls args =
       match decls, args with
       | [], [] -> []
@@ -531,7 +530,7 @@ let drop_local_defs typi args =
          end
       | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
       | _ -> assert false in
-    aux (List.rev decls) args
+    aux decls args
 
 let add_patterns_for_params_remove_local_defs (ind,j) l =
   let (mib,mip) = Global.lookup_inductive ind in
@@ -540,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
     if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
       (* Optimisation *) l
     else
-      let typi = mip.mind_nf_lc.(j-1) in
-      let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
-      drop_local_defs typi l in
+      let (ctx, _) = mip.mind_nf_lc.(j - 1) in
+      drop_local_defs mib.mind_params_ctxt ctx l in
   Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
 let add_alias ?loc na c =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4c02dc0f09..d937456bcb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -101,7 +101,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
   if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
-    substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
+  let (ctx, cty) = specif.(j - 1) in
+  substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx))
 
 (* Number of constructors *)
 
@@ -280,8 +281,7 @@ let make_case_info env ind style =
   let ind_tags =
     Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
-    Array.map2 (fun c n ->
-      let d,_ = decompose_prod_assum c in
+    Array.map2 (fun (d, _) n ->
       Context.Rel.to_tags (List.firstn n d))
       mip.mind_nf_lc mip.mind_consnrealdecls in
   let print_info = { ind_tags; cstr_tags; style } in
@@ -462,7 +462,8 @@ let compute_projections env (kn, i as ind) =
   let pkt = mib.mind_packets.(i) in
   let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
-  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let ctx, cty = pkt.mind_nf_lc.(0) in
+  let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   (* We build a substitution smashing the lets in the record parameters so
      that typechecking projections requires just a substitution and not
@@ -622,9 +623,7 @@ let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
-      (fun c ->
-        Context.Rel.length ((prod_assum c)) -
-        mib.mind_nparams)
+      (fun (d, _) -> List.length d - mib.mind_nparams)
       mip.mind_nf_lc in
   Array.map2 (set_names env sigma) arities brv
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b7090e69da..77ae09ee6f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -107,7 +107,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+  let typ = it_mkProd_or_LetIn typ ctx in
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let nparams = Array.length params in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 083661a64b..ff528bd2cf 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -61,7 +61,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib u typ params =
+let type_constructor mind mib u (ctx, typ) params =
+  let typ = it_mkProd_or_LetIn typ ctx in
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let ctyp = subst_instance_constr u ctyp in