#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The spirit of this proposal sounds nice, but there's a couple things that I'm worried about: * This proposal suggests accepting polytypes in all types of kind `Constraint`. Would that mean that the following would be accepted? {{{#!hs f :: (?x :: Proxy (forall a. Eq a => Eq (f a) :: Constraint)) => Int; f = 42 }}} Unlike in the original example, `Proxy (forall a. Eq a => Eq (f a) :: Constraint)` appears to be truly impredicative. * Let's suppose you define `type F2 f = (Functor f, forall a. Eq (f a))` (which would now be accepted under this proposal without needing `ImpredicativeTypes`) and later try to define `g :: Proxy (F2 Maybe); g = Proxy`. Would //that// count as impredicative? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler