The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This sounds like a bug in Coq that you should report.

On Thu, Mar 30, 2017, 7:47 PM John Wiegley <johnw AT newartisans.com> wrote:

Hello,

I'm working on some sample code that uses ltac to generalize a subset of
Gallina terms to any cartesian closed category, allowing me to then use
instance resolution to map to a different category for interpretation.  This
is based on work by Conal Elliot in his paper here:

    http://conal.net/papers/compiling-to-categories/

Everything seems to work well, until I get to a goal where the left-hand side
is the [arrow] category version of the term (i.e., Coq types and functions),
and the right-hand side is an extensional that wants to parameterize over
[arrow]:

    mulC ∘ (id △ id) = ?Goal@{T:=arrow; c:=Coq_Closed; n:=Coq_NumCat}

I would think that this should just unify as is, since [mulC ∘ (id △ id)], in
general form, where T is chosen to be arrow, turns into the exact [mulC ∘ (id
△ id)] on the LHS.

However, I get this error:

       Unable to unify "?Goal@{T:=arrow; c:=Coq_Closed; n:=Coq_NumCat}" with
       "mulC ∘ (id △ id)"
       (unable to find a well-typed instantiation for "?Goal": cannot ensure that
       "arrow Z Z" is a subtype of "T Z Z").

How do I tell Coq that in an environment where [T:=arrow], that [arrow] is
clearly always a subtype of [T]?

The code is here:

    https://github.com/jwiegley/categories/blob/master/Categories.v#L183

It works if I manually instantiate the evar using the general form of [mulC ∘
(id △ id)], but I haven't found a way to automate this choice.

Thanks,
--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2