title: Why can't Coq infer my coercion when applying arguments to coercible term?
body: <p>I'm trying to write a coercion of a specific sigma type into a binary relation. The coercion works when using a coercible term as a function argument, but not when using the same term as a function.</p>
  <p>Here is the code:</p>
  <pre><code>Definition relation A := A -&gt; A -&gt; Prop.
  
  Definition is_serial {A} (R: relation A) := forall x, exists y, R x y.
  
  Definition serial state := {R: relation state | is_serial R}.
  
  Definition serial_to_relation A (s: serial A) : relation A := proj1_sig s.
  Coercion serial_to_relation : serial &gt;-&gt; relation.
  
  Parameter foo: serial nat.
  Parameter bar: relation nat -&gt; Prop.
  
  (* Succeeds in coercing an argument. *)
  Check (bar foo).
  
  (* Fails to coerce when applying arguments to coercible term *)
  Fail Check (foo 1 2).
  </code></pre>
  <p>Here's an executable version of the snippet: <a href="https://x80.org/collacoq/udutosoher.coq" rel="nofollow noreferrer">https://x80.org/collacoq/udutosoher.coq</a></p>
  <p>Why does the second check fail? Did I make a mistake in my coercion definition? Or is this some limitation of coercion inference that I'm unaware of?</p>