[GHC] #11514: Impredicativity is still sneaking in

GHC ghc-devs at haskell.org
Thu Mar 21 16:59:51 UTC 2019


#11514: Impredicativity is still sneaking in
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
                                     |  ImpredicativeTypes
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Marge Bot <ben+marge-bot@…>):

 In [changeset:"8d18a873c5d7688c6e7d91efab6bb0d6f99393c6/ghc"
 8d18a873/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="8d18a873c5d7688c6e7d91efab6bb0d6f99393c6"
 Reject nested predicates in impredicativity checking

 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.
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11514#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list