snd $ compiles incorrectly

[HeinrichApfelmus]

There seems to be an issue when compiling the function application operator $ together with snd:

The file

module Test where

open import Haskell.Prelude

test : Int × Int → Int
test = λ x → snd $ x

{-# COMPILE AGDA2HS test #-}

is compiled to

module Test where

test :: (Int, Int) -> Int
test = (\ r -> snd r $)

which is not valid Haskell.

Apparently, something went wrong with the fixity of $ and the compilation of snd (Agda) to \ r -> snd r (Haskell). It appears to me that a parentheses are missing, a good compilation output would be

test = ((\ r -> snd r) $)

Agda2hs version: github:agda/agda2hs?ref=v1.2

[jespercockx]

I'm investigating this issue at the moment. If one ignores the gratuitous eta-contraction and eta-expansion Agda does for a moment, the real issue seems to be with pretty-printing of sections. We generate a LeftSection () (Lambda ...) op), but hs-src-exts does not put the parentheses around the lambda.

For lambdas specifically this is only a problem for left sections, but here is a similar issue with right sections (not involving lambdas):

test6 : Int → Int
test6 = _- (1 + 1)
{-# COMPILE AGDA2HS test6 #-}

gets compiled to the (type-incorrect)

test6 :: Int -> Int
test6 = (- 1 + 1)

I am trying to work around the pretty-printer by manually inserting more Parens constructors, but this really seems like something that ought to be handled by the pretty-printing library, not by us.

@flupe proposed in #274 to switch to ghc-source-gen, perhaps that would also fix this issue.

[jespercockx]

Related: #54

[HeinrichApfelmus]

, but this really seems like something that ought to be handled by the pretty-printing library, not by us.

Fair enough. I think that the main focus of haskell-src-exts was parsing rather than pretty-printing. One could imagine submitting a patch or forking a patched version, though.

@flupe proposed in #274 to switch to ghc-source-gen, perhaps that would also fix this issue.

Personally, I wouldn't recommend depending on ghc, because then the version of the pretty-printer will be tightly coupled to the version of the compiler. The ghc-source-gen package does seem to care about supporting older compiler versions, but every new GHC version could still come with a significant maintenance cost.

[jmchapman]

In the readme for ghc-source-gen it says that it supports ghc 8.2, 8.4, 8.6 and 8.8.

https://github.com/google/ghc-source-gen

[HeinrichApfelmus]

In the readme for ghc-source-gen it says that it supports ghc 8.2, 8.4, 8.6 and 8.8.

Sure. What I mean is that I'm more concerned about forward-portability — when GHC 10.2 is released, will ghc-source-gen adapt quickly enough for agda2hs to be able to switch to GHC 10.2 as well?

[jmchapman]

I think there are two issues:

1. ghc as a dependency of agda2hs (i.e. using ghc to build agda2hs itself).
2. ghc as the consumer of code generated by agda2hs.

I don't think these need to be the same version.

In the first case we would have to rely on any libraries being compatible with a new version of ghc. I understand you point to be that despite the fact that haskell-src-exts is unmaintained (/on 'life support') and would not support any new syntax introduced in a new version, as it is more loosely coupled it's more likely to continue to be compatible with new versions of ghc than the better maintained but more tightly coupled ghc-source-gen.

In the second case I don't see such an issue as the new version of ghc is likely to continue to compatible with the syntax of earlier versions.

[HeinrichApfelmus]

I understand your point to be that despite the fact that haskell-src-exts is unmaintained […], as it is more loosely coupled it's more likely to continue to be compatible with new versions of ghc than the better maintained but more tightly coupled ghc-source-gen.

Yes, that is what I was trying to say. 👍 Just my two cents, though, not my decision.

[jmchapman]

thanks! We're looking at the pros and cons.