[Agda] COMPILED_DATA directive for Maybe

[Nicolas Pouillard]

Excerpts from Nils Anders Danielsson's message of Mon Nov 23 13:50:09 +0100 2009:
> On 2009-11-22 23:05, Andrés Sicard-Ramírez wrote:
> > Any ideas how to define a COMPILED_DATA directive for the (new)
> > universe polymorphic datatype Maybe defined in Data.Maybe.Core?
> 
> If the universe polymorphism was uniform, then I believe it would be
> possible to map all variants of Maybe to the Haskell Maybe type.
> However, an Agda program can treat Maybe {zero} and Maybe {suc zero}
> differently, so this is not possible. If you want to interoperate with
> the Haskell Maybe type, then I suggest that you define a
> non-universe-polymorphic variant of Maybe in Foreign.Haskell.

Could we export Maybe {zero} which is really the Haskell one. It would
be nice to don't have to redefine a new one.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr