Valid hole fit is not valid under ImpredicativeTypes
Summary
While playing around with some code suggested on Reddit I ran into this strange situation. GHC lists print
as a valid hole fit, but when I actually try it it throws an error.
Steps to reproduce
$ ghci
GHCi, version 9.3.20210504: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/user/.ghci
ghci> :set -XOverloadedRecordDot
ghci> :set -XDataKinds
ghci> :set -XImpredicativeTypes
ghci> :set -XTypeFamilies
ghci> :set -XUndecidableInstances
ghci> import GHC.Records
ghci> data User = User { name :: String }
ghci> instance (a ~ (forall x . Show x => x -> IO ())) => HasField "myPrint" User a where getField self = _
<interactive>:20:101: error:
• Found hole: _ :: forall x. Show x => x -> IO ()
• In an equation for ‘getField’: getField self = _
In the instance declaration for ‘HasField "myPrint" User a’
• Relevant bindings include
self :: User (bound at <interactive>:20:94)
getField :: User -> a (bound at <interactive>:20:85)
Constraints include
a ~ (forall x. Show x => x -> IO ()) (from <interactive>:20:10-77)
Valid hole fits include
print :: forall a. Show a => a -> IO ()
(imported from ‘Prelude’ (and originally defined in ‘System.IO’))
mempty :: forall a. Monoid a => a
with mempty @(x -> IO ())
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
ghci> instance (a ~ (forall x . Show x => x -> IO ())) => HasField "myPrint" User a where getField self = print
<interactive>:21:101: error:
• Couldn't match type: a0 -> IO ()
with: forall x. Show x => x -> IO ()
Expected: a
Actual: a0 -> IO ()
• In the expression: print
In an equation for ‘getField’: getField self = print
In the instance declaration for ‘HasField "myPrint" User a’
Expected behavior
I expected the print
version to work without errors, but there might be another reason for the error.
Environment
- GHC version used: 9.3.20210504