Stream: math-comp users

Topic: Canonical structure creation warning

Pierre Jouvelot (Jan 20 2022 at 09:51):

I'd like to understand, and get rid of, a warning when creating a Canonical structure (following the one used for ordinals):

From mathcomp Require Import all_ssreflect.

Variable k n : nat.

Record O :=
Outcome {os : k.-tuple 'I_n;
ouniq : uniq os}.

Coercion os : O >-> tuple_of.

Canonical O_subType := Eval hnf in [subType for os].
Canonical O_eqType := Eval hnf in EqType _ [eqMixin     of O by <: ].
Canonical O_choiceType := Eval hnf in ChoiceType _ [choiceMixin of O by <:].
Canonical O_countType := Eval hnf in CountType _ [countMixin  of O by <:].
Canonical O_subCountType := Eval hnf in [subCountType of O].
Canonical O_finType := Eval hnf in FinType _ [finMixin    of O by <:].
Canonical O_subFinType := Eval hnf in [subFinType of O].
Canonical O_predType := PredType (fun o x => x \in os o).


The last command generates the following warning:

O_predType is defined
Warning: Projection value has no head constant: fun o : O => in_mem^~ (mem o) in canonical
instance O_predType of topred, ignoring it. [projection-no-head-constant,typechecker]


Interestingly enough, if I remove the O_predType command, the \in predicate doesn't work anymore, at least unless I provide the explicit projection os, even though the warning states that the command has, apparently, been ignored.

Any suggestion?

Enrico Tassi (Jan 20 2022 at 10:25):

In Coq 8.14 we have these two new things about canonical structures:

• Added: Enable canonical fun _ => _ projections, see Canonical Structures for details. (#14041, by Jan-Oliver Kaiser and Pierre Roux, reviewed by Cyril Cohen and Enrico Tassi).
• Added: Canonical Structure declarations now accept dependent function types forall _, _ as keys. (#14386, by Jan-Oliver Kaiser and Kazuhiko Sakaguchi).

I wonder if you are on 8.14

Cyril Cohen (Jan 20 2022 at 11:22):

The warning does not say the command is ignored. It says that only the canonical instance for thetopred projection is ignored, on the other hand, the canonical instance for the pred_sort projection, which is actually the one and only one that matters, is added.
The fix would be to disable locally the warning.

Pierre Jouvelot (Jan 20 2022 at 11:43):

Thanks for the detailed explanation. And indeed, I'm still using 8.13. I need to update my nix environment.

Enrico Tassi (Jan 20 2022 at 12:20):

Then the right fix is in mathcomp, we should flag the other field non canonical: https://coq.inria.fr/refman/language/core/records.html#grammar-token-record_field

Enrico Tassi (Jan 20 2022 at 12:23):

The attribute exists since 8.11

Cyril Cohen (Jan 23 2022 at 22:59):

Enrico Tassi said:

Then the right fix is in mathcomp, we should flag the other field non canonical: https://coq.inria.fr/refman/language/core/records.html#grammar-token-record_field

Nop! As noted in this thread, the right fix is not in the structure definition, since this overshoots all instances, it's in the instance declaration.

Enrico Tassi (Jan 24 2022 at 15:30):

I'm a bit lost, you say "...which is actually the one and only one that matters," so I guess the others don't need to be canonical, ever.

Last updated: Jan 29 2023 at 18:03 UTC