[GHC] #15828: Type family equation foralls allow strange re-quantification of class-bound type variables

[GHC]

#15828: Type family equation foralls allow strange re-quantification of class-bound
type variables
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.7
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code typechecks on GHC HEAD (8.7+):

 {{{#!hs
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 import Data.Kind

 class C1 a where
   type T1 a b
 class C2 a where
   type T2 a b

 instance C1 (Maybe a) where
   type forall a b. T1 (Maybe a) b = b
 instance C2 (Maybe a) where
   type forall   b. T2 (Maybe a) b = b
 }}}

 But ought it to? There is something funny happening in the `C1` instance:
 it's explicitly quantifying `a`, despite the fact that it had previously
 been quantified by the class head! Moreover, it appears that you can
 safely drop the `a` in the explicit `forall`, as the `C2 (Maybe a)`
 instance witnesses.

 What does the documentation have to say on this topic? This is all I could
 find:

 > When an explicit `forall` is present, all //type// variables mentioned
 must be bound by the `forall`.

 I couldn't find anything on the interaction between this feature and
 associated type families. We should:

 1. Decide which of the two programs above should be accepted, and
 2. Update the documentation to reflect this.

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