Be compatible with variable relevance inductives

interp/impargs.ml

@@ -472,7 +472,7 @@ let compute_mib_implicits flags kn =
         (fun i mip ->
           (* No need to care about constraints here *)
           let ty, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef (kn,i)) in
-          let r = Inductive.relevance_of_inductive env (kn,i) in
+          let r = (snd @@ Inductive.lookup_mind_specif env (kn,i)).mind_relevance in
           Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty))
         mib.mind_packets) in
   let env_ar = Environ.push_rel_context ar env in

kernel/cClosure.ml

@@ -799,7 +799,7 @@ let inductive_subst mib u pms =
   mk_pms (Array.length pms - 1) mib.mind_params_ctxt, u
 
 (* Iota-reduction: feed the arguments of the constructor to the branch *)
-let get_branch infos depth ci u pms (ind, c) br e args =
+let get_branch infos depth ci pms ((ind, c), u) br e args =
   let i = c - 1 in
   let args = drop_parameters depth ci.ci_npar args in
   let (_nas, br) = br.(i) in
@@ -1240,9 +1240,11 @@ let rec skip_irrelevant_stack info stk = match stk with
   let () = update m mk_irrelevant.mark mk_irrelevant.term in
   skip_irrelevant_stack info s
 
-let is_irrelevant_constructor infos (ind,_) = match infos.i_cache.i_mode with
-| Conversion -> Indset_env.mem ind infos.i_cache.i_env.irr_inds
-| Reduction -> false
+let is_irrelevant_constructor infos ((ind,_),u) =
+  match Indmap_env.find_opt ind (info_env infos).Environ.irr_inds with
+  | None -> false
+  | Some r ->
+    is_irrelevant infos @@ UVars.subst_instance_relevance u r
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -1361,14 +1363,15 @@ let rec knr info tab m stk =
             (* Similarly to fix, partially applied primitives are not Ntrl! *)
             (m, stk)
         | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk)))
-  | FConstruct(c,_u) ->
+  | FConstruct c ->
      let use_match = red_set info.i_flags fMATCH in
      let use_fix = red_set info.i_flags fFIX in
      if use_match || use_fix then
       (match [@ocaml.warning "-4"] strip_update_shift_app m stk with
-        | (depth, args, ZcaseT(ci,u,pms,_,br,e)::s) when use_match ->
+        | (depth, args, ZcaseT(ci,_,pms,_,br,e)::s) when use_match ->
             assert (ci.ci_npar>=0);
-            let (br, e) = get_branch info depth ci u pms c br e args in
+            (* instance on the case and instance on the constructor are compatible by typing *)
+            let (br, e) = get_branch info depth ci pms c br e args in
             knit info tab e br s
         | (_, cargs, Zfix(fx,par)::s) when use_fix ->
             let rarg = fapp_stack(m,cargs) in

kernel/environ.ml

@@ -83,7 +83,7 @@ type env = {
   env_universes_lbound : UGraph.Bound.t;
   env_qualities : Sorts.QVar.Set.t;
   irr_constants : Sorts.relevance Cmap_env.t;
-  irr_inds : Indset_env.t;
+  irr_inds : Sorts.relevance Indmap_env.t;
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
 }
@@ -113,7 +113,7 @@ let empty_env = {
   env_universes_lbound = UGraph.Bound.Set;
   env_qualities = Sorts.QVar.Set.empty;
   irr_constants = Cmap_env.empty;
-  irr_inds = Indset_env.empty;
+  irr_inds = Indmap_env.empty;
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
 }
@@ -644,8 +644,8 @@ let add_mind_key kn (mind, _ as mind_key) env =
       Globals.inductives = new_inds; }
   in
   let irr_inds = Array.fold_left_i (fun i irr_inds mip ->
-      if mip.mind_relevance == Sorts.Irrelevant
-      then Indset_env.add (kn, i) irr_inds
+      if mip.mind_relevance != Sorts.Relevant
+      then Indmap_env.add (kn, i) mip.mind_relevance irr_inds
       else irr_inds) env.irr_inds mind.mind_packets
   in
   { env with irr_inds; env_globals = new_globals }

kernel/environ.mli

@@ -74,8 +74,11 @@ type env = private {
   env_universes : UGraph.t;
   env_universes_lbound : UGraph.Bound.t;
   env_qualities : Sorts.QVar.Set.t;
-  irr_constants : Sorts.relevance Cmap_env.t;
-  irr_inds : Indset_env.t;
+  irr_constants : Sorts.relevance Cmap_env.t
+(** [irr_constants] is a cache of the relevances which are not Relevant.
+    In other words, [const_relevance == Option.default Relevant (find_opt con irr_constants)]. *);
+  irr_inds : Sorts.relevance Indmap_env.t
+(** [irr_inds] is a cache of the relevances which are not Relevant. cf [irr_constants]. *);
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
 }

kernel/indtypes.ml

@@ -160,7 +160,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive specif in
   let env' =
-    let r = (snd (fst specif)).mind_relevance in
+    let r = Inductive.relevance_of_ind_body (snd (fst specif)) u in
     let anon = Context.make_annot Anonymous r in
     let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
     push_rel decl env in

kernel/inductive.ml

@@ -216,9 +216,12 @@ let instantiate_universes ctx (templ, ar) args =
 
 (* Type of an inductive type *)
 
-let relevance_of_inductive env ind =
+let relevance_of_ind_body mip u =
+  UVars.subst_instance_relevance u mip.mind_relevance
+
+let relevance_of_inductive env (ind,u) =
   let _, mip = lookup_mind_specif env ind in
-  mip.mind_relevance
+  relevance_of_ind_body mip u
 
 let check_instance mib u =
   if not (match mib.mind_universes with
@@ -352,7 +355,7 @@ let expand_arity (mib, mip) (ind, u) params nas =
     let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
     mkApp (mkIndU (ind, u), args)
   in
-  let na = Context.make_annot Anonymous mip.mind_relevance in
+  let na = Context.make_annot Anonymous (relevance_of_ind_body mip u)  in
   let realdecls = LocalAssum (na, self) :: realdecls in
   instantiate_context u params nas realdecls
 
@@ -722,7 +725,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind mip env =
-    let r = mip.mind_relevance in
+    let r = relevance_of_ind_body mip u in
     let anon = Context.make_annot Anonymous r in
     let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,mip),u)) lpar) in
     push_rel decl env
@@ -1430,16 +1433,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
             else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody
     in
-    let ((ind, _), _) as res = check_occur fixenv 1 def in
+    let ((ind, u), _) as res = check_occur fixenv 1 def in
     let _, mip = lookup_mind_specif env ind in
     (* recursive sprop means non record with projections -> squashed *)
-    if mip.mind_relevance == Sorts.Irrelevant &&
-       not (Environ.is_type_in_type env (GlobRef.IndRef ind))
-    then
-      begin
-        if not (names.(i).Context.binder_relevance == Sorts.Irrelevant)
-        then raise_err env i FixpointOnIrrelevantInductive
-      end;
+    let () =
+      if Environ.is_type_in_type env (GlobRef.IndRef ind) then ()
+      else match relevance_of_ind_body mip u with
+        | Sorts.Irrelevant | Sorts.RelevanceVar _ ->
+          (* XXX if RelevanceVar also allow binder_relevance = the same var? *)
+          if not (names.(i).Context.binder_relevance == Sorts.Irrelevant)
+          then raise_err env i FixpointOnIrrelevantInductive
+        | Sorts.Relevant -> ()
+    in
     res
   in
   (* Do it on every fixpoint *)

kernel/inductive.mli

@@ -55,7 +55,9 @@ val constrained_type_of_inductive : mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters :
   mind_specif puniverses -> param_univs -> types constrained
 
-val relevance_of_inductive : env -> inductive -> Sorts.relevance
+val relevance_of_ind_body : one_inductive_body -> UVars.Instance.t -> Sorts.relevance
+
+val relevance_of_inductive : env -> pinductive -> Sorts.relevance
 
 val type_of_inductive : mind_specif puniverses -> types
 

kernel/relevanceops.ml

@@ -28,10 +28,8 @@ let relevance_of_constant env (c,u) =
   let decl = lookup_constant c env in
   UVars.subst_instance_relevance u decl.const_relevance
 
-let relevance_of_constructor env (((mi,i),_),u) =
-  let decl = lookup_mind mi env in
-  let packet = decl.mind_packets.(i) in
-  UVars.subst_instance_relevance u packet.mind_relevance
+let relevance_of_constructor env ((ind,_),u) =
+  Inductive.relevance_of_inductive env (ind,u)
 
 let relevance_of_projection_repr env (p, u) =
   let mib = lookup_mind (Names.Projection.Repr.mind p) env in

pretyping/cases.ml

@@ -1979,7 +1979,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
-          let ((ind,u),_) = dest_ind_family indf' in
+          let ((ind,_ as indu),_) = dest_ind_family indf' in
           let nrealargs_ctxt = inductive_nrealdecls env0 ind in
           let arsign = get_arity env0 indf' in
           let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
@@ -1993,7 +1993,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
                   List.rev realnal
               | None ->
                   List.make nrealargs_ctxt Anonymous in
-          let r = Inductive.relevance_of_inductive env0 ind in
+          let r = Inductive.relevance_of_inductive env0 indu in
           let t = EConstr.of_constr (build_dependent_inductive env0 indf') in
           LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in
   let rec buildrec n = function

pretyping/inductiveops.ml

@@ -74,7 +74,7 @@ let lift_inductive_family n = liftn_inductive_family n 1
 
 let substnl_ind_family l n = map_ind_family (substnl l n)
 
-let relevance_of_inductive_family env ((ind,_),_ : inductive_family) =
+let relevance_of_inductive_family env (ind,_ : inductive_family) =
   Inductive.relevance_of_inductive env ind
 
 type inductive_type = IndType of inductive_family * EConstr.constr list
@@ -430,7 +430,7 @@ let build_dependent_inductive env ((ind, params) as indf) =
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity_signature env sigma dep ((ind,_), _ as indf) =
+let make_arity_signature env sigma dep (ind, _ as indf) =
   let arsign = get_arity env indf in
   let r = Inductive.relevance_of_inductive env ind in
   let anon = make_annot Anonymous r in
@@ -577,7 +577,7 @@ let find_coinductive env sigma c =
 (* Type of Case predicates *)
 let arity_of_case_predicate env (ind,params) dep k =
   let arsign = get_arity env (ind,params) in
-  let r = Inductive.relevance_of_inductive env (fst ind) in
+  let r = Inductive.relevance_of_inductive env ind in
   let mind = build_dependent_inductive env (ind,params) in
   let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in
   Term.it_mkProd_or_LetIn concl arsign

tactics/eqschemes.ml

@@ -204,10 +204,10 @@ let build_sym_scheme env _handle ind =
     get_sym_eq_data env indu in
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in
-  let inds = snd (mind_arity mip) in
+  let inds = inductive_sort_family mip in
   let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in
   let applied_ind = build_dependent_inductive indu specif in
-  let indr = Sorts.relevance_of_sort_family inds in
+  let indr = UVars.subst_instance_relevance u mip.mind_relevance in
   let realsign_ind =
     name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
   let rci = Sorts.Relevant in (* TODO relevance *)
@@ -267,8 +267,8 @@ let build_sym_involutive_scheme env handle ind =
   let eq,eqrefl,ctx = get_coq_eq env ctx in
   let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.instance mkRel n paramsctxt) in
-  let inds = snd (mind_arity mip) in
-  let indr = Sorts.relevance_of_sort_family inds in
+  let inds = inductive_sort_family mip in
+  let indr = UVars.subst_instance_relevance u mip.mind_relevance in
   let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
@@ -383,8 +383,8 @@ let build_l2r_rew_scheme dep env handle ind kind =
     mkApp (mkConstructUi(indu,1),
       Array.concat [Context.Rel.instance mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
-  let inds = snd (mind_arity mip) in
-  let indr = Sorts.relevance_of_sort_family inds in
+  let inds = inductive_sort_family mip in
+  let indr = UVars.subst_instance_relevance u mip.mind_relevance in
   let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in
   let varHC,avoid = fresh env (Id.of_string "HC") avoid in
   let varP,_ = fresh env (Id.of_string "P") avoid in
@@ -501,8 +501,8 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     mkApp (mkConstructUi(indu,1),
       Array.concat [Context.Rel.instance mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
-  let inds = snd (mind_arity mip) in
-  let indr = Sorts.relevance_of_sort_family inds in
+  let inds = inductive_sort_family mip in
+  let indr = UVars.subst_instance_relevance u mip.mind_relevance in
   let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in
   let varHC,avoid = fresh env (Id.of_string "HC") avoid in
   let varP,_ = fresh env (Id.of_string "P") avoid in

tactics/tactics.ml

@@ -1716,7 +1716,7 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) =
           let ci = Inductiveops.make_case_info env ind RegularStyle in
           let br = [| mknas cs_args, b |] in
           let args = Context.Rel.instance mkRel 0 sign in
-          let pnas = Array.append (mknas arity) [|make_annot Anonymous mip.mind_relevance|] in
+          let pnas = Array.append (mknas arity) [|make_annot Anonymous (Inductive.relevance_of_ind_body mip (EConstr.Unsafe.to_instance u))|] in
           let p = (pnas, lift (Array.length pnas) t) in
           let c = mkCase (ci, u, Array.of_list params, (p, get_relevance decl), NoInvert, mkApp (c, args), br) in
           Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)

vernac/record.ml

@@ -476,7 +476,7 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) inhabitant_
   let r = mkIndU (indsp,uinstance) in
   let rp = applist (r, Context.Rel.instance_list mkRel 0 paramdecls) in
   let paramargs = Context.Rel.instance_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = make_annot (Name inhabitant_id) mip.mind_relevance in
+  let x = make_annot (Name inhabitant_id) (Inductive.relevance_of_ind_body mip uinstance) in
   let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in
   let lifted_fields = Vars.lift_rel_context 1 fields in
   let primitive =