So I am trying to do some stuff for key/value data types (maps/ trees ..etc) using cannonical structures,

The current situation is as follows:

We have canonical structure paremetrized by `A`

, `B`

, and type `M`

which depends on both `A`

and `B`

(map from A to B)

```
Module FinMap.
Record operations (A B: eqType) (M: eqType -> eqType -> Type) := Operations {
Empty : M A B;
}.
Structure type := Pack{
AT: eqType;
BT: eqType;
MT: eqType -> eqType -> Type;
ops: operations AT BT MT;
}.
Definition empty (e: type): (MT e (AT e) (BT e)) := (Empty (ops e)).
Arguments empty {e} : simpl never.
End FinMap.
```

Here is a toy type that should implement that structure above, with toy lemma `foo`

```
(* Tree from nat to type A *)
Inductive NTree (A: eqType): Type :=
| Nempty : NTree A
(*root with stuff follows here*).
Definition ntree_finmap_ops (A: eqType): FinMap.operations nat_eqType A (fun _ x => NTree x).
Proof.
constructor.
apply Nempty.
Qed.
Canonical Structure ptree_is_finmap {A}:= FinMap.Pack (ntree_finmap_ops A).
Lemma foo: forall A, exists (x: NTree A ), x = @FinMap.empty ptree_is_finmap.
Proof. intros; eauto. Qed.
```

Note how `foo`

is very annotated I assume that CS goal is to avoid this kind of annotations ?

So if I try to redo the lemma without it:

```
Lemma foo1: forall A, exists (x: NTree A ), x = FinMap.empty.
Admitted.
```

Coq complains with error

```
In environment
A : eqType
x : NTree A
The term "FinMap.empty" has type
"FinMap.MT ?e (FinMap.AT ?e) (FinMap.BT ?e)"
while it is expected to have type "NTree A".
```

It is not clear why coq fails to do the unification. if `?e`

is replaced by `ptree_is_finmap`

issue should be solved. Can any one offer some insights ?

Nice, this also looks like a bug and is probably related to coq/coq#14041

Here is what I think is a minimisation of the bug:

```
Structure type := Pack { sort: Type -> Type }.
Canonical unit_type : type := Pack (fun _ => unit).
Check (eq_refl : sort _ = fun _ => unit).
Check (eq_refl : sort unit_type _ = unit).
Fail Check (eq_refl : sort _ _ = unit).
```

(maybe it's related to coq/coq#16031)

Opened issue coq/coq#16755

one day I will have the sufficient knowledge to send pull request to coq!

Last updated: May 18 2024 at 10:02 UTC