conduit-1.3.4 builds with 9.0.1, but not HEAD, due to regression in typechecking sections
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, andx
is a variable that does not occur free ine
.
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