Would this permit explicit impredicativity as described in [1]? Simon mentions in [1] that explicit impredicativity is easier to implement than guarded impredicativity, although it's not clear to me if the latter would imply the former.

Ryan S.

-----

[1] https://gitlab.haskell.org/ghc/ghc/issues/14859