Why can't Coq infer my coercion when applying arguments to coercible term?

Question

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.

Here is the code:

Definition relation A := A -> A -> 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 >-> relation.

Parameter foo: serial nat.
Parameter bar: relation nat -> Prop.

(* Succeeds in coercing an argument. *)
Check (bar foo).

(* Fails to coerce when applying arguments to coercible term *)
Fail Check (foo 1 2).

Here's an executable version of the snippet: https://x80.org/collacoq/udutosoher.coq

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?

Answer 1

I think the problem in the last case is that Coq tries to infer a function type for foo and relation A is not literally a function type (only up to unfolding of the definition of relation).

If you add a coercion to Funclass (see the doc) as follows then the last test goes through

Definition serial_to_fun A (s: serial A) : A -> A -> Prop := proj1_sig s.
Coercion serial_to_fun : serial >-> Funclass.