Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.

12 files changed, 52 insertions, 37 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index ad91d31f87..1019f8f0c2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,10 +36,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_of_global ref : Name.t array =
-  try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
-  with Not_found -> [||]
-
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
       completely hackish and should be solved in upper layers instead. *)
@@ -55,8 +51,8 @@ let compute_instance_binders inst ubinders =
 
 type univ_name_list = Names.lname list
 
-let universe_binders_with_opt_names ref names =
-  let orig = universe_binders_of_global ref in
+let universe_binders_with_opt_names orig names =
+  let orig = AUContext.names orig in
   let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
diff --git a/engine/univNames.mli b/engine/univNames.mli
index dc669f45d6..6e68153ac2 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -29,5 +29,5 @@ type univ_name_list = Names.lname list
     of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
 
     Otherwise return the bound universe names registered for [ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
+val universe_binders_with_opt_names : AUContext.t ->
   univ_name_list option -> universe_binders
diff --git a/kernel/modops.ml b/kernel/modops.ml
index bab2eae3df..0dde1c7e75 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -47,10 +47,9 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.AUContext.t
+  | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 8e7e618fcd..0acd09fb12 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -106,10 +106,9 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.AUContext.t
+  | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d64342dbb0..347c30dd64 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -93,10 +93,8 @@ let check_conv_error error why cst poly f env a1 a2 =
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
 let check_polymorphic_instance error env auctx1 auctx2 =
-  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
-    error IncompatibleInstances
-  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
-    error (IncompatibleConstraints auctx1)
+  if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
   else
     Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0edf750997..2b3b4f9486 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -570,9 +570,9 @@ struct
   include S
 
   let pr prl c =
-    fold (fun (u1,op,u2) pp_std ->
-      pp_std ++ prl u1 ++ pr_constraint_type op ++
-	prl u2 ++ fnl () )  c (str "")
+    v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
+      hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
+       (elements c))
 
 end
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e698ba9f8f..712eb21ee6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,27 +71,26 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref udecl =
-  let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in
+  let env = Global.env () in
+  let typ, univs = Typeops.type_of_global_in_context env ref in
   let inst = Univ.make_abstract_instance univs in
-  let bl = UnivNames.universe_binders_with_opt_names ref udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
-      let env = Global.env () in
       let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let variance = match ref with
     | VarRef _ | ConstRef _ -> None
     | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
-      let mind = Environ.lookup_mind ind (Global.env ()) in
+      let mind = Environ.lookup_mind ind env in
       begin match mind.Declarations.mind_universes with
         | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
         | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
       end
   in
-  let env = Global.env () in
   let inst =
     if Global.is_polymorphic ref
     then Printer.pr_universe_instance sigma inst
@@ -571,7 +570,7 @@ let print_constant with_values sep sp udecl =
   in
   let ctx =
     UState.of_binders
-      (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl)
+      (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e..7ce08ed6bc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi =
 let pr_global_env = Nametab.pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
+let pr_universe_instance_constraints evd inst csts =
+  let open Univ in
+  let prlev = Termops.pr_evd_level evd in
+  let pcsts = if Constraint.is_empty csts then mt()
+    else str " |= " ++
+         prlist_with_sep (fun () -> str "," ++ spc())
+           (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v))
+           (Constraint.elements csts)
+  in
+  str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
+
 let pr_universe_instance evd inst =
-  str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+  pr_universe_instance_constraints evd inst Univ.Constraint.empty
 
 let pr_puniverses f env sigma (c,u) =
   if !Constrextern.print_universes
diff --git a/printing/printer.mli b/printing/printer.mli
index f9d1a62895..e50b02b508 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -85,6 +85,7 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
+val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index cc40c74998..2c3ab46670 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -119,7 +119,9 @@ let print_mutual_inductive env mind mib udecl =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names
+      (Declareops.inductive_polymorphic_context mib) udecl
+  in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -157,7 +159,9 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
+      udecl
+  in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
     let open Declarations in
@@ -296,7 +300,7 @@ let print_body is_impl extent env mp (l,body) =
       (match extent with
          | OnlyNames -> mt ()
          | WithContents ->
-            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in
+            let bl = UnivNames.universe_binders_with_opt_names ctx None in
             let sigma = Evd.from_ctx (UState.of_binders bl) in
 	    str " :" ++ spc () ++
             hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d63b6dbfce..4d3f7419e6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -41,8 +41,7 @@ Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
 Polymorphic bar@{u} = nat
      : Wrap@{u} Set
-(* u |= Set < u
-         *)
+(* u |= Set < u *)
 
 bar is universe polymorphic
 Polymorphic foo@{u UnivBinders.17 v} = 
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ba31f73030..6c7117b513 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -884,8 +884,6 @@ let explain_not_match_error = function
     let status b = if b then str"polymorphic" else str"monomorphic" in
       str "a " ++ status b ++ str" declaration was expected, but a " ++ 
 	status (not b) ++ str" declaration was found"
-  | IncompatibleInstances -> 
-    str"polymorphic universe instances do not match"
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
       Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
@@ -894,11 +892,22 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
       str "compared to " ++ spc () ++
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
-  | IncompatibleConstraints cst ->
-    str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in
-      (** FIXME: provide a proper naming for the bound variables *)
-      quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
+  | IncompatibleConstraints { got; expect } ->
+      let open Univ in
+    let pr_auctx auctx =
+      let sigma = Evd.from_ctx
+          (UState.of_binders
+             (UnivNames.universe_binders_with_opt_names auctx None))
+      in
+      let uctx = AUContext.repr auctx in
+      Printer.pr_universe_instance_constraints sigma
+        (UContext.instance uctx)
+        (UContext.constraints uctx)
+    in
+    str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++
+    str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++
+    (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else
+       fnl() ++ str "(incompatible constraints)")
 
 let explain_signature_mismatch l spec why =
   str "Signature components for label " ++ Label.print l ++