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.