Typeclasses uses tactics such as `simple apply`

during search. Am I able to replace these with refine based versions like `rapply`

?

That's a common request. `Set Typeclasses Filtered Unification`

uses refine instead but also imposes to use syntactic filtering first, with the inferred pattern for the hint (or one you specify yourself).

This seems to break a lot of things for me however. Typeclasses Debug also says that simple apply is still being used with filtered unification.

Here is with filtered unification:

```
1: looking for (IsEquiv (g o f)) without backtracking
1.1: unfold pointwise_paths on (IsEquiv (g o f)), 1 subgoal(s)
1.1-1 : (IsEquiv (fun x : A => g (f x)))
1.1-1: looking for (IsEquiv (fun x : A => g (f x))) without backtracking
1.1-1.1: simple apply @isequiv_compose with pattern
(IsEquiv (fun x : ?META93 => ?META98 (?META95 x))) on
(IsEquiv (fun x : A => g (f x))), 2 subgoal(s)
1.1-1.1-1 : (IsEquiv ?Goal0)
1.1-1.1-1: looking for (IsEquiv ?Goal0) with backtracking
1.1-1.1-1: no match for (IsEquiv ?Goal0), 7 possibilities
```

Here is without:

```
1: looking for (IsEquiv (g o f)) without backtracking
1.1: unfold pointwise_paths on (IsEquiv (g o f)), 1 subgoal(s)
1.1-1 : (IsEquiv (fun x : A => g (f x)))
1.1-1: looking for (IsEquiv (fun x : A => g (f x))) without backtracking
1.1-1.1: simple apply @isequiv_compose on
(IsEquiv (fun x : A => g (f x))), 2 subgoal(s)
1.1-1.1-1 : (IsEquiv f)
1.1-1.1-1: looking for (IsEquiv f) without backtracking
1.1-1.1-1.1: exact H0 on (IsEquiv f), 0 subgoal(s)
1.1-1.1-2 : (IsEquiv g)
1.1-1.1-2: looking for (IsEquiv g) without backtracking
1.1-1.1-2.1: exact H on (IsEquiv g), 0 subgoal(s)
Finished run 1 of resolution.
equiv_compose is defined
```

Why is filtered unification failing?

The matching code is very buggy, I'd recommend against using filtered unification.

Essentially it doesn't take evars properly into account, so the type of `H0`

is too constrained to match `isEquiv (fun x => (g (f x))`

Wait, it succeeded so matching succeded and it's evarconv/refine's unification that fails to instantiate ?Goal0 here it seems

Yes, the debug is misleading, it will keep printing "simple apply" even if the tactic is more `match_pattern p <*> refine lemma <*> shelve_unifiable`

But @Pierre-Marie Pédrot has a good point. Pattern matching is broken when the pattern contains evars. Though there are only metas generated here, so it should avoid that pitfall in general

@Matthieu Sozeau the difference of behaviour is *exactly* an instance of this problem, IIUC.

The goal contains an evar, and the matching algorithm fails.

If you can't have evars in your typeclass resolution it makes the flag essentially useless.

It's not super hard to fix, but this will change everything. So anyone using the flag (are there any?) will have to adapt the code.

But if you look at the trace without filtered unif, unification succeeded to produce `IsEquiv f`

and `IsEquiv g`

constraints by (apply) unification

applying H0, but it is filtered early with the flag on.

The goal `IsEquiv (fun x => g (f x))`

does not contain evars

Maybe in this instance there is more of an econstr problem

(oh, yes, and there is that.)

(pattern_of_constr delenda est.)

But yes you're right, as soon as the constraints will contain evars this will break too

We should at least patch `constr_matching`

to allow for the "right" behavior

Until then, `Hint Extern`

is your friend Ali

I think we should use a dedicate algorithm, constr_matching is already too complex for its own good

(and also use something else than pattern_of_constr)

Due to the backtracking you mean ?

no, there are Ltac considerations hardwired in constr_matching

By the way, I just enabled filtered unification for the HoTT library if you are looking for examples.

Last updated: Sep 30 2023 at 05:01 UTC