Stream: Coq devs & plugin devs

Topic: On η-expansion in hint matching


view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2021 at 16:24):

In a nutshell, syntactic matching allows η-expansion on variables but not constants.

view this post on Zulip 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) := _.

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2021 at 16:27):

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) := _.

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2021 at 16:30):

Is this expected?

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2021 at 16:35):

Interestingly, the latter was working in 8.12, but already fails in 8.13.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 30 2021 at 16:38):

Anybody has the least idea of the expected spec of this algorithm?

view this post on Zulip Paolo Giarrusso (Jul 31 2021 at 16:34):

I’m sure @Janno will at some be interested, tho he might be otherwise busy…

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 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.

This minimized example seems pretty close to what you describe. It's from perennial.

view this post on Zulip Pierre-Marie Pédrot (Jul 31 2021 at 21:26):

see https://github.com/coq/coq/pull/14732


Last updated: Oct 16 2021 at 07:02 UTC