(sorry for not minimizing the issue, I am totally drained for trying to identify the issue)

So I am importing those files:

https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/gmap.v

https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/fin_maps.v

https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/serde.v

And The general assumption here is that equal types may be replaced by equal types, where equal as in `Compute T1`

and `Compute T2`

results in the same value

So here is the situation:

We have a record for CS:

```
Module FinMap.
(*stuff*)
Structure type (K: eqType):= Pack{
MT: eqType -> Type -> Type;
ops: operations K MT;
lms: lemmas ops;
}.
End FinMap.
Definition finMap := FinMap.type.
Notation MapType K V e:= ((FinMap.MT e) K V).
```

We have a type for trie based maps along side with the implementation of its cannonical structure:

```
Definition GTrie (K V: Type) := Trie.Trie V.
Canonical Structure trie_is_fin_map (K: serDeEqType) :=
FinMap.Pack (GTrie.trie_finmap_lemmas K).
```

`Trie.Trie`

does not matter same are the most of what goes inside FinMap.Pack. Worth noting that `serDeEqType`

is another CS

Then there is the reality check:

```
Compute (MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)).
(*
= Trie.Trie bool
: Type
*)
Compute (GTrie nat bool).
(*
= Trie.Trie bool
: Type
*)
```

` (MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq))`

, `GTrie nat bool`

and `Trie.Trie bool`

are the same thing:

But then this is the problem

```
Check ({[1 := true]}). (*makes sense that the type has holes *)
(*
{[1 := true]}
: MapType nat_eqType bool ?e
where
?e : [ |- FinMap.type nat_eqType]
*)
Check ({[1 := true]} : MapType _ _ (trie_is_fin_map nat_is_serde_eq)). (* Should work and does work!*)
(*
{[1 := true]} : MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)
: MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)
*)
Fail Check ({[1 := true]} : GTrie nat bool). (* ??? should work but does not work! *)
(*
The command has indeed failed with message:
The term "{[1 := true]}" has type "MapType nat_eqType bool ?e"
while it is expected to have type "GTrie nat bool".
*)
Fail Check ({[1 := true]} : Trie.Trie bool). (* I get why this one fails, but equal types should be replacable, right ? *)
(*
The term "{[1 := true]}" has type "MapType nat_eqType bool ?e"
while it is expected to have type "Trie.Trie bool".
*)
```

Once again, I apologize for not minimizing the bug, but this one took a toll to find out

Also assuming that it is a bug, I would really like to see this one fixed asap so is this a beginner friendly bug that someone like me can work on ?

I did not try your code but:

- CS are indexed using the declared value and projection syntactically (no quotient)
- you can declare the same (morally) CS multiple times on convertible (but different) keys

Use `Print Canonical Projections`

to see the data base. IMO you should always pass the second argument to `Pack`

explicitly, that is tune the implicits, since that is the key used for indexing.

Well I passed the arguments manually to see if it makes a difference, and it worked! all four cases

But I don't understand the things you are trying to explain in the two points.

Also I am not sure what should I be looking for in the output of `Print Canonical Projections`

Here the key value is `GTrie`

, which is the "lowest" term all other computes to.

Unification faces problems like `projection ?CS = value`

, and if `value`

is a canonical key for `projection`

then `?CS`

is taken from the DB

if value is not a canonical key, it is unfolded, and then it loops

so if you canonical value is the normal form, eventually value will be reduced to it

my mistake ... it didn't actually work, it was `Fail Check`

that was green but I was too excited to double-check fast time.

The command prints,in an odd way, the mapping `(projection,value) -> CS_instance`

But now that I look again at your script, I'm not so sure I get what you are testing

So we have this:

```
GTrie.gtrie_finmap_ops <- FinMap.ops ( trie_is_fin_map )
GTrie.trie_finmap_lemmas <- FinMap.lms ( trie_is_fin_map )
GTrie <- FinMap.MT ( trie_is_fin_map )
```

In the first example, `MapType`

is a projection, but you also pass the projected, so there is no inference

yes first example works as expeced, the problem is with this case:

```
Fail Check ({[1 := true]} : GTrie nat bool). (* ??? should work but does not work! *)
```

which is the same as the projection but less verbose

You should try stuff lile `Check (eq_refl _ : GTrie = FinMap.MT _)`

roughly

the second `_`

is what CS fill in

(I may not have passed all argumnets, but the heads must be that)

```
Goal GTrie nat bool = MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq).
Proof.
by [].
Qed.
```

The last line of the DB is giving a solution for that exact problem

OK, then

```
Check (eq_refl _ : GTrie nat bool = MapType nat_eqType bool _)
```

should also work

That proof is goes through.

not the check one!

Since the missing piece is the canonical solution

(cannot unify "bool" and "Type").

The error message in complete is :

```
The term "eqxx ?x" has type "is_true (?x == ?x)"
while it is expected to have type
"GTrie nat bool = MapType nat_eqType bool ?t"
(cannot unify "bool" and "Type").
```

Hum, try `Check (erefl _ : ......)`

,

I must have done a mistake, I don't have a running Coq now

or maybe `(erefl : ... = ...)`

, whatever types

The idea is that you want the unification engine to solve the equation.

```
erefl ?x
: ?x = ?x
```

great, so

```
Check (erefl _ : GTrie nat bool = MapType nat_eqType bool _)
```

well it is strange, it failed again but with different error message:

```
The term "erefl (GTrie nat bool)" has type
"GTrie nat bool = GTrie nat bool"
while it is expected to have type
"GTrie nat bool = MapType nat_eqType bool ?t".
```

but apparently coq cannot solve it

once I start filling in the `_`

coq is able to solve it.

can you post again you Canonical declaration with all parameters explicit?

```
Canonical Structure trie_is_fin_map (K: serDeEqType) :=
@FinMap.Pack (SerDeEqType.to_eq K) GTrie (GTrie.gtrie_finmap_ops K) (GTrie.trie_finmap_lemmas K).
```

now that we are at it the SerDeEqType inherits from something called serde and eqType (at least as per my understanding of inheritence:

```
Module SerDeEqType.
Record mixin T := Mixin {
Eq_type: Equality.mixin_of T;
SerDe_ops: SerDe.operations T;
SerDe_lemmas: SerDe.lemmas SerDe_ops;
}.
Record type := Class {
SEQ: Type;
ops: mixin SEQ;
}.
Definition to_eq (t: type) : eqType :=
Equality.Pack (Eq_type (ops t)).
Definition to_serde (t: type) : serDe :=
SerDe.Pack (SerDe_lemmas (ops t)).
End SerDeEqType.
Canonical Structure SerDeEqType.to_eq.
Canonical Structure SerDeEqType.to_serde.
```

and `nat`

have this implemented.

walker said:

`Canonical Structure trie_is_fin_map (K: serDeEqType) := @FinMap.Pack (SerDeEqType.to_eq K) GTrie (GTrie.gtrie_finmap_ops K) (GTrie.trie_finmap_lemmas K).`

something is fishy, `GTrie : Type -> Type -> Type`

, but `Pack`

wants a `eqType -> Type -> Type`

...

I'm a bit lost without a running Coq

I tried doing `GTrie : serDeEqType -> Type -> Type`

but apparently it does (and shouldn't) not work in this case and coq failed to convert it to

```
The term "GTrie" has type "serDeEqType -> Type -> Type"
while it is expected to have type "eqType -> Type -> Type"
(cannot unify "eqType" and "serDeEqType").
```

Which makes sense.

in any case we can continue debugging tomorrow if you would like to.

it is also getting late here.

Hello again, I was able to create a relatively small self contained reproducer:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Module SerDeEqType.
Record mixin T := Mixin {
Eq_type: Equality.mixin_of T;
Serialize: T -> unit;
}.
Record type := Class {
SEQ: Type;
ops: mixin SEQ;
}.
Definition to_eq (t: type) : eqType :=
Equality.Pack (Eq_type (ops t)).
End SerDeEqType.
Canonical Structure SerDeEqType.to_eq.
Definition nat_serde_ops: SerDeEqType.mixin nat.
Proof.
constructor.
apply nat_eqMixin.
intros. apply tt. Defined.
Canonical Structure nat_is_serde_eq := @SerDeEqType.Class nat nat_serde_ops.
Module FinMap.
Record operations (K: eqType) (M: eqType -> Type -> Type) := Operations {
Empty V : M K V;
}.
Structure type (K: eqType):= Pack{
MT: eqType -> Type -> Type;
ops: operations K MT;
}.
End FinMap.
Definition map_empty {K V} {e: FinMap.type K}: FinMap.MT e K V := (FinMap.Empty (FinMap.ops e) V).
Definition GTrie (K V: Type) : Type := unit.
Definition gtrie_finmap_ops (K :SerDeEqType.type):
FinMap.operations (SerDeEqType.to_eq K) GTrie.
Proof. constructor. intros. apply tt. Defined.
Canonical Structure trie_is_fin_map (K: SerDeEqType.type) := FinMap.Pack (gtrie_finmap_ops K).
Check (map_empty : FinMap.MT (trie_is_fin_map nat_is_serde_eq) (SerDeEqType.to_eq nat_is_serde_eq) nat).
Check (map_empty: FinMap.MT (trie_is_fin_map nat_is_serde_eq) nat_eqType nat). (* works as well*)
Fail Check (map_empty : GTrie nat nat). (* <----- I want this one to work *)
```

I'm am not knowledgeable on CS, but I find suspicious that `nat_serde_ops`

is defined with `Qed`

: if I'm not mistaken, it means that the eqType instance contained in that definition won't be convertible to `nat_eqType`

.

right! my bad this is a bug in this minimal reproducer that was not in the original code, and fixing this makes the second check works! I edited the reproducer.

via trial and error I discovered that :

```
Module FinMap.
Record operations (K: eqType) (M: Type -> Type -> Type) := Operations {
Empty V : M K V;
}.
Structure type (K: eqType):= Pack{
MT: Type -> Type -> Type;
ops: operations K MT;
}.
End FinMap.
```

Should make things work,

That said, I still believe the old `FinMap`

module should also work and having it not working is some kind of bug in the unification algorithm.

Last updated: Aug 03 2024 at 23:02 UTC