Do not create global constraints for applied template polymorphic types

engine/termops.ml

@@ -1096,6 +1096,13 @@ let is_global = EConstr.isRefX
 
 let isGlobalRef = EConstr.isRef
 
+let is_template_polymorphic_ref env sigma f =
+  match EConstr.kind sigma f with
+  | Ind (ind, u) | Construct ((ind, _), u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_ind ind env
+  | _ -> false
+
 let is_template_polymorphic_ind env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) ->

engine/termops.mli

@@ -269,6 +269,7 @@ val is_global : Environ.env -> Evd.evar_map -> GlobRef.t -> constr -> bool
 val isGlobalRef : Evd.evar_map -> constr -> bool
 [@@ocaml.deprecated "(8.12) Use [EConstr.isRef] instead."]
 
+val is_template_polymorphic_ref : env -> Evd.evar_map -> constr -> bool
 val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
 
 val is_Prop : Evd.evar_map -> constr -> bool

kernel/inductive.mli

@@ -52,6 +52,11 @@ type template_univ =
 
 type param_univs = (expected:Univ.Level.t -> template_univ) list
 
+val instantiate_template_constraints
+  : template_univ Univ.Level.Map.t
+  -> Declarations.template_universes
+  -> Univ.Constraints.t
+
 val instantiate_template_universes : mind_specif -> param_univs ->
   Constraints.t * rel_context * template_univ Univ.Level.Map.t
 

pretyping/evarsolve.ml

@@ -160,7 +160,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (* Refresh the types of evars under template polymorphic references *)
   let rec refresh_term_evars ~onevars ~top t =
     match EConstr.kind !evdref t with
-    | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
+    | App (f, args) when Termops.is_template_polymorphic_ref env !evdref f ->
       let pos = get_polymorphic_positions env !evdref f in
         refresh_polymorphic_positions args pos; t
     | App (f, args) when top && isEvar !evdref f ->

pretyping/pretyping.ml

@@ -971,12 +971,12 @@ struct
         else sigma, resj
       | _ -> sigma, resj
     in
-    let rec apply_rec env sigma n body (subs, typ) val_before_bidi candargs bidiargs = function
+    let rec apply_rec env sigma n body (subs, typ) val_before_bidi candargs template bidiargs = function
       | [] ->
         let typ = Vars.esubst Vars.lift_substituend subs typ in
         let body = Coercion.force_app_body body in
         let resj = { uj_val = body; uj_type = typ } in
-        sigma, resj, val_before_bidi, List.rev bidiargs
+        sigma, resj, val_before_bidi, template, List.rev bidiargs
       | c::rest ->
         let bidi = n >= nargs_before_bidi in
         let argloc = loc_of_glob_constr c in
@@ -999,6 +999,24 @@ struct
           in
           sigma, body, na, c1, Esubst.subs_id 0, c2, trace
         in
+        let sigma, template, c1 = match template with
+          | None | Some ([],_) -> sigma, template, c1
+          | Some (None :: t, bound) -> sigma, Some (t,bound), c1
+          | Some (Some u0 :: t, bound) ->
+            (* template arg: type guaranteed to be syntactically an arity
+               we replace the output universe with a fresh one *)
+            let sigma, u = Evd.new_univ_level_variable UState.univ_flexible_alg sigma in
+            let s = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make u in
+            let ctx, _ = destArity sigma c1 in
+            let bound =
+              let u = Univ.Universe.make u in
+              Univ.Level.Map.update u0 (function
+                  | None -> Some u
+                  | Some u' -> Some (Univ.Universe.sup u u'))
+                bound
+            in
+            sigma, Some (t,bound), mkArity (ctx,s)
+        in
         let (sigma, hj), bidiargs =
           if bidi then
             (* We want to get some typing information from the context before
@@ -1025,12 +1043,47 @@ struct
         let subs = Esubst.subs_cons (Vars.make_substituend ujval) subs in
         let body = Coercion.push_arg body ujval in
         let val_before_bidi = if bidi then val_before_bidi else body in
-        apply_rec env sigma (n+1) body (subs, c2) val_before_bidi candargs bidiargs rest
+        apply_rec env sigma (n+1) body (subs, c2) val_before_bidi candargs template bidiargs rest
     in
     let typ = (Esubst.subs_id 0, fj.uj_type) in
     let body = (Coercion.start_app_body sigma fj.uj_val) in
-    let sigma, resj, val_before_bidi, bidiargs =
-      apply_rec env sigma 0 body typ body candargs [] args
+    let template_params, template = match EConstr.kind sigma fj.uj_val with
+      | Ind (ind,u) | Construct ((ind,_),u)
+        when EInstance.is_empty u && Environ.template_polymorphic_ind ind !!env ->
+        let mib = Environ.lookup_mind (fst ind) !!env in
+        let template = match mib.mind_template with
+        | None -> None
+        | Some t ->
+          let map = function Rel.Declaration.LocalAssum (_, t) -> Some t | LocalDef _ -> None in
+          let hyps = List.rev @@ List.map_filter map mib.Declarations.mind_params_ctxt in
+          let get_arity template c =
+            if template then
+              let decls, c = Term.decompose_prod_decls c in
+              match Constr.kind c with
+              | Sort (Sorts.Type u) ->
+                begin match Univ.Universe.level u with
+                | Some l -> Some l
+                | None -> assert false
+                end
+              | _ -> assert false
+            else None
+          in
+          let params = List.map2 get_arity t.Declarations.template_param_arguments hyps in
+          Some (params, Univ.Level.Map.empty)
+        in
+        template, mib.mind_template
+      | _ -> None, None
+    in
+    let sigma, resj, val_before_bidi, template_params, bidiargs =
+      apply_rec env sigma 0 body typ body candargs template_params [] args
+    in
+    let sigma = match template_params, template with
+      | None, None -> sigma
+      | Some _, None | None, Some _ -> assert false
+      | Some (_,bound), Some t ->
+        let bound = Univ.Level.Map.map (fun u -> TemplateUniv u) bound in
+        let csts = Inductive.instantiate_template_constraints bound t in
+        Evd.add_constraints sigma csts
     in
     let sigma, resj = refresh_template env sigma resj in
     let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~flags env sigma resj tycon in

pretyping/retyping.ml

@@ -173,10 +173,10 @@ let retype ?(polyprop=true) sigma =
          subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
-        let t = type_of_global_reference_knowing_parameters env f args in
-        strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
+      if Termops.is_template_polymorphic_ref env sigma f then
+        substituted_type_of_global_reference_knowing_parameters env f args
+      else
         strip_outer_cast sigma
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Proj (p,_,c) ->
@@ -211,6 +211,23 @@ let retype ?(polyprop=true) sigma =
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
     | _ -> decomp_sort env sigma (type_of env t)
 
+  and substituted_type_of_global_reference_knowing_parameters env c args =
+    match EConstr.kind sigma c with
+    | Ind (ind, u) ->
+      let ty = type_of_global_reference_knowing_parameters env c args in
+      strip_outer_cast sigma (subst_type env sigma ty (Array.to_list args))
+    | Construct ((ind, i), u) ->
+      let mib, mip = Inductive.lookup_mind_specif env ind in
+      let ty =
+        if mib.mind_nparams <= Array.length args then
+        (* Fully applied parameters, we do not have to substitute *)
+          EConstr.of_constr mip.mind_user_lc.(i - 1)
+      else
+        type_of_global_reference_knowing_parameters env c args
+      in
+      strip_outer_cast sigma (subst_type env sigma ty (Array.to_list args))
+    | _ -> assert false
+
   and type_of_global_reference_knowing_parameters env c args =
     match EConstr.kind sigma c with
     | Ind (ind, u) ->

pretyping/typing.ml

@@ -32,34 +32,47 @@ let meta_type env evd mv =
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
   meta_instance env evd ty
 
-let make_param_univs env sigma indu spec jl =
-  Array.to_list @@ Array.mapi (fun i j ~expected ->
-      match ESorts.kind sigma @@ Reductionops.sort_of_arity env sigma j.uj_type with
-      | Sorts.SProp | exception Reduction.NotArity ->
-        let indty = EConstr.of_constr @@
-          Inductive.type_of_inductive (spec, Unsafe.to_instance @@ snd indu)
+let fresh_template_context env0 sigma indu (mib, mip as spec) args =
+  let templ = match mib.Declarations.mind_template with
+  | None -> assert false
+  | Some t -> Array.of_list t.template_param_arguments
+  in
+  let ctx = List.rev (EConstr.of_rel_context mib.Declarations.mind_params_ctxt) in
+  let rec freshen i env sigma accu sorts = function
+  | [] -> sigma, List.rev sorts
+  | LocalAssum (na, t) as decl :: ctx ->
+    let sigma, decl, s =
+      if templ.(i) then
+        let decls, s0 = Reductionops.dest_arity env sigma t in
+        let sigma, s =
+          if i < Array.length args then match Reductionops.sort_of_arity env sigma args.(i).uj_type with
+          | s -> sigma, s
+          | exception Reduction.NotArity -> Evd.new_sort_variable Evd.univ_flexible sigma
+          else sigma, s0
+        in
+        let t = EConstr.it_mkProd_or_LetIn (mkSort s) decls in
+        let s ~expected = match ESorts.kind sigma s with
+        | Sorts.SProp ->
+          let indty = EConstr.of_constr @@
+            Inductive.type_of_inductive (spec, Unsafe.to_instance @@ snd indu)
+          in
+          error_cant_apply_bad_type env0 sigma
+            (i+1, mkType (Univ.Universe.make expected), args.(i).uj_type)
+            (make_judge (mkIndU indu) indty)
+            args
+        | Sorts.Prop -> TemplateProp
+        | Sorts.Set -> TemplateUniv Univ.Universe.type0
+        | Sorts.Type u | Sorts.QSort (_, u) -> TemplateUniv u
         in
-        error_cant_apply_bad_type env sigma
-          (i+1, mkType (Univ.Universe.make expected), j.uj_type)
-          (make_judge (mkIndU indu) indty)
-          jl
-      | Sorts.Prop -> TemplateProp
-      | Sorts.Set -> TemplateUniv Univ.Universe.type0
-      | Sorts.Type u | Sorts.QSort (_, u) -> TemplateUniv u)
-    jl
-
-let inductive_type_knowing_parameters env sigma (ind,u as indu) jl =
-  let u = Unsafe.to_instance u in
-  let mspec = lookup_mind_specif env ind in
-  let paramstyp = make_param_univs env sigma indu mspec jl in
-  Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
-
-let constructor_type_knowing_parameters env sigma (cstr, u) jl =
-  let u0 = Unsafe.to_instance u in
-  let (ind, _) = cstr in
-  let mspec = lookup_mind_specif env ind in
-  let paramstyp = make_param_univs env sigma (ind, u) mspec jl in
-  Inductive.type_of_constructor_knowing_parameters (cstr, u0) mspec paramstyp
+        sigma, LocalAssum (na, t), s
+      else
+        sigma, decl, (fun ~expected -> assert false)
+    in
+    freshen (i + 1) (push_rel decl env) sigma (decl :: accu) (s :: sorts) ctx
+  | LocalDef (na, b, t) as decl :: ctx ->
+    freshen i (push_rel decl env) sigma (decl :: accu) sorts ctx
+  in
+  freshen 0 env0 sigma [] [] ctx
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -76,7 +89,7 @@ let assumption_of_judgment env sigma j =
   with Type_errors.TypeError _ | PretypeError _ ->
     error_assumption env sigma j
 
-let judge_of_apply env sigma funj argjv =
+let judge_of_apply_core env sigma funj argjv =
   let rec apply_rec sigma n subs typ = function
   | [] ->
     let typ = Vars.esubst Vars.lift_substituend subs typ in
@@ -109,33 +122,53 @@ let judge_of_apply env sigma funj argjv =
   in
   apply_rec sigma 1 (Esubst.subs_id 0) funj.uj_type (Array.to_list argjv)
 
+let judge_of_applied ~check env sigma funj argjv =
+  let sigma =
+    if check then
+      let (sigma, _) = judge_of_apply_core env sigma funj argjv in
+      sigma
+    else sigma
+  in
+  let typ = hnf_prod_appvect env sigma (j_type funj) (Array.map j_val argjv) in
+  sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
+
+let judge_of_applied_inductive_knowing_parameters ~check env sigma (ind, u) argjv =
+  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+  let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let sigma, paramstyp = fresh_template_context env sigma (ind, u) specif argjv in
+  let u0 = EInstance.kind sigma u in
+  let ty, csts = Inductive.type_of_inductive_knowing_parameters (specif, u0) paramstyp in
+  let sigma = Evd.add_constraints sigma csts in
+  let funj = { uj_val = mkIndU (ind, u); uj_type = EConstr.of_constr (rename_type ty (GR.IndRef ind)) } in
+  judge_of_applied ~check env sigma funj argjv
+
+let judge_of_applied_constructor_knowing_parameters ~check env sigma ((ind, _ as cstr), u) argjv =
+  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+  let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let sigma, paramstyp = fresh_template_context env sigma (ind, u) specif argjv in
+  let u0 = EInstance.kind sigma u in
+  let ty, csts = Inductive.type_of_constructor_knowing_parameters (cstr, u0) specif paramstyp in
+  let sigma = Evd.add_constraints sigma csts in
+  let funj = { uj_val = mkConstructU (cstr, u); uj_type = (EConstr.of_constr (rename_type ty (GR.ConstructRef cstr))) } in
+  judge_of_applied ~check env sigma funj argjv
+
+let judge_of_apply env sigma fj args =
+  match EConstr.kind sigma fj.uj_val with
+  | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
+    judge_of_applied_inductive_knowing_parameters ~check:true env sigma (ind, u) args
+  | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
+    judge_of_applied_constructor_knowing_parameters ~check:true env sigma (cstr, u) args
+  | _ ->
+    (* No template polymorphism *)
+    judge_of_apply_core env sigma fj args
+
 let checked_appvect env sigma f args =
   let mk c = Retyping.get_judgment_of env sigma c in
   let sigma, j = judge_of_apply env sigma (mk f) (Array.map mk args) in
   sigma, j.uj_val
 
 let checked_applist env sigma f args = checked_appvect env sigma f (Array.of_list args)
 
-let judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv =
-  let ar, csts = inductive_type_knowing_parameters env sigma ind argjv in
-  let sigma = Evd.add_constraints sigma csts in
-  let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in
-  sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
-
-let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
-  let (sigma, j) = judge_of_apply env sigma funj argjv in
-  judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv
-
-let judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj cstr argjv =
-  let ar, csts = constructor_type_knowing_parameters env sigma cstr argjv in
-  let sigma = Evd.add_constraints sigma csts in
-  let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in
-  sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
-
-let judge_of_applied_constructor_knowing_parameters env sigma funj ind argjv =
-  let (sigma, j) = judge_of_apply env sigma funj argjv in
-  judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj ind argjv
-
 let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env sigma cj (Array.length explft);
@@ -564,18 +597,9 @@ let rec execute env sigma cstr =
       sigma, judge_of_projection env sigma p cj
 
     | App (f,args) ->
+        let sigma, fj = execute env sigma f in
         let sigma, jl = execute_array env sigma args in
-        (match EConstr.kind sigma f with
-            | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
-               let sigma, fj = execute env sigma f in
-               judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl
-            | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
-               let sigma, fj = execute env sigma f in
-               judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl
-            | _ ->
-               (* No template polymorphism *)
-               let sigma, fj = execute env sigma f in
-               judge_of_apply env sigma fj jl)
+        judge_of_apply env sigma fj jl
 
     | Lambda (name,c1,c2) ->
         let sigma, j = execute env sigma c1 in
@@ -809,9 +833,9 @@ let rec recheck_against env sigma good c =
         let sigma, jl = execute_array env sigma args in
         (match EConstr.kind sigma f with
          | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
-           maybe_changed (judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl)
+           maybe_changed (judge_of_applied_inductive_knowing_parameters ~check:true env sigma (ind, u) jl)
          | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
-           maybe_changed (judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl)
+           maybe_changed (judge_of_applied_constructor_knowing_parameters ~check:true env sigma (cstr, u) jl)
          | _ ->
            (* No template polymorphism *)
            maybe_changed (judge_of_apply env sigma fj jl))
@@ -826,11 +850,16 @@ let rec recheck_against env sigma good c =
         if unchanged changedargs && bodyonly changedf
         then assume_unchanged_type sigma
         else
+          (* FIXME: the template poly cases are generating useless constraints *)
           (match EConstr.kind sigma f with
            | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
              let sigma, _ = judge_of_apply_against env sigma changedf fj jl in
              let jl = Array.map snd jl in
-             maybe_changed (judge_of_applied_inductive_knowing_parameters_nocheck env sigma fj (ind, u) jl)
+             maybe_changed (judge_of_applied_inductive_knowing_parameters ~check:false env sigma (ind, u) jl)
+           | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
+             let sigma, _ = judge_of_apply_against env sigma changedf fj jl in
+             let jl = Array.map snd jl in
+             maybe_changed (judge_of_applied_constructor_knowing_parameters ~check:false env sigma (cstr, u) jl)
            | _ ->
              (* No template polymorphism *)
              maybe_changed (judge_of_apply_against env sigma changedf fj jl))

proofs/clenv.ml

@@ -679,7 +679,7 @@ let rec mk_refgoals env sigma goalacc conclty trm = match trm with
   gl::goalacc, conclty, sigma, ev
 | RfApp (f, l) ->
   let (acc',hdty,sigma,applicand) = match f with
-  | RfGround f when Termops.is_template_polymorphic_ind env sigma f ->
+  | RfGround f when Termops.is_template_polymorphic_ref env sigma f ->
     let ty =
       (* Template polymorphism of definitions and inductive types *)
       let args, _ = List.split_when (fun p -> not (is_ground p)) l in