Why do coercions not work inside pairs? In my project I have coercions from Foo to Bar, which works well if I have one Foo but want one Bar. But it does not work if I want a pair of Bars, but have a pair of Foos.
Inductive Foo := foo.
Inductive Bar := fromFoo of Foo.
Coercion fromFoo : Foo >-> Bar.
(* This works *)
Definition bar : Bar := foo.
(* This fails *)
Fail Definition bars : (Bar * Bar) := (foo,foo).
Why would Coq not insert the coercion here?