I've created a type that define (nat,bool) -> T couples:
Definition pprod_nb : Set := forall T:Set, (nat -> bool -> T) -> T.
Now i want to specialize pprod_nb with T = nat :
(nat -> bool -> nat) -> nat
My question is : how to specify a type of the form forall T:Set, ... ?
First of all, your type pprod_nb is too large (it's a function type) to be a Set, so you need to make it a Type or you'll get a universe inconsistency error:
Definition pprod_nb : Type := forall T:Set, (nat -> bool -> T) -> T.
If I understand correctly you mean "specialize" and not "specify". The type above can't be specialized since it's a higher-order or rank 2 type (a term you would see in Haskell if you use an appropriate extension, like Rank2Types). Instead, it refers to functions that work for all types T; since polymorphic functions can't inspect types and behave differently for different types in Coq (the technical term for this is parametric polymorphism), such functions behave uniformly regardless of what result type T they produce.
Here's another higher-order type (it's not a type on its own, it's a function that produces a type) that you can specialize:
Definition pprod_nb' : Set -> Type := fun T:Set => (nat -> bool -> T) -> T.
Eval compute in (pprod_nb' nat).
(*
= (nat -> bool -> nat) -> nat
: Type
*)
(* check that these two definitions are indeed exactly the same *)
Theorem pprod_nb'_is_pprod_nb_forall :
pprod_nb = forall T, pprod_nb' T.
Proof. reflexivity. Qed.
I've written it in a way to highlight similarity to your pprod_nb definition, but it would more naturally be written Definition pprod_nb' T := (nat -> bool -> T) -> T.