aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/07-commands-and-options/11258-coherence.rst10
-rw-r--r--doc/sphinx/addendum/implicit-coercions.rst6
-rw-r--r--pretyping/classops.ml28
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/pretyping.ml31
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.out24
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.v51
7 files changed, 129 insertions, 23 deletions
diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst
new file mode 100644
index 0000000000..f04a120417
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11258-coherence.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+ The :cmd:`Coercion` command has been improved to check the coherence of the
+ inheritance graph. It checks whether a circular inheritance path of `C >-> C`
+ is convertible with the identity function or not, then report it as an
+ ambiguous path if it is not. The new mechanism does not report ambiguous
+ paths that are redundant with others. For example, checking the ambiguity of
+ `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
+ not be reported
+ (`#11258 <https://github.com/coq/coq/pull/11258>`_,
+ by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c3b197288f..19b33f0d90 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -165,6 +165,12 @@ Declaring Coercions
convertible with existing ones when they have coercions that don't satisfy
the uniform inheritance condition.
+ .. warn:: ... is not definitionally an identity function.
+
+ If a coercion path has the same source and target class, that is said to be
+ circular. When a new circular coercion path is not convertible with the
+ identity function, it will be reported as ambiguous.
+
.. cmdv:: Local Coercion @qualid : @class >-> @class
Declares the construction denoted by :token:`qualid` as a coercion local to
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index c12a236d8e..16021b66f8 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -297,15 +297,15 @@ let lookup_pattern_path_between env (s,t) =
(* rajouter une coercion dans le graphe *)
-let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref =
ref (fun _ -> str "<a class path>")
let install_path_printer f = path_printer := f
let print_path x = !path_printer x
-let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
- ref (fun _ _ _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref =
+ ref (fun _ _ _ _ _ -> false)
let install_path_comparator f = path_comparator := f
@@ -315,7 +315,10 @@ let warn_ambiguous_path =
CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
(fun l -> prlist_with_sep fnl (fun (c,p,q) ->
str"New coercion path " ++ print_path (c,p) ++
- str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
+ if List.is_empty q then
+ str" is not definitionally an identity function."
+ else
+ str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -334,10 +337,23 @@ let add_coercion_in_graph env sigma (ic,source,target) =
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
let try_add_new_path (i,j as ij) p =
+ (* If p is a cycle, we check whether p is definitionally an identity
+ function or not. If it is not, we report p as an ambiguous inheritance
+ path. *)
+ if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
+ ambig_paths := (ij,p,[])::!ambig_paths;
if not (Bijint.Index.equal i j) || different_class_params env i then
match lookup_path_between_class ij with
| q ->
- if not (compare_path env sigma p q) then
+ (* p has the same source and target classes as an existing path q. We
+ report them as ambiguous inheritance paths if
+ 1. p and q have no common element, and
+ 2. p and q are not convertible.
+ If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2,
+ convertibility of p1 and q1, also, p2 and q2 should be checked; thus,
+ checking the ambiguity of p and q is redundant with them. *)
+ if not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p ||
+ compare_path env sigma i p q) then
ambig_paths := (ij,p,q)::!ambig_paths;
false
| exception Not_found -> (add_new_path ij p; true)
@@ -355,7 +371,7 @@ let add_coercion_in_graph env sigma (ic,source,target) =
try_add_new_path1 (s,target) (p@[ic]);
ClPairMap.iter
(fun (u,v) q ->
- if not (Bijint.Index.equal u v) && Bijint.Index.equal u target && not (List.equal coe_info_typ_equal p q) then
+ if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 9c5274286e..9f633843eb 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -111,7 +111,7 @@ val lookup_pattern_path_between :
val install_path_printer :
((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
val install_path_comparator :
- (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
+ (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
(**/**)
(** {6 This is for printing purpose } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 43f9e55e14..0364e1b61f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1325,19 +1325,20 @@ let understand_ltac flags env sigma lvar kind c =
let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
(sigma, c)
-let path_convertible env sigma p q =
+let path_convertible env sigma i p q =
let open Classops in
let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in
let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in
+ let mkGSort u = DAst.make @@ Glob_term.GSort u in
let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
let path_to_gterm p =
match p with
| ic :: p' ->
let names =
- List.map (fun n -> Id.of_string ("x" ^ string_of_int n))
- (List.interval 0 ic.coe_param)
+ List.init (ic.coe_param + 1)
+ (fun n -> Id.of_string ("x" ^ string_of_int n))
in
List.fold_right
(fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
@@ -1345,9 +1346,29 @@ let path_convertible env sigma p q =
(fun t ic ->
mkGApp (mkGRef ic.coe_value,
List.make ic.coe_param (mkGHole ()) @ [t]))
- (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names))
+ (mkGApp (mkGRef ic.coe_value, List.map mkGVar names))
p'
- | [] -> anomaly (str "A coercion path shouldn't be empty.")
+ | [] ->
+ (* identity function for the class [i]. *)
+ let cl,params = class_info_from_index i in
+ let clty =
+ match cl with
+ | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
+ | CL_FUN -> anomaly (str "A source class must not be Funclass.")
+ | CL_SECVAR v -> mkGRef (GlobRef.VarRef v)
+ | CL_CONST c -> mkGRef (GlobRef.ConstRef c)
+ | CL_IND i -> mkGRef (GlobRef.IndRef i)
+ | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p))
+ in
+ let names =
+ List.init params.cl_param
+ (fun n -> Id.of_string ("x" ^ string_of_int n))
+ in
+ List.fold_right
+ (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
+ mkGLambda (Name (Id.of_string "x"),
+ mkGApp (clty, List.map mkGVar names),
+ mkGVar (Id.of_string "x"))
in
try
let sigma,tp = understand_tcc env sigma (path_to_gterm p) in
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index dc793598a9..ac5a09bad7 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -7,6 +7,16 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
[ac] : A >-> C
[bd] : B >-> D
[cd] : C >-> D
+File "stdin", line 26, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+[ac] : A >-> C
+[ac; cd] : A >-> D
+[ab] : A >-> B
+[cd] : C >-> D
+[bc] : B >-> C
+[bc; cd] : B >-> D
[B_A] : B >-> A
[C_A] : C >-> A
[D_B] : D >-> B
@@ -21,7 +31,7 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
-File "stdin", line 103, characters 0-86:
+File "stdin", line 121, characters 0-86:
Warning:
New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
@@ -34,3 +44,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
+File "stdin", line 130, characters 0-47:
+Warning:
+New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 131, characters 0-64:
+Warning:
+New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 132, characters 0-51:
+Warning:
+New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
+[ambiguous-paths,typechecker]
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
index a4af27539c..41322045f2 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -16,6 +16,24 @@ End test1.
Module test2.
Section test2.
+
+Variable (A B C D : Type).
+Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
+
+Local Coercion ac : A >-> C.
+Local Coercion cd : C >-> D.
+Local Coercion ab : A >-> B.
+Local Coercion bc : B >-> C.
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *)
+(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
Variable (A : Type) (P Q : A -> Prop).
Record B := {
@@ -39,11 +57,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
Print Graph.
-End test2.
-End test2.
+End test3.
+End test3.
-Module test3.
-Section test3.
+Module test4.
+Section test4.
Variable (A : Type) (P Q : A -> Prop).
@@ -71,11 +89,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
Print Graph.
-End test3.
-End test3.
+End test4.
+End test4.
-Module test4.
-Section test4.
+Module test5.
+Section test5.
Variable (A : Type) (P Q : A -> Prop).
@@ -105,5 +123,18 @@ Local Coercion D_C (d : D) : C true :=
Print Graph.
-End test4.
-End test4.
+End test5.
+End test5.
+
+Module test6.
+Record > NAT := wrap_nat { unwrap_nat :> nat }.
+Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE := wrap_Type { unwrap_Type :> Type }.
+End test6.
+
+Module test7.
+Set Primitive Projections.
+Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
+Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
+End test7.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:25:48 +0000