diff options
| author | Gaëtan Gilbert | 2018-11-02 12:55:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:09:52 +0100 |
| commit | 14c5b4bb8a9c5f62081594d2beaca274eaa0b8f3 (patch) | |
| tree | a8093604c95ccd1081aedab2de45d01920af1334 /vernac | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Print full binders in subtyping incompatible polymorphism error.
Close #8891
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 20 |
1 files changed, 13 insertions, 7 deletions
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 ++ |