Skip to content

Reject nested predicates in impredicativity checking

Ryan Scott requested to merge RyanGlScott/ghc:wip/T11514 into master

When GHC attempts to unify a metavariable with a type containing foralls, it will be rejected as an occurrence of impredicativity. GHC was /not/ extending the same treatment to predicate types, such as in the following (erroneous) example from #11514 (closed):

foo :: forall a. (Show a => a -> a) -> ()
foo = undefined

This will attempt to instantiate undefined at (Show a => a -> a) -> (), which is impredicative. This patch catches impredicativity arising from predicates in this fashion.

Since GHC is pickier about impredicative instantiations, some test cases needed to be updated to be updated so as not to fall afoul of the new validity check. (There were a surprising number of impredicative uses of undefined!) Moreover, the T14828 test case now has slightly less informative types shown with :print. This is due to a a much deeper issue with the GHCi debugger (see #14828 (closed)).

Fixes #11514 (closed).

Edited by Ryan Scott

Merge request reports