[Agda] ... because it contains Dec which does not have a COMPILE pragma.

[Johannes Waldmann]

Hi.

when extracting Haskell code from this Agda module
https://gitlab.imn.htwk-leipzig.de/waldmann/cetera/-/tree/weights

I am getting this error

  ... R.agda:658,1-37

The type {C : Set} → DecidableEquality C → Certificate C → Bool
cannot be translated to a corresponding Haskell type, because it
contains Dec which does not have a COMPILE pragma.

I thought I was being clever by using decidable things,
and following recommendations, e.g.,
https://plfa.github.io/Decidable/#the-best-of-both-worlds
and I was hoping that the "proof" part of Dec will be erased.
How can this be done? (I can't put a COMPILE pragma for Dec
in my module, and I don't want to give up the Dec type
as that would entail duplication of code/proof,
if I understand the documentation right(

Best regards, Johannes.

NB: this is my very first Agda project,
so I'm sure it's ignoring tons of guidelines.
I can beautify later, and I welcome suggestions for that,
but for now I just want this to work.