The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Another similar problem with coercions - the source and destination 
types also have to be names, not terms.  Hence, one cannot do:

Coercion f : (foo a) >-> (bar b).

I tried to fool this by using abbreviations, such as:

Notation fooa := (foo a).
Notation barb := (bar b).
Coercion f : fooa >-> barb.

Interestingly, the Coercion command in this case did not fail, but also 
did not have any impact.

I think I will add this to bug #2322.

-- Jonathan

On 02/24/2016 03:05 PM, Jason Gross wrote:
> 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
> <https://coq.inria.fr/bugs/show_bug.cgi?id=3115> (identity coercion
> limitations), bug #3389
> <https://coq.inria.fr/bugs/show_bug.cgi?id=3389> (feature
> request for your "always unfolding", which I called "expand_invisible"), bug
> #2322 <https://coq.inria.fr/bugs/show_bug.cgi?id=2322> (terms as
> coercions), and bug #4593 <https://coq.inria.fr/bugs/show_bug.cgi?id=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