Add new module Dec for decidability proofs (compiled to Bool)

[jespercockx]

No description provided.

[flupe]

Do you think you could remove the old definition of Reflects? and maybe just define patterns synonyms for ofY and ofN if you don't want to touch Haskell.Law too much.

On a side note, I don't think anything from Haskell.Law should be exported in Haskell.Prelude.

[flupe]

Currently, this module (if it was compiled to Haskell) would generate a single type alias type Dec = Bool. Using Dec from some other module compiled with agda2hs would thus produce Haskell code with an explicit import to Haskell.Extra.Dec which doesn't exist.

Two ways to go about it:

• Hardcode the mapping from Haskell.Extra.Dec.Dec to Bool in agda2hs, and as a policy enforce that all definitions in Haskell.Extra get desugared into Haskell code that still has no dependencies other than the (Haskell) Prelude.
• Have an extended (agda2hs) Haskell prelude available as a Haskell library.

[jespercockx]

Ideally we would not compile Dec at all and instead have agda2hs rewrite it to Bool. That shouldn't be too hard to do.

[flupe]

Yeah, I was also thinking about your other opened PRs defining modules in Haskell.Extra like loop.

[jespercockx]

That one's here https://hackage.haskell.org/package/extra-1.7.14/docs/Control-Monad-Extra.html#v:loop

[jespercockx]

That "close PR" button is altogether too close to the "comment" button

[jespercockx]

I've updated this PR to address your comments @flupe , the commits should be self-explanatory.

[flupe]

Very nice! So currently putting inline after the identifier in the COMPILE pragma doesn't throw any error and is just ignored?