Fix for #357

[jespercockx]

This fixes #357 by adding a check that type arguments are valid Haskell types before dropping them. It also makes some changes to the Prelude (in particular to guard) so it conforms to this new check.

[flupe]

What's the motivation for changing the interface of Erase and making the field an instance? Seems like it forces explicit brackets {{}} everywhere.

[jespercockx]

Well, it was to make sure that instance search could actually find an element of type Erase A when there is an erased instance of type A in scope. But I found a better way to get the same effect, which does not break backwards compatibility (see newly pushed version).

[flupe]

Is it a situation that arises often? Having instances of a laying around? For equality proofs I get, but otherwise not so sure. But I trust you that the interface hasn't changed :). (I would have kept the old Erase definition and defined iErased separately but it probably doesn't matter much. And with yours one can decide to match and directly introduce an instance, which I don't know if you can do otherwise)

[jespercockx]

The opposite way (defining Erased as the constructor and iErased as the pattern synonym) is not accepted by Agda:

.../agda2hs/lib/Haskell/Extra/Erase.agda:22,21-22: error: [IllegalInstanceVariableInPatternSynonym]
Variable is bound as instance in pattern synonym, but does not
resolve as instance in pattern: x
when scope checking the declaration
  pattern iErased ⦃ x ⦄ = Erased x

[flupe]

Looks good! The errors are perhaps not ideal to get what's wrong but I understand it would be annoying to make them clearer.

[jespercockx]

There's a problem with this PR, namely that it breaks the use of the Functor instance for functions. Here's a contrived example:

open import Haskell.Prelude

test : Bool → Bool
test = not <$> not

{-# COMPILE AGDA2HS test #-}

Error message:

Not supported: type-level lambda λ b → Bool → b

The type argument to _<$>_ is λ b → Bool → b which agda2hs sensibly complains is not valid Haskell. Agda does not have function arrow sections.

The only way I can think of to prevent the eta-expansion on the Agda side is to wrap the function type in a (transparent) record type.

[jespercockx]

I tried to fix the problem with the Functor instance for the function type by defining

record Function (a b : Set) : Set where
  field
    apply : a → b
open Function public

{-# COMPILE AGDA2HS Function unboxed #-}

but unfortunately it seems we do not properly support partially applied unboxed record types. Trying to compile the not <$> not example results in an internal error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/Agda2Hs/Compile/Type.hs:163:17 in main:Agda2Hs.Compile.Type

(the same problem happens for partially applied tuple types.)

It is actually not so obvious how agda2hs should figure out that Function a should compile to a -> here. Perhaps it warrants building special support for this type into agda2hs?

Second thought: if we are anyway hard-coding things into agda2hs, it would be easier to just recognize λ b → a → b and compile it to a ->.

[jespercockx]

Second thought: if we are anyway hard-coding things into agda2hs, it would be easier to just recognize λ b → a → b and compile it to a ->.

I implemented this idea, replacing a -> by (->) a since Haskell apparently does not support function arrow sections. I also added support for compiling λ a b → a → b to (->), so once we add the Arrow or Profunctor classes we should also be able to define instances of them for (->).