Re: #11514: Impredicativity is still sneaking in

"GHC" <[email protected]> Thu, 21 Mar 2019 16:59:51 -0000
Newsgroups gmane.comp.lang.haskell.glasgow.bugs
Message-ID <[email protected]>
--===============0670266827329459390==
Content-Type: multipart/related;
 boundary="===============1255256468243764984=="

--===============1255256468243764984==
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit

#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>