[GHC] #14859: Allow explicit impredicativity

GHC ghc-devs at haskell.org
Thu Oct 25 12:56:16 UTC 2018


#14859: Allow explicit impredicativity
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      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 goldfire):

 Impredicativity is perfectly fine in Core. (At least in theory. I'm sure
 panics await.) So giving users controlled access to it in source Haskell
 is safe, in that we won't launch the rockets. As we open this gate,
 horrors might await us on the other side, but they should all be type
 inference horrors, not type safety ones.

 I am thus in support of this direction of travel.

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


More information about the ghc-tickets mailing list