## Stream: Coq users

### Topic: Canonical structures for depenent types

#### walker (Oct 29 2022 at 19:16):

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.
``````

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 ?

#### Cyril Cohen (Oct 29 2022 at 22:02):

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).
``````

#### Cyril Cohen (Oct 29 2022 at 22:04):

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

#### Cyril Cohen (Oct 29 2022 at 22:20):

Opened issue coq/coq#16755

#### walker (Oct 30 2022 at 08:06):

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

Last updated: Sep 26 2023 at 13:01 UTC