title: Coercion in pairs
body: <p>Why do coercions not work inside pairs? In my project I have coercions from <code>Foo</code> to <code>Bar</code>, which works well if I have one <code>Foo</code> but want one <code>Bar</code>. But it does not work if I want a pair of <code>Bar</code>s, but have a pair of <code>Foo</code>s.</p>
  <pre><code>Inductive Foo := foo.
  Inductive Bar := fromFoo of Foo.
  
  Coercion fromFoo : Foo &gt;-&gt; Bar.
  
  (* This works *)
  Definition bar : Bar := foo.
  (* This fails *)
  Fail Definition bars : (Bar * Bar) := (foo,foo).
  </code></pre>
  <p>Why would Coq not insert the coercion here?</p>