The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> So, the backtracking must occur entirely within

> the extern hints?

Yes.

> It's unfortunate that the context search is
> needed each time.  This must get really slow when the number of A's gets
> large.

Yeah, it's unfortunate that it incurs an exponential overhead.  Hopefully you won't need it for long lists?

> Thanks, Jason! 

Glad to help!

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

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