Merge PR coq#20012: More informative error from universe instance len…

…gth mismatch

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

dev/ci/user-overlays/20012-SkySkimmer-instance-length-mismatch-error.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi instance-length-mismatch-error 20012

engine/univGen.ml

@@ -30,6 +30,7 @@ let diff_sort_context ((qs,us),csts) ((qs',us'),csts') =
   (QVar.Set.diff qs qs', Level.Set.diff us us'), Constraints.diff csts csts'
 
 type univ_length_mismatch = {
+  gref : GlobRef.t;
   actual : int * int;
   expect : int * int;
 }
@@ -38,14 +39,15 @@ compliation with -rectypes to crash. *)
 exception UniverseLengthMismatch of univ_length_mismatch
 
 let () = CErrors.register_handler (function
-    | UniverseLengthMismatch { actual=(aq,au); expect=(eq,eu) } ->
+    | UniverseLengthMismatch { gref; actual=(aq,au); expect=(eq,eu) } ->
       let ppreal, ppexpected =
         if aq = 0 && eq = 0 then Pp.(int au, int eu)
         else Pp.(str "(" ++ int aq ++ str " | " ++ int au ++ str ")"
                 , str "(" ++ int eq ++ str " | " ++ int eu ++ str ")")
       in
-      Some Pp.(str "Universe instance length is " ++ ppreal
-               ++ str " but should be " ++ ppexpected ++ str".")
+      Some Pp.(str "Universe instance length for " ++ Nametab.pr_global_env Id.Set.empty gref ++
+               spc() ++ str "is " ++ ppreal ++
+               spc() ++ str "but should be " ++ ppexpected ++ str".")
   | _ -> None)
 
 (* Generator of levels *)
@@ -82,24 +84,25 @@ let fresh_instance auctx : _ in_sort_context_set =
   let inst = Instance.of_array (qinst,uinst) in
   inst, ((qctx,uctx), AbstractContext.instantiate inst auctx)
 
-let existing_instance ?loc auctx inst =
+let existing_instance ?loc ~gref auctx inst =
   let () =
     let actual = Instance.length inst
     and expect = AbstractContext.size auctx in
       if not (UVars.eq_sizes actual expect) then
-        Loc.raise ?loc (UniverseLengthMismatch { actual; expect })
+        Loc.raise ?loc (UniverseLengthMismatch { gref; actual; expect })
       else ()
   in
   inst, ((Sorts.QVar.Set.empty,Level.Set.empty), AbstractContext.instantiate inst auctx)
 
 let fresh_instance_from ?loc ctx = function
-  | Some inst -> existing_instance ?loc ctx inst
+  | Some (gref,inst) -> existing_instance ?loc ~gref ctx inst
   | None -> fresh_instance ctx
 
 (** Fresh universe polymorphic construction *)
 
 let fresh_global_instance ?loc ?names env gr =
   let auctx = Environ.universes_of_global env gr in
+  let names = Option.map (fun x -> gr, x) names in
   let u, ctx = fresh_instance_from ?loc auctx names in
   u, ctx
 

engine/univGen.mli

@@ -15,6 +15,7 @@ open Univ
 open UVars
 
 type univ_length_mismatch = {
+  gref : GlobRef.t;
   actual : int * int;
   expect : int * int;
 }
@@ -47,7 +48,8 @@ val diff_sort_context : sort_context_set -> sort_context_set -> sort_context_set
 
 val fresh_instance : AbstractContext.t -> Instance.t in_sort_context_set
 
-val fresh_instance_from : ?loc:Loc.t -> AbstractContext.t -> Instance.t option ->
+(** The globref is only used for the error message when there is a mismatch. *)
+val fresh_instance_from : ?loc:Loc.t -> AbstractContext.t -> (GlobRef.t * Instance.t) option ->
   Instance.t in_sort_context_set
 
 val fresh_sort_in_family : Sorts.family ->

pretyping/pretyping.ml

@@ -576,6 +576,7 @@ let pretype_ref ?loc sigma env ref us =
         | Some (qs,us) ->
             let open UnivGen in
             Loc.raise ?loc (UniverseLengthMismatch {
+              gref = ref;
               actual = List.length qs, List.length us;
               expect = 0, 0;
             }));
@@ -1584,14 +1585,19 @@ let pretype_type self c ?loc ~flags valcon (env : GlobEnv.t) sigma = match DAst.
 
   let pretype_array self (u,t,def,ty) =
     fun ?loc ~flags tycon env sigma ->
+    let array_kn =   match (!!env).retroknowledge.Retroknowledge.retro_array with
+  | Some c -> c
+  | None -> CErrors.user_err Pp.(str"The type array must be registered before this construction can be typechecked.")
+    in
     let sigma, u = match u with
       | None -> sigma, None
       | Some ([],[u]) ->
         let sigma, u = glob_level ?loc sigma u in
         sigma, Some u
       | Some (qs,us) ->
-          let open UnivGen in
+        let open UnivGen in
           Loc.raise ?loc (UniverseLengthMismatch {
+            gref = ConstRef array_kn;
             actual = List.length qs, List.length us;
             expect = 0, 1;
           })
@@ -1612,7 +1618,7 @@ let pretype_type self c ?loc ~flags valcon (env : GlobEnv.t) sigma = match DAst.
         (ESorts.make (Sorts.sort_of_univ (Univ.Universe.make u)))
     in
     let u = UVars.Instance.of_array ([||],[| u |]) in
-    let ta = EConstr.of_constr @@ Typeops.type_of_array !!env u in
+    let ta = EConstr.mkConstU (array_kn, EInstance.make u) in
     let j = {
       uj_val = EConstr.mkArray(EInstance.make u, Array.map (fun j -> j.uj_val) jt, jdef.uj_val, jty.utj_val);
       uj_type = EConstr.mkApp(ta,[|jdef.uj_type|])

printing/printer.ml

@@ -187,7 +187,7 @@ let universe_binders_with_opt_names orig names =
   let qorig, uorig as orig = Array.to_list qorig, Array.to_list uorig in
   let qdecl, udecl = match names with
   | None -> orig
-  | Some (qdecl,udecl) ->
+  | Some (gref, (qdecl, udecl)) ->
     try
       let qs =
         List.map2 (fun orig {CAst.v = na} ->
@@ -205,6 +205,7 @@ let universe_binders_with_opt_names orig names =
     with Invalid_argument _ ->
       let open UnivGen in
       raise (UniverseLengthMismatch {
+          gref;
           actual = List.length qorig, List.length uorig;
           expect = List.length qdecl, List.length udecl;
         })

printing/printer.mli

@@ -140,7 +140,7 @@ val pr_universes  : evar_map ->
 
     Inefficient on large contexts due to name generation. *)
 val universe_binders_with_opt_names : UVars.AbstractContext.t ->
-  UnivNames.full_name_list option -> UnivNames.universe_binders * UnivNames.rev_binders
+  (GlobRef.t * UnivNames.full_name_list) option -> UnivNames.universe_binders * UnivNames.rev_binders
 
 (** Printing global references using names as short as possible *)
 

test-suite/output/UnivBinders.out

@@ -112,10 +112,10 @@ punwrap is transparent
 Expands to: Constant UnivBinders.punwrap
 File "./output/UnivBinders.v", line 104, characters 0-19:
 The command has indeed failed with message:
-Universe instance length is 3 but should be 1.
+Universe instance length for foo is 3 but should be 1.
 File "./output/UnivBinders.v", line 105, characters 0-20:
 The command has indeed failed with message:
-Universe instance length is 0 but should be 1.
+Universe instance length for mono is 0 but should be 1.
 File "./output/UnivBinders.v", line 108, characters 0-33:
 The command has indeed failed with message:
 This object does not support universe names.

vernac/prettyp.ml

@@ -56,6 +56,7 @@ let print_basename cst = pr_global (GlobRef.ConstRef cst)
 let print_ref env reduce ref udecl =
   let typ, univs = Typeops.type_of_global_in_context env ref in
   let inst = UVars.make_abstract_instance univs in
+  let udecl = Option.map (fun x -> ref, x) udecl in
   let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_names bl) in
   let typ =
@@ -239,6 +240,7 @@ let print_squash env ref udecl = match ref with
     | None -> []
     | Some squash ->
       let univs = Environ.universes_of_global env ref in
+      let udecl = Option.map (fun x -> ref, x) udecl in
       let bl = Printer.universe_binders_with_opt_names univs udecl in
       let sigma = Evd.from_ctx (UState.of_names bl) in
       let inst = if fst @@ UVars.AbstractContext.size univs = 0 then mt()
@@ -578,6 +580,7 @@ let print_constant env ~with_values with_implicit cst udecl =
   let cb = Environ.lookup_constant cst env in
   let typ = cb.const_type in
   let univs = cb.const_universes in
+  let udecl = Option.map (fun x -> GlobRef.ConstRef cst, x) udecl in
   let uctx =
     UState.of_names
       (Printer.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)

vernac/printmod.ml

@@ -159,6 +159,7 @@ let pr_mutual_inductive_body env mind mib udecl =
        | PrimRecord l -> "Record", true, Array.map_to_list (fun (id,_,_,_) -> Name id) l
        | FakeRecord | NotRecord -> "Variant", false, default_as
   in
+  let udecl = Option.map (fun x -> GlobRef.IndRef (mind,0), x) udecl in
   let bl = Printer.universe_binders_with_opt_names
       (Declareops.inductive_polymorphic_context mib) udecl
   in