The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The issue with axioms sounds like a bug.  Is it present in 8.4?  In any case, you should report it in the bug tracker.

[Local Existing Class] should be requested on the bug tracker with this example about variables.

Does creating a typeclass hint at level 0 that wraps all hypotheses for you work?  (Does it fire before assumptions?  Does it fire before assumptions if you make it a local hint extern and stick it after all the variables?)

On Thu, Jun 30, 2016, 8:28 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 06/29/2016 10:06 PM, Jonathan Leivent wrote:
>
>
> On 06/29/2016 01:05 PM, Jonathan Leivent wrote:
>>
>>
>> On 06/29/2016 12:38 PM, Matthieu Sozeau wrote:
>>> Hi Jonathan,
>>>
>>>    short answer is not currently. I would advise to make an
>>> abbreviation
>>> class eqC instead. The fact that local hypotheses of
>>> typeclass type are automatically considered for resolution is a
>>> feature. It
>>> could be an option of individual class declarations
>>> to not do that: only explicit Instances/Existing Instances for that
>>> class
>>> would be considered. We'd certainly need to devise a
>>> way to declare when a local binder (in fun (x : C foo) y => t) or a
>>> goal
>>> hypothesis (e.g. after intro H) should be considered though.
>>> Best,
>>> -- Matthieu
>>
>> Thanks, Matthieu.
>>
>> What do you mean by an "abbreviation class eqC"?
>
> Here's a guess - instead of "Existing Class eq", I tried this:
>
> Class eqC {T}(a b : T) := equals : eq a b.
> Hint Resolve equals : typeclass_instances.
>
> with some specific Instances of eqC.
>
> However, this seems to require the explicit use of "typeclass eauto" -
> a hole of eq type won't get filled automatically, unlike what was
> happening in the Existing Class eq case (and happening too often). I
> would like to have the holes corresponding to the instances of eqC
> automatically filled in.  Is there some other way to do this?
>
> -- Jonathan
>

I found an ugly workaround: use Existing Class eq, and wrap any
subsequent hypothesis-like declaration that one does not want to be
considered an instance, then unwrap it in a definition.  This works
because complete definitions are not automatically considered instances
of the Existing Class - although, is that a bug?  Why aren't definitions
considered just declarations with proofs? Anyway, that's how it works
(though none of this is in the refman or typeclassestut, or anywhere I
googled) - so the workaround is:

Existing Class eq.

Variable T : Type.

Structure NonInstance X := { unwrap_noninstance : X }.

Axiom eqT_ : NonInstance (forall a b : T, a = b).
Definition eqT := unwrap_noninstance _ eqT_.

Print HintDb typeclass_instances.

(* neither eqT_ nor eqT appear:
Discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Cut: emp
For any goal ->
*)

For Axioms, the NonInstance wrapper seems like a somewhat plausible
workaround, but it is probably too ugly for section Variables or module
Parameters, as one would have to wrap the corresponding actual parameters.

I think I am stuck using "Existing Class eq" if the objective is to have
at least some eq holes automatically filled.  I tried limiting the scope
of Existing Class eq by wrapping it in a section or module - but that
doesn't limit it.  And "Local Existing Class" is not legal.  This makes
"Existing Class" a dangerous thing to use in a shared module, especially
on ubiquitous types like eq.

How about this for an enhancement: allow the "Instance foo ... : T ...
:= ..." syntax for T even when it is not previously declared a class.
Currently, this produces the error "T is not a declared type class".
This would make T into an existing class in a limited capacity, so that
it only accepts such explicitly declared instances.

Although I also think "Local Existing Class" is worth adding as well.

-- Jonathan