[Agda] COMPILED_DATA directive for Maybe

[Nicolas Pouillard]

Excerpts from Dan Doel's message of Mon Nov 23 23:24:42 +0100 2009:
> On Monday 23 November 2009 4:35:09 pm Nicolas Pouillard wrote:
> > > Why Maybe {zero} is the Haskell one? It seems each Maybe {a : Level}
> > > could be.
> > 
> > Maybe I understand this wrong but for me Maybe {zero} is a type (Set0)
> >  which classifies values, whereas Maybe {suc zero} is a Set1 which
> >  classifies types. Moreover in Haskell sorts classify types and sorts are
> >  only made of * (Star) and arrows (I mean without the fancy GHC
> >  extensions).
> 
> Well, things aren't quite so simple. Set1 doesn't just contain types, it 
> contains datakinds, so to speak. And moreover, some Agda types are forced into 
> Set1 when they are able to live in * due to a moderate level of 
> impredicativity in the Haskell type system (assuming higher-rank types). For 
> instance:
> 
>   data Step a s = Done | Yield a s
> 
>   data Stream a where
>     Unfold :: forall s. s -> (s -> Step a s) -> Stream a

Yes I agree with the impredicativity point. Actually implementing a bit of
StreamFusion was my first use of this new feature.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr