The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Axiom A : Type.

Existing Class A.

Axioms a a' : A.

Existing Instances a a'.

Class MultiA (n : nat) {x : A} := dummy : list A.

Hint Extern 0 (@MultiA 0 ?x) => (exact nil) : typeclass_instances.

Hint Extern 0 (@MultiA (S ?n) ?x) => (let prev := constr:(_ : @MultiA n _) in

                                      match eval cbv beta in prev with

                                      | context[cons x _] => fail 1

                                      | ?prev' => exact (cons x prev')

                                      end) : typeclass_instances.

Goal True.

  pose (_ : MultiA 2). (* m := ((a :: a' :: nil)%list : MultiA 2) : MultiA 2 *)

There's probably a way to do this without giving the length of the list ahead of time, but I hope this gives a bit of insight into the model I'm using of typeclass resolution hackery.

On Wed, Mar 9, 2016 at 9:44 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/09/2016 09:06 PM, Jason Gross wrote:
>> But, is there a way to have something print both foo_a and foo_b?
> Axiom A : Type.
> Existing Class A.
> Axioms a a' : A.
> Existing Instances a a'.
>
> Class MultiA {x : A} := dummy : True.
>
> Hint Extern 0 (@MultiA ?x) => idtac x; fail : typeclass_instances.
>
> Goal True.
>    try pose (_ : MultiA).
> (* a'
> a
> a'
> a
> a'
> a
> a'
> a *)
>
>
> Not sure why there's so much duplication, but can you make this work?

That's a strange solution.  But, as far as I can tell, it can only
print.  One can't make other use of the non-most-recent instances,
right?  In fact, MultiA has to not have any actual instances for this to
work, it seems.

-- Jonathan