title: Why Coq does not infer the type parameter
body: <p>I've defined the following type which has the exact same structure as <code>option</code>.</p>
  <pre><code>Inductive optionX A := NoneX | SomeX (a : A).
  </code></pre>
  <p>While <code>Check Some 1</code> correctly infers the type parameter A, <code>Check SomeX 1</code> produces the message</p>
  <pre><code>The term &quot;1&quot; has type &quot;nat&quot; while it is expected to have type &quot;Type&quot;.
  </code></pre>
  <p>Am I missing something? Note that it works fine if I explicitly provide the type parameter: <code>Check SomeX(nat) 1</code>.</p>