sort poly (not for inductive output type)

checker/checker.ml

@@ -245,7 +245,7 @@ let explain_exn = function
     let msg =
       if CDebug.(get_flag misc) then
         str "." ++ spc() ++
-          UGraph.explain_universe_inconsistency Univ.Level.raw_pr i
+          UGraph.explain_universe_inconsistency Sorts.QVar.raw_pr Univ.Level.raw_pr i
       else
         mt() in
       hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
@@ -287,11 +287,13 @@ let explain_exn = function
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
+      | UnsatisfiedQConstraints _ -> str"UnsatisfiedQConstraints"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
       | BadBinderRelevance _ -> str"BadBinderRelevance"
       | BadCaseRelevance _ -> str"BadCaseRelevance"
       | BadInvert -> str"BadInvert"
+      | UndeclaredQualities _ -> str"UndeclaredQualities"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"
       | BadVariance _ -> str "BadVariance"
       ))

checker/values.ml

@@ -94,6 +94,12 @@ let v_level = v_tuple "level" [|Int;v_raw_level|]
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
 
+let v_qvar = v_sum "qvar" 0 [|[|Int|];[|String;Int|]|]
+
+let v_constant_quality = v_enum "constant_quality" 3
+
+let v_quality = v_sum "quality" 0 [|[|v_qvar|];[|v_constant_quality|]|]
+
 let v_cstrs =
   Annot
     ("Univ.constraints",
@@ -103,16 +109,16 @@ let v_cstrs =
 
 let v_variance = v_enum "variance" 3
 
-let v_instance = Annot ("instance", Array v_level)
-let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
+let v_instance = Annot ("instance", v_pair (Array v_quality) (Array v_level))
+let v_abs_context = v_tuple "abstract_universe_context" [|v_pair (Array v_name) (Array v_name); v_cstrs|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|]
+let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|];[|v_qvar;v_univ(*QSort*)|]|]
 let v_sortfam = v_enum "sorts_family" 4
 
-let v_relevance = v_sum "relevance" 2 [||]
+let v_relevance = v_sum "relevance" 2 [|[|v_qvar|]|]
 let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]

dev/top_printers.ml

@@ -260,10 +260,11 @@ let ppuni_level u = pp (Level.raw_pr u)
 let ppqvar q = pp (QVar.raw_pr q)
 let ppesorts s = pp (Sorts.debug_print (Evd.MiniEConstr.ESorts.unsafe_to_sorts s))
 
-let prlev l = UnivNames.pr_with_global_universes l
+let prlev l = UnivNames.pr_level_with_global_universes l
+let prqvar q = Sorts.QVar.raw_pr q
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
-let ppuniverse_instance l = pp (Instance.pr prlev l)
-let ppuniverse_context l = pp (pr_universe_context prlev l)
+let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
+let ppuniverse_context l = pp (pr_universe_context prqvar prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)
 let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)
@@ -281,14 +282,16 @@ let ppnamedcontextval e =
   pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppaucontext auctx =
-  let nas = AbstractContext.names auctx in
-  let prlev l = match Level.var_index l with
-    | Some n -> (match nas.(n) with
-        | Anonymous -> prlev l
+  let qnas, unas = AbstractContext.names auctx in
+  let prgen pr var_index nas l = match var_index l with
+    | Some n -> (match unas.(n) with
+        | Anonymous -> pr l
         | Name id -> Id.print id)
-    | None -> prlev l
+    | None -> pr l
   in
-  pp (pr_universe_context prlev (AbstractContext.repr auctx))
+  let prqvar l = prgen prqvar Sorts.QVar.var_index qnas l in
+  let prlev l = prgen prlev Level.var_index unas l in
+  pp (pr_universe_context prqvar prlev (AbstractContext.repr auctx))
 
 
 let ppenv e = pp
@@ -375,6 +378,9 @@ let constr_display csr =
   and univ_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Universe.raw_pr u ++ fnl ())
 
+  and quality_display q =
+    incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Sorts.Quality.raw_pr q ++ fnl ())
+
   and level_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.raw_pr u ++ fnl ())
 
@@ -387,8 +393,15 @@ let constr_display csr =
     | QSort (q, u) -> univ_display u; Printf.sprintf "QSort(%s, %i)" (Sorts.QVar.to_string q) !cnt
 
   and universes_display l =
+    let qs, us = Instance.to_array l in
+    let qs = Array.fold_right (fun x i ->
+        quality_display x;
+        (string_of_int !cnt)^
+        (if not(i="") then (" "^i) else ""))
+        qs ""
+    in
     Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
-        then (" "^i) else "")) (Instance.to_array l) ""
+        then (" "^i) else "")) us (if qs = "" then "" else (qs^" | "))
 
   and name_display x = match x.binder_name with
     | Name id -> "Name("^(Id.to_string id)^")"
@@ -527,7 +540,9 @@ let print_pure_constr csr =
   and box_display c = open_hovbox 1; term_display c; close_box()
 
   and universes_display u =
-    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) (Instance.to_array u)
+    let qs, us = Instance.to_array u in
+    Array.iter (fun u -> print_space (); pp (Sorts.Quality.raw_pr u)) qs;
+    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) us
 
   and sort_display = function
     | SProp -> print_string "SProp"

engine/eConstr.ml

@@ -572,31 +572,14 @@ let compare_constr sigma cmp c1 c2 =
   let cmp nargs c1 c2 = cmp c1 c2 in
   compare_gen kind eq_inst eq_sorts (eq_existential cmp) cmp 0 c1 c2
 
-let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
-  let open UnivProblem in
-  if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
-  else
-    let make u = Sorts.sort_of_univ @@ Univ.Universe.make u in
-    CArray.fold_left3
-      (fun cstrs v u u' ->
-         let open UVars.Variance in
-         match v with
-         | Irrelevant -> Set.add (UWeak (u,u')) cstrs
-         | Covariant ->
-           (match cv_pb with
-            | Conversion.CONV -> Set.add (UEq (make u, make u')) cstrs
-            | Conversion.CUMUL -> Set.add (ULe (make u, make u')) cstrs)
-         | Invariant ->
-           Set.add (UEq (make u, make u')) cstrs)
-      cstrs variances (UVars.Instance.to_array u) (UVars.Instance.to_array u')
-
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
   match mind.Declarations.mind_variance with
   | None -> enforce_eq_instances_univs false u1 u2 cstrs
   | Some variances ->
     let num_param_arity = Conversion.inductive_cumulativity_arguments spec in
-    compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
+    if not (Int.equal num_param_arity nargs) then enforce_eq_instances_univs false u1 u2 cstrs
+    else compare_cumulative_instances cv_pb  variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
@@ -607,8 +590,11 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
+      let qs1, us1 = UVars.Instance.to_array u1
+      and qs2, us2 = UVars.Instance.to_array u2 in
+      let cstrs = enforce_eq_qualities qs1 qs2 cstrs in
       Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
-        cstrs (UVars.Instance.to_array u1) (UVars.Instance.to_array u2)
+        cstrs us1 us2
 
 let eq_universes env sigma cstrs cv_pb refargs l l' =
   if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
@@ -619,7 +605,7 @@ let eq_universes env sigma cstrs cv_pb refargs l l' =
     let open UnivProblem in
     match refargs with
     | Some (ConstRef c, 1) when Environ.is_array_type env c ->
-      cstrs := compare_cumulative_instances cv_pb true [|UVars.Variance.Irrelevant|] l l' !cstrs;
+      cstrs := compare_cumulative_instances cv_pb [|UVars.Variance.Irrelevant|] l l' !cstrs;
       true
     | None | Some (ConstRef _, _) ->
       cstrs := enforce_eq_instances_univs true l l' !cstrs; true
@@ -714,31 +700,77 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' 0 m n in
     if res then Some !cstrs else None
 
+let add_universes_of_instance sigma (qs,us) u =
+  let u = EInstance.kind sigma u in
+  let qs', us' = UVars.Instance.levels u in
+  let qs = Sorts.Quality.(Set.fold (fun q qs -> match q with
+      | QVar q -> Sorts.QVar.Set.add q qs
+      | QConstant _ -> qs)
+      qs' qs)
+  in
+  qs, Univ.Level.Set.union us us'
+
+let fold_annot_relevance f acc na =
+  f acc na.Context.binder_relevance
+
+let fold_case_under_context_relevance f acc (nas,_) =
+  Array.fold_left (fold_annot_relevance f) acc nas
+
+let fold_rec_declaration_relevance f acc (nas,_,_) =
+  Array.fold_left (fold_annot_relevance f) acc nas
+
+let fold_constr_relevance sigma f acc c =
+  match kind sigma c with
+  | Rel _ | Var _ | Meta _ | Evar _
+  |  Sort _ | Cast _ | App _
+  | Const _ | Ind _ | Construct _ | Proj _
+  | Int _ | Float _ | Array _ -> acc
+
+  | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
+    fold_annot_relevance f acc na
+
+  | Case (ci,_u,_params,ret,_iv,_v,brs) ->
+    let acc = f acc ci.ci_relevance in
+    let acc = fold_case_under_context_relevance f acc ret in
+    let acc = CArray.fold_left (fold_case_under_context_relevance f) acc brs in
+    acc
+
+  | Fix (_,data)
+  | CoFix (_,data) ->
+    fold_rec_declaration_relevance f acc data
+
+let add_relevance sigma (qs,us as v) r =
+  let open Sorts in
+  (* NB this normalizes above_prop to Relevant which makes it disappear *)
+  match UState.nf_relevance (Evd.evar_universe_context sigma) r with
+  | Irrelevant | Relevant -> v
+  | RelevanceVar q -> QVar.Set.add q qs, us
+
 let universes_of_constr sigma c =
   let open Univ in
-  let open UVars in
   let rec aux s c =
+    let s = fold_constr_relevance sigma (add_relevance sigma) s c in
     match kind sigma c with
-    | Const (c, u) ->
-      Level.Set.fold Level.Set.add (Instance.levels (EInstance.kind sigma u)) s
-    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-      Level.Set.fold Level.Set.add (Instance.levels (EInstance.kind sigma u)) s
-    | Sort u ->
-      let sort = ESorts.kind sigma u in
-      if Sorts.is_small sort then s
-      else
-        Level.Set.fold Level.Set.add (Sorts.levels sort) s
+    | Const (_, u) | Ind (_, u) | Construct (_,u) -> add_universes_of_instance sigma s u
+    | Sort u -> begin match ESorts.kind sigma u with
+        | Type u ->
+          Util.on_snd (Level.Set.fold Level.Set.add (Universe.levels u)) s
+        | QSort (q, u) ->
+          let qs, us = s in
+          Sorts.QVar.Set.add q qs, Level.Set.union us (Universe.levels u)
+        | SProp | Prop | Set -> s
+      end
     | Evar (k, args) ->
       let concl = Evd.evar_concl (Evd.find_undefined sigma k) in
       fold sigma aux (aux s concl) c
     | Array (u,_,_,_) ->
-      let s = Level.Set.fold Level.Set.add (Instance.levels (EInstance.kind sigma u)) s in
+      let s = add_universes_of_instance sigma s u in
       fold sigma aux s c
     | Case (_,u,_,_,_,_,_) ->
-      let s = Level.Set.fold Level.Set.add (Instance.levels (EInstance.kind sigma u)) s in
+      let s = add_universes_of_instance sigma s u in
       fold sigma aux s c
     | _ -> fold sigma aux s c
-  in aux Level.Set.empty c
+  in aux (Sorts.QVar.Set.empty,Level.Set.empty) c
 
 open Context
 open Environ

engine/eConstr.mli

@@ -334,7 +334,7 @@ val fold_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> t -> 'b) -> '
 
 (** Gather the universes transitively used in the term, including in the
    type of evars appearing in it. *)
-val universes_of_constr : Evd.evar_map -> t -> Univ.Level.Set.t
+val universes_of_constr : Evd.evar_map -> t -> Sorts.QVar.Set.t * Univ.Level.Set.t
 
 (** {6 Substitutions} *)
 
@@ -368,7 +368,7 @@ val noccur_between : Evd.evar_map -> int -> int -> t -> bool
 val closedn : Evd.evar_map -> int -> t -> bool
 val closed0 : Evd.evar_map -> t -> bool
 
-val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+val subst_univs_level_constr : UVars.full_level_subst -> t -> t
 val subst_instance_context : UVars.Instance.t -> rel_context -> rel_context
 val subst_instance_constr : UVars.Instance.t -> t -> t
 

engine/evarutil.ml

@@ -35,7 +35,7 @@ let finalize ?abort_on_undefined_evars sigma f =
   let sigma = minimize_universes sigma in
   let uvars = ref Univ.Level.Set.empty in
   let v = f (fun c ->
-      let varsc = EConstr.universes_of_constr sigma c in
+      let _, varsc = EConstr.universes_of_constr sigma c in
       let c = EConstr.to_constr ?abort_on_undefined_evars sigma c in
       uvars := Univ.Level.Set.union !uvars varsc;
       c)
@@ -67,12 +67,9 @@ let whd_evar = EConstr.whd_evar
 let nf_evar sigma c =
   let lsubst = Evd.universe_subst sigma in
   let evar_value ev = Evd.existential_opt_value0 sigma ev in
-  let level_value l =
-    UnivSubst.level_subst_of (fun l -> UnivFlex.normalize_univ_variable lsubst l) l
-  in
-  let sort_value s = UState.nf_sort (Evd.evar_universe_context sigma) s in
-  let rel_value r = UState.nf_relevance (Evd.evar_universe_context sigma) r in
-  EConstr.of_constr @@ UnivSubst.nf_evars_and_universes_opt_subst evar_value level_value sort_value rel_value (EConstr.Unsafe.to_constr c)
+  let univ_value l = UnivFlex.normalize_univ_variable lsubst l in
+  let qvar_value q = UState.nf_qvar (Evd.evar_universe_context sigma) q in
+  EConstr.of_constr @@ UnivSubst.nf_evars_and_universes_opt_subst evar_value qvar_value univ_value (EConstr.Unsafe.to_constr c)
 
 let j_nf_evar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
@@ -763,14 +760,20 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
   let open UnivProblem in
   let cstrs = Univ.Constraints.empty in
   let soft = Set.empty in
+  let qs, us = UVars.Instance.to_array u
+  and qs', us' = UVars.Instance.to_array u' in
+  let qcstrs = enforce_eq_qualities qs qs' Set.empty in
+  match Evd.add_universe_constraints sigma qcstrs with
+  | exception UGraph.UniverseInconsistency p -> Inr p
+  | sigma ->
   let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
       let open UVars.Variance in
       match v with
       | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft
       | Covariant when cv_pb == Conversion.CUMUL ->
         Univ.Constraints.add (u,Univ.Le,u') cstrs, soft
       | Covariant | Invariant -> Univ.Constraints.add (u,Univ.Eq,u') cstrs, soft)
-      (cstrs,soft) variances (UVars.Instance.to_array u) (UVars.Instance.to_array u')
+      (cstrs,soft) variances us us'
   in
   match Evd.add_constraints sigma cstrs with
   | sigma ->
@@ -779,11 +782,17 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
 
 let compare_constructor_instances evd u u' =
   let open UnivProblem in
-  let soft =
-    Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs)
-      Set.empty (UVars.Instance.to_array u) (UVars.Instance.to_array u')
-  in
-  Evd.add_universe_constraints evd soft
+  let qs, us = UVars.Instance.to_array u
+  and qs', us' = UVars.Instance.to_array u' in
+  let qcstrs = enforce_eq_qualities qs qs' Set.empty in
+  match Evd.add_universe_constraints evd qcstrs with
+  | exception UGraph.UniverseInconsistency p -> Inr p
+  | evd ->
+    let soft =
+      Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs)
+        Set.empty us us'
+    in
+    Inl (Evd.add_universe_constraints evd soft)
 
 (** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
     [t] and [u] up to existential variable instantiation and

engine/evarutil.mli

@@ -194,9 +194,12 @@ val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array
   (evar_map, UGraph.univ_inconsistency) Util.union
 
 (** We should only compare constructors at convertible types, so this
-   is only an opportunity to unify universes. *)
+    is only an opportunity to unify universes.
+
+    But what about qualities?
+*)
 val compare_constructor_instances : evar_map ->
-  UVars.Instance.t -> UVars.Instance.t -> evar_map
+  UVars.Instance.t -> UVars.Instance.t -> (evar_map, UGraph.univ_inconsistency) Util.union
 
 (** {6 Unification problems} *)
 type unification_pb = conv_pb * env * constr * constr