what's the problem? #75
Conversation
| Print Instances PER. | ||
| Typeclasses eauto := debug. | ||
| Set Typeclasses Debug. | ||
| typeclasses eauto. |
There was a problem hiding this comment.
Type class resolution fails.
There was a problem hiding this comment.
eauto with typeclass_instances succeeds. anyway to fix this? typeclass resolution doesn't look at the context at all?
There was a problem hiding this comment.
You can check the trace with typeclasses eauto || idtac. For this specific case, the following is the trace:
Debug: 1: looking for (PER R) without backtracking
Debug: 1.1: simple eapply @per_elem_PER on (PER R), 1 subgoal(s)
Debug: 1.1-1 : (per_univ_elem ?i ?A ?B R)
Debug: 1.1-1: looking for (per_univ_elem ?i ?A ?B R) with backtracking
Debug: 1.1-1: no match for (per_univ_elem ?i ?A ?B R), 0 possibilities
Debug: 1.2: simple apply @Equivalence_PER on (PER R), 1 subgoal(s)
Debug: 1.2-1 : (Equivalence R)
Debug: 1.2-1: looking for (Equivalence R) without backtracking
Debug: 1.2-1: no match for (Equivalence R), 0 possibilities
In other words, it fails to find per_univ_elem ?i ?A ?B R), unlike eauto. So indeed, it seems like it ignores the local context.
There was a problem hiding this comment.
But the documentation says like this...
When considering local hypotheses, we use the transparent state of the first hint database given. Using an empty database (created with Create HintDb for example) with unfoldable variables and constants as the first argument of typeclasses eauto hence makes resolution with the local hypotheses use full conversion during unification.
which is confusing. It seems like it considers local hypothesis, but then why does it fails to find per_univ_elem?
There was a problem hiding this comment.
yeah I don't get it. It might just look for classes in the local contexts.
There was a problem hiding this comment.
I want to add
#[global]
Hint Extern 1 => eassumption : typeclass_instances.
What do you think?
There was a problem hiding this comment.
Sounds OK, we don't need to use typeclasses eauto in the proofs very often anyway.
There was a problem hiding this comment.
It's also very tempting to swap the order of per_univ_elem. How many times do we have to use PER properties later?
What exactly is going wrong here?