Add built-in support for Delay monad

[jespercockx]

Currently there is no good way to define potentially-looping functions with agda2hs. We have the loop function in Haskell.Extra.Loop but it still requires a proof of termination if you want to use it on the Agda side. This PR adds support for the Delay monad to agda2hs, in a way that is completely transparent in the resulting Haskell code.

[jespercockx]

Hm, I just realized this is not sound, since it is possible to distinguish between now and later in Agda. For example, one can write the following function:

bad : Delay a ∞ → Bool
bad (now x) = True
bad (later x) = False

which would get compiled to

bad :: a -> Bool
bad x = True
bad x = False

which is, well, bad.

If we want to have actual support for delay, we should enforce somehow that the result is the same in both cases, or simply forbid pattern matching on Delay altogether.

[jespercockx]

Perhaps we could allow a single function runDelay defined like this:

runDelay : {@0 x : a} (y : Delay a ∞) → @0 HasResult x y → a
runDelay (now x) now = x
runDelay (later y) (later p) = runDelay (y .force) p

plus possibly a proof that the result of runDelay is indeed equal to x.

[jespercockx]

@flupe this is ready now, could you do a quick review?

[flupe]

lgtm