Lazy instantiation is incompatible with implicit parameters
In thinking about issues around #17173 (closed), I came up with this silliness:
getx :: (?x :: Bool -> Bool) => Bool -> Bool
getx = ?x
z3 = (let ?x = not in getx) False
GHC's current response is utter garbage:
Scratch.hs:52:23: error:
• Couldn't match type ‘?x::Bool -> Bool’ with ‘Bool’
Expected type: Bool -> Bool -> Bool
Actual type: (?x::Bool -> Bool) => Bool -> Bool
• In the expression: getx
In the expression: let ?x = not in getx
In the expression: (let ?x = not in getx) False
|
52 | z3 = (let ?x = not in getx) False
|
The "couldn't match type" bit is ill-kinded, and I have no idea why GHC is expecting Bool -> Bool -> Bool
here. But the root cause, I believe, is lazy instantiation. Functions are instantiated lazily. So the let ?x = not in getx
is instantiated lazily. The body of a let
inherits its instantiation behavior from the outer context. So the getx
is instantiated lazily. This means that GHC happily infers type (?x :: Bool -> Bool) => Bool -> Bool
for getx
. And then, with no incentive to instantiate, it infers (let ?x = not in getx) :: (?x :: Bool -> Bool) => Bool -> Bool
. Now, when we apply such a thing to a term argument, GHC instantiates. But, lo!, there is no longer a ?x :: Bool -> Bool
constraint in scope, causing unhappiness.
If we instantiate eagerly, I claim this should all work just fine.
I believe this will be fixed alongside #17173 (closed), but given that #17173 (closed) is about general improvement rather than bug-fixing, I made this outright bug a separate ticket.