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?
In Coq 8.14 we have these two new things about canonical structures:
I wonder if you are on 8.14
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.
Thanks for the detailed explanation. And indeed, I'm still using 8.13. I need to update my nix environment.
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
The attribute exists since 8.11
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.
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: Oct 13 2024 at 01:02 UTC