Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"

4 files changed, 28 insertions, 14 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 884a1ef18c..15b1f0a0c6 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -484,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
 let eq_recarg r1 r2 = match r1, r2 with
   | Norec, Norec -> true
-  | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-  | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
+  | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2
+  | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2
   | _ -> false
 
 let eq_wf_paths = Rtree.equal eq_recarg
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index bb0db8cfe9..4de5977666 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -502,10 +502,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
       indlc
   in mk_paths (Mrec ind) irecargs
 
+let prrecarg = function
+  | Norec -> str "Norec"
+  | Mrec (mind,i) ->
+     str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+  | Imbr (mind,i) ->
+     str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+
 let check_subtree t1 t2 =
   let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in
   if not (Rtree.equiv eq_recarg cmp_labels t1 t2)
-  then failwith "bad recursive trees"
+  then user_err Pp.(str "Bad recursive tree: found " ++ fnl ()
+    ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl ()
+    ++ Rtree.pp_tree prrecarg t2)
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
 let check_positivity env_ar mind params nrecp inds =
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 22353ec168..8d426a3c05 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -381,7 +381,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) ||
+    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)
@@ -435,20 +435,14 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let eq_recarg r1 r2 = match r1, r2 with
-| Norec, Norec -> true
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
-
 let eq_wf_paths = Rtree.equal eq_recarg
 
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
 | Imbr i1, Imbr i2
-| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None
-| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None
+| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None
 | _ -> None
 
 let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec
@@ -544,7 +538,7 @@ let lookup_subterms env ind =
 
 let match_inductive ind ra =
   match ra with
-    | (Mrec i | Imbr i) -> eq_ind ind i
+    | (Mrec i | Imbr i) -> eq_ind_chk ind i
     | Norec -> false
 
 (* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -645,7 +639,7 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-	     | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+             | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' ->
 			   build_recargs_nested ienv tree (ind_kn, largs)
 	     | _ -> mk_norec
        end
diff --git a/test-suite/coqchk/include.v b/test-suite/coqchk/include.v
new file mode 100644
index 0000000000..6232c1b80f
--- /dev/null
+++ b/test-suite/coqchk/include.v
@@ -0,0 +1,11 @@
+(* See https://github.com/coq/coq/issues/5747 *)
+Module Type S.
+End S.
+
+Module N.
+Inductive I := .
+End N.
+
+Module M : S.
+  Include N.
+End M.