Improve bad variance error message: mention expected and actual variances

3 files changed, 25 insertions, 16 deletions

diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 2f9fb8686d..d02f92ef26 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -16,7 +16,10 @@ open Variance
 open Util
 
 exception TrivialVariance
-exception BadVariance of Level.t
+
+(** Not the same as Type_errors.BadVariance because we don't have the env where we raise. *)
+exception BadVariance of Level.t * Variance.t * Variance.t
+(* some ocaml bug is triggered if we make this an inline record *)
 
 module Inf : sig
   type variances
@@ -39,10 +42,18 @@ end = struct
     univs : (mode * inferred) LMap.t;
   }
 
+  let to_variance = function
+    | IrrelevantI -> Irrelevant
+    | CovariantI -> Covariant
+
+  let to_variance_opt o = Option.cata to_variance Invariant o
+
   let infer_level_eq u variances =
     match LMap.find_opt u variances.univs with
     | None -> variances
-    | Some (Check, _) -> raise (BadVariance u)
+    | Some (Check, expected) ->
+      let expected = to_variance expected in
+      raise (BadVariance (u, expected, Invariant))
     | Some (Infer, _) ->
       let univs = LMap.remove u variances.univs in
       if LMap.is_empty univs then raise TrivialVariance;
@@ -54,9 +65,9 @@ end = struct
       LMap.update u (function
           | None -> None
           | Some (_,CovariantI) as x -> x
-          | Some (Infer,IrrelevantI) ->
-            Some (Infer,CovariantI)
-          | Some (Check,IrrelevantI) -> raise (BadVariance u))
+          | Some (Infer,IrrelevantI) -> Some (Infer,CovariantI)
+          | Some (Check,IrrelevantI) ->
+            raise (BadVariance (u, Irrelevant, Covariant)))
         variances.univs
     in
     if univs == variances.univs then variances else {variances with univs}
@@ -74,11 +85,8 @@ end = struct
     {univs; orig_array=us}
 
   let finish variances =
-    Array.map (fun (u,_check) ->
-        match LMap.find_opt u variances.univs with
-        | None -> Invariant
-        | Some (_,CovariantI) -> Covariant
-        | Some (_,IrrelevantI) -> Irrelevant)
+    Array.map
+      (fun (u,_check) -> to_variance_opt (Option.map snd (LMap.find_opt u variances.univs)))
       variances.orig_array
 
 end
@@ -264,4 +272,5 @@ let infer_inductive ~env_params univs entries =
   try infer_inductive_core env_params univs entries
   with
   | TrivialVariance -> Array.make (Array.length univs) Invariant
-  | BadVariance u -> Type_errors.error_bad_variance env_params u
+  | BadVariance (lev, expected, actual) ->
+    Type_errors.error_bad_variance env_params ~lev ~expected ~actual
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 624604976e..bcb7aa88ca 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -69,7 +69,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
-  | BadVariance of Level.t
+  | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
 
 type type_error = (constr, types) ptype_error
 
@@ -164,8 +164,8 @@ let error_bad_relevance env =
 let error_bad_invert env =
   raise (TypeError (env, BadInvert))
 
-let error_bad_variance env u =
-  raise (TypeError (env, BadVariance u))
+let error_bad_variance env ~lev ~expected ~actual =
+  raise (TypeError (env, BadVariance {lev;expected;actual}))
 
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 7a7dba68b3..bcdcab9db7 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -70,7 +70,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
-  | BadVariance of Level.t
+  | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
 
 type type_error = (constr, types) ptype_error
 
@@ -147,7 +147,7 @@ val error_bad_relevance : env -> 'a
 
 val error_bad_invert : env -> 'a
 
-val error_bad_variance : env -> Level.t -> 'a
+val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
 
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error