Merge PR #10202: Slightly more robust manual implicit arguments

Reviewed-by: ejgallego

7 files changed, 150 insertions, 59 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ff115a3e48..c699f79351 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -256,7 +256,9 @@ type intern_env = {
   unb: bool;
   tmp_scope: Notation_term.tmp_scope_name option;
   scopes: Notation_term.scope_name list;
-  impls: internalization_env }
+  impls: internalization_env;
+  impl_binder_index: int option;
+}
 
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
@@ -317,27 +319,50 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
-let build_impls = function
-  |Implicit -> (function
-                  |Name id ->  Some (id, Impargs.Manual, (true,true))
-                  |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
-  |Explicit -> fun _ -> None
-
-let impls_type_list ?(args = []) =
-  let rec aux acc c = match DAst.get c with
-    | GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
-    | _ -> (Variable,[],List.append args (List.rev acc),[])
+
+let warn_shadowed_implicit_name =
+  CWarnings.create ~name:"shadowed-implicit-name" ~category:"syntax"
+    Pp.(fun na -> str "Making shadowed name of implicit argument accessible by position.")
+
+let exists_name na l =
+  match na with
+  | Name id -> List.exists (function Some (ExplByName id',_,_) -> Id.equal id id' | _ -> false) l
+  | _ -> false
+
+let build_impls ?loc n bk na acc =
+  match bk with
+  | Implicit ->
+    let na =
+       if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+       else na in
+    let impl = match na with
+     | Name id -> Some (ExplByName id,Manual,(true,true))
+     | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+     impl :: acc
+  | Explicit -> None :: acc
+
+let impls_binder_list =
+  let rec aux acc n = function
+    | (na,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders
+    | (na,bk,Some _,_) :: binders -> aux acc n binders
+    | [] -> (n,acc)
   in aux []
 
-let impls_term_list ?(args = []) =
-  let rec aux acc c = match DAst.get c with
-    | GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+let impls_type_list n ?(args = []) =
+  let rec aux acc n c = match DAst.get c with
+    | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
+    | _ -> (Variable,[],List.rev acc,[])
+  in aux args n
+
+let impls_term_list n ?(args = []) =
+  let rec aux acc n c = match DAst.get c with
+    | GLambda (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
     | GRec (fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-       let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
-         aux acc' bds.(nb)
-    |_ -> (Variable,[],List.append args (List.rev acc),[])
-  in aux []
+       let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
+       aux acc' n bds.(nb)
+    |_ -> (Variable,[],List.rev acc,[])
+  in aux args n
 
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
 let rec check_capture ty = let open CAst in function
@@ -396,6 +421,14 @@ let remember_binders_impargs env bl =
 let restore_binders_impargs env l =
   List.fold_right pure_push_name_env l env
 
+let warn_unexpected_implicit_binder_declaration =
+  CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax"
+    Pp.(fun () -> str "Unexpected implicit binder declaration.")
+
+let check_implicit_meaningful ?loc k env =
+  if k = Implicit && env.impl_binder_index = None then
+    warn_unexpected_implicit_binder_declaration ?loc ()
+
 let intern_generalized_binder intern_type ntnvars
     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
@@ -408,6 +441,7 @@ let intern_generalized_binder intern_type ntnvars
   let env' = List.fold_left
     (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
     env fvs in
+  check_implicit_meaningful ?loc b' env;
   let bl = List.map
     CAst.(map (fun id ->
       (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
@@ -423,8 +457,10 @@ let intern_generalized_binder intern_type ntnvars
               | _ -> default_non_dependent_ident
             in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
           in Name name
-    | _ -> na
-  in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
+    | _ -> na in
+  let impls = impls_type_list 1 ty' in
+  (push_name_env ntnvars impls env' (make ?loc na),
+   (make ?loc (na,b',ty')) :: List.rev bl)
 
 let intern_assumption intern ntnvars env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
@@ -432,9 +468,10 @@ let intern_assumption intern ntnvars env nal bk ty =
   | Default k ->
       let ty = intern_type env ty in
       check_capture ty nal;
-      let impls = impls_type_list ty in
+      let impls = impls_type_list 1 ty in
       List.fold_left
         (fun (env, bl) ({loc;v=na} as locna) ->
+          check_implicit_meaningful ?loc k env;
           (push_name_env ntnvars impls env locna,
            (make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
         (env, []) nal
@@ -457,7 +494,8 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
 let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
   let term = intern env def in
   let ty = Option.map (intern env) ty in
-  (push_name_env ntnvars (impls_term_list term) env locna,
+  let impls = impls_term_list 1 term in
+  (push_name_env ntnvars impls env locna,
    (na,Explicit,term,ty))
 
 let intern_cases_pattern_as_binder ?loc ntnvars env p =
@@ -1105,7 +1143,8 @@ let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false ;
-       tmp_scope = None; scopes = []; impls = empty_internalization_env}
+       tmp_scope = None; scopes = []; impls = empty_internalization_env;
+       impl_binder_index = None}
       Environ.empty_named_context_val
       (vars, Id.Map.empty) None [] r
   in r
@@ -1872,10 +1911,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (* We add the recursive functions to the environment *)
         let env_rec = List.fold_left_i (fun i en name ->
            let (_,bli,tyi,_) = idl_temp.(i) in
-           let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
-           let fix_args = List.map (fun (na, bk, t, _) -> build_impls bk na) bli in
-           push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
-           en (CAst.make @@ Name name)) 0 env lf in
+           let binder_index,fix_args = impls_binder_list 1 bli in
+           let impls = impls_type_list ~args:fix_args binder_index tyi in
+           push_name_env ntnvars impls en (CAst.make @@ Name name)) 0 env lf in
         let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) ->
             (* We add the binders common to body and type to the environment *)
             let env_body = restore_binders_impargs env_rec before_impls in
@@ -1904,9 +1942,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             (bl,intern_type env' ty,bl_impls)) dl in
         let env_rec = List.fold_left_i (fun i en name ->
           let (bli,tyi,_) = idl_tmp.(i) in
-          let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
-          let cofix_args =  List.map (fun (na, bk, _, _) -> build_impls bk na) bli in
-          push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
+          let binder_index,cofix_args = impls_binder_list 1 bli in
+          push_name_env ntnvars (impls_type_list ~args:cofix_args binder_index tyi)
             en (CAst.make @@ Name name)) 0 env lf in
         let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) ->
           (* We add the binders common to body and type to the environment *)
@@ -1927,11 +1964,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
         expand_binders ?loc mkGLambda bl (intern env' c2)
     | CLetIn (na,c1,t,c2) ->
-        let inc1 = intern (reset_tmp_scope env) c1 in
-        let int = Option.map (intern_type env) t in
+        let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in
+        let int = Option.map (intern_type_restart_implicit env) t in
         DAst.make ?loc @@
         GLetIn (na.CAst.v, inc1, int,
-          intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
+          intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
     | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
@@ -2114,7 +2151,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     (* Parsing existential variables *)
     | CEvar (n, l) ->
         DAst.make ?loc @@
-        GEvar (n, List.map (on_snd (intern env)) l)
+        GEvar (n, List.map (on_snd (intern_no_implicit env)) l)
     | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
@@ -2127,8 +2164,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     )
   and intern_type env = intern (set_type_scope env)
 
+  and intern_no_implicit env = intern {env with impl_binder_index = None}
+
+  and intern_restart_implicit env = intern {env with impl_binder_index = Some 0}
+
+  and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0}
+
   and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
-    intern_local_binder_aux intern ntnvars env bind
+    intern_local_binder_aux intern_restart_implicit ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern env n pl =
@@ -2160,7 +2203,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 
   and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (* the "match" part *)
-    let tm' = intern env tm in
+    let tm' = intern_no_implicit env tm in
     (* the "as" part *)
     let extra_id,na =
       let loc = tm'.CAst.loc in
@@ -2229,7 +2272,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             let id = name_of_implicit imp in
             let (_,a) = Id.Map.find id eargs in
             let eargs' = Id.Map.remove id eargs in
-            intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
+            intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs' rargs
           with Not_found ->
           if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then
             (* Less regular arguments than expected: complete *)
@@ -2241,7 +2284,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
               ) :: aux (n+1) impl' subscopes' eargs rargs
           end
       | (imp::impl', a::rargs') ->
-          intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
+          intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs rargs'
       | (imp::impl', []) ->
           if not (Id.Map.is_empty eargs) then
             (let (id,(loc,_)) = Id.Map.choose eargs in
@@ -2271,7 +2314,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | [] -> []
     | a::args ->
         let (enva,subscopes) = apply_scope_env env subscopes in
-        (intern enva a) :: (intern_args env subscopes args)
+        (intern_no_implicit enva a) :: (intern_args env subscopes args)
 
   in
   try
@@ -2307,7 +2350,7 @@ let intern_gen kind env sigma
   let tmp_scope = scope_of_type_kind sigma kind in
   internalize env {ids = extract_ids env; unb = false;
                          tmp_scope = tmp_scope; scopes = [];
-                         impls = impls}
+                         impls; impl_binder_index = Some 0}
     pattern_mode (ltacvars, Id.Map.empty) c
 
 let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
@@ -2389,7 +2432,8 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
   let tmp_scope = scope_of_type_kind sigma kind in
   let impls = empty_internalization_env in
-  internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+  internalize env
+    {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0}
     pattern_mode (ltacvars, vl) c
 
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
@@ -2397,7 +2441,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
-  let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
+  let c = internalize env
+    {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None}
     false (empty_ltac_sign, vl) a in
   (* Splits variables into those that are binding, bound, or both *)
   (* Translate and check that [c] has all its free variables bound in [vars] *)
@@ -2433,7 +2478,8 @@ let intern_context env impl_env binders =
                let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
                (env, bl))
             ({ids = extract_ids env; unb = false;
-              tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
+              tmp_scope = None; scopes = []; impls = impl_env;
+              impl_binder_index = Some 0}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2aa002ead1..df28b32f81 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
 open EConstr
 open Reductionops
 open Namegen
+open Constrexpr
 
 module NamedDecl = Context.Named.Declaration
 
@@ -289,7 +290,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal
 
 type implicit_status =
     (* None = Not implicit *)
-    (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
+    (explicitation * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
 
@@ -299,9 +300,12 @@ let is_status_implicit = function
   | None -> false
   | _ -> true
 
+let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+
 let name_of_implicit = function
   | None -> anomaly (Pp.str "Not an implicit argument.")
-  | Some (id,_,_) -> id
+  | Some (ExplByName id,_,_) -> id
+  | Some (ExplByPos (k,_),_,_) -> name_of_pos k
 
 let maximal_insertion_of = function
   | Some (_,_,(b,_)) -> b
@@ -336,7 +340,7 @@ let rec prepare_implicits f = function
   | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
   | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
-      Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+      Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
 let set_manual_implicits flags enriching autoimps l =
@@ -346,15 +350,14 @@ let set_manual_implicits flags enriching autoimps l =
        let imps' = merge (k+1) autoimps explimps in
        begin match autoimp, explimp.CAst.v with
        | (Name id,_), Some (_,max) ->
-          Some (id, Manual, (set_maximality imps' max, true))
+          Some (ExplByName id, Manual, (set_maximality imps' max, true))
        | (Name id,Some exp), None when enriching ->
-          Some (id, exp, (set_maximality imps' flags.maximal, true))
+          Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
        | (Name _,_), None -> None
        | (Anonymous,_), Some (Name id,max) ->
-          Some (id,Manual,(max,true))
+          Some (ExplByName id,Manual,(max,true))
        | (Anonymous,_), Some (Anonymous,max) ->
-          let id = Id.of_string ("arg_" ^ string_of_int k) in
-          Some (id,Manual,(max,true))
+          Some (ExplByPos (k,None),Manual,(max,true))
        | (Anonymous,_), None -> None
        end :: imps'
     | [], [] -> []
@@ -464,7 +467,7 @@ let implicits_of_global ref =
         | [], _ -> []
         | _, [] -> implicits
         | Some (_, x,y) :: implicits, Name id :: names ->
-           Some (id, x,y) :: rename implicits names
+           Some (ExplByName id, x,y) :: rename implicits names
         | imp :: implicits, _ :: names -> imp :: rename implicits names
       in
       List.map (fun (t, il) -> t, rename il rename_l) l
@@ -494,7 +497,7 @@ let impls_of_context ctx =
   let map decl =
     let id = NamedDecl.get_id decl in
     match Id.Map.get id !sec_implicits with
-    | Glob_term.Implicit -> Some (id, Manual, (true, true))
+    | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
     | Glob_term.Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -655,12 +658,12 @@ let compute_implicit_statuses autoimps l =
   let rec aux i = function
     | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
     | Name id :: autoimps, MaximallyImplicit :: manualimps ->
-       Some (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+       Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
     | Name id :: autoimps, Implicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
        let max = set_maximality imps' false in
        if max then warn_set_maximal_deprecated i;
-       Some (id, Manual, (max, true)) :: imps'
+       Some (ExplByName id, Manual, (max, true)) :: imps'
     | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
        user_err ~hdr:"set_implicits"
          (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 8fa69e818a..ef3c2496f4 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -68,7 +68,7 @@ type maximal_insertion = bool (** true = maximal contextual insertion *)
 
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
-type implicit_status = (Id.t * implicit_explanation *
+type implicit_status = (Constrexpr.explicitation * implicit_explanation *
                           (maximal_insertion * force_inference)) option
     (** [None] = Not implicit *)
 
diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+   be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
 
 Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
 Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 23853890d8..ecaaedca53 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -124,3 +124,36 @@ Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
 (* Check global implicit declaration over ref not in section *)
 
 Section D. Global Arguments eq [A] _ _. End D.
+
+(* Check local manual implicit arguments *)
+(* Gives a warning and make the second x anonymous *)
+(* Isn't the name "arg_1" a bit fragile though? *)
+
+Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+
+(* Check the existence of a shadowing warning *)
+
+Set Warnings "+syntax".
+Fail Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+Set Warnings "syntax".
+
+(* Test failure when implicit arguments are mentioned in subterms
+   which are not types of variables *)
+
+Set Warnings "+syntax".
+Fail Check (id (forall {a}, a)).
+Set Warnings "syntax".
+
+(* Miscellaneous tests *)
+
+Check let f := fun {x:nat} y => y=true in f false.
+
+(* Isn't the name "arg_1" a bit fragile, here? *)
+
+Check fun f : forall {_:nat}, nat => f (arg_1:=0).
+
+(* This test was wrongly warning/failing at some time *)
+
+Set Warnings "+syntax".
+Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
+Set Warnings "syntax".
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+        (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
          scopes @ [None]) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..eb7b28f15b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -255,9 +255,13 @@ let needs_extra_scopes ref scopes =
   let ty, _ctx = Typeops.type_of_global_in_context env ref in
   aux env ty scopes
 
+let implicit_name_of_pos = function
+  | Constrexpr.ExplByName id -> Name id
+  | Constrexpr.ExplByPos (n,k) -> Anonymous
+
 let implicit_kind_of_status = function
   | None -> Anonymous, NotImplicit
-  | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+  | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
 
 let dummy = {
   Vernacexpr.implicit_status = NotImplicit;