I don't see how a tiny bit of impredicativity just for bottoms can cause
#11431: GHC instantiates levity-polymorphic type variables with foralls -------------------------------------+------------------------------------- Reporter: gridaphobe | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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 simonpj): trouble. Impredicativity never causes trouble for the dynamic semantics; after all Core is impredicative. In contrast levity-polymorphism does. Impredicativity does cause trouble for type inference -- see zillions of papers on the subject. In contrast levity-polymorphism does not. (Except in enforcing the restrictions that levity polyormophism must follow to avoid screwing up the dynamic semantics.) There is no reason (that I can see) that the restrictions for levity polymorophism should be sufficient to avoid all type- inference/impredicativity difficulties. Maybe so, but it would be a coincidence. There's an engineering issue too. Richard is about to eliminate `RetTv`. But `RetTv` is essential to the implementation that accepts the above program. Are we going to leave `RetTv` for this sole (ill-defined) purpose? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11431#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler