From 9a81055a7f846c64128c1d54ab3630b53bbd3d22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 10 Jan 2025 17:38:02 +0100 Subject: [PATCH] More informative error from universe instance length mismatch (print the globref in question, cf output test change) --- engine/univGen.ml | 15 +++++++++------ engine/univGen.mli | 4 +++- pretyping/pretyping.ml | 10 ++++++++-- printing/printer.ml | 3 ++- printing/printer.mli | 2 +- test-suite/output/UnivBinders.out | 4 ++-- vernac/prettyp.ml | 3 +++ vernac/printmod.ml | 1 + 8 files changed, 29 insertions(+), 13 deletions(-) diff --git a/engine/univGen.ml b/engine/univGen.ml index f8cac3cbb277..097d317bdad1 100644 --- a/engine/univGen.ml +++ b/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 diff --git a/engine/univGen.mli b/engine/univGen.mli index dd96d7004a49..735118120d01 100644 --- a/engine/univGen.mli +++ b/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 -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3ae7f446e055..77d16e68192e 100644 --- a/pretyping/pretyping.ml +++ b/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|]) diff --git a/printing/printer.ml b/printing/printer.ml index c25e82fee8c3..50a93ef6395f 100644 --- a/printing/printer.ml +++ b/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; }) diff --git a/printing/printer.mli b/printing/printer.mli index 0d25c3b36273..295da591f170 100644 --- a/printing/printer.mli +++ b/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 *) diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a705c9ea04d1..458cfc24ca3d 100644 --- a/test-suite/output/UnivBinders.out +++ b/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. diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 3f45b0909190..ee271a265c7d 100644 --- a/vernac/prettyp.ml +++ b/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) diff --git a/vernac/printmod.ml b/vernac/printmod.ml index 24295857e5c2..14a3d7342dcc 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -158,6 +158,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