GitLab

While patching head.hackage recently, I discovered recently that the conduit-1.3.4 library fails to build on HEAD, despite compiling with 9.0.1. This is due to a typechecker regression introduced in commit 4196969c (Improve handling of overloaded labels, literals, lists etc). The issue concerns the way that GHC typechecks left and right sections. Here is a minimized example that illustrates the issue with a right section:

{-# LANGUAGE RankNTypes #-}
module Bug where

f :: a -> forall b. b -> a
f x _ = x

g :: a -> a
g = (`f` "hello")

This compiles on 9.0.1, but fails on HEAD with the following error:

$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2             ( Bug2.hs, Bug2.o )

Bug2.hs:8:6: error:
    • Couldn't match type: forall c1. c1 -> String
                     with: c -> String
      Expected: b -> c -> String
        Actual: b -> forall c. c -> String
    • In the expression: "hello" `j`
      In an equation for ‘k’: k = ("hello" `j`)
    • Relevant bindings include
        k :: b -> c -> String (bound at Bug2.hs:8:1)
  |
8 | k = ("hello" `j`)
  |      ^^^^^^^^^^^

It's tempting to say that this should be rejected because of simplified subsumption, but that's not the full story. For one thing, 9.0.1 introduced simplified subsumption, but the code above typechecks under 9.0.1, so this is a HEAD-specific phenomenon. Moreover, Section 3.5 of the Haskell 2010 Report specifically requires that the following identities hold for sections:

Translation: The following identities hold:

(op e) 	= 	\ x -> x op e
(e op) 	= 	\ x -> e op x

where op is a binary operator, e is an expression, and x is a variable that does not occur free in e.

Therefore, the definition of g should be equivalent to:

g :: a -> a
g = \x -> x `f` "hello"

And indeed, that typechecks on both 9.0.1 and HEAD. Therefore, I'm going to deem this a regression, since the Haskell 2010 Report seems to indicate that this ought to work.

The example above uses a right section, but the same issue applies to left sections as well, as shown by this example:

{-# LANGUAGE RankNTypes #-}
module Bug2 where

j :: a -> b -> forall c. c -> a
j x _ _ = x

k :: b -> c -> String
k = ("hello" `j`)

Again, this typechecks on 9.0.1 but not on HEAD:

$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2             ( Bug2.hs, Bug2.o )

Bug2.hs:8:6: error:
    • Couldn't match type: forall c1. c1 -> String
                     with: c -> String
      Expected: b -> c -> String
        Actual: b -> forall c. c -> String
    • In the expression: "hello" `j`
      In an equation for ‘k’: k = ("hello" `j`)
    • Relevant bindings include
        k :: b -> c -> String (bound at Bug2.hs:8:1)
  |
8 | k = ("hello" `j`)
  |      ^^^^^^^^^^^

However, the equivalent eta-expanded version of k typechecks on both 9.0.1 and HEAD:

k :: b -> c -> String
k = \x -> "hello" `j` x

cc @simonpj