Add error for overloaded Haskell constructors

[PPKFS]

Solves #125.

Unfortunately, it seems the Agda compiler only does its compiler magic for each definition independently, so there is no state carried over as to the previous definitions that have been compiled.

We check all the constructors generated for duplicates prior to writeOutput in postCompile and refuse to continue if there are duplicates. This does also add scaffolding for future post-compilation, pre-render verification steps.

[jespercockx]

Unfortunately, it seems the Agda compiler only does its compiler magic for each definition independently, so there is no state carried over as to the previous definitions that have been compiled.

Yes, we have discussed this limitation before, and then we came to the conclusion that the best way to have some shared state would be to use an IORef (which is possible since the C monad implements MonadIO).

However, for this issue the solution you propose also seems like a reasonable approach.

[jespercockx]

Maybe you could just make verifyOutput a part of writeModule, or else add a new function that does these two functions in sequence?

[PPKFS]

I think a new function is probably best. Having writeModule, in Render, also do final verification feels like a weird mixup of concerns

[jespercockx]

The test suite fails on the following:

== Comparing output ==
diff -r build/Issue125.err golden/Issue125.err
1c1
< Cannot generate multiple constructors with the same identifier: ACtr
---
> Found multiple declarations of constructor: ACtr

Please run make test and make golden and then commit the changes to the golden files.

[PPKFS]

I was looking for a cabal test equivalent and didn't think to check for a makefile. Oops.