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))
, thendo { x <- r ; ... }
should succeed withx :: MVar (forall a. a->a)
, as we would if it was(>>=) r blah
. But currently we don't because we go viatcSyntaxOp
(intcDoStmt
). 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]
thenx = [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
.