Generic

Generic copied to clipboard

Currently there is a build failure like:

Checking Everything (/build/source/Everything.agda).
 Checking Generic.Test (/build/source/src/Generic/Test.agda).
  Checking Generic.Test.Data (/build/source/src/Generic/Test/Data.agda).
   Checking Generic.Test.Data.Fin (/build/source/src/Generic/Test/Data/Fin.agda).
    Checking Generic.Main (/build/source/src/Generic/Main.agda).
     Checking Generic.Core (/build/source/src/Generic/Core.agda).
      Checking Generic.Lib.Prelude (/build/source/src/Generic/Lib/Prelude.agda).
       Checking Generic.Lib.Intro (/build/source/src/Generic/Lib/Intro.agda).
       Checking Generic.Lib.Equality.Propositional (/build/source/src/Generic/Lib/Equality/Propositional.agda).
       Checking Generic.Lib.Equality.Coerce (/build/source/src/Generic/Lib/Equality/Coerce.agda).
        Checking Generic.Lib.Decidable (/build/source/src/Generic/Lib/Decidable.agda).
         Checking Generic.Lib.Equality.Heteroindexed (/build/source/src/Generic/Lib/Equality/Heteroindexed.agda).
         Checking Generic.Lib.Data.Sum (/build/source/src/Generic/Lib/Data/Sum.agda).
         Checking Generic.Lib.Data.Product (/build/source/src/Generic/Lib/Data/Product.agda).
          Checking Generic.Lib.Category (/build/source/src/Generic/Lib/Category.agda).
       Checking Generic.Lib.Equality.Congn (/build/source/src/Generic/Lib/Equality/Congn.agda).
        Checking Generic.Lib.Data.Nat (/build/source/src/Generic/Lib/Data/Nat.agda).
        Checking Generic.Lib.Data.Pow (/build/source/src/Generic/Lib/Data/Pow.agda).
        Checking Generic.Lib.Data.Sets (/build/source/src/Generic/Lib/Data/Sets.agda).
       Checking Generic.Lib.Data.String (/build/source/src/Generic/Lib/Data/String.agda).
       Checking Generic.Lib.Data.Maybe (/build/source/src/Generic/Lib/Data/Maybe.agda).
       Checking Generic.Lib.Data.List (/build/source/src/Generic/Lib/Data/List.agda).
       Checking Generic.Lib.Reflection.Core (/build/source/src/Generic/Lib/Reflection/Core.agda).
/build/source/src/Generic/Lib/Reflection/Core.agda:8,45-90
The module Reflection.Argument.Information doesn't export the
following:
  relevance
when scope checking the declaration
  open import Reflection.Argument.Information public
                                              using (ArgInfo; visibility; relevance)
/build/source/src/Generic/Lib/Reflection/Core.agda:174,37-46
Not in scope:
  relevance
  at /build/source/src/Generic/Lib/Reflection/Core.agda:174,37-46
    (did you mean
       'Agda.Builtin.Reflection.Relevance.relevant' or
       'Agda.Builtin.Reflection.Relevance' or
       'Agda.Builtin.Reflection.relevant' or
       'Reflection._

See:

• https://github.com/NixOS/nixpkgs/pull/130424#issuecomment-885563001
• https://hydra.nixos.org/build/148413834/nixlog/1/tail

I'd like this too!

I'll look into it this weekend.

(my machine has died, so the next weekend or the one after that)

So I tried to update the library, but Reflection has changed a lot and now it's not clear to me at all how to do the same thing that I used to do before with the new version of Reflection. In particular, in some places String names have changed to De Bruijn indices and it's not clear to me how to move from the latter to the former (or vice versa).

I have like zero time these days, so that's about as much as I can contribute.

You will likely have better luck with https://github.com/flupe/generics

Thanks for investigating, and for all of your time!