Incorrect transpilation of polymorphic `where` clauses

[HeinrichApfelmus]

Consider the following program

test : {{_ : Ord a}} → a → a → a → a
test x1 x2 x3 = min x1 y
  where
    y = max x2 x3

Agda2hs 1.2 transpiles this into

test :: Ord a => a -> a -> a -> a
test x1 x2 x3 = min x1 y
  where
    y :: a
    y = max x2 x3

However, this is not valid Haskell: The type signature y :: a is understood as a polymorphic value y : ∀ a. a, but what we really want is that the a is the same as the one in the type signature of test. However, this requires the use of the ScopedTypeVariables extension and an explicit introduction test :: forall a. Ord a => a -> a -> a -> a.

For reference, here is the error message when compiling the generated Haskell code:

 error: [GHC-25897]
    • Couldn't match expected type ‘a1’ with actual type ‘a’
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          y :: forall a1. a1
        at haskell/Cardano/Wallet/Deposit/Pure/RollbackWindow.hs:75:5-10
      ‘a’ is a rigid type variable bound by
        the type signature for:
          test :: forall a. Ord a => a -> a -> a -> a
        at haskell/Cardano/Wallet/Deposit/Pure/RollbackWindow.hs:72:1-33
    • In the first argument of ‘max’, namely ‘x2’
      In the expression: max x2 x3
      In an equation for ‘y’: y = max x2 x3

[flupe]

This is a known issue. See #85 and the current workaround introduced in #103. That is, to get explicit foralls you need to introduce an anonymous module with implicit Set parameter.

From test/ScopedTypeVariables.agda, this:

module _ {@0 a : Set} {{_ : Eq a}} where
  foo : a → Bool
  foo x = it x == x
    where
      it : a -> a
      it = const x
{-# COMPILE AGDA2HS foo #-}

becomes

foo :: forall a . Eq a => a -> Bool
foo x = it x == x
  where
    it :: a -> a
    it = const x

[jespercockx]

Still, we should report a proper error rather than generate invalid Haskell code.

[HeinrichApfelmus]

Still, we should report a proper error rather than generate invalid Haskell code.

Why report an error? The definition test looks like legal Haskell-in-Agda to me, the issue is that the result of the transpilation is simply wrong. (If the transpilation had omitted the type signature on y, the code would have been valid Haskell.)

[flupe]

I think figuring out when to throw an error for this is probably only slightly less difficult than automatically inserting the explicit foralls, so hopefully by then we won't need the workaround nor the error :)

[HeinrichApfelmus]

By the way, I think that this error is one of those instance where a formal specification of the translation from Haskell-in-Agda to Haskell is warranted. One could argue that "it's just surface syntax", but this specific argument has a slippery slope (see e.g. type systems such as TypeScript for untyped languages such as JavaScript "are just surface syntax") and these errors do affect the correctness of the translation.

[HeinrichApfelmus]

inserting the explicit foralls, so hopefully by then we won't need the workaround nor the error :)

From a software engineering perspective, I would go the other way round: Insert forall in the intermediate syntax by default, then have a transpiler pass where superfluous forall are removed. At worst, one would fail to remove some forall, but never miss inserting one.

[flupe]

Iirc I have a stale branch where this is the behavior you mention: all foralls are made explicit. Maybe I can find this stale branch and put it under a flag or something, but it generates really unreadable Haskell which is part of the appeal of agda2hs.
Also, the problem was not only that foralls should be made explicit but that the name they are bound with in function clauses (where where blocks appear) is consistent throughout clauses and is the same as the one in the type signature (which is what Haskell binds it to).
Doing this check is more or less the same as figuring out whether a type parameters needs to be made explicit to be brought into scope.

By the way, I think that this error is one of those instance where a formal specification of the translation from Haskell-in-Agda to Haskell is warranted

Agreed, working on it

[jespercockx]

One question here is whether we care about being able to generate code that uses explicit foralls (which we can already do, it just requires some extra work on the Agda side) or we just want to make sure that the code we generate is valid Haskell. In the latter case, we could make the translation much easier by using explicit type abstractions which were added in GHC 9.10. I just tested and the following code is accepted by GHC 9.10:

{-# LANGUAGE TypeAbstractions #-}

test :: Ord a => a -> a -> a -> a
test @a x1 x2 x3 = min x1 y
  where
    y :: a
    y = max x2 x3

Of course, only supporting a very recent version of GHC is not ideal, but neither is adding a bunch of (probably brittle) logic for trying to turn Agda-style implicit type arguments into Haskell-style scoped type variables.

[jespercockx]

Another alternative would be to omit type annotations on where declarations by default, which also gets rid of the problem (but might run into problems when combined with Haskell features that inhibit inference).

[HeinrichApfelmus]

we just want to make sure that the code we generate is valid Haskell.

I think that the crux here is the question — what is "valid Haskell"?

The standard defines Haskell as an implementation of Hindler-Milner type system, where all explicit forall can be elided. I think that this is a perfectly valid transpilation target.

In contrast, explicit forall are something that you would expect in System F or dependently typed languages.

The point is that the question of "When can we elide forall?" is the same question as "Are we in the Hindley-Milner subset of System F"? The former looks like a usability question, whereas the latter looks like a type system question, but they are really the same question — and the usability of Hindler-Milner is precisely why it was picked as basis for Haskell. Again, I think it's perfectly justified to spend effort on clarifying that question.

Of course, only supporting a very recent version of GHC is not ideal

Not to mention that TypeAbstractions introduces a style of Haskell that is different from ScopedTypeVariables.

[jespercockx]

Not to mention that TypeAbstractions introduces a style of Haskell that is different from ScopedTypeVariables.

Exactly, which is why I asked the question whether we care about what precise Haskell is generated, or just that it is valid.

It sounds to me that you are proposing to keep agda2hs-generated code within the Hindley-Milner fragment of Haskell, in which case we could solve this by just omitting the type signatures on where-declarations. Would you be fine with that solution? I think it definitely has some benefits, not the least its simplicity.

(Or slightly more complicated, we could check if the type uses any type variables from the parent clause, and only omit it if it does.)

[HeinrichApfelmus]

It sounds to me that you are proposing to keep agda2hs-generated code within the Hindley-Milner fragment of Haskel […]. Would you be fine with that solution?

Yes, absolutely. I very much prefer the Hindley-Milner fragment of Haskell when possible.

l, in which case we could solve this by just omitting the type signatures on where-declarations.

However, I think that for Hindley-Milner + Type classes, you can't always omit type signatures, and ScopedTypeVariables is sometimes be necessary. The Haskell standard ('98 or 2010) also allows polymorphic recursion, if I recall correctly.

In these cases, a principled solution might be to run the type inference algorithm and reintroduce type signatures in the event that the principal type does not exit, e.g. is ambiguous.