Conformance testing of the agda2hs Prelude

[jespercockx]

It would be good to have some kind of testing that ensures our implementation of the Haskell prelude is correct. For example, for each function we could compile our implementation to Haskell and use QuickCheck to check that it is equivalent to the builtin one.

[HeinrichApfelmus]

The following would be more modest in scope, but already useful:

• Automatically check that the function names are in scope.
• Automatically check that the functions have the same types in Agda and in Haskell.

Both can be achieved with the method described in #316 . (Unsurprisingly — the problem is essentially that of importing a Haskell module, here the Prelude). The idea would be to automatically generated definitions of the form

import qualified Prelude

foo :: Bar → Baz
foo = Prelude.foo

and run the Haskell compiler on it. Specifically, the definition foo and its type signature is automatically generated from the definition in .agda.