[GHC] #16116: Explicit foralls in associated type family equations are oblivious to class-bound variables

[GHC]

#16116: Explicit foralls in associated type family equations are oblivious to
class-bound variables
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:
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):

 That's a good point. I think that check is a relic from commit
 171101beca39befde191baff5027c417bcc709ee, which made an attempt to reject
 programs like this one:

 {{{#!hs
 instance C ('KProxy :: KProxy o) where
     type F 'KProxy = NatTr (Proxy :: o -> *)
 }}}

 Since `o` isn't //explicitly// bound on the left-hand side. However, we
 later reversed this policy in commit
 0829821a6b886788a3ba6989e57e25a037bb6d05, where it was decided that it was
 OK to mention type variables on the RHSes of type family instances even if
 they're implicitly bound (i.e., we should accept `F 'KProxy` above).

 In light of this, I'd agree that `null bad_tvs` validity check serves no
 purpose. Removing it does make the program work again, (and validates,
 aside from some expected error message wibbles in `T5515`) which is an
 encouraging sign.

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