#11319: ImpredicativeTypes even more broken than usual -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | ImpredicativeTypes Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): It would make sense that the type-checker rewrite from visible type application would break impredicativity even more than usual. Given its already-quite-broken state, I didn't try to salvage it. I don't want to completely kill it, though, as it sometimes is useful, if just for experimentation. And visible types lets you climb out of any hole you get in. For example, this works: {{{ {-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-} module Bug where f :: forall a f. Applicative f => f (Maybe a) f = pure (Nothing @a) }}} All that said, I'll take a look at this one, as it would be nice to be less broken. And my hunch is that this will be quite easy to fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11319#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler