[GHC] #14860: QuantifiedConstraints: Can't quantify constraint involving type family

[GHC]

#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