Hi. In the (heavily minimized) script below, there is a unification failure that surprises me between `proj f x`

and `proj ?g x`

as I would expect `?g`

to be instanciated with `generic_S`

. Note that removing the argument `x`

makes the unification work (which is even weirder). Experimentation has shown that unicoq finds that it should try the canonical instance but does not look for the typeclass instance to fill in the hole of `generic_S`

. From the debugging messages, it looks like Coq unifies `?g`

with `f`

at some point, but setting `?g := f`

would make the term ill-typed. Can someone tell me what is happening here, and if this is already known, if there is something I can do?

The code:

```
Class A (T : Type) (dummy x : T) := ClassA {
_ : True
}.
Structure S (T : Type) (dummy : T) := PackS {
proj : T;
class : @A T dummy proj
}.
Canonical generic_S (T : Type) (dummy : T) (x : T) (c : @A T dummy x) :=
@PackS T dummy x c.
Definition strue := S (bool -> bool) (fun _ => true).
Definition sfalse := S (bool -> bool) (fun _ => false).
Instance ctransfer (f : strue) : A (bool -> bool) (fun _ => false) (proj _ _ f) := @ClassA _ _ (proj _ _ f) I.
Goal forall (f : strue) (x : bool) P, (forall (g : sfalse), P (proj _ _ g x)) -> P (proj _ _ f x).
Proof.
intros.
Set Debug "unification".
Fail refine (X _).
Succeed refine (X (generic_S _ _ _ _)).
Require Import Unicoq.Unicoq.
Set Unicoq Debug.
Fail refine (X _).
refine (X (generic_S _ _ _ _)).
Qed.
```

The error and debugging messages for l. 23 (`Fail refine (X \_)`

) :

```
Class A (T : Type) (dummy x : T) := ClassA {
_ : True
}.
Structure S (T : Type) (dummy : T) := PackS {
proj : T;
class : @A T dummy proj
}.
Canonical generic_S (T : Type) (dummy : T) (x : T) (c : @A T dummy x) :=
@PackS T dummy x c.
Definition strue := S (bool -> bool) (fun _ => true).
Definition sfalse := S (bool -> bool) (fun _ => false).
Instance ctransfer (f : strue) : A (bool -> bool) (fun _ => false) (proj _ _ f) := @ClassA _ _ (proj _ _ f) I.
Goal forall (f : strue) (x : bool) P, (forall (g : sfalse), P (proj _ _ g x)) -> P (proj _ _ f x).
Proof.
intros.
Set Debug "unification".
Fail refine (X _).
Succeed refine (X (generic_S _ _ _ _)).
Require Import Unicoq.Unicoq.
Set Unicoq Debug.
Fail refine (X _).
refine (X (generic_S _ _ _ _)).
Qed.
```

I suspect you didn't mean to paste the code twice?

@Quentin VERMANDE: What would you expect?

- That an inhabitant of
`S`

is automatically inferred to be a`PackS`

? If yes, this is indeed a limitation of the current unification that it does not try to instantiate products/records with pairs/tuples. - That a canonical inference
`?g := generic_S ... (proj ... f) ?c`

is deduced from`proj ... ?g == proj ... f`

? If yes, this would also be a priori possible and maybe a specialist of canonical projection can comment about what happens (cc @Enrico Tassi).

Sorry, that was silly, I updated the message.

[at]Hugo Herbelin Coq already does what you state as your second option, but it looks like it never considers unifying `proj _ _ ?g`

and `proj _ _ f`

. What really strikes me is the fact that the unification fails only when I apply `proj _ _ ?g`

and `proj _ _ f`

to `x`

.

What really strikes me is the fact that the unification fails only when I apply

`proj _ _ ?g`

and`proj _ _ f`

to`x`

.

Right, there is there room for improvement. When trying to solve the canonical projection, the unification "forgets" to remove the `x`

and tries `proj _ _ ?g ≣ proj _ _ f x`

instead of `proj _ _ ?g ≣ proj _ _ f`

. Of course, the former then fails.

I suggest you fill a bug/wish report (maybe @Enrico Tassi, who is a canonical projection expert, will have something to say about it).

It looks like I never opened the issue, for which I apologize. Here it is : https://github.com/coq/coq/issues/18343

Last updated: Oct 13 2024 at 01:02 UTC