The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/09/2016 10:11 PM, Jason Gross wrote:
> 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.

OK - I think I get it.  So, the backtracking must occur entirely within 
the extern hints?  The list is then needed to accumulate the results 
seen during backtracking.  It's unfortunate that the context search is 
needed each time.  This must get really slow when the number of A's gets 
large.

I think the length of the list could be eliminated by having a dedicated 
first (or highest cost) instance of A that the second hint uses to know 
to stop looking for more.

Thanks, Jason!  Now I have to see if I can repackage this to use...

-- Jonathan