diff options
| -rw-r--r-- | interp/implicit_quantifiers.ml | 47 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13117.v | 23 |
2 files changed, 53 insertions, 17 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0ed0b8a1a5..0f05cc5e10 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -122,12 +122,24 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id +let rec is_class_arg c = + let open Constr in + match kind c with + | Prod (_,_,c) + | Cast (c,_,_) + | LetIn (_,_,_,c) -> is_class_arg c + | _ -> + let c, _ = decompose_appvect c in + match destRef c with + | exception DestKO -> false + | r, _ -> is_class r + let combine_params avoid applied needed = let named, applied = List.partition (function (t, Some {CAst.loc;v=ExplByName id}) -> - let is_id (_, decl) = Name.equal (Name id) (RelDecl.get_name decl) in + let is_id decl = Name.equal (Name id) (RelDecl.get_name decl) in if not (List.exists is_id needed) then user_err ?loc (str "Wrong argument name: " ++ Id.print id); true @@ -138,25 +150,27 @@ let combine_params avoid applied needed = named in let rec aux ids avoid app need = - match app, need with - - | _, (_, LocalDef _) :: need -> aux ids avoid app need + match need with + | [] -> begin match app with + | [] -> List.rev ids, avoid + | (x, _) :: _ -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") + end - | [], [] -> List.rev ids, avoid + | LocalDef _ :: need -> aux ids avoid app need - | _, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> - aux (Id.List.assoc id named :: ids) avoid app need - | (x, _) :: app, (false, _) :: need -> aux (x :: ids) avoid app need + | LocalAssum ({binder_name=Name id}, _) :: need when Id.List.mem_assoc id named -> + aux (Id.List.assoc id named :: ids) avoid app need - | _, (true, decl) :: need - | [], (false, decl) :: need -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - let t' = CAst.make @@ CRef (qualid_of_ident id',None) in - aux (t' :: ids) (Id.Set.add id' avoid) app need + | decl :: need -> + begin match app, is_class_arg (get_type decl) with + | (x, _) :: app, false -> aux (x :: ids) avoid app need - | (x,_) :: _, [] -> - user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") + | [], false | _, true -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need + end in aux [] avoid applied needed @@ -186,8 +200,7 @@ let implicit_application env ty = let sigma = Evd.from_env env in let c = class_info env sigma gr in let (ci, rd) = c.cl_context in - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid par pars in + let args, avoid = combine_params avoid par (List.rev rd) in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = diff --git a/test-suite/bugs/closed/bug_13117.v b/test-suite/bugs/closed/bug_13117.v new file mode 100644 index 0000000000..5db3f9fadc --- /dev/null +++ b/test-suite/bugs/closed/bug_13117.v @@ -0,0 +1,23 @@ + +Class A := {}. + +Class B (x:A) := {}. +Class B' (a:=A) (x:a) := {}. + +Fail Definition foo a `{B a} := 0. +Definition foo a `{B' a} := 0. + +Record C (x:A) := {}. +Existing Class C. + +Fail Definition bar a `{C a} := 0. + + +Definition X := Type. + +Class Y (x:X) := {}. + +Definition before `{Y Set} := 0. + +Existing Class X. +Fail Definition after `{Y Set} := 0. |