Sorry I didn't have a specific example prepared for the call. Here's a file that illustrates quite nicely what I was referring to: https://gist.github.com/Janno/a9bd105f427954438f930d9ccd30683d
If you run the file (8.11 should it do just fine) you'll see that the apply
call in the first module will try all instances, even though it should be clear statically that none of the instances for addition can possibly work. The second module manually stratifies the Simplify
class and now we don't seem to be wasting any time on impossible unification checks.
The example is stupid and possibly even contrived but I have real code (not yet public but it hopefully will be at some point) that has seen enormous speedups from this technique. The unification algorithm used by type class search is extremely bad when it comes to unification problems that come up when canonical structures are used and so in one instance we sped up proofs by 25% simply by adding a new layer of typeclasses like I do in the gist. 25% is a lot for such a simple change.
Oh, hold on a second I forgot to add the crucial instance. Don't be surprised, right now the example proves nothing :D
Never mind, I used :>
which registers the right instance automatically
@Matthieu Sozeau is this behaviour expected? Is there a way for users to avoid writing these sub-classes manually?
this is very suspicious indeed, the dnet returns everything including stuff that shouldn't match
oh my
I think this is because pattern expansion is not stable under evar unfolding
ah no
it's just the algorithm for dnets which is funny
if it sees a constant that is transparent, it claims it could be anything so virtually everything matches
(* doesn't even try SimplifyAdd at all and even if it did it would fail immediately without trying all the instances of SimplifyAdd *)
this is a priority issue, if the mult instance is at priority 2 instead of 1 it tries addition, fails, then tries mult
so here Simplify (mul X Y)
matches anything of the form Simplify _
instead of Simplify (mul _ _)
I guess this makes sense, somehow
this is a priority issue, if the mult instance is at priority 2 instead of 1 it tries addition, fails, then tries mult
Interesting. I suppose the instance generated by :>
has the "wrong" priority for my demonstration.
we need to allow arbitrary δ unfolding
typeclass matching is higher-order is the bottom line I believe?
we need to allow arbitrary δ unfolding
How about a flag? Something like Hint Mode
for delta unfolding? I think Typeclasses Opaque
helps here but I might have messed up my experiment.
it should help indeed
This will speed up iris and similar typeclass-driven developments immensely
or more probably break a lot of stuff
Sorry, Typeclasses Opaque
does not help here as far as I can tell
hm, we have several transparency tables in the hintdb
the dnet is probably looking at the wrong one
I think a lot of people would be extremely grateful if this could be fixed :)
fixed with respect to what specification, that's the usual problem :/
Well, if Nat.add
is Typeclass Opaque
then none of the instances for it should be tried in my example. Is that possible?
In fact, wouldn't it already be the case that, if we have Typeclass Opaque Nat.add
then all of the instances would fail even if they were applicable after reduction of Nat.add
?
The problem is mul
, not add
but I see your point
Oh, right, sorry. Okay, assume all constants were made Typeclasses Opaque
, even mul
. It's a big ask of the user but it would still be an improvement. Could we have the "right", i.e. fast behavior then?
I guess so, assuming we sort out the reason why we have so many transparent states in the database
So which transparent state is the dnet using?
good question, I am trying to understand
in the meantime, I've found the option I mentioned before
it's Typeclasses Filtered Unification
which does something very similar to first-order unification on goals
Right, not a very memorable name.. I thought that one had some sort of drawback that made it either ineffective or unusable. I'll try to find out which.
honestly I don't understand why our auto-like tactics have such a complex implementation
the simplest one is eauto, which apart from being broken, is straightforward
this option seems to be a global thing that affects all typeclasses.. that's going to make it impossible to activate in most developments, I think
Can you confirm that setting Typeclasses Opaque
of Nat.mul
solves the problem though?
No, it does not currently solve the problem as far as I can tell
(ah, it seems you need to set both add and mul opaque, but then it does work)
the discrimination is cut of both for the pattern and the term being matched, so if you want that two constants don't match both must be set opaque
Indeed, interesting. So my request was already fulfilled.. now one just needs to find every single constant used anywhere ever to make everything faster :D
we can add a command to turn everything opaque though
For a single type class? that would be great!
yes, we have access to the global so should be fine
I wonder if a better alternative would be Typeclasses Default Opaque/Transparent <class>
(the latter being the current default I guess?)
That way one could still make certain constants transparent later?
Be careful that making everything Opaque will make some things not match syntactically because of implicit arguments in many cases.
Indeed the Filtered Unification
is a bit drastic, but it gives the most control on which patterns trigger which hint (you get to give the syntactic pattern yourself)
You can already do Hint Constants/Variables Opaque : typeclass_instances
, at your own risk :)
You can already do Hint Constants/Variables Opaque : typeclass_instances, at your own risk :)
Interesting! What does Hint Variables do? Is it for existential variables?
Be careful that making everything Opaque will make some things not match syntactically because of implicit arguments in many cases.
Do you have an example for this? I would only be declaring the head constants opaque so if those match the parameters would still be unified (if possible), right?
Yes, it's more in cases like setoid rewriting where if you make e.g. "relation" opaque you won't get unifications with "A -> A -> Prop". In general type aliases are one case where this breaks.
Hint Variables is about section/goal variables
Here's my experience report: I set Hint Constant Opaque
for the various databases we use for TC-guided proof search. I had to add various exceptions by making them Hint Transparent
again. Some of those, I think, would be unnecessary if tactic unification wasn't so crazy but the rest is well-motivated.
Finding out which constants are blockers is a pain but I used the following recipe: Set Typeclassses Debug Verbosity 2
, look for the failing instance and copy the part that says cannot unify X and Y
. Use Hint resolve eq_refl : your_db
, then assert (X = Y)
and finally alternate between Fail typeclasses eauto with your_db
and various incantations of cbn
and unfold
until eauto
no longer fails. Then convert your reduction tactics into new Hint Transparent
exceptions.
We got a 30% reduction in ltac execution time from this. Not bad for an afternoon's work.
The number of instances considered by typeclass search went down by a factor of 5!
Last updated: Oct 13 2024 at 01:02 UTC