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

user_11126632 0
Viewed 72

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?

coq
2 Answers

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.
user_78074380

Well. It is just not able to "understand" that you want it to coerce to relation nat.

When you write Check (bar foo). coq should unify type which the bar is expecting (namely relation nat) and the type which foo has (namely serial nat). So, coq tryes to unify serial nat and relation nat and since these types are not convertable, coq "understands" that it needs try to use coercion. So, it tryes to find coercion from serial nat to relation nat. And since you have provided such a coercion, it succeeds.

Edit. When you write Check (foo 1 2). coq will try to unify type of the foo (namely serial nat) and type of function like (nat -> nat -> A) . So, again, it just does able not see that you want it to coerce foo to relation nat.

user_20666150
Related