I've defined the following type which has the exact same structure as option.
Inductive optionX A := NoneX | SomeX (a : A).
While Check Some 1 correctly infers the type parameter A, Check SomeX 1 produces the message
The term "1" has type "nat" while it is expected to have type "Type".
Am I missing something? Note that it works fine if I explicitly provide the type parameter: Check SomeX(nat) 1.
Coq has an implicit arguments mechanism for this kind of situation:
Inductive optionX A := NoneX | SomeX (a : A).
Arguments NoneX {A}.
Arguments SomeX {A} a. (* Curly braces means "please try to infer this" *)
Check SomeX 1.
(* You can turn off argument inference with @ *)
Check @NoneX nat. (* optionX nat *)
Note that the expression that you had earlier, SomeX(nat) 1, is parsed the same way as SomeX nat 1, which is the constant SomeX applied to the arguments nat and 1. The mechanism for supplying type arguments is the same as how you supply other kinds of arguments.
The reference manual has more information on implicit arguments.