aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10177-SkySkimmer-generalize.sh6
-rw-r--r--interp/constrexpr.ml4
-rw-r--r--interp/constrexpr_ops.ml4
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/implicit_quantifiers.ml59
-rw-r--r--library/libnames.ml3
-rw-r--r--library/libnames.mli3
-rw-r--r--parsing/g_constr.mlg4
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--test-suite/bugs/closed/bug_10176.v7
10 files changed, 59 insertions, 42 deletions
diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh
new file mode 100644
index 0000000000..a89f6aca1b
--- /dev/null
+++ b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then
+
+ quickchick_CI_REF=generalize
+ quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+
+fi
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9f778d99e9..3ebbbdfb88 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -40,8 +40,8 @@ type explicitation =
type binder_kind =
| Default of binding_kind
- | Generalized of binding_kind * binding_kind * bool
- (** Inner binding, outer bindings, typeclass-specific flag
+ | Generalized of binding_kind * bool
+ (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 443473d5b6..bcb2f34377 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
let binder_kind_eq b1 b2 = match b1, b2 with
| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
-| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
- binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+| Generalized (ck1, b1), Generalized (ck2, b2) ->
+ binding_kind_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f06493b374..753065b7dd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
{env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type ntnvars
- env {loc;v=na} b b' t ty =
+ env {loc;v=na} b' t ty =
let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
let ty, ids' =
if t then ty, ids else
@@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
env fvs in
let bl = List.map
CAst.(map (fun id ->
- (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+ (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty =
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
- | Generalized (b,b',t) ->
- let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
+ | Generalized (b',t) ->
+ let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in
env, b
let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 6277d874dd..bac46c2d2f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -196,10 +196,9 @@ let combine_params avoid fn applied needed =
user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
-let combine_params_freevar =
- fun avoid (_, decl) ->
- let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
+let combine_params_freevar avoid (_, decl) =
+ let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+ (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
let destClassApp cl =
let open CAst in
@@ -222,34 +221,34 @@ let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
- let gr = Nametab.locate qid in
- if Typeclasses.is_class gr then Some (clapp, gr) else None
+ if Libnames.idset_mem_qualid qid env then None
+ else
+ let gr = Nametab.locate qid in
+ if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
in
- match is_class with
- | None -> ty, env
- | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
- let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
- let c, avoid =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let c = class_info env sigma gr in
- let (ci, rd) = c.cl_context in
- if not allow_partial then
- begin
- let opt_succ x n = match x with
- | None -> succ n
- | Some _ -> n
- in
- let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
- let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
- if not (Int.equal needlen applen) then
- mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
- end;
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params avoid f par pars in
- CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
- in c, avoid
+ match is_class with
+ | None -> ty, env
+ | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
+ let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c = class_info env sigma gr in
+ let (ci, rd) = c.cl_context in
+ if not allow_partial then
+ begin
+ let opt_succ x n = match x with
+ | None -> succ n
+ | Some _ -> n
+ in
+ let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+ if not (Int.equal needlen applen) then
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+ end;
+ let pars = List.rev (List.combine ci rd) in
+ let args, avoid = combine_params avoid f par pars in
+ CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
let warn_ignoring_implicit_status =
CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/library/libnames.ml b/library/libnames.ml
index 87c4de42e8..41b38e0378 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,6 +162,9 @@ let qualid_basename qid =
let qualid_path qid =
qid.CAst.v.dirpath
+let idset_mem_qualid qid s =
+ qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s
+
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/libnames.mli b/library/libnames.mli
index bbb4d2a058..7d77d95991 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> DirPath.t
val qualid_basename : qualid -> Id.t
+val idset_mem_qualid : qualid -> Id.Set.t -> bool
+(** false when the qualid is not an ident *)
+
(** {6 ... } *)
(** some preset paths *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 4a9190c10a..6df97609f5 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -500,9 +500,9 @@ GRAMMAR EXTEND Gram
| "{"; id=name; idl=LIST1 name; "}" ->
{ List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
| "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
- { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc }
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
| "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
- { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc }
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc }
| "'"; p = pattern LEVEL "0" ->
{ let (p, ty) =
match p.CAst.v with
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 78733784a7..9d3ed40f6c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -339,8 +339,7 @@ let tag_var = tag Tag.variable
let pr_binder many pr (nal,k,t) =
match k with
- | Generalized (b, b', t') ->
- assert (match b with Implicit -> true | _ -> false);
+ | Generalized (b', t') ->
begin match nal with
|[{loc; v=Anonymous}] ->
hov 1 (str"`" ++ (surround_impl b'
diff --git a/test-suite/bugs/closed/bug_10176.v b/test-suite/bugs/closed/bug_10176.v
new file mode 100644
index 0000000000..fdb0eb87a4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10176.v
@@ -0,0 +1,7 @@
+Class Foo (xxx:nat) := foo : nat.
+
+Lemma aa `{Foo} : nat. Abort.
+
+Fail Lemma xy (Foo:bool->Type) `{Foo} : nat.
+
+Fail Lemma yx (Fooo:bool->Type) `{Fooo} : nat.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:51:44 +0000