diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index ae5c4b6880..bcb7aa88ca 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error = | DisallowedSProp | BadRelevance | BadInvert + | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t } type type_error = (constr, types) ptype_error @@ -163,6 +164,9 @@ let error_bad_relevance env = let error_bad_invert env = raise (TypeError (env, BadInvert)) +let error_bad_variance env ~lev ~expected ~actual = + raise (TypeError (env, BadVariance {lev;expected;actual})) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -207,3 +211,4 @@ let map_ptype_error f = function | DisallowedSProp -> DisallowedSProp | BadRelevance -> BadRelevance | BadInvert -> BadInvert +| BadVariance u -> BadVariance u |