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.

5 files changed, 17 insertions, 10 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 6777e0c223..567850645e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -166,7 +166,7 @@ type one_inductive_body = {
 
     mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
 
-    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
+    mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
  (** Number of expected proper arguments of the constructors (w/o params) *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9e0230c3ba..d56502a095 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -214,7 +214,7 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
@@ -299,9 +299,8 @@ let hcons_ind_arity =
 
 let hcons_mind_packet oib =
   let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
-  let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in
-  (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
-  let nf = if Array.equal (==) user nf then user else nf in
+  let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in
+  let nf = Array.Smart.map map oib.mind_nf_lc in
   { oib with
     mind_typename = Names.Id.hcons oib.mind_typename;
     mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8f06e1e4b8..457c17907e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib =
   let pkt = mib.mind_packets.(i) in
   let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context 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 cty = it_mkProd_or_LetIn cty ctx in
+  let rctx, _ = decompose_prod_assum (substl subst cty) 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
@@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
   (* Check one inductive *)
   let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
     (* Type of constructors in normal form *)
-    let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in
+    let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in
     let consnrealdecls =
       Array.map (fun (d,_) -> Context.Rel.length d)
 	splayed_lc in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 848ae65c51..f4c2483c14 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) =
 
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
-    Array.map (constructor_instantiate kn u mib) specif
+  let map (ctx, c) =
+    let cty = Term.it_mkProd_or_LetIn c ctx in
+    constructor_instantiate kn u mib cty
+  in
+  Array.map map specif
 
 let arities_of_constructors ind specif =
   arities_of_specif (fst (fst ind), snd ind) specif
@@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params =
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
 let build_branches_type (ind,u) (_,mip as specif) params p =
-  let build_one_branch i cty =
+  let build_one_branch i (ctx, c) =
+    let cty = Term.it_mkProd_or_LetIn c ctx in
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
     let (cstrsign,ccl) = Term.decompose_prod_assum typi in
     let nargs = Context.Rel.length cstrsign in
@@ -597,6 +602,7 @@ let lambda_implicit_lift n a =
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
 let abstract_mind_lc ntyps npars lc =
+  let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in
   if Int.equal npars 0 then
     lc
   else
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3c1464c6c9..ad35c16c22 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
 
 val lambda_implicit_lift : int -> constr -> constr
 
-val abstract_mind_lc : int -> Int.t -> constr array -> constr array
+val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array