Typecheck pseudo sort poly inductives in kernel using above prop qvar

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

@@ -96,7 +96,9 @@ let check_univ_leq ?(is_real_arg=false) env u info =
       | HasRelevantArg -> info
       | NoRelevantArg -> match u with
         | Sorts.SProp -> info
-        | QSort (q,_) -> if Sorts.Quality.equal (QVar q) (Sorts.quality info.ind_univ)
+        | QSort (q,_) ->
+          if Environ.Internal.is_above_prop env q
+          || Sorts.Quality.equal (QVar q) (Sorts.quality info.ind_univ)
           then { info with record_arg_info = HasRelevantArg }
           else info
         | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg }
@@ -109,12 +111,15 @@ let check_univ_leq ?(is_real_arg=false) env u info =
     info
 
   | Prop, SProp -> { info with ind_squashed = Some AlwaysSquashed }
-  | (SProp|Prop), QSort _ -> add_squash (Sorts.quality u) info
+  | (SProp|Prop), QSort (q,_) ->
+    if Environ.Internal.is_above_prop env q then info
+    else add_squash (Sorts.quality u) info
   | Prop, (Prop | Set | Type _) -> info
 
   | Set, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed }
-  | Set, QSort (_, indu) ->
-    if UGraph.check_leq (universes env) Universe.type0 indu
+  | Set, QSort (q, indu) ->
+    if Environ.Internal.is_above_prop env q then info
+    else if UGraph.check_leq (universes env) Universe.type0 indu (* XXX always true *)
     then add_squash qtype info
     else { info with missing = u :: info.missing }
   | Set, Set -> info
@@ -227,6 +232,11 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) =
     | _ -> check_univ_leq env_ar_par Sorts.set univ_info
   in
   let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in
+  let () = if univ_info.ind_template then match univ_info.ind_squashed with
+      | None | Some AlwaysSquashed -> ()
+      | Some (SometimesSquashed _) ->
+      CErrors.user_err Pp.(str "Cannot handle sometimes squashed template polymorphic type.")
+  in
   (* generalize the constructors over the parameters *)
   let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in
   (arity, lc), (indices, splayed_lc), univ_info
@@ -304,7 +314,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 +344,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 +362,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 +381,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 +404,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 +467,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 +496,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 +576,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