The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

This is a follow-up to the "overloading natural number notations for 
user types" thread.
Suppose one has a generic inductive type, such as:

Inductive foo(S : Set) : Set :=
| Foo(x : S).

And then wishes to declare coercions from various Sets, for example nat, 
to the corresponding foo.  Coq does not allow the following:

Coercion (Foo nat) : nat >-> foo.

as it requires that the Coercion command's first arg is a name.  It also 
doesn't allow using implicits, as in:

Arguments Foo {S} x.
Coercion Foo : nat >-> foo.

Instead, one must use an intermediate function for the coercion, such as:

Definition nat2foo := Foo nat.
Coercion nat2foo : nat >-> foo.

Why is there this restriction?  Why doesn't Coq allow partially 
parameterized functions as coercions?

Note that this restriction would not be so bad if there was a way to 
declare nat2foo as "always unfolding".  Meaning, not just something like 
"Strategy expand [nat2foo].",  but that nat2foo is always immediately 
unfolded - that it behaves almost like a notation. Otherwise, consider a 
rewrite rule such as:

Variables F G : (foo nat) -> nat.
Axiom rw : F 1 = G 2.

Because rw was defined using the nat2foo coercion, it can't handle cases 
where nat2foo doesn't appear:

Goal F 1 = G 2.
cbv. (*unfolds nat2foo*)
Fail rewrite rw.

-- Jonathan