
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): In response to goldfire's question, let me ask an analogous one. Currently, we allow this: {{{#!hs instance (forall xx. c (Free c xx)) => Monad (Free c) where Free f >>= g = f g }}} Also, assume there is no `Show (Free Show xx)` instance. Now suppose we are given `(forall xx. c (Free c xx))`, and we want to prove `Show (Free Show xx)`. In considering the wanted `Show (Free Show xx)`, we have two choices of how to proceed: 1. Use the given and succeed. 2. Attempt to resolve the `Show (Free Show xx)` instance and fail. The exact same problem seems to arise here, so why isn't this disallowed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler