[Agda] COMPILED_DATA directive for Maybe

[Andrés Sicard-Ramírez]

Nicolas,

On Mon, Nov 23, 2009 at 10:31 AM, Nicolas Pouillard
<nicolas.pouillard at gmail.com> wrote:
> 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.
>

Why Maybe {zero} is the Haskell one? It seems each Maybe {a : Level} could be.

-- 
Andrés