Always drop "Haskell." prefix from module names

[jespercockx]

This supersedes #297. The idea (due to @omelkonian) is that any module starting with Haskell. should be treated as defining part of the FFI with Haskell and should thus not be checked for having COMPILE pragmas, but instead be assumed to exist on the Haskell side while dropping the Haskell. prefix from the module name.

[jespercockx]

Three things to consider before merging this:

• There is a risk of introducing a name collision between Haskell.Foo.Bar and Foo.Bar. Can we do anything about this?
• Should we enforce that Haskell. modules do not produce any output?
• Can we make it clearer to the user that defining a Haskell. module is an unsafe thing to do? We can certainly add a note to the documentation, but is there anything else we can do?

[jespercockx]

Related: #316

[viktorcsimma]

This is a nice idea:) I often utilise similar concepts, and this would be of great help.

• For the first one: I have checked this and GHC, in this case, prefers the user-defined module. So Foo.Bar would trump Haskell.Foo.Bar in this case. See example.zip here. But I do not have an idea on how to circumvent this, apart from a note in the docs.
• For the second: I think we should. If the output were Foo.Bar, it would trump the Haskell builtin version, which we probably do not want. If it were Haskell.Foo.Bar, it would be an ordinary agda2hs-generated module.
• For the third: what about hiding the feature behind a flag? Like with --erasure in Agda. Then, if the user defines a module beginning with Haskell., we fail and tell them to change the name, or add the flag if they know what they are doing. (It would be even better if we could add this flag to a language pragma at the top of the file.)

[jespercockx]

Regarding the first two: actually, if we implement the second and enforce no Haskell code being generated from Haskell. files, then there is no risk of conflicts. There is one module in our own prelude that does not conform to this restriction (https://github.com/agda/agda2hs/blob/master/lib/Haskell/Extra/Loop.agda), but I don't think anyone is using it so we could just drop it.

I like the idea of having a pragma that should be in every module under Haskell., that way we can prevent users from accidentally running into this feature.

[jespercockx]

I added the check that modules under the Haskell. namespace do not produce any Haskell output, solving the first two problems. I don't think that 3 is such a big problem anymore, since the Haskell code will not compile anyway unless the corresponding Haskell bindings are already there. So let's just leave it as it is now, and add the flag if it proves to be really necessary.