diff options
| author | Matthieu Sozeau | 2014-10-02 23:48:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-02 23:57:22 +0200 |
| commit | a0e47bcf277d11ec7d2272bc5167fee898ad9016 (patch) | |
| tree | e4323e150457f947400cd26c84ef294f33c1da97 /toplevel | |
| parent | 0c320e79ba30bf567d4ca194bc114d733baf76e5 (diff) | |
Implement module subtyping for polymorphic constants (errors on
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 54f7179508..15d6e29eb2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -819,6 +819,23 @@ let explain_not_match_error = function | NoTypeConstraintExpected -> strbrk "a definition whose type is constrained can only be subtype " ++ strbrk "of a definition whose type is itself constrained" + | PolymorphicStatusExpected b -> + 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 incon + | IncompatiblePolymorphism (env, t1, t2) -> + str "conversion of polymorphic values generates additional constraints: " ++ + quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ + str "compared to " ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env Evd.empty t2) + | IncompatibleConstraints cst -> + str " the expected (polymorphic) constraints do not imply " ++ + quote (Univ.pr_constraints cst) let explain_signature_mismatch l spec why = str "Signature components for label " ++ str (Label.to_string l) ++ |