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

[Johannes Waldmann]

> The type {C : Set} → DecidableEquality C → Certificate C → Bool
> cannot be translated to a corresponding Haskell type, 

OK,  I could solve this, by making the function monomorphic
and fixing the (Dec _) argument on the Agda side,
so it does not show up on the Haskell side (I think)

- J.