Stream: Hierarchy Builder devs & users

Topic: Projection value has no head constant. Is that bad ?


view this post on Zulip Florent Hivert (Nov 27 2023 at 16:53):

The following code

Record invlim := MkInvLim {
                     invlimthr :> forall i, Obj i;
                     _ : `[< isthread Sys invlimthr >];
                   }.

HB.instance Definition _ := [isSub for invlimthr].
HB.instance Definition _ := gen_eqMixin invlim.
HB.instance Definition _ := gen_choiceMixin invlim.

triggers the following warning

arning: Projection value has no head constant:
fun (K : invlim -> Type)
  (K_S : forall (x : forall i : I, Obj i)
           (Px : (fun x0 : forall i : I, Obj i => `[< isthread Sys x0 >]) x),
         K (MkInvLim Px)) (u : invlim) =>
match u as u0 return (K u0) with
| @MkInvLim x Px => K_S x Px
end in canonical instance HB_unnamed_factory_142 of isSub.Sub_rect, ignoring
it. [projection-no-head-constant,records,default]

What does it mean ? Is that Bad ?

view this post on Zulip Pierre Roux (Nov 27 2023 at 17:05):

I guess it means it's not able to instanciate something due to the "key" having no head constant. If you got the instances you were expecting, it's probably fine, otherwise it's indeed bad.

view this post on Zulip Florent Hivert (Nov 27 2023 at 20:22):

I manage to fix the first code. I got a second one with the same error but I don't know how to fix it:

Variable R : ringType.
Variable n : nat.

Implicit Types (p q r s : {poly R}).

Record truncfps := MkTfps { tfps : {poly R}; _ : size tfps <= n.+1 }.

HB.instance Definition _ := [isSub for tfps].        (* <=      Warning here *)
HB.instance Definition _ := [Choice of truncfps by <:].

Any idea how to fix the problem ?

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:10):

@Florent Hivert the warning is spurious, the canonical projections on non "keys" should be ignored. It's a known (but apparently unreported) issue in HB, where we should add a declaration of the form "canonical=false" when we declare mixin instances in hb.

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:13):

@Cyril Cohen So I can safely ignore the warning for the moment. Thanks for the confirmation. Do you want me to create an issue on HB github with the example on polynomials above ?

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:15):

Oh wait, I'm not sure anymore... what happens if you do:

Variable R : ringType.
Variable n : nat.

Implicit Types (p q r s : {poly R}).

Record truncfps := MkTfps { tfps : {poly R}; _ : size tfps <= n.+1 }.

HB.instance Definition _ : isSub _ _ truncfps := [isSub for tfps]. (* <=   is there a warning here *)

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:20):

Error:
Definition illtyped: In environment
R : ringType
n : nat
The term "[isSub for tfps]" has type
 "isSub.axioms_ {poly R} (fun x : {poly R} => size x <= n.+1) truncfps"
while it is expected to have type "SubType.axioms_ ?p truncfps".

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:22):

I missed two _, so I patched my code, please amend accordingly

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:25):

Again an error message. I fixed my post consistently with you editing.

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:28):

I amended again, thanks

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:30):

This time I got the warning back:

HB_unnamed_factory_1 is defined
Warning: Projection value has no head constant:
fun (K : truncfps -> Type)
  (K_S : forall (x : {poly R}) (Px : (fun x0 : {poly R} => size x0 <= n.+1) x),
         K (MkTfps Px)) (u : truncfps) =>
match u as u0 return (K u0) with
| @MkTfps x Px => K_S x Px
end in canonical instance HB_unnamed_factory_1 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]
tfps_truncfps__canonical__eqtype_SubType is defined

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:33):

So the warning is what I said in the beginning... I would be grateful if you added an issue

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:38):

This is now: https://github.com/math-comp/hierarchy-builder/issues/402

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:51):

Happy to help testing the thing ! :smile:


Last updated: Apr 21 2024 at 01:02 UTC