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`

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.

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

Last updated: Oct 13 2024 at 01:02 UTC