Skip to content
  • Ryan Scott's avatar
    Reject nested predicates in impredicativity checking · 8d18a873
    Ryan Scott authored and Marge Bot's avatar Marge Bot committed
    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:
    
    ```haskell
    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).
    
    Fixes #11514.
    8d18a873