Trying to make the behaviour of dnets used by hint matching more uniform I've stumbled upon the following surprising behaviour of discriminated hints (i.e. virtually only used by the typeclass mechanism)
In a nutshell, syntactic matching allows η-expansion on variables but not constants.
That is, the following works:
Class Reflexive0 {A : Type} (R : A -> Prop) : Prop := {}.
Axiom A : Type.
Definition foo {R} {HR : @Reflexive0 A R} : @Reflexive0 A (fun x => R x) := _.
But the following does not:
Class Reflexive0 {A : Type} (R : A -> Prop) : Prop := {}.
Axiom A : Type.
Axiom R : A -> Prop.
Definition foo {HR : @Reflexive0 A R} : @Reflexive0 A (fun x => R x) := _.
Is this expected?
Interestingly, the latter was working in 8.12, but already fails in 8.13.
To add insult to injury, the first example is asymmetrical. If you reverse the η-long form as in
Class Reflexive0 {A : Type} (R : A -> Prop) : Prop := {}.
Axiom A : Type.
Definition foo {R : A -> Prop} {HR : @Reflexive0 A (fun x => R x)} : @Reflexive0 A R := _.
then it fails as well.
Anybody has the least idea of the expected spec of this algorithm?
I’m sure @Janno will at some be interested, tho he might be otherwise busy…
My 2 cents would be that matching should be up to eta-expansion if there’s a way to retain the performance (at least asymptotically)
I’ve seen another example where eta-expansion worked on defined constants, but stopped working on TC Opaque
ones; IIRC your axiom R
is treated as transparent in 8.12 and opaque in 8.13 thanks to your much appreciated fix in https://github.com/coq/coq/pull/12565.
I didn’t finish diagnosing my example, but it seemed that whether I needed the eta-expanded or eta-reduced instance depended on what form was produced by _unification_ — in my case, HO unification. So I had predicates byte
and bytes
and in a proof I needed something like Fractional byte
and Fractional (fun q, bytes q)
— in a way that seemed unpredictable; I’d bet that in other proofs I might need Fractional (fun q, byte q)
and Fractional byte
. This was in some OSS code using Iris, and I’d be willing to minimize it if it helps you here.
TC search up to eta expansion sounds very useful. I think it would actually alleviate a really, really big problem with template polymorphism and classes such as FMap
which really ought to be defined for fun T => list T
instead of just list
to avoid restricting the template universe of list
. As far as I remember this cannot be done currently and is the reason that iris stdpp imposes pretty surprising universe restrictions on client code.
Shouldn't be too hard to η-normalize patterns and terms in dnets, I am on it.
More generally, this kind of strict matching in dnets will wreak havoc with terms that enjoy additional conversion rules regardless of their opacity status. I am thinking in particular about SProp, and potentially some other η-rules although the latter is more uncommon.
Paolo Giarrusso said:
I didn’t finish diagnosing my example, but it seemed that whether I needed the eta-expanded or eta-reduced instance depended on what form was produced by _unification_ — in my case, HO unification. So I had predicates
byte
andbytes
and in a proof I needed something likeFractional byte
andFractional (fun q, bytes q)
— in a way that seemed unpredictable; I’d bet that in other proofs I might needFractional (fun q, byte q)
andFractional byte
. This was in some OSS code using Iris, and I’d be willing to minimize it if it helps you here.
This minimized example seems pretty close to what you describe. It's from perennial.
see https://github.com/coq/coq/pull/14732
Last updated: May 31 2023 at 15:01 UTC