The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Much like the uniform inheritance condition, I believe the answer is "hysterical raisins" and "lack of time or manpower to fix it" and "pull requests are welcome".

You might be interested in [Set Keyed Unification] in Coq 8.5 (to handle your rewriting issue), bug #3115 (identity coercion limitations), bug #3389 (feature request for your "always unfolding", which I called "expand_invisible"), bug #2322 (terms as coercions), and bug #4593 (one I just reported about removing the uniform inheritance condition).

On Wed, Feb 24, 2016, 11:34 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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