This ticket is to track progress on implementing ["A quick look at impredicativity"](https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/). The branch is `wip/T18126`. The MR for code review is !3220. Still to do (in the future) =============== * [x] 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 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`.