[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:  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):

 I mean, that technically works, but you're cheating a little, as you're
 changing the definition of `Apply`. In the code that I actually want to
 write, such a transformation is impossible, since I need to be able to use
 the last argument of `Apply` in its definition.

 In any case, I don't see why this type-families-in-instance restriction
 need apply here. I can certainly see why we'd rule out:

 {{{#!hs
 instance C (F a) where ...
 }}}

 As a top-level instance. However, as a quantified constraint:

 {{{#!hs
 forall a. Show (Apply f a)
 }}}

 This should be acceptable. Whenever you _use_ this constraint, it
 certainly must be the case that we reduce this to something that is type-
 family–free. This is why this would work:

 {{{#!hs
 test :: ExTyFam Proxy -> String
 test = show
 }}}

 Since we would be able to reduce `forall a. Show (Apply Proxy a)` to
 `forall a. Show (Proxy a)`, which has no type families. (If that weren't
 the case, then I'd certainly expect GHC to error.)

 Does that make sense? This is exactly along the same vein as previous
 generalizations brought about due to quantified constraints. After all, we
 don't allow this as a top-level instance:

 {{{#!hs
 instance Show a => c (F a)
 }}}

 But we //do// allow this to appear as a quantified constraint (when we use
 it, it must be the case that this turns into something with an actual
 class for `c`). This proposed generalization fits into that tradition.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14860#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler