Print full binders in subtyping incompatible polymorphism error.

Close #8891

6 files changed, 30 insertions, 16 deletions

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/printing/printer.ml b/printing/printer.ml
index da364c8b9e..8227933433 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) -> 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/vernac/himsg.ml b/vernac/himsg.ml
index ba31f73030..ad70f2067b 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,19 @@ 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
+    (** FIXME: provide a proper naming for the bound variables *)
+    let pr_auctx auctx =
+      let uctx = AUContext.repr auctx in
+      Printer.pr_universe_instance_constraints Evd.empty
+        (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
+       spc() ++ str "(incompatible constraints)")
 
 let explain_signature_mismatch l spec why =
   str "Signature components for label " ++ Label.print l ++