Subtyping inference for inductoves and records

Also reinferred after sections discharge

5 files changed, 114 insertions, 69 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d8252ea9b..1f8600dc2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -655,3 +655,68 @@ let control_only_guard env c =
     iter_constr_with_full_binders push_rel iter env c
   in
   iter env c
+
+(* inference of subtyping condition for inductive types *)
+
+let infer_inductive_subtyping_arity_constructor
+  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
+  let update_contexts (env, evd, csts) csts' =
+    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
+  in
+  let basic_check (env, evd, csts) tp =
+    let csts' =
+      Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+    in update_contexts (env, evd, csts) csts'
+  in
+  let infer_typ typ ctxs =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try
+           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
+         with Reduction.NotConvertible -> 
+           anomaly ~label:"inference of record/inductive subtyping relation failed"
+             (Pp.str "Can't infer subtyping for record/inductive type")
+       end
+     | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = Reduction.dest_prod env arcn in
+  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
+  if not is_arity then basic_check last_contexts codom else last_contexts
+
+let infer_inductive_subtyping env evd mind_ent =
+  let { Entries.mind_entry_inds = entries;
+        Entries.mind_entry_polymorphic = poly;
+        Entries.mind_entry_universes = ground_uinfind;
+      } = mind_ent
+  in
+  let uinfind =
+    if poly then
+    begin
+      let uctx = Univ.UInfoInd.univ_context ground_uinfind in
+      let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
+      let dosubst = subst_univs_level_constr sbsubst in
+      let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+      let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+      let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+      let env' = Environ.push_context uctx env in
+      let env' = Environ.push_context uctx_other env' in
+      let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
+      let (_, _, subtyp_constraints) =
+        List.fold_left
+         (fun ctxs indentry ->
+            let ctxs' = infer_inductive_subtyping_arity_constructor
+                          ctxs dosubst indentry.Entries.mind_entry_arity true
+            in
+            List.fold_left
+             (fun ctxs cons ->
+                infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
+             ctxs' indentry.Entries.mind_entry_lc
+         ) (env', evd', Univ.Constraint.empty) entries
+      in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
+           Univ.UContext.make
+             (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
+               subtyp_constraints))
+    end
+    else ground_uinfind
+  in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index bdb6f996b..7d89b1b2b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,3 +199,8 @@ val type_of_inductive_knowing_conclusion :
 
 (********************)
 val control_only_guard : env -> types -> unit
+
+(* inference of subtyping condition for inductive types *)
+
+val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
+  Entries.mutual_inductive_entry
diff --git a/vernac/command.ml b/vernac/command.ml
index b23eb9e6b..35b75370e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,32 +573,6 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
-let infer_inductive_subtyping_arity_constructor
-  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
-  let update_contexts (env, evd, csts) csts' =
-    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
-  in
-  let basic_check (env, evd, csts) tp =
-    let csts' =
-      Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
-    in update_contexts (env, evd, csts) csts'
-  in
-  let infer_typ typ ctxs =
-   match typ with
-     | LocalAssum (_, typ') ->
-       begin
-         try
-           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
-         with Reduction.NotConvertible -> 
-           anomaly ~label:"inference of record/inductive subtyping relation failed"
-             (Pp.str "Can't infer subtyping for record/inductive type")
-       end
-     | _ -> anomaly (Pp.str "")
-  in
-  let typs, codom = Reduction.dest_prod env arcn in
-  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
-  if not is_arity then basic_check last_contexts codom else last_contexts
-
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -676,41 +650,17 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
   let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
-  let uinfind =
-    let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
-    let dosubst = subst_univs_level_constr sbsubst in
-    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
-    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env' = Environ.push_context uctx env_ar_params in
-    let env' = Environ.push_context uctx_other env' in
-    let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
-    let (_, _, subtyp_constraints) =
-      List.fold_left
-       (fun ctxs indentry ->
-          let ctxs' = infer_inductive_subtyping_arity_constructor
-                        ctxs dosubst indentry.mind_entry_arity true
-          in
-          List.fold_left
-           (fun ctxs cons ->
-              infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
-           ctxs' indentry.mind_entry_lc
-       ) (env', evd', Univ.Constraint.empty) entries
-    in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
-         Univ.UContext.make
-           (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
-             subtyp_constraints))
-  in
   (* Build the mutual inductive entry *)
-  { mind_entry_params = List.map prepare_param ctx_params;
-    mind_entry_record = None;
-    mind_entry_finite = finite;
-    mind_entry_inds = entries;
-    mind_entry_polymorphic = poly;
-    mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uinfind;
-  },
-    pl, impls
+  let mind_ent = 
+    { mind_entry_params = List.map prepare_param ctx_params;
+      mind_entry_record = None;
+      mind_entry_finite = finite;
+      mind_entry_inds = entries;
+      mind_entry_polymorphic = poly;
+      mind_entry_private = if prv then Some false else None;
+      mind_entry_universes = ground_uinfind;
+    }
+  in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 91e126ef1..21ffa4cbf 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -105,17 +105,30 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
-  let univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *)
+  let univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
     | None -> None
   in
-  { mind_entry_record = record;
-    mind_entry_finite = mib.mind_finite;
-    mind_entry_params = params';
-    mind_entry_inds = inds';
-    mind_entry_polymorphic = mib.mind_polymorphic;
-    mind_entry_private = mib.mind_private;
-    mind_entry_universes = univ_info_ind
-  }
+  let mind_ent =
+    { mind_entry_record = record;
+      mind_entry_finite = mib.mind_finite;
+      mind_entry_params = params';
+      mind_entry_inds = inds';
+      mind_entry_polymorphic = mib.mind_polymorphic;
+      mind_entry_private = mib.mind_private;
+      mind_entry_universes = univ_info_ind
+    }
+  in
+  if mib.mind_polymorphic then
+    begin
+      let env = Global.env () in
+      let env' = Environ.push_context univs env in
+      let (env'', typed_params) = Typeops.infer_local_decls env' params' in
+      let evd = Evd.from_env env'' in
+      Inductiveops.infer_inductive_subtyping env'' evd mind_ent
+    end
+  else
+    mind_ent
+
diff --git a/vernac/record.ml b/vernac/record.ml
index 64f5e81d4..84312594d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -405,6 +405,18 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_universes = ctx;
     }
   in
+  let mie =
+    if poly then
+      begin
+        let env = Global.env () in
+        let env' = Environ.push_context (Univ.UInfoInd.univ_context ctx) env in
+        let env'' = Environ.push_rel_context params env' in
+        let evd = Evd.from_env env'' in
+        Inductiveops.infer_inductive_subtyping env'' evd mie
+      end
+    else
+       mie
+  in
   let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in