[Agda] Using Haskell type class constraints with Agda types

[Alexander Ben Nasrallah]

Hi there,

I'm currently playing around with Agdas FFI. I know that "There is
(currently) no way to map a Haskell type with type class constraints to
an Agda type." The manual describes a workaround for how to pass
postulated Haskell types to postulated functions with type class
contraints in Agda.

https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html#handling-typeclass-constraints

I was wondering if it is possible to modify the
workaround, so I can pass a non-postulated Agda type to postulated
functions with constraints.

Concrete I would like to (de)serialize JSON using Aeson. Therefore I
defined a record `ToJSON` which shall resemble the `ToJSON` type class.
Now I would like to pass `ToJSON` instance arguments to postulated
functions with `ToJSON` type class contraints.

I unsuccessfully tried a few approaches. Here is my current work in progress:

https://gitlab.com/neosimsim/verified-parsing/-/blob/aeson/src/Foreign/Haskell/Data/Aeson.agda#L34

Does anyone have any ideas, how to make this work or is it just not
possible (yet)?

Kind regards
Alex