Merge PR #8665: Fix a few bugs in the checker

3 files changed, 58 insertions, 29 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 0478765a81..50e65ef587 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -310,25 +310,31 @@ let failwith_non_pos_list n ntypes l =
   List.iter (failwith_non_pos n ntypes) l;
   anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
 
-(* Conclusion of constructors: check the inductive type is called with
-   the expected parameters *)
-let check_correct_par (env,n,ntypes,_) hyps l largs =
-  let nparams = rel_context_nhyps hyps in
-  let largs = Array.of_list largs in
-  if Array.length largs < nparams then
-    raise (IllFormedInd (LocalNotEnoughArgs l));
-  let (lpar,largs') = Array.chop nparams largs in
-  let nhyps = List.length hyps in
-  let rec check k index = function
+(* Check the inductive type is called with the expected parameters *)
+(* [n] is the index of the last inductive type in [env] *)
+let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
+  let nparams = rel_context_nhyps paramdecls in
+  let args = Array.of_list args in
+  if Array.length args < nparams then
+    raise (IllFormedInd (LocalNotEnoughArgs ind_index));
+  let (params,realargs) = Array.chop nparams args in
+  let nparamdecls = List.length paramdecls in
+  let rec check param_index paramdecl_index = function
     | [] -> ()
-    | LocalDef _ :: hyps -> check k (index+1) hyps
-    | _::hyps ->
-        match whd_all env lpar.(k) with
-	  | Rel w when w = index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
-  in check (nparams-1) (n-nhyps) hyps;
-  if not (Array.for_all (noccur_between n ntypes) largs') then
-    failwith_non_pos_vect n ntypes largs'
+    | LocalDef _ :: paramdecls ->
+      check param_index (paramdecl_index+1) paramdecls
+    | _::paramdecls ->
+        match whd_all env params.(param_index) with
+          | Rel w when Int.equal w paramdecl_index ->
+            check (param_index-1) (paramdecl_index+1) paramdecls
+          | _ ->
+            let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
+            let err =
+              LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
+            raise (IllFormedInd err)
+  in check (nparams-1) (n-nparamdecls) paramdecls;
+  if not (Array.for_all (noccur_between n ntypes) realargs) then
+    failwith_non_pos_vect n ntypes realargs
 
 (* Arguments of constructor: check the number of recursive parameters nrecp.
     the first parameters which are constant in recursive arguments
@@ -412,8 +418,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
               | Some b ->
 	          check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
 	| Rel k ->
-            (try
-              let (ra,rarg) = List.nth ra_env (k-1) in
+            (try let (ra,rarg) = List.nth ra_env (k-1) in
+            let largs = List.map (whd_all env) largs in
 	      (match ra with
                   Mrec _ -> check_rec_par ienv hyps nrecp largs
 		|  _ -> ());
diff --git a/checker/inductive.ml b/checker/inductive.ml
index d15380643f..5e34f04f51 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
+let is_primitive_record (mib,_) =
+  match mib.mind_record with
+  | PrimRecord _ -> true
+  | NotRecord | FakeRecord -> false
+
 let extended_rel_list n hyps =
   let rec reln l p = function
     | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
@@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c =
 (* Checking the case annotation is relevant *)
 
 let check_case_info env indsp ci =
-  let (mib,mip) = lookup_mind_specif env indsp in
+  let mib, mip as spec = lookup_mind_specif env indsp in
   if
     not (eq_ind_chk indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
-    (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
+    (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
+    is_primitive_record spec
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
@@ -801,10 +807,23 @@ let rec subterm_specif renv stack t =
 	    subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
-      | (Meta _|Evar _) -> Dead_code
-
-      (* Other terms are not subterms *)
-      | _ -> Not_subterm
+    | (Meta _|Evar _) -> Dead_code
+
+    | Proj (p, c) ->
+      let subt = subterm_specif renv stack c in
+      (match subt with
+       | Subterm (_s, wf) ->
+         (* We take the subterm specs of the constructor of the record *)
+         let wf_args = (dest_subterms wf).(0) in
+         (* We extract the tree of the projected argument *)
+         let n = Projection.arg p in
+         spec_of_tree (List.nth wf_args n)
+       | Dead_code -> Dead_code
+       | Not_subterm -> Not_subterm)
+
+    (* Other terms are not subterms *)
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+      | Construct _ | CoFix _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
@@ -856,6 +875,8 @@ let filter_stack_domain env p stack =
     match stack, t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
+      let ctx, a = dest_prod_assum env a in
+      let env = push_rel_context ctx env in
       let ty, args = decompose_app (whd_all env a) in
       let elt = match ty with
       | Ind ind -> 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0916d98ddf..e2c605dde8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -198,9 +198,11 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     assert (Array.length mib2.mind_packets = 1);
     assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
     assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
-    check
-      (fun l1 l2 -> List.equal Name.equal l1 l2)
-      (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+    check (List.equal Name.equal)
+      (fun mib ->
+         let nparamdecls = List.length mib.mind_params_ctxt in
+         let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
+         snd (List.chop nparamdecls names))
   end;
   (* we first check simple things *)
   Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;