(* Nevertheless, argty is well-typed only in context. *)
(* Thus I generate a name (name_hint) in context and *)
(* then I generate a name --- using the hint name_hint *)
(* Nevertheless, argty is well-typed only in context. *)
(* Thus I generate a name (name_hint) in context and *)
(* then I generate a name --- using the hint name_hint *)