Possible work-around for implicit params and simplified subsumption?
What
The IHP project has been working on upgrading to GHC 9.2.1 from GHC 8.10.7, and the new simplified subsumption changes to the type checker have caused a major breakage.
I'm writing here to hopefully find a way to satisfy the new type checker without causing breaking changes in IHP projects.
Example of breakage
I've produced a small example here that the new type checker fails to accept:
type T = (?a :: Int) => IO ()
f :: [String] -> T
f xs = mapM_ g xs
g :: String -> T
g _ = pure ()
• Couldn't match type: (?a::Int) => IO ()
with: IO b0
Expected: String -> IO b0
Actual: String -> T
As noted in the proposal for simplified subsumption, this can be fixed by manually eta-expanding g
:
f xs = mapM_ (\x -> g x) xs
For IHP, a framework designed for bringing people into Haskell, this would be an unsatisfying solution as shown by the following example:
Example from IHP
For context, in IHP the issue lies around a type
type Html = (?context :: ControllerContext) => Html5.Html
which is used like:
renderUsers :: [User] -> Html
renderUsers users = [hsx|
<ul>
{forEach users renderUser}
</ul>
|]
renderUser :: User -> Html
renderUser user = [hsx|<li>{get #name user}</li>|]
This fails to type check in GHC 9.2.
Avoiding eta-expanding manually
Getting new Haskell users to understand and the connection on their own that \x -> f x
is equivalent to f
is a big milestone their journey. Breaking this understanding by requiring users to expand forEach users (\u -> renderUser u)
in this one (but very common) case would result in lots of frustration and a big hurdle to learning. If at all possible, we'd like to avoid pushing this burden on users.
Other possible solutions?
- Is there some less invasive technique than eta-expanding get get these programs to type-check that we don't know about?
- Do the unsound program transformation that motivated this change happen with implicit params? If not, would it be possible to add the behavior back in GHC? I understand that simplifying the type-checker was also a goal of the original change as well, I'd imagine this probably isn't feasible while maintaining the new simplicity.
- Type checker plugin: Would we be able to provide proof in a GHC type-checker plugin to accept these programs? If so, what proof would we even be looking to provide?
Thank you for the help, and thanks for everyone here's hard work on GHC