Implement Quick Look impredicativity

This ticket is to track progress on implementing "A quick look at impredicativity".

The branch is wip/T18126. The MR for code review is !3220 (closed).

Still to do (in the future)

• Do-notation is not handled well (eg tcfail165). If we have r :: IO (MVar (forall a. a->a)), then do { x <- r ; ... } should succeed with x :: MVar (forall a. a->a), as we would if it was (>>=) r blah. But currently we don't because we go via tcSyntaxOp (in tcDoStmt). This should get fixed automatically when we complete the work on rebindable syntax. See #21206 (closed) for some concrete ideas

• Explicit lists don't work. E.g. if ids :: [forall a.a->a] then

  x = [ids, ids]

  fails. NB: works ok if the type is being checked; e.g. this is fine:

  x :: [[forall a.a->a]]
  x = [ids, ids]

  The problem is in inference. This is tracked in #20805 (along with a similar failure for tuples).

• Tuple sections fail; see tcrun042 for example.

• Left and right sections fail. E.g. #8808, function g2'

• QL isn't applied in kinds at all. That is, we get no help with doing impredicative instantiation in types, only in terms. E.g. dependent/should_fail/T15859a.