I'm trying to make the `ZmodQuotType`

notation found in "ring_quotient.v" work, however I keep getting the same errors.

To demonstrate, consider the following lemma:

```
Lemma MyError o mul Q mix : forall (a : (RingQuotType o mul Q mix)), a == a.
```

This statement does not typecheck and gives the error:

```
In environment
o : ?T
mul : ?T1 -> ?T1 -> ?T1
Q : Type
mix : ?T0
x : phantom (quot_class_of ?T1 ?qT) (quot_class ?qT)
The term "x" has type "phantom (quot_class_of ?T1 ?qT) (quot_class ?qT)"
while it is expected to have type "phantom (quot_class_of ?T1 Q) ?qc".
```

Taking a deeper look at the definition in "ring_quotient.v" we find:

```
Notation RingQuotType o mul Q mix :=
(@RingQuotType_pack _ _ _ _ _ o mul Q _ _ _ _ id id mix).
```

The error seems to come from the two `id`

symbols. I'm not too familiar with phantom types but I guess these are to ensure the quot and ring types are compatible. Replacing them with underscores allows the lemma to typecheck but I'm not sure that is the right thing to do.

Can anyone shed any light on this error? (Also the same thing happens with the `ZmodQuotType`

notation).

It probably means that Q need to have more structure than a bare Type. I guess at least eqType or even ringType.

(deleted)

Last updated: Jul 25 2024 at 15:02 UTC