Pierre-Marie Pédrot (Jul 30 2021 at 16:24): Pierre-Marie Pédrot (Jul 30 2021 at 16:24):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)
Pierre-Marie Pédrot (Jul 30 2021 at 16:24):In a nutshell, syntactic matching allows η-expansion on variables but not constants.
Pierre-Marie Pédrot (Jul 30 2021 at 16:26):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?
Pierre-Marie Pédrot (Jul 30 2021 at 16:35):Interestingly, the latter was working in 8.12, but already fails in 8.13.
Pierre-Marie Pédrot (Jul 30 2021 at 16:37):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.
Pierre-Marie Pédrot (Jul 30 2021 at 16:38):Anybody has the least idea of the expected spec of this algorithm?
Paolo Giarrusso (Jul 31 2021 at 16:34):I’m sure @Janno will at some be interested, tho he might be otherwise busy…
Paolo Giarrusso (Jul 31 2021 at 16:35):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)
Paolo Giarrusso (Jul 31 2021 at 16:42):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.
Paolo Giarrusso (Jul 31 2021 at 16:48):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.
Janno (Jul 31 2021 at 17:14):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.
Pierre-Marie Pédrot (Jul 31 2021 at 17:27):Shouldn't be too hard to η-normalize patterns and terms in dnets, I am on it.
Pierre-Marie Pédrot (Jul 31 2021 at 17:37):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.
Janno (Jul 31 2021 at 18:29):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
byteandbytesand in a proof I needed something likeFractional byteandFractional (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.
Pierre-Marie Pédrot (Jul 31 2021 at 21:26):see https://github.com/coq/coq/pull/14732
Last updated: May 31 2023 at 15:01 UTC