#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints 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 goldfire): I agree with comment:19. Depending on how you read it, the rule is this: * You cannot mention locally quantified variables in the arguments to a type family. where "locally quantified" is meant to refer to the quantification in a quantified constraint. My "depending on how you read it" is about the fact that `b` isn't really an argument to type family `T` in `T a b`. Instead, `a` is the only argument to `T`, and `b` is an argument to the reduct of `T a`. This is pedantic, but I think it's a healthy way to understand what's going on. I also want to back Simon up in his refusal to allow locally quantified variables in arguments to type families: the problem is all about backtracking. See my comment:6, which spells trouble. I don't think the more nuanced rule described in comment:19 and here will be hard to implement. The flattener already treats the `a` and `b` in `T a b` quite differently. See the difference between `flatten_fam_app` and `flatten_exact_fam_app_fully`. The former takes `T a b` and decomposes to pass only `T a` to the latter. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler