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 illkinded, 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 bugfixing, I made this outright bug a separate ticket.