#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 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I've discovered a way to work around the issue in comment:18. This is the instance we are trying to write: {{{#!hs class (forall b. Show b => Show (T a b)) => C a where type family T a :: * -> * }}} This doesn't work because the head of that quantified constraint mentions `T`, which is a type family. The normal trick is to add an extra constraint `ta ~ T a` and change the head of the quantified constraint to `Show (ta b)`. But where do we quantify `ta`? The answer to this question eluded me for the longest time, but it turns out the answer is shockingly simple: just quantify `ta` in the quantified constraint itself! That is to say, just do this: {{{#!hs class (forall ta b. (ta ~ T a, Show b) => Show (ta b)) => C a where type family T a :: * -> * }}} That's it! Now the instance typechecks, just like we've always dreamed of. I've tried this trick out on a large codebase that makes heavy use of quantified superclasses of this form, and it appears to work remarkably well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler