Fully sort polymorphic inductives

kernel/indTyping.ml

@@ -66,12 +66,11 @@ let mind_check_names mie =
 (************************************************************************)
 
 
-let no_sort_variable () =
-  CErrors.user_err (Pp.str "Sort variables not yet supported for the inductive's sort.")
-
 type record_arg_info =
   | NoRelevantArg
   | HasRelevantArg
+  (** HasRelevantArg means when the record is relevant at least one arg is relevant.
+      When the record is in a polymorphic sort this can mean one arg is in the same sort. *)
 
 type univ_info =
   { ind_squashed : squash_info option
@@ -94,9 +93,13 @@ let check_univ_leq ?(is_real_arg=false) env u info =
   let open Sorts.Quality in
   let info = if not is_real_arg then info
     else match info.record_arg_info with
-    | NoRelevantArg | HasRelevantArg -> match u with
-      | Sorts.SProp | QSort _ -> info
-      | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg }
+      | HasRelevantArg -> info
+      | NoRelevantArg -> match u with
+        | Sorts.SProp -> info
+        | QSort (q,_) -> if 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 }
   in
   if (Environ.type_in_type env) then info
   else match u, info.ind_univ with
@@ -319,11 +322,7 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
       args,out)
       splayed_lc
   in
-  let ind_univ = match univ_info.ind_univ with
-    | QSort _ -> no_sort_variable ()
-    | _ ->
-      UVars.subst_sort_level_sort usubst univ_info.ind_univ
-  in
+  let ind_univ = UVars.subst_sort_level_sort usubst univ_info.ind_univ in
 
   let arity =
     if univ_info.ind_template then

kernel/inductive.ml

@@ -334,10 +334,9 @@ let is_squashed ((_,mip),u) =
     | AlwaysSquashed -> Some inds
     | SometimesSquashed squash ->
       match inds with
-      | Sorts.Set ->
-        (* impredicative set squashes are always AlwaysSquashed *)
-        assert false
-      | Sorts.Type _ -> None
+      (* impredicative set squashes are always AlwaysSquashed,
+         so here it is a sort poly squash (see "foo6" in test sort_poly.v) *)
+      | Sorts.Set | Sorts.Type _ -> None
       | _ ->
         let squash = List.map (UVars.subst_instance_quality u) squash in
         if List.for_all (fun q -> quality_leq q (Sorts.quality inds)) squash then None

pretyping/inductiveops.ml

@@ -243,10 +243,9 @@ let is_squashed sigma ((_,mip),u) =
     | AlwaysSquashed -> Some (EConstr.ESorts.make inds)
     | SometimesSquashed squash ->
       match inds with
-      | Sorts.Set ->
-        (* impredicative set squashes are always AlwaysSquashed *)
-        assert false
-      | Sorts.Type _ -> None
+      (* impredicative set squashes are always AlwaysSquashed, so here
+         we have a sort poly squash *)
+      | Sorts.Set | Sorts.Type _ -> None
       | _ ->
         let squash = List.map (UVars.subst_instance_quality u) squash in
         let nfq q = UState.nf_quality (Evd.evar_universe_context sigma) q in

test-suite/success/sort_poly.v

@@ -91,8 +91,7 @@ Module Inference.
 End Inference.
 
 Module Inductives.
-  (* TODO sort variable in the output sort *)
-  Fail Inductive foo1@{s| |} : Type@{s|Set} := .
+  Inductive foo1@{s| |} : Type@{s|Set} := .
 
   Inductive foo2@{s| |} := Foo2 : Type@{s|Set} -> foo2.
 
@@ -117,6 +116,57 @@ Module Inductives.
     : P f
     := match f with Foo5 _ a => H a end.
 
+  (* all sort poly output with nonzero contructors are squashed (avoid interfering with uip) *)
+  Inductive foo6@{s| |} : Type@{s|Set} := Foo6.
+  Check foo6_sind.
+
+  Fail Definition foo6_rect (P:foo6 -> Type)
+    (H : P Foo6)
+    (f : foo6)
+    : P f
+    := match f with Foo6 => H end.
+  (* XXX error message is pretty bad *)
+
+  Definition foo6_prop_rect (P:foo6 -> Type)
+    (H : P Foo6)
+    (f : foo6@{Prop|})
+    : P f
+    := match f with Foo6 => H end.
+
+  Definition foo6_type_rect (P:foo6 -> Type)
+    (H : P Foo6)
+    (f : foo6@{Type|})
+    : P f
+    := match f with Foo6 => H end.
+
+  Definition foo6_qsort_rect@{s|u|} (P:foo6 -> Type@{s|u})
+    (H : P Foo6)
+    (f : foo6@{s|})
+    : P f
+    := match f with Foo6 => H end.
+
+  Fail Definition foo6_2qsort_rect@{s s'|u|} (P:foo6 -> Type@{s|u})
+    (H : P Foo6)
+    (f : foo6@{s'|})
+    : P f
+    := match f with Foo6 => H end.
+
+  Inductive foo7@{s| |} : Type@{s|Set} := Foo7_1 | Foo7_2.
+  Check foo7_sind.
+  Fail Check foo7_ind.
+
+  Definition foo7_prop_ind (P:foo7 -> Prop)
+    (H : P Foo7_1) (H' : P Foo7_2)
+    (f : foo7@{Prop|})
+    : P f
+    := match f with Foo7_1 => H | Foo7_2 => H' end.
+
+  Fail Definition foo7_prop_rect (P:foo7 -> Type)
+    (H : P Foo7_1) (H' : P Foo7_2)
+    (f : foo7@{Prop|})
+    : P f
+    := match f with Foo7_1 => H | Foo7_2 => H' end.
+
   Set Primitive Projections.
   Set Warnings "+records".
 
@@ -129,8 +179,7 @@ Module Inductives.
   (* R3@{SProp Type|} may not be primitive  *)
   Fail Record R3@{s s'| |} (A:Type@{s|Set}) : Type@{s'|Set} := { R3f1 : A }.
 
-  (* TODO sort variable in output sort *)
-  Fail Record R4@{s| |} (A:Type@{s|Set}) : Type@{s|Set} := { R4f1 : A}.
+  Record R4@{s| |} (A:Type@{s|Set}) : Type@{s|Set} := { R4f1 : A}.
 
   (* non SProp instantiation must be squashed *)
   Fail Record R5@{s| |} (A:Type@{s|Set}) : SProp := { R5f1 : A}.

test-suite/success/sort_poly_extraction.v

@@ -7,4 +7,15 @@ Definition bar := foo@{Prop|}.
 
 Fail Extraction bar.
 
-(* the actual problem only appears once we have inductives with sort poly output *)
+(* the actual problem only appears once we have inductives with sort poly output: *)
+
+Inductive Pair@{s|u|} (A:Type@{s|u}) : Type@{s|u} := pair : A -> A -> Pair A.
+
+Definition use_pair@{s|+|} A (k:A->nat) (x:Pair@{s|_} A) :=
+  k (match x with pair _ x _ => x end).
+
+Definition make_pair := pair@{Prop|_} _ I I.
+
+Definition hell := use_pair True (fun _ => 0) make_pair.
+
+Fail Recursive Extraction hell.

vernac/comInductive.ml

@@ -233,7 +233,8 @@ let inductive_levels env evd arities ctors =
   let less_than_2 = function [] | [_] -> true | _ :: _ :: _ -> false in
   let evd = List.fold_left (fun evd (raw_arity,(_,s),ctors) ->
       if less_than_2 ctors || is_impredicative_sort evd s then evd
-      else Evd.set_leq_sort env evd ESorts.set s)
+      else (* >=2 constructors is like having a bool argument *)
+        include_constructor_argument env evd ~ctor_sort:ESorts.set ~inductive_sort:s)
       evd inds
   in
   (* If indices_matter, the index telescope acts like an extra