Typecheck pseudo sort poly inductives in kernel using above prop qvar

We have a back and forth

~~~
elaboration -> econstr with qvar ->
cominductive -> inductive entry without qvar ->
indtyping -> inductive entry with qvar -> inductive entry without qvar ->
declarations
~~~

which should be cleaned up someday.

Author: SkySkimmer

kernel/environ.ml

@@ -1043,3 +1043,13 @@ struct
   let hash _env c = GlobRef.CanOrd.hash c
   let canonize _env c = GlobRef.canonize c
 end
+
+module Internal = struct
+  let for_checking_pseudo_sort_poly env =
+    let q = Sorts.QVar.make_var 0 in
+    assert (not (Sorts.QVar.Set.mem q env.env_qualities));
+    let env = map_universes UGraph.Internal.for_checking_pseudo_sort_poly env in
+    { env with env_qualities = Sorts.QVar.Set.add q env.env_qualities }
+
+  let is_above_prop env q = UGraph.Internal.is_above_prop env.env_universes q
+end

kernel/environ.mli

@@ -463,3 +463,11 @@ val no_link_info : link_info
 
 (** Primitives *)
 val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env
+
+module Internal : sig
+  (** Makes qvar 0 bound and treated as above prop.
+      Do not use outside kernel inductive typechecking. *)
+  val for_checking_pseudo_sort_poly : env -> env
+
+  val is_above_prop : env -> Sorts.QVar.t -> bool
+end

kernel/indTyping.ml

@@ -304,7 +304,7 @@ let get_arity c =
   | _ -> None
 
 let get_template (mie:mutual_inductive_entry) = match mie.mind_entry_universes with
-| Monomorphic_ind_entry | Polymorphic_ind_entry _ -> None
+| Monomorphic_ind_entry | Polymorphic_ind_entry _ -> mie, None
 | Template_ind_entry {univs=(template_univs, _ as template_context); pseudo_sort_poly} ->
   let params = mie.mind_entry_params in
   let ind =
@@ -334,7 +334,7 @@ let get_template (mie:mutual_inductive_entry) = match mie.mind_entry_universes w
   (** params *)
   (* for each non-letin param, find whether it binds a template univ *)
   let template_params =
-    CList.filter_map (fun param ->
+    CList.map (fun param ->
         match param with
         | LocalDef (_,b,t) ->
           check_not_appearing b;
@@ -352,8 +352,8 @@ let get_template (mie:mutual_inductive_entry) = match mie.mind_entry_universes w
   in
   let bound_in_params =
     List.fold_left (fun bound_in_params -> function
-        | None -> bound_in_params
-        | Some l ->
+        | Some None | None -> bound_in_params
+        | Some (Some l) ->
           if Level.Set.mem l bound_in_params then
             CErrors.user_err Pp.(str "Non-linear template level " ++ Level.raw_pr l)
           else Level.Set.add l bound_in_params)
@@ -371,15 +371,15 @@ let get_template (mie:mutual_inductive_entry) = match mie.mind_entry_universes w
   in
 
   (** arity *)
-  let () =
+  let arity_for_pseudo_poly =
     (* don't use get_arity, we allow constant template poly (eg eq) *)
     let (decls, s) = Term.decompose_prod_decls ind.mind_entry_arity in
     let () = if not (isSort s) then
         CErrors.user_err Pp.(str "Template polymorphic inductive's type must be a syntactic arity.")
     in
     check_not_appearing_rel_ctx decls;
     match destSort s with
-    | SProp | Prop | Set -> ()
+    | SProp | Prop | Set -> None
     | QSort _ -> assert false
     | Type u ->
       (* forbid template poly with an increment on a template univ in the conclusion
@@ -394,13 +394,49 @@ let get_template (mie:mutual_inductive_entry) = match mie.mind_entry_universes w
       if has_increment then
         CErrors.user_err
           Pp.(str "Template polymorphism with conclusion strictly larger than a bound universe not supported.")
+      else Some (decls, u)
   in
 
   (** ctors *)
   let () = List.iter check_not_appearing ind.mind_entry_lc in
 
-  Some {
-    template_param_arguments = List.rev_map Option.has_some template_params;
+  (* for typechecking pseudo sort poly, replace Type@{u} with Type@{Var 0 | u}
+     in the conclusion and for the bound univs which appear in the conclusion
+     XXX it would be nicer to have the higher layers send us qvars instead *)
+  let mie = match pseudo_sort_poly, arity_for_pseudo_poly with
+    | TemplateUnivOnly, _ -> mie
+    | TemplatePseudoSortPoly, None ->
+      CErrors.user_err Pp.(str "Invalid pseudo sort poly template inductive.")
+    | TemplatePseudoSortPoly, Some (indices, concl) ->
+      let concl_bound_univs = Level.Set.inter template_univs (Universe.levels concl) in
+      let bound_qvar = Sorts.QVar.make_var 0 in
+      let params = List.map (fun param ->
+          match param with
+          | LocalDef _ -> param (* letin *)
+          | LocalAssum (na, t) ->
+            match get_arity t with
+            | None -> param
+            | Some (decls, l) ->
+              if Level.Set.mem l concl_bound_univs then
+                let l = Universe.make l in
+                LocalAssum (na, it_mkProd_or_LetIn (mkSort (Sorts.qsort bound_qvar l)) decls)
+              else param)
+          params
+      in
+      let arity = it_mkProd_or_LetIn (mkSort (Sorts.qsort bound_qvar concl)) indices in
+      { mie with
+        mind_entry_params = params;
+        mind_entry_inds =
+          [{ind with
+            mind_entry_arity = arity;
+           }];
+      }
+  in
+
+  let template_assums = CList.filter_map (fun x -> x) template_params in
+
+  mie, Some {
+    template_param_arguments = List.rev_map Option.has_some template_assums;
     template_context;
     template_pseudo_sort_poly = pseudo_sort_poly;
   }
@@ -421,7 +457,7 @@ let abstract_packets env usubst ((arity,lc),(indices,splayed_lc),univ_info) =
 
   let arity =
     if univ_info.ind_template then
-      TemplateArity { template_level = univ_info.ind_univ; }
+      TemplateArity { template_level = ind_univ; }
     else
       RegularArity {mind_user_arity = arity; mind_sort = ind_univ}
   in
@@ -450,17 +486,15 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   assert (List.is_empty (Environ.rel_context env));
 
   (* universes *)
-  let template = get_template mie in
+  let mie, template = get_template mie in
 
   let env_univs =
     match mie.mind_entry_universes with
     | Template_ind_entry {univs=ctx; pseudo_sort_poly} ->
+      let env =  Environ.push_context_set ~strict:false ctx env in
       begin match pseudo_sort_poly with
-      | TemplatePseudoSortPoly ->
-        (* For that particular case, we typecheck the inductive in an environment
-           where the universes introduced by the definition are only [>= Prop] *)
-        Environ.push_floating_context_set ctx env
-      | TemplateUnivOnly -> Environ.push_context_set ~strict:false ctx env
+      | TemplatePseudoSortPoly -> Environ.Internal.for_checking_pseudo_sort_poly env
+      | TemplateUnivOnly -> env
       end
     | Monomorphic_ind_entry -> env
     | Polymorphic_ind_entry ctx -> push_context ctx env
@@ -532,8 +566,19 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
 
   (* Abstract universes *)
   let usubst, univs = match mie.mind_entry_universes with
-  | Monomorphic_ind_entry | Template_ind_entry _ ->
-    UVars.empty_sort_subst, Monomorphic
+  | Monomorphic_ind_entry ->
+      UVars.empty_sort_subst, Monomorphic
+  | Template_ind_entry info -> begin match info.pseudo_sort_poly with
+      | TemplateUnivOnly -> UVars.empty_sort_subst, Monomorphic
+      | TemplatePseudoSortPoly ->
+        (* replace Type@{Var 0 | u} back to Type@{u}
+           XXX it would be nicer to keep the qvar in the declared structure *)
+        let qsubst =
+          Sorts.QVar.Map.singleton (Sorts.QVar.make_var 0) Sorts.Quality.(QConstant QType)
+        in
+        let usubst = Univ.empty_level_subst in
+        (qsubst, usubst), Monomorphic
+    end
   | Polymorphic_ind_entry uctx ->
     let (inst, auctx) = UVars.abstract_universes uctx in
     let inst = UVars.make_instance_subst inst in

kernel/inductive.ml

@@ -118,10 +118,16 @@ let no_sort_variable () =
 
 type template_univ =
   | TemplateProp
+  | TemplateAboveProp of Sorts.QVar.t * Universe.t
   | TemplateUniv of Universe.t
 
 let max_template_universe u v = match u, v with
   | TemplateProp, x | x, TemplateProp -> x
+  | TemplateAboveProp (q1,u), TemplateAboveProp (q2,v) ->
+    if Sorts.QVar.equal q1 q2 then TemplateAboveProp (q1, Universe.sup u v)
+    else TemplateUniv (Universe.sup u v)
+  | TemplateAboveProp (_, u), TemplateUniv v
+  | TemplateUniv u, TemplateAboveProp (_,v)
   | TemplateUniv u, TemplateUniv v -> TemplateUniv (Universe.sup u v)
 
 (* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
@@ -191,32 +197,34 @@ let subst_univs_sort (subs, pseudo_sort_poly) = function
   let u = Universe.repr u in
   let supern u n = iterate Universe.super n u in
   let map (u, n) =
-    if Level.is_set u then Some (Universe.type0, n)
+    if Level.is_set u then TemplateUniv (supern Universe.type0 n)
     else match Level.Map.find u subs, pseudo_sort_poly with
     | TemplateProp, TemplatePseudoSortPoly ->
       if Int.equal n 0 then
         (* This is an instantiation of a template universe by Prop, ignore it *)
-        None
+        TemplateProp
       else
         (* Prop + S n actually means Set + S n *)
-        Some (Universe.type0, n)
+        TemplateUniv (supern Universe.type0 n)
+    | TemplateAboveProp (q, u), TemplatePseudoSortPoly ->
+      TemplateAboveProp (q, supern u n)
     | TemplateProp, TemplateUnivOnly ->
       (* exploit Prop <= Set *)
-      Some (Universe.type0, n)
-    | TemplateUniv v, _ -> Some (v,n)
+      TemplateUniv (supern Universe.type0 n)
+    | TemplateAboveProp (_, u), TemplateUnivOnly ->
+      TemplateUniv (supern u n)
+    | TemplateUniv v, _ -> TemplateUniv (supern v n)
     | exception Not_found ->
       (* Either an unbound template universe due to missing arguments, or a
          global one appearing in the inductive arity. *)
-      Some (Universe.make u, n)
+      TemplateUniv (supern (Universe.make u) n)
   in
-  let u = List.filter_map map u in
-  match u with
-  | [] ->
-    (* No constraints, fall in Prop *)
+  let u = List.map map u in
+  match List.fold_left max_template_universe TemplateProp u with
+  | TemplateProp ->
     Sorts.prop
-  | (u,n) :: rest ->
-    let fold accu (u, n) = Universe.sup accu (supern u n) in
-    Sorts.sort_of_univ (List.fold_left fold (supern u n) rest)
+  | TemplateUniv u -> Sorts.sort_of_univ u
+  | TemplateAboveProp (q,u) -> Sorts.qsort q u
 
 let get_arity c =
   let decls, c = Term.decompose_prod_decls c in

kernel/inductive.mli

@@ -48,6 +48,7 @@ val instantiate_inductive_constraints :
 
 type template_univ =
   | TemplateProp
+  | TemplateAboveProp of Sorts.QVar.t * Universe.t
   | TemplateUniv of Universe.t
 
 type param_univs = (expected:Univ.Level.t -> template_univ) list

kernel/typeops.ml

@@ -63,23 +63,32 @@ let infer_assumption env t ty =
   with TypeError _ ->
     error_assumption env (make_judge t ty)
 
+let nf_relevance env = function
+  | Sorts.RelevanceVar q as r ->
+    if Environ.Internal.is_above_prop env q then Sorts.Relevant
+    else r
+  | (Sorts.Irrelevant | Sorts.Relevant) as r -> r
+
+let check_relevance env r r' =
+  Sorts.relevance_equal (nf_relevance env r) (nf_relevance env r')
+
 let check_assumption env x t ty =
   let r = x.binder_relevance in
   let r' = infer_assumption env t ty in
-  if Sorts.relevance_equal r r' then ()
+  if check_relevance env r r' then ()
   else
     error_bad_binder_relevance env r' (RelDecl.LocalAssum (x, t))
 
-let check_binding_relevance na1 na2 =
+let check_binding_relevance env na1 na2 =
   (* Since we know statically the relevance here, we are stricter *)
-  assert (Sorts.relevance_equal (binder_relevance na1) (binder_relevance na2))
+  assert (check_relevance env (binder_relevance na1) (binder_relevance na2))
 
 let esubst u s c =
   Vars.esubst Vars.lift_substituend s (subst_instance_constr u c)
 
 exception ArgumentsMismatch
 
-let instantiate_context u subst nas ctx =
+let instantiate_context env u subst nas ctx =
   let open Context.Rel.Declaration in
   let instantiate_relevance na =
     { na with binder_relevance = UVars.subst_instance_relevance u na.binder_relevance }
@@ -91,15 +100,15 @@ let instantiate_context u subst nas ctx =
     let subst = Esubst.subs_liftn i subst in
     let na = instantiate_relevance na in
     let ty = esubst u subst ty in
-    let () = check_binding_relevance na nas.(i) in
+    let () = check_binding_relevance env na nas.(i) in
     LocalAssum (nas.(i), ty) :: ctx
   | LocalDef (na, ty, bdy) :: ctx ->
     let ctx = instantiate (pred i) ctx in
     let subst = Esubst.subs_liftn i subst in
     let na = instantiate_relevance na in
     let ty = esubst u subst ty in
     let bdy = esubst u subst bdy in
-    let () = check_binding_relevance na nas.(i) in
+    let () = check_binding_relevance env na nas.(i) in
     LocalDef (nas.(i), ty, bdy) :: ctx
   in
   instantiate (Array.length nas - 1) ctx
@@ -397,7 +406,9 @@ let make_param_univs env indu spec args argtys =
       | Prop -> TemplateProp
       | Set -> TemplateUniv Universe.type0
       | Type u -> TemplateUniv u
-      | QSort _ -> assert false)
+      | QSort (q,u) ->
+        assert (Environ.Internal.is_above_prop env q);
+        TemplateAboveProp (q,u))
     argtys
 
 let type_of_inductive_knowing_parameters env (ind,u as indu) args argst =
@@ -473,8 +484,9 @@ let check_branch_types env (_mib, mip) ci u pms c _ct lft (pctx, p) =
     error_ill_formed_branch env c ((ci.ci_ind, i + 1), u) brt expbrt
 
 let should_invert_case env r ci =
-  Sorts.relevance_equal r Sorts.Relevant &&
+  check_relevance env r Sorts.Relevant &&
   let mib,mip = lookup_mind_specif env ci.ci_ind in
+  (* mind_relevance cannot be a pseudo sort poly variable so don't use check_relevance *)
   Sorts.relevance_equal mip.mind_relevance Sorts.Irrelevant &&
   (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks
      but we don't do special reduction in such cases
@@ -522,7 +534,7 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, rp, pt) iv c
   in
   let () =
     let expected = Sorts.relevance_of_sort sp in
-    if Sorts.relevance_equal rp expected then ()
+    if check_relevance env rp expected then ()
     else
       error_bad_case_relevance env expected (ci, u, pms, ((pnas, p), rp), iv, c, lf)
   in
@@ -601,15 +613,15 @@ let type_of_global_in_context env r =
 let check_assum_annot env s x t =
   let r = x.binder_relevance in
   let r' = Sorts.relevance_of_sort s in
-  if Sorts.relevance_equal r' r
+  if check_relevance env r' r
   then ()
   else error_bad_binder_relevance env r' (RelDecl.LocalAssum (x, t))
 
 
 let check_let_annot env s x c t =
   let r = x.binder_relevance in
   let r' = Sorts.relevance_of_sort s in
-  if Sorts.relevance_equal r' r
+  if check_relevance env r' r
   then ()
   else error_bad_binder_relevance env r' (RelDecl.LocalDef (x, c, t))
 
@@ -652,7 +664,7 @@ and execute_aux tbl env cstr =
     | Proj (p, r, c) ->
       let ct = execute tbl env c in
       let r', ty = type_of_projection env p (self c) ct in
-      assert (Sorts.relevance_equal r r');
+      assert (check_relevance env r r');
       ty
 
     (* Lambda calculus operators *)
@@ -752,7 +764,7 @@ and execute_aux tbl env cstr =
           in
           let realdecls = LocalAssum (Context.make_annot Anonymous mip.mind_relevance, self) :: realdecls in
           let realdecls =
-            try instantiate_context u paramsubst nas realdecls
+            try instantiate_context env u paramsubst nas realdecls
             with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) (HConstr.self c) None
           in
           let p_env = Environ.push_rel_context realdecls env in
@@ -768,7 +780,7 @@ and execute_aux tbl env cstr =
           let (ctx, cty) = mip.mind_nf_lc.(i) in
           let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
           let ctx =
-            try instantiate_context u paramsubst nas ctx
+            try instantiate_context env u paramsubst nas ctx
             with ArgumentsMismatch ->
               (* Despite the name, the toplevel message is reasonable *)
               error_elim_arity env (ci.ci_ind, u) (self c) None