Add support for Data.Dynamic

[jespercockx]

Haskell's Data.Dynamic library (https://hackage.haskell.org/package/base-prelude-1.6.1.1/docs/BasePrelude.html#v:Dynamic) allows dynamic typing in Haskell for all values of Typeable types. It could be possible to add support for a COMPILE AGDA2HS DYNAMIC pragma that compiles an Agda type to Dynamic in Haskell, as long as all the possible concrete types this value could compute to are instances of Typeable.

The main use case for this that I see would be to more easily support compiling existing Agda functions that do not necessarily fall into the fragment accepted by agda2hs. In particular, types that are defined through large elimination, i.e. functions into Set, could be compiled into Dynamic which would enable compiling functions that use them. But there might be other use cases too.

[jespercockx]

I just realize that this would not really work for the use case that I described, unless all the possible types returned by the function are also compiled to Dynamic. However, it would still be interesting to have support for Data.Dynamic in general, so I'm keeping this issue open for that.

[jespercockx]

I just happened to think about this feature again. One possibility would be to have the Agda version of Dynamic take an erased parameter of type Set , so it would still be possible to reason about the static type of Dynamic values on the Agda side. In particular this erased type could make free use of type-level functions.