Stream: Hierarchy Builder devs & users

Topic: Huge error message I can't manage to understand.


view this post on Zulip Florent Hivert (Oct 07 2024 at 06:44):

Hello ! I defined a structure for modeling functors:

HB.mixin Record isFunctor (C D : category) (F : C -> D) := {
    actm : forall a b, {hom a, b} -> {hom F a, F b} ;
    functor_ext_hom : FunctorLaws.ext actm ;
    functor_id_hom : FunctorLaws.id actm ;
    functor_comp_hom : FunctorLaws.comp actm
  }.
HB.structure Definition Functor C D := {F of isFunctor C D F}.

I'm trying to build an instance and HB is failing for a reason I don't understand. When I write

Check @isFunctor.Build Sets (LModules R)
    (@freeLmod R) freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.

I get

isFunctor.phant_Build freeLmod_ext freeLmod_id freeLmod_comp
     : isFunctor.axioms_ [the category of choiceType] [the category of
         lmodType R] (fun T : [the category of choiceType] => { freemod R [T] })

which seem to indicate that everything is ok. But

HB.instance Definition _ :=
  @isFunctor.Build Sets (LModules R)
    (@freeLmod R) freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.

gives the following huge message

Error:
term->gref: input has no global reference: fun `T`
 (app
   [global (const «Category.sort»),
    app
     [global (const «TheCanonical.get»),
      sort (typ «HB_unnamed_factory_102.u0»),
      global (indt «Category.type»), global (indt «Choice.type»),
      global (const «Choice_type__canonical__category_Category»),
      app
       [fun `s` (global (indt «Category.type»)) c0 \
         app
          [global (indc «TheCanonical.Put»),
           sort (typ «HB_unnamed_factory_102.u0»),
           global (indt «Category.type»), global (indt «Choice.type»),
           app [global (const «Category.sort»), c0], c0],
        global (const «Choice_type__canonical__category_Category»)]]]) c0 \
 app
  [pglobal (const «reverse_coercion»)
    «Category.axioms_.u0 freeLmod_mor.u4»,
   app
    [global (const «Category.sort»),
     app
      [global (const «TheCanonical.get»),
       sort (typ «HB_unnamed_factory_102.u1»),
       global (indt «Category.type»),
       app [global (indt «GRing.Lmodule.type»), global (const «R»)],
       app
        [global (const «Lmodule_type__canonical__category_Category»),
         global (const «R»)],
       app
        [fun `s` (global (indt «Category.type»)) c1 \
          app
           [global (indc «TheCanonical.Put»),
            sort (typ «HB_unnamed_factory_102.u1»),
            global (indt «Category.type»),
            app [global (indt «GRing.Lmodule.type»), global (const «R»)],
            app [global (const «Category.sort»), c1], c1],
         app
          [global (const «Lmodule_type__canonical__category_Category»),
           global (const «R»)]]]], sort (typ «freeLmod_mor.u3»),
   app
    [global (const «msetcompl_freeLmod__canonical__GRing_Lmodule»),
     global (const «R»), c0],
   app
    [global (const «freeLmod»),
     app
      [global (const «GRing_Ring__to__GRing_Nmodule»), global (const «R»)],
     c0]]

Does this makes sense to someone ? Any suggestion ?

view this post on Zulip Cyril Cohen (Oct 07 2024 at 07:30):

Can you printfreeLmod please?

view this post on Zulip Florent Hivert (Oct 07 2024 at 08:03):

Sure

freeLmod =
fun (R : nmodType) (T : choiceType) => {fsfun T -> R with 0}
     : nmodType -> choiceType -> Type

view this post on Zulip Florent Hivert (Oct 07 2024 at 08:04):

By the way the code is in https://github.com/hivert/Adjoint
The problem is at the end of https://github.com/hivert/Adjoint/blob/main/theories/examples.v

view this post on Zulip Cyril Cohen (Oct 07 2024 at 12:06):

I expect a eta expansion of freeLmod is triggered accidentally, and we fail to check this is ok in HB.

view this post on Zulip Cyril Cohen (Oct 07 2024 at 12:06):

NB: you should be able to remove all the [the ...]

view this post on Zulip Cyril Cohen (Oct 07 2024 at 12:08):

I think the eta conversion is triggered because of the typechecking of @freeLmod T as a choiceType -> choiceType... Which is unfortunate because that's exacly what we want...

view this post on Zulip Cyril Cohen (Oct 07 2024 at 12:09):

I'll investigate later..

view this post on Zulip Florent Hivert (Oct 08 2024 at 10:26):

FYI, I manage to solve / workaround the problem with

Definition freeLmod_functor a : lmodType R := {freemod R[a]}.
HB.instance Definition _ :=
  @isFunctor.Build Sets (LModules R) freeLmod_functor
     freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.

view this post on Zulip Cyril Cohen (Oct 08 2024 at 11:32):

That's what I was going to suggest you.

view this post on Zulip Cyril Cohen (Oct 08 2024 at 11:32):

but that's a workaround indeed.

view this post on Zulip Florent Hivert (Oct 08 2024 at 11:39):

I just got :smiley:

Let F : {functor Sets -> LModules R} := functor_freeLmod R.
Let G : {functor LModules R -> Sets} := forget_LModules_to_Sets R.

Definition adj_FreeLmod_forget : F -| G := AdjointFunctors.mk triL_fm triR_fm.

Last updated: Oct 13 2024 at 01:02 UTC